Metamath Proof Explorer

Theorem txindislem

Description: Lemma for txindis . (Contributed by Mario Carneiro, 14-Aug-2015)

Ref Expression
Assertion txindislem 
|- ( ( _I ` A ) X. ( _I ` B ) ) = ( _I ` ( A X. B ) )

Proof

Step Hyp Ref Expression
1 0xp 
 |-  ( (/) X. ( _I ` B ) ) = (/)
2 fvprc 
 |-  ( -. A e. _V -> ( _I ` A ) = (/) )
3 2 xpeq1d 
 |-  ( -. A e. _V -> ( ( _I ` A ) X. ( _I ` B ) ) = ( (/) X. ( _I ` B ) ) )
4 simpr 
 |-  ( ( -. A e. _V /\ B = (/) ) -> B = (/) )
5 4 xpeq2d 
 |-  ( ( -. A e. _V /\ B = (/) ) -> ( A X. B ) = ( A X. (/) ) )
6 xp0 
 |-  ( A X. (/) ) = (/)
7 5 6 eqtrdi 
 |-  ( ( -. A e. _V /\ B = (/) ) -> ( A X. B ) = (/) )
8 7 fveq2d 
 |-  ( ( -. A e. _V /\ B = (/) ) -> ( _I ` ( A X. B ) ) = ( _I ` (/) ) )
9 0ex 
 |-  (/) e. _V
10 fvi 
 |-  ( (/) e. _V -> ( _I ` (/) ) = (/) )
11 9 10 ax-mp 
 |-  ( _I ` (/) ) = (/)
12 8 11 eqtrdi 
 |-  ( ( -. A e. _V /\ B = (/) ) -> ( _I ` ( A X. B ) ) = (/) )
13 dmexg 
 |-  ( ( A X. B ) e. _V -> dom ( A X. B ) e. _V )
14 dmxp 
 |-  ( B =/= (/) -> dom ( A X. B ) = A )
15 14 eleq1d 
 |-  ( B =/= (/) -> ( dom ( A X. B ) e. _V <-> A e. _V ) )
16 13 15 syl5ib 
 |-  ( B =/= (/) -> ( ( A X. B ) e. _V -> A e. _V ) )
17 16 con3d 
 |-  ( B =/= (/) -> ( -. A e. _V -> -. ( A X. B ) e. _V ) )
18 17 impcom 
 |-  ( ( -. A e. _V /\ B =/= (/) ) -> -. ( A X. B ) e. _V )
19 fvprc 
 |-  ( -. ( A X. B ) e. _V -> ( _I ` ( A X. B ) ) = (/) )
20 18 19 syl 
 |-  ( ( -. A e. _V /\ B =/= (/) ) -> ( _I ` ( A X. B ) ) = (/) )
21 12 20 pm2.61dane 
 |-  ( -. A e. _V -> ( _I ` ( A X. B ) ) = (/) )
22 1 3 21 3eqtr4a 
 |-  ( -. A e. _V -> ( ( _I ` A ) X. ( _I ` B ) ) = ( _I ` ( A X. B ) ) )
23 xp0 
 |-  ( ( _I ` A ) X. (/) ) = (/)
24 fvprc 
 |-  ( -. B e. _V -> ( _I ` B ) = (/) )
25 24 xpeq2d 
 |-  ( -. B e. _V -> ( ( _I ` A ) X. ( _I ` B ) ) = ( ( _I ` A ) X. (/) ) )
26 simpr 
 |-  ( ( -. B e. _V /\ A = (/) ) -> A = (/) )
27 26 xpeq1d 
 |-  ( ( -. B e. _V /\ A = (/) ) -> ( A X. B ) = ( (/) X. B ) )
28 0xp 
 |-  ( (/) X. B ) = (/)
29 27 28 eqtrdi 
 |-  ( ( -. B e. _V /\ A = (/) ) -> ( A X. B ) = (/) )
30 29 fveq2d 
 |-  ( ( -. B e. _V /\ A = (/) ) -> ( _I ` ( A X. B ) ) = ( _I ` (/) ) )
31 30 11 eqtrdi 
 |-  ( ( -. B e. _V /\ A = (/) ) -> ( _I ` ( A X. B ) ) = (/) )
32 rnexg 
 |-  ( ( A X. B ) e. _V -> ran ( A X. B ) e. _V )
33 rnxp 
 |-  ( A =/= (/) -> ran ( A X. B ) = B )
34 33 eleq1d 
 |-  ( A =/= (/) -> ( ran ( A X. B ) e. _V <-> B e. _V ) )
35 32 34 syl5ib 
 |-  ( A =/= (/) -> ( ( A X. B ) e. _V -> B e. _V ) )
36 35 con3d 
 |-  ( A =/= (/) -> ( -. B e. _V -> -. ( A X. B ) e. _V ) )
37 36 impcom 
 |-  ( ( -. B e. _V /\ A =/= (/) ) -> -. ( A X. B ) e. _V )
38 37 19 syl 
 |-  ( ( -. B e. _V /\ A =/= (/) ) -> ( _I ` ( A X. B ) ) = (/) )
39 31 38 pm2.61dane 
 |-  ( -. B e. _V -> ( _I ` ( A X. B ) ) = (/) )
40 23 25 39 3eqtr4a 
 |-  ( -. B e. _V -> ( ( _I ` A ) X. ( _I ` B ) ) = ( _I ` ( A X. B ) ) )
41 fvi 
 |-  ( A e. _V -> ( _I ` A ) = A )
42 fvi 
 |-  ( B e. _V -> ( _I ` B ) = B )
43 xpeq12 
 |-  ( ( ( _I ` A ) = A /\ ( _I ` B ) = B ) -> ( ( _I ` A ) X. ( _I ` B ) ) = ( A X. B ) )
44 41 42 43 syl2an 
 |-  ( ( A e. _V /\ B e. _V ) -> ( ( _I ` A ) X. ( _I ` B ) ) = ( A X. B ) )
45 xpexg 
 |-  ( ( A e. _V /\ B e. _V ) -> ( A X. B ) e. _V )
46 fvi 
 |-  ( ( A X. B ) e. _V -> ( _I ` ( A X. B ) ) = ( A X. B ) )
47 45 46 syl 
 |-  ( ( A e. _V /\ B e. _V ) -> ( _I ` ( A X. B ) ) = ( A X. B ) )
48 44 47 eqtr4d 
 |-  ( ( A e. _V /\ B e. _V ) -> ( ( _I ` A ) X. ( _I ` B ) ) = ( _I ` ( A X. B ) ) )
49 22 40 48 ecase 
 |-  ( ( _I ` A ) X. ( _I ` B ) ) = ( _I ` ( A X. B ) )