Metamath Proof Explorer


Theorem mbfeqalem2

Description: Lemma for mbfeqa . (Contributed by Mario Carneiro, 2-Sep-2014) (Proof shortened by AV, 19-Aug-2022)

Ref Expression
Hypotheses mbfeqa.1 φ A
mbfeqa.2 φ vol * A = 0
mbfeqa.3 φ x B A C = D
mbfeqalem.4 φ x B C
mbfeqalem.5 φ x B D
Assertion mbfeqalem2 φ x B C MblFn x B D MblFn

Proof

Step Hyp Ref Expression
1 mbfeqa.1 φ A
2 mbfeqa.2 φ vol * A = 0
3 mbfeqa.3 φ x B A C = D
4 mbfeqalem.4 φ x B C
5 mbfeqalem.5 φ x B D
6 inundif x B D -1 y x B C -1 y x B D -1 y x B C -1 y = x B D -1 y
7 incom x B D -1 y x B C -1 y = x B C -1 y x B D -1 y
8 dfin4 x B C -1 y x B D -1 y = x B C -1 y x B C -1 y x B D -1 y
9 7 8 eqtri x B D -1 y x B C -1 y = x B C -1 y x B C -1 y x B D -1 y
10 id x B C -1 y dom vol x B C -1 y dom vol
11 1 2 3 4 5 mbfeqalem1 φ x B C -1 y x B D -1 y dom vol
12 difmbl x B C -1 y dom vol x B C -1 y x B D -1 y dom vol x B C -1 y x B C -1 y x B D -1 y dom vol
13 10 11 12 syl2anr φ x B C -1 y dom vol x B C -1 y x B C -1 y x B D -1 y dom vol
14 9 13 eqeltrid φ x B C -1 y dom vol x B D -1 y x B C -1 y dom vol
15 3 eqcomd φ x B A D = C
16 1 2 15 5 4 mbfeqalem1 φ x B D -1 y x B C -1 y dom vol
17 16 adantr φ x B C -1 y dom vol x B D -1 y x B C -1 y dom vol
18 unmbl x B D -1 y x B C -1 y dom vol x B D -1 y x B C -1 y dom vol x B D -1 y x B C -1 y x B D -1 y x B C -1 y dom vol
19 14 17 18 syl2anc φ x B C -1 y dom vol x B D -1 y x B C -1 y x B D -1 y x B C -1 y dom vol
20 6 19 eqeltrrid φ x B C -1 y dom vol x B D -1 y dom vol
21 inundif x B C -1 y x B D -1 y x B C -1 y x B D -1 y = x B C -1 y
22 incom x B C -1 y x B D -1 y = x B D -1 y x B C -1 y
23 dfin4 x B D -1 y x B C -1 y = x B D -1 y x B D -1 y x B C -1 y
24 22 23 eqtri x B C -1 y x B D -1 y = x B D -1 y x B D -1 y x B C -1 y
25 id x B D -1 y dom vol x B D -1 y dom vol
26 difmbl x B D -1 y dom vol x B D -1 y x B C -1 y dom vol x B D -1 y x B D -1 y x B C -1 y dom vol
27 25 16 26 syl2anr φ x B D -1 y dom vol x B D -1 y x B D -1 y x B C -1 y dom vol
28 24 27 eqeltrid φ x B D -1 y dom vol x B C -1 y x B D -1 y dom vol
29 11 adantr φ x B D -1 y dom vol x B C -1 y x B D -1 y dom vol
30 unmbl x B C -1 y x B D -1 y dom vol x B C -1 y x B D -1 y dom vol x B C -1 y x B D -1 y x B C -1 y x B D -1 y dom vol
31 28 29 30 syl2anc φ x B D -1 y dom vol x B C -1 y x B D -1 y x B C -1 y x B D -1 y dom vol
32 21 31 eqeltrrid φ x B D -1 y dom vol x B C -1 y dom vol
33 20 32 impbida φ x B C -1 y dom vol x B D -1 y dom vol
34 33 ralbidv φ y ran . x B C -1 y dom vol y ran . x B D -1 y dom vol
35 4 fmpttd φ x B C : B
36 ismbf x B C : B x B C MblFn y ran . x B C -1 y dom vol
37 35 36 syl φ x B C MblFn y ran . x B C -1 y dom vol
38 5 fmpttd φ x B D : B
39 ismbf x B D : B x B D MblFn y ran . x B D -1 y dom vol
40 38 39 syl φ x B D MblFn y ran . x B D -1 y dom vol
41 34 37 40 3bitr4d φ x B C MblFn x B D MblFn