Theorem txsubsp 15912

Description: The subspace of a topological product space induced by a subset with a Cartesian product representation is a topological product of the subspaces induced by the subspaces of the terms of the products.

Hypotheses

Ref	Expression
txsubsp.1	|- X = U.R
txsubsp.2	|- Y = U.S

Assertion

Ref	Expression
txsubsp	|- (((R e. Top /\ S e. Top) /\ (A C_ X /\ B C_ Y)) -> (subSp` <.(A X. B), (R X.t S)>.) = ((subSp` <.A, R>.) X.t (subSp` <.B, S>.)))

Proof of Theorem txsubsp

Step	Hyp	Ref	Expression
1		txval 8932	. . . . . . . . . 10 |- ((R e. Top /\ S e. Top) -> (R X.t S) = (topGen` {z | E.u e. R E.v e. S z = (u X. v)}))
2	1	eleq2d 1964	. . . . . . . . 9 |- ((R e. Top /\ S e. Top) -> (y e. (R X.t S) <-> y e. (topGen` {z | E.u e. R E.v e. S z = (u X. v)})))
3		txbas 8933	. . . . . . . . . 10 |- ((R e. Top /\ S e. Top) -> {z | E.u e. R E.v e. S z = (u X. v)} e. Bases)
4		eltg3 8896	. . . . . . . . . 10 |- ({z | E.u e. R E.v e. S z = (u X. v)} e. Bases -> (y e. (topGen` {z | E.u e. R E.v e. S z = (u X. v)}) <-> E.t(t C_ {z | E.u e. R E.v e. S z = (u X. v)} /\ y = U.t)))
5	3, 4	syl 12	. . . . . . . . 9 |- ((R e. Top /\ S e. Top) -> (y e. (topGen` {z | E.u e. R E.v e. S z = (u X. v)}) <-> E.t(t C_ {z | E.u e. R E.v e. S z = (u X. v)} /\ y = U.t)))
6	2, 5	bitrd 587	. . . . . . . 8 |- ((R e. Top /\ S e. Top) -> (y e. (R X.t S) <-> E.t(t C_ {z | E.u e. R E.v e. S z = (u X. v)} /\ y = U.t)))
7	6	adantr 425	. . . . . . 7 |- (((R e. Top /\ S e. Top) /\ (A C_ X /\ B C_ Y)) -> (y e. (R X.t S) <-> E.t(t C_ {z | E.u e. R E.v e. S z = (u X. v)} /\ y = U.t)))
8		ineq1 2789	. . . . . . . . . . . 12 |- (y = U.t -> (y i^i (A X. B)) = (U.t i^i (A X. B)))
9		inuni 3470	. . . . . . . . . . . 12 |- (U.t i^i (A X. B)) = U.{q | E.x e. t q = (x i^i (A X. B))}
10	8, 9	syl6eq 1944	. . . . . . . . . . 11 |- (y = U.t -> (y i^i (A X. B)) = U.{q | E.x e. t q = (x i^i (A X. B))})
11	10	eleq1d 1963	. . . . . . . . . 10 |- (y = U.t -> ((y i^i (A X. B)) e. (topGen` {w | E.r e. (subSp` <.A, R>.)E.s e. (subSp` <.B, S>.)w = (r X. s)}) <-> U.{q | E.x e. t q = (x i^i (A X. B))} e. (topGen` {w | E.r e. (subSp` <.A, R>.)E.s e. (subSp` <.B, S>.)w = (r X. s)})))
12		txbas 8933	. . . . . . . . . . . . . . 15 |- (((subSp` <.A, R>.) e. Top /\ (subSp` <.B, S>.) e. Top) -> {w | E.r e. (subSp` <.A, R>.)E.s e. (subSp` <.B, S>.)w = (r X. s)} e. Bases)
13		stoig3 10253	. . . . . . . . . . . . . . . 16 |- ((R e. Top /\ A C_ U.R) -> (subSp` <.A, R>.) e. Top)
14		txsubsp.1	. . . . . . . . . . . . . . . . 17 |- X = U.R
15	14	sseq2i 2642	. . . . . . . . . . . . . . . 16 |- (A C_ X <-> A C_ U.R)
16	13, 15	sylan2b 501	. . . . . . . . . . . . . . 15 |- ((R e. Top /\ A C_ X) -> (subSp` <.A, R>.) e. Top)
17		stoig3 10253	. . . . . . . . . . . . . . . 16 |- ((S e. Top /\ B C_ U.S) -> (subSp` <.B, S>.) e. Top)
18		txsubsp.2	. . . . . . . . . . . . . . . . 17 |- Y = U.S
19	18	sseq2i 2642	. . . . . . . . . . . . . . . 16 |- (B C_ Y <-> B C_ U.S)
20	17, 19	sylan2b 501	. . . . . . . . . . . . . . 15 |- ((S e. Top /\ B C_ Y) -> (subSp` <.B, S>.) e. Top)
21	12, 16, 20	syl2an 503	. . . . . . . . . . . . . 14 |- (((R e. Top /\ A C_ X) /\ (S e. Top /\ B C_ Y)) -> {w | E.r e. (subSp` <.A, R>.)E.s e. (subSp` <.B, S>.)w = (r X. s)} e. Bases)
22		tgcl 8894	. . . . . . . . . . . . . 14 |- ({w | E.r e. (subSp` <.A, R>.)E.s e. (subSp` <.B, S>.)w = (r X. s)} e. Bases -> (topGen` {w | E.r e. (subSp` <.A, R>.)E.s e. (subSp` <.B, S>.)w = (r X. s)}) e. Top)
23	21, 22	syl 12	. . . . . . . . . . . . 13 |- (((R e. Top /\ A C_ X) /\ (S e. Top /\ B C_ Y)) -> (topGen` {w | E.r e. (subSp` <.A, R>.)E.s e. (subSp` <.B, S>.)w = (r X. s)}) e. Top)
24	23	an4s 566	. . . . . . . . . . . 12 |- (((R e. Top /\ S e. Top) /\ (A C_ X /\ B C_ Y)) -> (topGen` {w | E.r e. (subSp` <.A, R>.)E.s e. (subSp` <.B, S>.)w = (r X. s)}) e. Top)
25	24	adantr 425	. . . . . . . . . . 11 |- ((((R e. Top /\ S e. Top) /\ (A C_ X /\ B C_ Y)) /\ t C_ {z | E.u e. R E.v e. S z = (u X. v)}) -> (topGen` {w | E.r e. (subSp` <.A, R>.)E.s e. (subSp` <.B, S>.)w = (r X. s)}) e. Top)
26		eleq1 1957	. . . . . . . . . . . . . 14 |- (q = (x i^i (A X. B)) -> (q e. (topGen` {w | E.r e. (subSp` <.A, R>.)E.s e. (subSp` <.B, S>.)w = (r X. s)}) <-> (x i^i (A X. B)) e. (topGen` {w | E.r e. (subSp` <.A, R>.)E.s e. (subSp` <.B, S>.)w = (r X. s)})))
27	21	an4s 566	. . . . . . . . . . . . . . . . 17 |- (((R e. Top /\ S e. Top) /\ (A C_ X /\ B C_ Y)) -> {w | E.r e. (subSp` <.A, R>.)E.s e. (subSp` <.B, S>.)w = (r X. s)} e. Bases)
28		bastg 8892	. . . . . . . . . . . . . . . . 17 |- ({w | E.r e. (subSp` <.A, R>.)E.s e. (subSp` <.B, S>.)w = (r X. s)} e. Bases -> {w | E.r e. (subSp` <.A, R>.)E.s e. (subSp` <.B, S>.)w = (r X. s)} C_ (topGen` {w | E.r e. (subSp` <.A, R>.)E.s e. (subSp` <.B, S>.)w = (r X. s)}))
29	27, 28	syl 12	. . . . . . . . . . . . . . . 16 |- (((R e. Top /\ S e. Top) /\ (A C_ X /\ B C_ Y)) -> {w | E.r e. (subSp` <.A, R>.)E.s e. (subSp` <.B, S>.)w = (r X. s)} C_ (topGen` {w | E.r e. (subSp` <.A, R>.)E.s e. (subSp` <.B, S>.)w = (r X. s)}))
30	29	ad2antrr 440	. . . . . . . . . . . . . . 15 |- (((((R e. Top /\ S e. Top) /\ (A C_ X /\ B C_ Y)) /\ t C_ {z | E.u e. R E.v e. S z = (u X. v)}) /\ x e. t) -> {w | E.r e. (subSp` <.A, R>.)E.s e. (subSp` <.B, S>.)w = (r X. s)} C_ (topGen` {w | E.r e. (subSp` <.A, R>.)E.s e. (subSp` <.B, S>.)w = (r X. s)}))
31		eqid 1884	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (u i^i A) = (u i^i A)
32		ineq1 2789	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (x = u -> (x i^i A) = (u i^i A))
33	32	eqeq2d 1895	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (x = u -> ((u i^i A) = (x i^i A) <-> (u i^i A) = (u i^i A)))
34	33	rcla4ev 2381	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((u e. R /\ (u i^i A) = (u i^i A)) -> E.x e. R (u i^i A) = (x i^i A))
35	31, 34	mpan2 760	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (u e. R -> E.x e. R (u i^i A) = (x i^i A))
36	35	ad2antrl 442	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((((R e. Top /\ S e. Top) /\ (A C_ X /\ B C_ Y)) /\ (u e. R /\ v e. S)) -> E.x e. R (u i^i A) = (x i^i A))
37		simplll 452	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((((R e. Top /\ S e. Top) /\ (A C_ X /\ B C_ Y)) /\ (u e. R /\ v e. S)) -> R e. Top)
38		visset 2295	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- u e. _V
39	38	inex1 3452	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (u i^i A) e. _V
40	39	a1i 8	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((((R e. Top /\ S e. Top) /\ (A C_ X /\ B C_ Y)) /\ (u e. R /\ v e. S)) -> (u i^i A) e. _V)
41		ssexg 3457	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ((A C_ X /\ X e. _V) -> A e. _V)
42		uniexg 3795	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (R e. Top -> U.R e. _V)
43	42, 14	syl5eqel 1975	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (R e. Top -> X e. _V)
44	41, 43	sylan2 500	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((A C_ X /\ R e. Top) -> A e. _V)
45	44	ancoms 484	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((R e. Top /\ A C_ X) -> A e. _V)
46	45	ad2ant2r 445	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (((R e. Top /\ S e. Top) /\ (A C_ X /\ B C_ Y)) -> A e. _V)
47	46	adantr 425	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((((R e. Top /\ S e. Top) /\ (A C_ X /\ B C_ Y)) /\ (u e. R /\ v e. S)) -> A e. _V)
48		issubspt 10247	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((R e. Top /\ (u i^i A) e. _V /\ A e. _V) -> ((u i^i A) e. (subSp` <.A, R>.) <-> E.x e. R (u i^i A) = (x i^i A)))
49	37, 40, 47, 48	syl111anc 1100	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((((R e. Top /\ S e. Top) /\ (A C_ X /\ B C_ Y)) /\ (u e. R /\ v e. S)) -> ((u i^i A) e. (subSp` <.A, R>.) <-> E.x e. R (u i^i A) = (x i^i A)))
50	36, 49	mpbird 213	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((((R e. Top /\ S e. Top) /\ (A C_ X /\ B C_ Y)) /\ (u e. R /\ v e. S)) -> (u i^i A) e. (subSp` <.A, R>.))
51		eqid 1884	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (v i^i B) = (v i^i B)
52		ineq1 2789	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (x = v -> (x i^i B) = (v i^i B))
53	52	eqeq2d 1895	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (x = v -> ((v i^i B) = (x i^i B) <-> (v i^i B) = (v i^i B)))
54	53	rcla4ev 2381	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((v e. S /\ (v i^i B) = (v i^i B)) -> E.x e. S (v i^i B) = (x i^i B))
55	51, 54	mpan2 760	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (v e. S -> E.x e. S (v i^i B) = (x i^i B))
56	55	ad2antll 443	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((((R e. Top /\ S e. Top) /\ (A C_ X /\ B C_ Y)) /\ (u e. R /\ v e. S)) -> E.x e. S (v i^i B) = (x i^i B))
57		simpllr 453	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((((R e. Top /\ S e. Top) /\ (A C_ X /\ B C_ Y)) /\ (u e. R /\ v e. S)) -> S e. Top)
58		inex1g 3454	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (v e. S -> (v i^i B) e. _V)
59	58	ad2antll 443	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((((R e. Top /\ S e. Top) /\ (A C_ X /\ B C_ Y)) /\ (u e. R /\ v e. S)) -> (v i^i B) e. _V)
60		ssexg 3457	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ((B C_ Y /\ Y e. _V) -> B e. _V)
61		uniexg 3795	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (S e. Top -> U.S e. _V)
62	61, 18	syl5eqel 1975	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (S e. Top -> Y e. _V)
63	60, 62	sylan2 500	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((B C_ Y /\ S e. Top) -> B e. _V)
64	63	ancoms 484	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((S e. Top /\ B C_ Y) -> B e. _V)
65	64	ad2ant2l 444	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (((R e. Top /\ S e. Top) /\ (A C_ X /\ B C_ Y)) -> B e. _V)
66	65	adantr 425	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((((R e. Top /\ S e. Top) /\ (A C_ X /\ B C_ Y)) /\ (u e. R /\ v e. S)) -> B e. _V)
67		issubspt 10247	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((S e. Top /\ (v i^i B) e. _V /\ B e. _V) -> ((v i^i B) e. (subSp` <.B, S>.) <-> E.x e. S (v i^i B) = (x i^i B)))
68	57, 59, 66, 67	syl111anc 1100	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((((R e. Top /\ S e. Top) /\ (A C_ X /\ B C_ Y)) /\ (u e. R /\ v e. S)) -> ((v i^i B) e. (subSp` <.B, S>.) <-> E.x e. S (v i^i B) = (x i^i B)))
69	56, 68	mpbird 213	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((((R e. Top /\ S e. Top) /\ (A C_ X /\ B C_ Y)) /\ (u e. R /\ v e. S)) -> (v i^i B) e. (subSp` <.B, S>.))
70		inxp 4109	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((u X. v) i^i (A X. B)) = ((u i^i A) X. (v i^i B))
71	70	a1i 8	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((((R e. Top /\ S e. Top) /\ (A C_ X /\ B C_ Y)) /\ (u e. R /\ v e. S)) -> ((u X. v) i^i (A X. B)) = ((u i^i A) X. (v i^i B)))
72		xpeq1 4016	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (r = (u i^i A) -> (r X. s) = ((u i^i A) X. s))
73	72	eqeq2d 1895	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (r = (u i^i A) -> (((u X. v) i^i (A X. B)) = (r X. s) <-> ((u X. v) i^i (A X. B)) = ((u i^i A) X. s)))
74		xpeq2 4017	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (s = (v i^i B) -> ((u i^i A) X. s) = ((u i^i A) X. (v i^i B)))
75	74	eqeq2d 1895	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (s = (v i^i B) -> (((u X. v) i^i (A X. B)) = ((u i^i A) X. s) <-> ((u X. v) i^i (A X. B)) = ((u i^i A) X. (v i^i B))))
76	73, 75	rcla42ev 2385	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (((u i^i A) e. (subSp` <.A, R>.) /\ (v i^i B) e. (subSp` <.B, S>.) /\ ((u X. v) i^i (A X. B)) = ((u i^i A) X. (v i^i B))) -> E.r e. (subSp` <.A, R>.)E.s e. (subSp` <.B, S>.)((u X. v) i^i (A X. B)) = (r X. s))
77	50, 69, 71, 76	syl111anc 1100	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((((R e. Top /\ S e. Top) /\ (A C_ X /\ B C_ Y)) /\ (u e. R /\ v e. S)) -> E.r e. (subSp` <.A, R>.)E.s e. (subSp` <.B, S>.)((u X. v) i^i (A X. B)) = (r X. s))
78		visset 2295	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- v e. _V
79	38, 78	xpex 4096	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (u X. v) e. _V
80	79	inex1 3452	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((u X. v) i^i (A X. B)) e. _V
81		eqeq1 1890	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (w = ((u X. v) i^i (A X. B)) -> (w = (r X. s) <-> ((u X. v) i^i (A X. B)) = (r X. s)))
82	81	2rexbidv 2141	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (w = ((u X. v) i^i (A X. B)) -> (E.r e. (subSp` <.A, R>.)E.s e. (subSp` <.B, S>.)w = (r X. s) <-> E.r e. (subSp` <.A, R>.)E.s e. (subSp` <.B, S>.)((u X. v) i^i (A X. B)) = (r X. s)))
83	80, 82	elab 2403	. . . . . . . . . . . . . . . . . . . . . . 23 |- (((u X. v) i^i (A X. B)) e. {w | E.r e. (subSp` <.A, R>.)E.s e. (subSp` <.B, S>.)w = (r X. s)} <-> E.r e. (subSp` <.A, R>.)E.s e. (subSp` <.B, S>.)((u X. v) i^i (A X. B)) = (r X. s))
84	77, 83	sylibr 217	. . . . . . . . . . . . . . . . . . . . . 22 |- ((((R e. Top /\ S e. Top) /\ (A C_ X /\ B C_ Y)) /\ (u e. R /\ v e. S)) -> ((u X. v) i^i (A X. B)) e. {w | E.r e. (subSp` <.A, R>.)E.s e. (subSp` <.B, S>.)w = (r X. s)})
85	84	ex 402	. . . . . . . . . . . . . . . . . . . . 21 |- (((R e. Top /\ S e. Top) /\ (A C_ X /\ B C_ Y)) -> ((u e. R /\ v e. S) -> ((u X. v) i^i (A X. B)) e. {w | E.r e. (subSp` <.A, R>.)E.s e. (subSp` <.B, S>.)w = (r X. s)}))
86		ineq1 2789	. . . . . . . . . . . . . . . . . . . . . . 23 |- (x = (u X. v) -> (x i^i (A X. B)) = ((u X. v) i^i (A X. B)))
87	86	eleq1d 1963	. . . . . . . . . . . . . . . . . . . . . 22 |- (x = (u X. v) -> ((x i^i (A X. B)) e. {w | E.r e. (subSp` <.A, R>.)E.s e. (subSp` <.B, S>.)w = (r X. s)} <-> ((u X. v) i^i (A X. B)) e. {w | E.r e. (subSp` <.A, R>.)E.s e. (subSp` <.B, S>.)w = (r X. s)}))
88	87	biimprcd 173	. . . . . . . . . . . . . . . . . . . . 21 |- (((u X. v) i^i (A X. B)) e. {w | E.r e. (subSp` <.A, R>.)E.s e. (subSp` <.B, S>.)w = (r X. s)} -> (x = (u X. v) -> (x i^i (A X. B)) e. {w | E.r e. (subSp` <.A, R>.)E.s e. (subSp` <.B, S>.)w = (r X. s)}))
89	85, 88	syl6 25	. . . . . . . . . . . . . . . . . . . 20 |- (((R e. Top /\ S e. Top) /\ (A C_ X /\ B C_ Y)) -> ((u e. R /\ v e. S) -> (x = (u X. v) -> (x i^i (A X. B)) e. {w | E.r e. (subSp` <.A, R>.)E.s e. (subSp` <.B, S>.)w = (r X. s)})))
90	89	r19.23advv 2218	. . . . . . . . . . . . . . . . . . 19 |- (((R e. Top /\ S e. Top) /\ (A C_ X /\ B C_ Y)) -> (E.u e. R E.v e. S x = (u X. v) -> (x i^i (A X. B)) e. {w | E.r e. (subSp` <.A, R>.)E.s e. (subSp` <.B, S>.)w = (r X. s)}))
91	90	imp 377	. . . . . . . . . . . . . . . . . 18 |- ((((R e. Top /\ S e. Top) /\ (A C_ X /\ B C_ Y)) /\ E.u e. R E.v e. S x = (u X. v)) -> (x i^i (A X. B)) e. {w | E.r e. (subSp` <.A, R>.)E.s e. (subSp` <.B, S>.)w = (r X. s)})
92		visset 2295	. . . . . . . . . . . . . . . . . . 19 |- x e. _V
93		eqeq1 1890	. . . . . . . . . . . . . . . . . . . 20 |- (z = x -> (z = (u X. v) <-> x = (u X. v)))
94	93	2rexbidv 2141	. . . . . . . . . . . . . . . . . . 19 |- (z = x -> (E.u e. R E.v e. S z = (u X. v) <-> E.u e. R E.v e. S x = (u X. v)))
95	92, 94	elab 2403	. . . . . . . . . . . . . . . . . 18 |- (x e. {z | E.u e. R E.v e. S z = (u X. v)} <-> E.u e. R E.v e. S x = (u X. v))
96	91, 95	sylan2b 501	. . . . . . . . . . . . . . . . 17 |- ((((R e. Top /\ S e. Top) /\ (A C_ X /\ B C_ Y)) /\ x e. {z | E.u e. R E.v e. S z = (u X. v)}) -> (x i^i (A X. B)) e. {w | E.r e. (subSp` <.A, R>.)E.s e. (subSp` <.B, S>.)w = (r X. s)})
97		ssel2 2616	. . . . . . . . . . . . . . . . 17 |- ((t C_ {z | E.u e. R E.v e. S z = (u X. v)} /\ x e. t) -> x e. {z | E.u e. R E.v e. S z = (u X. v)})
98	96, 97	sylan2 500	. . . . . . . . . . . . . . . 16 |- ((((R e. Top /\ S e. Top) /\ (A C_ X /\ B C_ Y)) /\ (t C_ {z | E.u e. R E.v e. S z = (u X. v)} /\ x e. t)) -> (x i^i (A X. B)) e. {w | E.r e. (subSp` <.A, R>.)E.s e. (subSp` <.B, S>.)w = (r X. s)})
99	98	anassrs 489	. . . . . . . . . . . . . . 15 |- (((((R e. Top /\ S e. Top) /\ (A C_ X /\ B C_ Y)) /\ t C_ {z | E.u e. R E.v e. S z = (u X. v)}) /\ x e. t) -> (x i^i (A X. B)) e. {w | E.r e. (subSp` <.A, R>.)E.s e. (subSp` <.B, S>.)w = (r X. s)})
100	30, 99	sseldd 2620	. . . . . . . . . . . . . 14 |- (((((R e. Top /\ S e. Top) /\ (A C_ X /\ B C_ Y)) /\ t C_ {z | E.u e. R E.v e. S z = (u X. v)}) /\ x e. t) -> (x i^i (A X. B)) e. (topGen` {w | E.r e. (subSp` <.A, R>.)E.s e. (subSp` <.B, S>.)w = (r X. s)}))
101	26, 100	syl5cbir 228	. . . . . . . . . . . . 13 |- (((((R e. Top /\ S e. Top) /\ (A C_ X /\ B C_ Y)) /\ t C_ {z | E.u e. R E.v e. S z = (u X. v)}) /\ x e. t) -> (q = (x i^i (A X. B)) -> q e. (topGen` {w | E.r e. (subSp` <.A, R>.)E.s e. (subSp` <.B, S>.)w = (r X. s)})))
102	101	r19.23adva 2216	. . . . . . . . . . . 12 |- ((((R e. Top /\ S e. Top) /\ (A C_ X /\ B C_ Y)) /\ t C_ {z | E.u e. R E.v e. S z = (u X. v)}) -> (E.x e. t q = (x i^i (A X. B)) -> q e. (topGen` {w | E.r e. (subSp` <.A, R>.)E.s e. (subSp` <.B, S>.)w = (r X. s)})))
103	102	abssdv 2681	. . . . . . . . . . 11 |- ((((R e. Top /\ S e. Top) /\ (A C_ X /\ B C_ Y)) /\ t C_ {z | E.u e. R E.v e. S z = (u X. v)}) -> {q | E.x e. t q = (x i^i (A X. B))} C_ (topGen` {w | E.r e. (subSp` <.A, R>.)E.s e. (subSp` <.B, S>.)w = (r X. s)}))
104		uniopn 8867	. . . . . . . . . . 11 |- (((topGen` {w | E.r e. (subSp` <.A, R>.)E.s e. (subSp` <.B, S>.)w = (r X. s)}) e. Top /\ {q | E.x e. t q = (x i^i (A X. B))} C_ (topGen` {w | E.r e. (subSp` <.A, R>.)E.s e. (subSp` <.B, S>.)w = (r X. s)})) -> U.{q | E.x e. t q = (x i^i (A X. B))} e. (topGen` {w | E.r e. (subSp` <.A, R>.)E.s e. (subSp` <.B, S>.)w = (r X. s)}))
105	25, 103, 104	syl11anc 524	. . . . . . . . . 10 |- ((((R e. Top /\ S e. Top) /\ (A C_ X /\ B C_ Y)) /\ t C_ {z | E.u e. R E.v e. S z = (u X. v)}) -> U.{q | E.x e. t q = (x i^i (A X. B))} e. (topGen` {w | E.r e. (subSp` <.A, R>.)E.s e. (subSp` <.B, S>.)w = (r X. s)}))
106	11, 105	syl5cbir 228	. . . . . . . . 9 |- ((((R e. Top /\ S e. Top) /\ (A C_ X /\ B C_ Y)) /\ t C_ {z | E.u e. R E.v e. S z = (u X. v)}) -> (y = U.t -> (y i^i (A X. B)) e. (topGen` {w | E.r e. (subSp` <.A, R>.)E.s e. (subSp` <.B, S>.)w = (r X. s)})))
107	106	expimpd 404	. . . . . . . 8 |- (((R e. Top /\ S e. Top) /\ (A C_ X /\ B C_ Y)) -> ((t C_ {z | E.u e. R E.v e. S z = (u X. v)} /\ y = U.t) -> (y i^i (A X. B)) e. (topGen` {w | E.r e. (subSp` <.A, R>.)E.s e. (subSp` <.B, S>.)w = (r X. s)})))
108	107	19.23adv 1584	. . . . . . 7 |- (((R e. Top /\ S e. Top) /\ (A C_ X /\ B C_ Y)) -> (E.t(t C_ {z | E.u e. R E.v e. S z = (u X. v)} /\ y = U.t) -> (y i^i (A X. B)) e. (topGen` {w | E.r e. (subSp` <.A, R>.)E.s e. (subSp` <.B, S>.)w = (r X. s)})))
109	7, 108	sylbid 220	. . . . . 6 |- (((R e. Top /\ S e. Top) /\ (A C_ X /\ B C_ Y)) -> (y e. (R X.t S) -> (y i^i (A X. B)) e. (topGen` {w | E.r e. (subSp` <.A, R>.)E.s e. (subSp` <.B, S>.)w = (r X. s)})))
110		eleq1a 1966	. . . . . 6 |- ((y i^i (A X. B)) e. (topGen` {w | E.r e. (subSp` <.A, R>.)E.s e. (subSp` <.B, S>.)w = (r X. s)}) -> (x = (y i^i (A X. B)) -> x e. (topGen` {w | E.r e. (subSp` <.A, R>.)E.s e. (subSp` <.B, S>.)w = (r X. s)})))
111	109, 110	syl6 25	. . . . 5 |- (((R e. Top /\ S e. Top) /\ (A C_ X /\ B C_ Y)) -> (y e. (R X.t S) -> (x = (y i^i (A X. B)) -> x e. (topGen` {w | E.r e. (subSp` <.A, R>.)E.s e. (subSp` <.B, S>.)w = (r X. s)}))))
112	111	r19.23adv 2215	. . . 4 |- (((R e. Top /\ S e. Top) /\ (A C_ X /\ B C_ Y)) -> (E.y e. (R X.t S)x = (y i^i (A X. B)) -> x e. (topGen` {w | E.r e. (subSp` <.A, R>.)E.s e. (subSp` <.B, S>.)w = (r X. s)})))
113		eqid 1884	. . . . . . 7 |- (R X.t S) = (R X.t S)
114	113	txtop 8934	. . . . . 6 |- ((R e. Top /\ S e. Top) -> (R X.t S) e. Top)
115	114	adantr 425	. . . . 5 |- (((R e. Top /\ S e. Top) /\ (A C_ X /\ B C_ Y)) -> (R X.t S) e. Top)
116	92	a1i 8	. . . . 5 |- (((R e. Top /\ S e. Top) /\ (A C_ X /\ B C_ Y)) -> x e. _V)
117		xpexg 4095	. . . . . . 7 |- ((A e. _V /\ B e. _V) -> (A X. B) e. _V)
118	117, 45, 64	syl2an 503	. . . . . 6 |- (((R e. Top /\ A C_ X) /\ (S e. Top /\ B C_ Y)) -> (A X. B) e. _V)
119	118	an4s 566	. . . . 5 |- (((R e. Top /\ S e. Top) /\ (A C_ X /\ B C_ Y)) -> (A X. B) e. _V)
120		issubspt 10247	. . . . 5 |- (((R X.t S) e. Top /\ x e. _V /\ (A X. B) e. _V) -> (x e. (subSp` <.(A X. B), (R X.t S)>.) <-> E.y e. (R X.t S)x = (y i^i (A X. B))))
121	115, 116, 119, 120	syl111anc 1100	. . . 4 |- (((R e. Top /\ S e. Top) /\ (A C_ X /\ B C_ Y)) -> (x e. (subSp` <.(A X. B), (R X.t S)>.) <-> E.y e. (R X.t S)x = (y i^i (A X. B))))
122		txval 8932	. . . . . . 7 |- (((subSp` <.A, R>.) e. Top /\ (subSp` <.B, S>.) e. Top) -> ((subSp` <.A, R>.) X.t (subSp` <.B, S>.)) = (topGen` {w | E.r e. (subSp` <.A, R>.)E.s e. (subSp` <.B, S>.)w = (r X. s)}))
123	122, 16, 20	syl2an 503	. . . . . 6 |- (((R e. Top /\ A C_ X) /\ (S e. Top /\ B C_ Y)) -> ((subSp` <.A, R>.) X.t (subSp` <.B, S>.)) = (topGen` {w | E.r e. (subSp` <.A, R>.)E.s e. (subSp` <.B, S>.)w = (r X. s)}))
124	123	eleq2d 1964	. . . . 5 |- (((R e. Top /\ A C_ X) /\ (S e. Top /\ B C_ Y)) -> (x e. ((subSp` <.A, R>.) X.t (subSp` <.B, S>.)) <-> x e. (topGen` {w | E.r e. (subSp` <.A, R>.)E.s e. (subSp` <.B, S>.)w = (r X. s)})))
125	124	an4s 566	. . . 4 |- (((R e. Top /\ S e. Top) /\ (A C_ X /\ B C_ Y)) -> (x e. ((subSp` <.A, R>.) X.t (subSp` <.B, S>.)) <-> x e. (topGen` {w | E.r e. (subSp` <.A, R>.)E.s e. (subSp` <.B, S>.)w = (r X. s)})))
126	112, 121, 125	3imtr4d 602	. . 3 |- (((R e. Top /\ S e. Top) /\ (A C_ X /\ B C_ Y)) -> (x e. (subSp` <.(A X. B), (R X.t S)>.) -> x e. ((subSp` <.A, R>.) X.t (subSp` <.B, S>.))))
127		txval 8932	. . . . . . . 8 |- (((subSp` <.A, R>.) e. Top /\ (subSp` <.B, S>.) e. Top) -> ((subSp` <.A, R>.) X.t (subSp` <.B, S>.)) = (topGen` {z | E.u e. (subSp` <.A, R>.)E.v e. (subSp` <.B, S>.)z = (u X. v)}))
128	127	eleq2d 1964	. . . . . . 7 |- (((subSp` <.A, R>.) e. Top /\ (subSp` <.B, S>.) e. Top) -> (x e. ((subSp` <.A, R>.) X.t (subSp` <.B, S>.)) <-> x e. (topGen` {z | E.u e. (subSp` <.A, R>.)E.v e. (subSp` <.B, S>.)z = (u X. v)})))
129		txbas 8933	. . . . . . . 8 |- (((subSp` <.A, R>.) e. Top /\ (subSp` <.B, S>.) e. Top) -> {z | E.u e. (subSp` <.A, R>.)E.v e. (subSp` <.B, S>.)z = (u X. v)} e. Bases)
130		eltg3 8896	. . . . . . . 8 |- ({z | E.u e. (subSp` <.A, R>.)E.v e. (subSp` <.B, S>.)z = (u X. v)} e. Bases -> (x e. (topGen` {z | E.u e. (subSp` <.A, R>.)E.v e. (subSp` <.B, S>.)z = (u X. v)}) <-> E.t(t C_ {z | E.u e. (subSp` <.A, R>.)E.v e. (subSp` <.B, S>.)z = (u X. v)} /\ x = U.t)))
131	129, 130	syl 12	. . . . . . 7 |- (((subSp` <.A, R>.) e. Top /\ (subSp` <.B, S>.) e. Top) -> (x e. (topGen` {z | E.u e. (subSp` <.A, R>.)E.v e. (subSp` <.B, S>.)z = (u X. v)}) <-> E.t(t C_ {z | E.u e. (subSp` <.A, R>.)E.v e. (subSp` <.B, S>.)z = (u X. v)} /\ x = U.t)))
132	128, 131	bitrd 587	. . . . . 6 |- (((subSp` <.A, R>.) e. Top /\ (subSp` <.B, S>.) e. Top) -> (x e. ((subSp` <.A, R>.) X.t (subSp` <.B, S>.)) <-> E.t(t C_ {z | E.u e. (subSp` <.A, R>.)E.v e. (subSp` <.B, S>.)z = (u X. v)} /\ x = U.t)))
133	132, 16, 20	syl2an 503	. . . . 5 |- (((R e. Top /\ A C_ X) /\ (S e. Top /\ B C_ Y)) -> (x e. ((subSp` <.A, R>.) X.t (subSp` <.B, S>.)) <-> E.t(t C_ {z | E.u e. (subSp` <.A, R>.)E.v e. (subSp` <.B, S>.)z = (u X. v)} /\ x = U.t)))
134	133	an4s 566	. . . 4 |- (((R e. Top /\ S e. Top) /\ (A C_ X /\ B C_ Y)) -> (x e. ((subSp` <.A, R>.) X.t (subSp` <.B, S>.)) <-> E.t(t C_ {z | E.u e. (subSp` <.A, R>.)E.v e. (subSp` <.B, S>.)z = (u X. v)} /\ x = U.t)))
135		eleq1 1957	. . . . . . 7 |- (x = U.t -> (x e. (subSp` <.(A X. B), (R X.t S)>.) <-> U.t e. (subSp` <.(A X. B), (R X.t S)>.)))
136		xpss12 4089	. . . . . . . . . . . 12 |- ((A C_ X /\ B C_ Y) -> (A X. B) C_ (X X. Y))
137	136	adantl 424	. . . . . . . . . . 11 |- (((R e. Top /\ S e. Top) /\ (A C_ X /\ B C_ Y)) -> (A X. B) C_ (X X. Y))
138	113, 14, 18	txuni 8935	. . . . . . . . . . . 12 |- ((R e. Top /\ S e. Top) -> U.(R X.t S) = (X X. Y))
139	138	adantr 425	. . . . . . . . . . 11 |- (((R e. Top /\ S e. Top) /\ (A C_ X /\ B C_ Y)) -> U.(R X.t S) = (X X. Y))
140	137, 139	sseqtr4d 2654	. . . . . . . . . 10 |- (((R e. Top /\ S e. Top) /\ (A C_ X /\ B C_ Y)) -> (A X. B) C_ U.(R X.t S))
141		stoig3 10253	. . . . . . . . . 10 |- (((R X.t S) e. Top /\ (A X. B) C_ U.(R X.t S)) -> (subSp` <.(A X. B), (R X.t S)>.) e. Top)
142	115, 140, 141	syl11anc 524	. . . . . . . . 9 |- (((R e. Top /\ S e. Top) /\ (A C_ X /\ B C_ Y)) -> (subSp` <.(A X. B), (R X.t S)>.) e. Top)
143	142	adantr 425	. . . . . . . 8 |- ((((R e. Top /\ S e. Top) /\ (A C_ X /\ B C_ Y)) /\ t C_ {z | E.u e. (subSp` <.A, R>.)E.v e. (subSp` <.B, S>.)z = (u X. v)}) -> (subSp` <.(A X. B), (R X.t S)>.) e. Top)
144		sstr 2625	. . . . . . . . . 10 |- ((t C_ {z | E.u e. (subSp` <.A, R>.)E.v e. (subSp` <.B, S>.)z = (u X. v)} /\ {z | E.u e. (subSp` <.A, R>.)E.v e. (subSp` <.B, S>.)z = (u X. v)} C_ (subSp` <.(A X. B), (R X.t S)>.)) -> t C_ (subSp` <.(A X. B), (R X.t S)>.))
145		xpeq12 4020	. . . . . . . . . . . . . . . . . . . . 21 |- ((u = (r i^i A) /\ v = (s i^i B)) -> (u X. v) = ((r i^i A) X. (s i^i B)))
146		inxp 4109	. . . . . . . . . . . . . . . . . . . . 21 |- ((r X. s) i^i (A X. B)) = ((r i^i A) X. (s i^i B))
147	145, 146	syl6eqr 1946	. . . . . . . . . . . . . . . . . . . 20 |- ((u = (r i^i A) /\ v = (s i^i B)) -> (u X. v) = ((r X. s) i^i (A X. B)))
148	147	a1i 8	. . . . . . . . . . . . . . . . . . 19 |- ((((R e. Top /\ S e. Top) /\ (A C_ X /\ B C_ Y)) /\ (r e. R /\ s e. S)) -> ((u = (r i^i A) /\ v = (s i^i B)) -> (u X. v) = ((r X. s) i^i (A X. B))))
149		bastg 8892	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ({z | E.u e. R E.v e. S z = (u X. v)} e. Bases -> {z | E.u e. R E.v e. S z = (u X. v)} C_ (topGen` {z | E.u e. R E.v e. S z = (u X. v)}))
150	3, 149	syl 12	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((R e. Top /\ S e. Top) -> {z | E.u e. R E.v e. S z = (u X. v)} C_ (topGen` {z | E.u e. R E.v e. S z = (u X. v)}))
151	150	adantr 425	. . . . . . . . . . . . . . . . . . . . . 22 |- (((R e. Top /\ S e. Top) /\ (r e. R /\ s e. S)) -> {z | E.u e. R E.v e. S z = (u X. v)} C_ (topGen` {z | E.u e. R E.v e. S z = (u X. v)}))
152		simprl 450	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (((R e. Top /\ S e. Top) /\ (r e. R /\ s e. S)) -> r e. R)
153		simprr 451	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (((R e. Top /\ S e. Top) /\ (r e. R /\ s e. S)) -> s e. S)
154		eqidd 1885	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (((R e. Top /\ S e. Top) /\ (r e. R /\ s e. S)) -> (r X. s) = (r X. s))
155		xpeq1 4016	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (u = r -> (u X. v) = (r X. v))
156	155	eqeq2d 1895	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (u = r -> ((r X. s) = (u X. v) <-> (r X. s) = (r X. v)))
157		xpeq2 4017	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (v = s -> (r X. v) = (r X. s))
158	157	eqeq2d 1895	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (v = s -> ((r X. s) = (r X. v) <-> (r X. s) = (r X. s)))
159	156, 158	rcla42ev 2385	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((r e. R /\ s e. S /\ (r X. s) = (r X. s)) -> E.u e. R E.v e. S (r X. s) = (u X. v))
160	152, 153, 154, 159	syl111anc 1100	. . . . . . . . . . . . . . . . . . . . . . 23 |- (((R e. Top /\ S e. Top) /\ (r e. R /\ s e. S)) -> E.u e. R E.v e. S (r X. s) = (u X. v))
161		visset 2295	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- r e. _V
162		visset 2295	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- s e. _V
163	161, 162	xpex 4096	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (r X. s) e. _V
164		eqeq1 1890	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (z = (r X. s) -> (z = (u X. v) <-> (r X. s) = (u X. v)))
165	164	2rexbidv 2141	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (z = (r X. s) -> (E.u e. R E.v e. S z = (u X. v) <-> E.u e. R E.v e. S (r X. s) = (u X. v)))
166	163, 165	elab 2403	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((r X. s) e. {z | E.u e. R E.v e. S z = (u X. v)} <-> E.u e. R E.v e. S (r X. s) = (u X. v))
167	160, 166	sylibr 217	. . . . . . . . . . . . . . . . . . . . . 22 |- (((R e. Top /\ S e. Top) /\ (r e. R /\ s e. S)) -> (r X. s) e. {z | E.u e. R E.v e. S z = (u X. v)})
168	151, 167	sseldd 2620	. . . . . . . . . . . . . . . . . . . . 21 |- (((R e. Top /\ S e. Top) /\ (r e. R /\ s e. S)) -> (r X. s) e. (topGen` {z | E.u e. R E.v e. S z = (u X. v)}))
169	1	adantr 425	. . . . . . . . . . . . . . . . . . . . 21 |- (((R e. Top /\ S e. Top) /\ (r e. R /\ s e. S)) -> (R X.t S) = (topGen` {z | E.u e. R E.v e. S z = (u X. v)}))
170	168, 169	eleqtrrd 1974	. . . . . . . . . . . . . . . . . . . 20 |- (((R e. Top /\ S e. Top) /\ (r e. R /\ s e. S)) -> (r X. s) e. (R X.t S))
171	170	adantlr 429	. . . . . . . . . . . . . . . . . . 19 |- ((((R e. Top /\ S e. Top) /\ (A C_ X /\ B C_ Y)) /\ (r e. R /\ s e. S)) -> (r X. s) e. (R X.t S))
172	148, 171	jctild 662	. . . . . . . . . . . . . . . . . 18 |- ((((R e. Top /\ S e. Top) /\ (A C_ X /\ B C_ Y)) /\ (r e. R /\ s e. S)) -> ((u = (r i^i A) /\ v = (s i^i B)) -> ((r X. s) e. (R X.t S) /\ (u X. v) = ((r X. s) i^i (A X. B)))))
173		ineq1 2789	. . . . . . . . . . . . . . . . . . . 20 |- (y = (r X. s) -> (y i^i (A X. B)) = ((r X. s) i^i (A X. B)))
174	173	eqeq2d 1895	. . . . . . . . . . . . . . . . . . 19 |- (y = (r X. s) -> ((u X. v) = (y i^i (A X. B)) <-> (u X. v) = ((r X. s) i^i (A X. B))))
175	174	rcla4ev 2381	. . . . . . . . . . . . . . . . . 18 |- (((r X. s) e. (R X.t S) /\ (u X. v) = ((r X. s) i^i (A X. B))) -> E.y e. (R X.t S)(u X. v) = (y i^i (A X. B)))
176	172, 175	syl6 25	. . . . . . . . . . . . . . . . 17 |- ((((R e. Top /\ S e. Top) /\ (A C_ X /\ B C_ Y)) /\ (r e. R /\ s e. S)) -> ((u = (r i^i A) /\ v = (s i^i B)) -> E.y e. (R X.t S)(u X. v) = (y i^i (A X. B))))
177	176	ex 402	. . . . . . . . . . . . . . . 16 |- (((R e. Top /\ S e. Top) /\ (A C_ X /\ B C_ Y)) -> ((r e. R /\ s e. S) -> ((u = (r i^i A) /\ v = (s i^i B)) -> E.y e. (R X.t S)(u X. v) = (y i^i (A X. B)))))
178	177	r19.23advv 2218	. . . . . . . . . . . . . . 15 |- (((R e. Top /\ S e. Top) /\ (A C_ X /\ B C_ Y)) -> (E.r e. R E.s e. S (u = (r i^i A) /\ v = (s i^i B)) -> E.y e. (R X.t S)(u X. v) = (y i^i (A X. B))))
179		reeanv 2249	. . . . . . . . . . . . . . 15 |- (E.r e. R E.s e. S (u = (r i^i A) /\ v = (s i^i B)) <-> (E.r e. R u = (r i^i A) /\ E.s e. S v = (s i^i B)))
180	178, 179	syl5ibr 224	. . . . . . . . . . . . . 14 |- (((R e. Top /\ S e. Top) /\ (A C_ X /\ B C_ Y)) -> ((E.r e. R u = (r i^i A) /\ E.s e. S v = (s i^i B)) -> E.y e. (R X.t S)(u X. v) = (y i^i (A X. B))))
181		simpl 346	. . . . . . . . . . . . . . . . 17 |- ((R e. Top /\ A C_ X) -> R e. Top)
182	38	a1i 8	. . . . . . . . . . . . . . . . 17 |- ((R e. Top /\ A C_ X) -> u e. _V)
183		issubspt 10247	. . . . . . . . . . . . . . . . 17 |- ((R e. Top /\ u e. _V /\ A e. _V) -> (u e. (subSp` <.A, R>.) <-> E.r e. R u = (r i^i A)))
184	181, 182, 45, 183	syl111anc 1100	. . . . . . . . . . . . . . . 16 |- ((R e. Top /\ A C_ X) -> (u e. (subSp` <.A, R>.) <-> E.r e. R u = (r i^i A)))
185		simpl 346	. . . . . . . . . . . . . . . . 17 |- ((S e. Top /\ B C_ Y) -> S e. Top)
186	78	a1i 8	. . . . . . . . . . . . . . . . 17 |- ((S e. Top /\ B C_ Y) -> v e. _V)
187		issubspt 10247	. . . . . . . . . . . . . . . . 17 |- ((S e. Top /\ v e. _V /\ B e. _V) -> (v e. (subSp` <.B, S>.) <-> E.s e. S v = (s i^i B)))
188	185, 186, 64, 187	syl111anc 1100	. . . . . . . . . . . . . . . 16 |- ((S e. Top /\ B C_ Y) -> (v e. (subSp` <.B, S>.) <-> E.s e. S v = (s i^i B)))
189	184, 188	bi2anan9 694	. . . . . . . . . . . . . . 15 |- (((R e. Top /\ A C_ X) /\ (S e. Top /\ B C_ Y)) -> ((u e. (subSp` <.A, R>.) /\ v e. (subSp` <.B, S>.)) <-> (E.r e. R u = (r i^i A) /\ E.s e. S v = (s i^i B))))
190	189	an4s 566	. . . . . . . . . . . . . 14 |- (((R e. Top /\ S e. Top) /\ (A C_ X /\ B C_ Y)) -> ((u e. (subSp` <.A, R>.) /\ v e. (subSp` <.B, S>.)) <-> (E.r e. R u = (r i^i A) /\ E.s e. S v = (s i^i B))))
191	79	a1i 8	. . . . . . . . . . . . . . 15 |- (((R e. Top /\ S e. Top) /\ (A C_ X /\ B C_ Y)) -> (u X. v) e. _V)
192		issubspt 10247	. . . . . . . . . . . . . . 15 |- (((R X.t S) e. Top /\ (u X. v) e. _V /\ (A X. B) e. _V) -> ((u X. v) e. (subSp` <.(A X. B), (R X.t S)>.) <-> E.y e. (R X.t S)(u X. v) = (y i^i (A X. B))))
193	115, 191, 119, 192	syl111anc 1100	. . . . . . . . . . . . . 14 |- (((R e. Top /\ S e. Top) /\ (A C_ X /\ B C_ Y)) -> ((u X. v) e. (subSp` <.(A X. B), (R X.t S)>.) <-> E.y e. (R X.t S)(u X. v) = (y i^i (A X. B))))
194	180, 190, 193	3imtr4d 602	. . . . . . . . . . . . 13 |- (((R e. Top /\ S e. Top) /\ (A C_ X /\ B C_ Y)) -> ((u e. (subSp` <.A, R>.) /\ v e. (subSp` <.B, S>.)) -> (u X. v) e. (subSp` <.(A X. B), (R X.t S)>.)))
195		eleq1a 1966	. . . . . . . . . . . . 13 |- ((u X. v) e. (subSp` <.(A X. B), (R X.t S)>.) -> (z = (u X. v) -> z e. (subSp` <.(A X. B), (R X.t S)>.)))
196	194, 195	syl6 25	. . . . . . . . . . . 12 |- (((R e. Top /\ S e. Top) /\ (A C_ X /\ B C_ Y)) -> ((u e. (subSp` <.A, R>.) /\ v e. (subSp` <.B, S>.)) -> (z = (u X. v) -> z e. (subSp` <.(A X. B), (R X.t S)>.))))
197	196	r19.23advv 2218	. . . . . . . . . . 11 |- (((R e. Top /\ S e. Top) /\ (A C_ X /\ B C_ Y)) -> (E.u e. (subSp` <.A, R>.)E.v e. (subSp` <.B, S>.)z = (u X. v) -> z e. (subSp` <.(A X. B), (R X.t S)>.)))
198	197	abssdv 2681	. . . . . . . . . 10 |- (((R e. Top /\ S e. Top) /\ (A C_ X /\ B C_ Y)) -> {z | E.u e. (subSp` <.A, R>.)E.v e. (subSp` <.B, S>.)z = (u X. v)} C_ (subSp` <.(A X. B), (R X.t S)>.))
199	144, 198	sylan2 500	. . . . . . . . 9 |- ((t C_ {z | E.u e. (subSp` <.A, R>.)E.v e. (subSp` <.B, S>.)z = (u X. v)} /\ ((R e. Top /\ S e. Top) /\ (A C_ X /\ B C_ Y))) -> t C_ (subSp` <.(A X. B), (R X.t S)>.))
200	199	ancoms 484	. . . . . . . 8 |- ((((R e. Top /\ S e. Top) /\ (A C_ X /\ B C_ Y)) /\ t C_ {z | E.u e. (subSp` <.A, R>.)E.v e. (subSp` <.B, S>.)z = (u X. v)}) -> t C_ (subSp` <.(A X. B), (R X.t S)>.))
201		uniopn 8867	. . . . . . . 8 |- (((subSp` <.(A X. B), (R X.t S)>.) e. Top /\ t C_ (subSp` <.(A X. B), (R X.t S)>.)) -> U.t e. (subSp` <.(A X. B), (R X.t S)>.))
202	143, 200, 201	syl11anc 524	. . . . . . 7 |- ((((R e. Top /\ S e. Top) /\ (A C_ X /\ B C_ Y)) /\ t C_ {z | E.u e. (subSp` <.A, R>.)E.v e. (subSp` <.B, S>.)z = (u X. v)}) -> U.t e. (subSp` <.(A X. B), (R X.t S)>.))
203	135, 202	syl5cbir 228	. . . . . 6 |- ((((R e. Top /\ S e. Top) /\ (A C_ X /\ B C_ Y)) /\ t C_ {z | E.u e. (subSp` <.A, R>.)E.v e. (subSp` <.B, S>.)z = (u X. v)}) -> (x = U.t -> x e. (subSp` <.(A X. B), (R X.t S)>.)))
204	203	expimpd 404	. . . . 5 |- (((R e. Top /\ S e. Top) /\ (A C_ X /\ B C_ Y)) -> ((t C_ {z | E.u e. (subSp` <.A, R>.)E.v e. (subSp` <.B, S>.)z = (u X. v)} /\ x = U.t) -> x e. (subSp` <.(A X. B), (R X.t S)>.)))
205	204	19.23adv 1584	. . . 4 |- (((R e. Top /\ S e. Top) /\ (A C_ X /\ B C_ Y)) -> (E.t(t C_ {z | E.u e. (subSp` <.A, R>.)E.v e. (subSp` <.B, S>.)z = (u X. v)} /\ x = U.t) -> x e. (subSp` <.(A X. B), (R X.t S)>.)))
206	134, 205	sylbid 220	. . 3 |- (((R e. Top /\ S e. Top) /\ (A C_ X /\ B C_ Y)) -> (x e. ((subSp` <.A, R>.) X.t (subSp` <.B, S>.)) -> x e. (subSp` <.(A X. B), (R X.t S)>.)))
207	126, 206	impbid 574	. 2 |- (((R e. Top /\ S e. Top) /\ (A C_ X /\ B C_ Y)) -> (x e. (subSp` <.(A X. B), (R X.t S)>.) <-> x e. ((subSp` <.A, R>.) X.t (subSp` <.B, S>.))))
208	207	eqrdv 1882	1 |- (((R e. Top /\ S e. Top) /\ (A C_ X /\ B C_ Y)) -> (subSp` <.(A X. B), (R X.t S)>.) = ((subSp` <.A, R>.) X.t (subSp` <.B, S>.)))

Syntax hints:   -> wi 3   <-> wb 163   /\ wa 240   = wceq 1298   e. wcel 1300  E.wex 1326  {cab 1871  E.wrex 2106  _Vcvv 2292   i^i cin 2592   C_ wss 2593  <.cop 3046  U.cuni 3177   X. cxp 3984  ` cfv 3998  (class class class)co 4884  Topctop 8857  Basesctb 8859  topGenctg 8860   X.t ctx 8930  subSpcsubsp 10242

This theorem is referenced by:  cnresoprab2 15916  phtpycolem3 16053  phtpycolem4 16054  pcohtpylem3 16082  pcorevlem 16086

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-13 1311  ax-14 1312  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865  ax-rep 3428  ax-sep 3438  ax-nul 3445  ax-pow 3481  ax-pr 3524  ax-un 3790  ax-reg 5695

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-3an 860  df-ex 1327  df-sb 1536  df-eu 1775  df-mo 1776  df-clab 1872  df-cleq 1877  df-clel 1880  df-ne 2019  df-ral 2109  df-rex 2110  df-rab 2112  df-v 2294  df-sbc 2454  df-csb 2541  df-dif 2597  df-un 2600  df-in 2603  df-ss 2605  df-nul 2876  df-if 2983  df-pw 3035  df-sn 3049  df-pr 3050  df-op 3053  df-uni 3178  df-iun 3257  df-br 3339  df-opab 3396  df-id 3586  df-xp 4000  df-rel 4001  df-cnv 4002  df-co 4003  df-dm 4004  df-rn 4005  df-res 4006  df-ima 4007  df-fun 4008  df-fn 4009  df-fv 4014  df-opr 4886  df-oprab 4887  df-top 8861  df-topsp 8862  df-bases 8863  df-topgen 8864  df-tx 8931  df-subsp 10243

Copyright terms: Public domain