Metamath Proof Explorer

Theorem xpmapenlem

Description: Lemma for xpmapen . (Contributed by NM, 1-May-2004) (Revised by Mario Carneiro, 16-Nov-2014)

Ref Expression
Hypotheses xpmapen.1 
|- A e. _V
xpmapen.2 
|- B e. _V
xpmapen.3 
|- C e. _V
xpmapenlem.4 
|- D = ( z e. C |-> ( 1st ` ( x ` z ) ) )
xpmapenlem.5 
|- R = ( z e. C |-> ( 2nd ` ( x ` z ) ) )
xpmapenlem.6 
|- S = ( z e. C |-> <. ( ( 1st ` y ) ` z ) , ( ( 2nd ` y ) ` z ) >. )
Assertion xpmapenlem 
|- ( ( A X. B ) ^m C ) ~~ ( ( A ^m C ) X. ( B ^m C ) )

Proof

Step Hyp Ref Expression
1 xpmapen.1 
 |-  A e. _V
2 xpmapen.2 
 |-  B e. _V
3 xpmapen.3 
 |-  C e. _V
4 xpmapenlem.4 
 |-  D = ( z e. C |-> ( 1st ` ( x ` z ) ) )
5 xpmapenlem.5 
 |-  R = ( z e. C |-> ( 2nd ` ( x ` z ) ) )
