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	imbitrid	|- ( 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	imbitrid	|- ( 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 ) )