6 xpmapenlem.6 
 |-  S = ( z e. C |-> <. ( ( 1st ` y ) ` z ) , ( ( 2nd ` y ) ` z ) >. )
7 ovex 
 |-  ( ( A X. B ) ^m C ) e. _V
8 ovex 
 |-  ( A ^m C ) e. _V
9 ovex 
 |-  ( B ^m C ) e. _V
10 8 9 xpex 
 |-  ( ( A ^m C ) X. ( B ^m C ) ) e. _V
11 1 2 xpex 
 |-  ( A X. B ) e. _V
12 11 3 elmap 
 |-  ( x e. ( ( A X. B ) ^m C ) <-> x : C --> ( A X. B ) )
13 ffvelrn 
 |-  ( ( x : C --> ( A X. B ) /\ z e. C ) -> ( x ` z ) e. ( A X. B ) )
14 12 13 sylanb 
 |-  ( ( x e. ( ( A X. B ) ^m C ) /\ z e. C ) -> ( x ` z ) e. ( A X. B ) )
15 xp1st 
 |-  ( ( x ` z ) e. ( A X. B ) -> ( 1st ` ( x ` z ) ) e. A )
16 14 15 syl 
 |-  ( ( x e. ( ( A X. B ) ^m C ) /\ z e. C ) -> ( 1st ` ( x ` z ) ) e. A )
17 16 4 fmptd 
 |-  ( x e. ( ( A X. B ) ^m C ) -> D : C --> A )
18 1 3 elmap 
 |-  ( D e. ( A ^m C ) <-> D : C --> A )
19 17 18 sylibr 
 |-  ( x e. ( ( A X. B ) ^m C ) -> D e. ( A ^m C ) )
20 xp2nd 
 |-  ( ( x ` z ) e. ( A X. B ) -> ( 2nd ` ( x ` z ) ) e. B )
21 14 20 syl 
 |-  ( ( x e. ( ( A X. B ) ^m C ) /\ z e. C ) -> ( 2nd ` ( x ` z ) ) e. B )
22 21 5 fmptd 
 |-  ( x e. ( ( A X. B ) ^m C ) -> R : C --> B )
23 2 3 elmap 
 |-  ( R e. ( B ^m C ) <-> R : C --> B )
24 22 23 sylibr 
 |-  ( x e. ( ( A X. B ) ^m C ) -> R e. ( B ^m C ) )
25 19 24 opelxpd 
 |-  ( x e. ( ( A X. B ) ^m C ) -> <. D , R >. e. ( ( A ^m C ) X. ( B ^m C ) ) )
26 xp1st 
 |-  ( y e. ( ( A ^m C ) X. ( B ^m C ) ) -> ( 1st ` y ) e. ( A ^m C ) )
27 1 3 elmap 
 |-  ( ( 1st ` y ) e. ( A ^m C ) <-> ( 1st ` y ) : C --> A )
28 26 27 sylib 
 |-  ( y e. ( ( A ^m C ) X. ( B ^m C ) ) -> ( 1st ` y ) : C --> A )
29 28 ffvelrnda 
 |-  ( ( y e. ( ( A ^m C ) X. ( B ^m C ) ) /\ z e. C ) -> ( ( 1st ` y ) ` z ) e. A )
30 xp2nd 
 |-  ( y e. ( ( A ^m C ) X. ( B ^m C ) ) -> ( 2nd ` y ) e. ( B ^m C ) )
31 2 3 elmap 
 |-  ( ( 2nd ` y ) e. ( B ^m C ) <-> ( 2nd ` y ) : C --> B )
32 30 31 sylib 
 |-  ( y e. ( ( A ^m C ) X. ( B ^m C ) ) -> ( 2nd ` y ) : C --> B )
33 32 ffvelrnda 
 |-  ( ( y e. ( ( A ^m C ) X. ( B ^m C ) ) /\ z e. C ) -> ( ( 2nd ` y ) ` z ) e. B )
34 29 33 opelxpd 
 |-  ( ( y e. ( ( A ^m C ) X. ( B ^m C ) ) /\ z e. C ) -> <. ( ( 1st ` y ) ` z ) , ( ( 2nd ` y ) ` z ) >. e. ( A X. B ) )
35 34 6 fmptd 
 |-  ( y e. ( ( A ^m C ) X. ( B ^m C ) ) -> S : C --> ( A X. B ) )
36 11 3 elmap 
 |-  ( S e. ( ( A X. B ) ^m C ) <-> S : C --> ( A X. B ) )
37 35 36 sylibr 
 |-  ( y e. ( ( A ^m C ) X. ( B ^m C ) ) -> S e. ( ( A X. B ) ^m C ) )
38 1st2nd2 
 |-  ( y e. ( ( A ^m C ) X. ( B ^m C ) ) -> y = <. ( 1st ` y ) , ( 2nd ` y ) >. )
39 38 ad2antlr 
 |-  ( ( ( x e. ( ( A X. B ) ^m C ) /\ y e. ( ( A ^m C ) X. ( B ^m C ) ) ) /\ x = S ) -> y = <. ( 1st ` y ) , ( 2nd ` y ) >. )
40 28 feqmptd 
 |-  ( y e. ( ( A ^m C ) X. ( B ^m C ) ) -> ( 1st ` y ) = ( z e. C |-> ( ( 1st ` y ) ` z ) ) )
41 40 ad2antlr 
 |-  ( ( ( x e. ( ( A X. B ) ^m C ) /\ y e. ( ( A ^m C ) X. ( B ^m C ) ) ) /\ x = S ) -> ( 1st ` y ) = ( z e. C |-> ( ( 1st ` y ) ` z ) ) )
42 simplr 
 |-  ( ( ( ( x e. ( ( A X. B ) ^m C ) /\ y e. ( ( A ^m C ) X. ( B ^m C ) ) ) /\ x = S ) /\ z e. C ) -> x = S )
43 42 fveq1d 
 |-  ( ( ( ( x e. ( ( A X. B ) ^m C ) /\ y e. ( ( A ^m C ) X. ( B ^m C ) ) ) /\ x = S ) /\ z e. C ) -> ( x ` z ) = ( S ` z ) )
44 opex 
 |-  <. ( ( 1st ` y ) ` z ) , ( ( 2nd ` y ) ` z ) >. e. _V
45 6 fvmpt2 
 |-  ( ( z e. C /\ <. ( ( 1st ` y ) ` z ) , ( ( 2nd ` y ) ` z ) >. e. _V ) -> ( S ` z ) = <. ( ( 1st ` y ) ` z ) , ( ( 2nd ` y ) ` z ) >. )
46 44 45 mpan2 
 |-  ( z e. C -> ( S ` z ) = <. ( ( 1st ` y ) ` z ) , ( ( 2nd ` y ) ` z ) >. )
47 46 adantl 
 |-  ( ( ( ( x e. ( ( A X. B ) ^m C ) /\ y e. ( ( A ^m C ) X. ( B ^m C ) ) ) /\ x = S ) /\ z e. C ) -> ( S ` z ) = <. ( ( 1st ` y ) ` z ) , ( ( 2nd ` y ) ` z ) >. )
48 43 47 eqtrd 
 |-  ( ( ( ( x e. ( ( A X. B ) ^m C ) /\ y e. ( ( A ^m C ) X. ( B ^m C ) ) ) /\ x = S ) /\ z e. C ) -> ( x ` z ) = <. ( ( 1st ` y ) ` z ) , ( ( 2nd ` y ) ` z ) >. )
49 48 fveq2d 
 |-  ( ( ( ( x e. ( ( A X. B ) ^m C ) /\ y e. ( ( A ^m C ) X. ( B ^m C ) ) ) /\ x = S ) /\ z e. C ) -> ( 1st ` ( x ` z ) ) = ( 1st ` <. ( ( 1st ` y ) ` z ) , ( ( 2nd ` y ) ` z ) >. ) )
50 fvex 
 |-  ( ( 1st ` y ) ` z ) e. _V
51 fvex 
 |-  ( ( 2nd ` y ) ` z ) e. _V
52 50 51 op1st 
 |-  ( 1st ` <. ( ( 1st ` y ) ` z ) , ( ( 2nd ` y ) ` z ) >. ) = ( ( 1st ` y ) ` z )
53 49 52 eqtrdi 
 |-  ( ( ( ( x e. ( ( A X. B ) ^m C ) /\ y e. ( ( A ^m C ) X. ( B ^m C ) ) ) /\ x = S ) /\ z e. C ) -> ( 1st ` ( x ` z ) ) = ( ( 1st ` y ) ` z ) )
54 53 mpteq2dva 
 |-  ( ( ( x e. ( ( A X. B ) ^m C ) /\ y e. ( ( A ^m C ) X. ( B ^m C ) ) ) /\ x = S ) -> ( z e. C |-> ( 1st ` ( x ` z ) ) ) = ( z e. C |-> ( ( 1st ` y ) ` z ) ) )
55 4 54 syl5eq 
 |-  ( ( ( x e. ( ( A X. B ) ^m C ) /\ y e. ( ( A ^m C ) X. ( B ^m C ) ) ) /\ x = S ) -> D = ( z e. C |-> ( ( 1st ` y ) ` z ) ) )
56 41 55 eqtr4d 
 |-  ( ( ( x e. ( ( A X. B ) ^m C ) /\ y e. ( ( A ^m C ) X. ( B ^m C ) ) ) /\ x = S ) -> ( 1st ` y ) = D )
57 32 feqmptd 
 |-  ( y e. ( ( A ^m C ) X. ( B ^m C ) ) -> ( 2nd ` y ) = ( z e. C |-> ( ( 2nd ` y ) ` z ) ) )
58 57 ad2antlr 
 |-  ( ( ( x e. ( ( A X. B ) ^m C ) /\ y e. ( ( A ^m C ) X. ( B ^m C ) ) ) /\ x = S ) -> ( 2nd ` y ) = ( z e. C |-> ( ( 2nd ` y ) ` z ) ) )
59 48 fveq2d 
 |-  ( ( ( ( x e. ( ( A X. B ) ^m C ) /\ y e. ( ( A ^m C ) X. ( B ^m C ) ) ) /\ x = S ) /\ z e. C ) -> ( 2nd ` ( x ` z ) ) = ( 2nd ` <. ( ( 1st ` y ) ` z ) , ( ( 2nd ` y ) ` z ) >. ) )
60 50 51 op2nd 
 |-  ( 2nd ` <. ( ( 1st ` y ) ` z ) , ( ( 2nd ` y ) ` z ) >. ) = ( ( 2nd ` y ) ` z )
61 59 60 eqtrdi 
 |-  ( ( ( ( x e. ( ( A X. B ) ^m C ) /\ y e. ( ( A ^m C ) X. ( B ^m C ) ) ) /\ x = S ) /\ z e. C ) -> ( 2nd ` ( x ` z ) ) = ( ( 2nd ` y ) ` z ) )
62 61 mpteq2dva 
 |-  ( ( ( x e. ( ( A X. B ) ^m C ) /\ y e. ( ( A ^m C ) X. ( B ^m C ) ) ) /\ x = S ) -> ( z e. C |-> ( 2nd ` ( x ` z ) ) ) = ( z e. C |-> ( ( 2nd ` y ) ` z ) ) )
63 5 62 syl5eq 
 |-  ( ( ( x e. ( ( A X. B ) ^m C ) /\ y e. ( ( A ^m C ) X. ( B ^m C ) ) ) /\ x = S ) -> R = ( z e. C |-> ( ( 2nd ` y ) ` z ) ) )
64 58 63 eqtr4d 
 |-  ( ( ( x e. ( ( A X. B ) ^m C ) /\ y e. ( ( A ^m C ) X. ( B ^m C ) ) ) /\ x = S ) -> ( 2nd ` y ) = R )
65 56 64 opeq12d 
 |-  ( ( ( x e. ( ( A X. B ) ^m C ) /\ y e. ( ( A ^m C ) X. ( B ^m C ) ) ) /\ x = S ) -> <. ( 1st ` y ) , ( 2nd ` y ) >. = <. D , R >. )
66 39 65 eqtrd 
 |-  ( ( ( x e. ( ( A X. B ) ^m C ) /\ y e. ( ( A ^m C ) X. ( B ^m C ) ) ) /\ x = S ) -> y = <. D , R >. )
67 simpll 
 |-  ( ( ( x e. ( ( A X. B ) ^m C ) /\ y e. ( ( A ^m C ) X. ( B ^m C ) ) ) /\ y = <. D , R >. ) -> x e. ( ( A X. B ) ^m C ) )
68 67 12 sylib 
 |-  ( ( ( x e. ( ( A X. B ) ^m C ) /\ y e. ( ( A ^m C ) X. ( B ^m C ) ) ) /\ y = <. D , R >. ) -> x : C --> ( A X. B ) )
69 68 feqmptd 
 |-  ( ( ( x e. ( ( A X. B ) ^m C ) /\ y e. ( ( A ^m C ) X. ( B ^m C ) ) ) /\ y = <. D , R >. ) -> x = ( z e. C |-> ( x ` z ) ) )
70 simpr 
 |-  ( ( ( x e. ( ( A X. B ) ^m C ) /\ y e. ( ( A ^m C ) X. ( B ^m C ) ) ) /\ y = <. D , R >. ) -> y = <. D , R >. )
71 70 fveq2d 
 |-  ( ( ( x e. ( ( A X. B ) ^m C ) /\ y e. ( ( A ^m C ) X. ( B ^m C ) ) ) /\ y = <. D , R >. ) -> ( 1st ` y ) = ( 1st ` <. D , R >. ) )
72 19 ad2antrr 
 |-  ( ( ( x e. ( ( A X. B ) ^m C ) /\ y e. ( ( A ^m C ) X. ( B ^m C ) ) ) /\ y = <. D , R >. ) -> D e. ( A ^m C ) )
73 24 ad2antrr 
 |-  ( ( ( x e. ( ( A X. B ) ^m C ) /\ y e. ( ( A ^m C ) X. ( B ^m C ) ) ) /\ y = <. D , R >. ) -> R e. ( B ^m C ) )
74 op1stg 
 |-  ( ( D e. ( A ^m C ) /\ R e. ( B ^m C ) ) -> ( 1st ` <. D , R >. ) = D )
75 72 73 74 syl2anc 
 |-  ( ( ( x e. ( ( A X. B ) ^m C ) /\ y e. ( ( A ^m C ) X. ( B ^m C ) ) ) /\ y = <. D , R >. ) -> ( 1st ` <. D , R >. ) = D )
76 71 75 eqtrd 
 |-  ( ( ( x e. ( ( A X. B ) ^m C ) /\ y e. ( ( A ^m C ) X. ( B ^m C ) ) ) /\ y = <. D , R >. ) -> ( 1st ` y ) = D )
77 76 fveq1d 
 |-  ( ( ( x e. ( ( A X. B ) ^m C ) /\ y e. ( ( A ^m C ) X. ( B ^m C ) ) ) /\ y = <. D , R >. ) -> ( ( 1st ` y ) ` z ) = ( D ` z ) )
78 fvex 
 |-  ( 1st ` ( x ` z ) ) e. _V
79 4 fvmpt2 
 |-  ( ( z e. C /\ ( 1st ` ( x ` z ) ) e. _V ) -> ( D ` z ) = ( 1st ` ( x ` z ) ) )
80 78 79 mpan2 
 |-  ( z e. C -> ( D ` z ) = ( 1st ` ( x ` z ) ) )
81 77 80 sylan9eq 
 |-  ( ( ( ( x e. ( ( A X. B ) ^m C ) /\ y e. ( ( A ^m C ) X. ( B ^m C ) ) ) /\ y = <. D , R >. ) /\ z e. C ) -> ( ( 1st ` y ) ` z ) = ( 1st ` ( x ` z ) ) )
82 70 fveq2d 
 |-  ( ( ( x e. ( ( A X. B ) ^m C ) /\ y e. ( ( A ^m C ) X. ( B ^m C ) ) ) /\ y = <. D , R >. ) -> ( 2nd ` y ) = ( 2nd ` <. D , R >. ) )
83 op2ndg 
 |-  ( ( D e. ( A ^m C ) /\ R e. ( B ^m C ) ) -> ( 2nd ` <. D , R >. ) = R )
84 72 73 83 syl2anc 
 |-  ( ( ( x e. ( ( A X. B ) ^m C ) /\ y e. ( ( A ^m C ) X. ( B ^m C ) ) ) /\ y = <. D , R >. ) -> ( 2nd ` <. D , R >. ) = R )
85 82 84 eqtrd 
 |-  ( ( ( x e. ( ( A X. B ) ^m C ) /\ y e. ( ( A ^m C ) X. ( B ^m C ) ) ) /\ y = <. D , R >. ) -> ( 2nd ` y ) = R )
86 85 fveq1d 
 |-  ( ( ( x e. ( ( A X. B ) ^m C ) /\ y e. ( ( A ^m C ) X. ( B ^m C ) ) ) /\ y = <. D , R >. ) -> ( ( 2nd ` y ) ` z ) = ( R ` z ) )
87 fvex 
 |-  ( 2nd ` ( x ` z ) ) e. _V
88 5 fvmpt2 
 |-  ( ( z e. C /\ ( 2nd ` ( x ` z ) ) e. _V ) -> ( R ` z ) = ( 2nd ` ( x ` z ) ) )
89 87 88 mpan2 
 |-  ( z e. C -> ( R ` z ) = ( 2nd ` ( x ` z ) ) )
90 86 89 sylan9eq 
 |-  ( ( ( ( x e. ( ( A X. B ) ^m C ) /\ y e. ( ( A ^m C ) X. ( B ^m C ) ) ) /\ y = <. D , R >. ) /\ z e. C ) -> ( ( 2nd ` y ) ` z ) = ( 2nd ` ( x ` z ) ) )
91 81 90 opeq12d 
 |-  ( ( ( ( x e. ( ( A X. B ) ^m C ) /\ y e. ( ( A ^m C ) X. ( B ^m C ) ) ) /\ y = <. D , R >. ) /\ z e. C ) -> <. ( ( 1st ` y ) ` z ) , ( ( 2nd ` y ) ` z ) >. = <. ( 1st ` ( x ` z ) ) , ( 2nd ` ( x ` z ) ) >. )
92 68 ffvelrnda 
 |-  ( ( ( ( x e. ( ( A X. B ) ^m C ) /\ y e. ( ( A ^m C ) X. ( B ^m C ) ) ) /\ y = <. D , R >. ) /\ z e. C ) -> ( x ` z ) e. ( A X. B ) )
93 1st2nd2 
 |-  ( ( x ` z ) e. ( A X. B ) -> ( x ` z ) = <. ( 1st ` ( x ` z ) ) , ( 2nd ` ( x ` z ) ) >. )
94 92 93 syl 
 |-  ( ( ( ( x e. ( ( A X. B ) ^m C ) /\ y e. ( ( A ^m C ) X. ( B ^m C ) ) ) /\ y = <. D , R >. ) /\ z e. C ) -> ( x ` z ) = <. ( 1st ` ( x ` z ) ) , ( 2nd ` ( x ` z ) ) >. )
95 91 94 eqtr4d 
 |-  ( ( ( ( x e. ( ( A X. B ) ^m C ) /\ y e. ( ( A ^m C ) X. ( B ^m C ) ) ) /\ y = <. D , R >. ) /\ z e. C ) -> <. ( ( 1st ` y ) ` z ) , ( ( 2nd ` y ) ` z ) >. = ( x ` z ) )
96 95 mpteq2dva 
 |-  ( ( ( x e. ( ( A X. B ) ^m C ) /\ y e. ( ( A ^m C ) X. ( B ^m C ) ) ) /\ y = <. D , R >. ) -> ( z e. C |-> <. ( ( 1st ` y ) ` z ) , ( ( 2nd ` y ) ` z ) >. ) = ( z e. C |-> ( x ` z ) ) )
97 6 96 syl5eq 
 |-  ( ( ( x e. ( ( A X. B ) ^m C ) /\ y e. ( ( A ^m C ) X. ( B ^m C ) ) ) /\ y = <. D , R >. ) -> S = ( z e. C |-> ( x ` z ) ) )
98 69 97 eqtr4d 
 |-  ( ( ( x e. ( ( A X. B ) ^m C ) /\ y e. ( ( A ^m C ) X. ( B ^m C ) ) ) /\ y = <. D , R >. ) -> x = S )
99 66 98 impbida 
 |-  ( ( x e. ( ( A X. B ) ^m C ) /\ y e. ( ( A ^m C ) X. ( B ^m C ) ) ) -> ( x = S <-> y = <. D , R >. ) )
100 7 10 25 37 99 en3i 
 |-  ( ( A X. B ) ^m C ) ~~ ( ( A ^m C ) X. ( B ^m C ) )