Theorem subsubtop 15423

Description: Equivalence of being a subspace of a subspace and being a subspace of the original.

Hypothesis

Ref	Expression
subsubtop.1	|- X = U.J

Assertion

Ref	Expression
subsubtop	|- ((J e. Top /\ S C_ T /\ T C_ X) -> (subSp` <.S, (subSp` <.T, J>.)>.) = (subSp` <.S, J>.))

Proof of Theorem subsubtop

Step	Hyp	Ref	Expression
1		simp1 876	. . . . . . 7 |- ((J e. Top /\ S C_ T /\ T C_ X) -> J e. Top)
2		ssexg 3457	. . . . . . . . . 10 |- ((T C_ U.J /\ U.J e. _V) -> T e. _V)
3	2	ancoms 484	. . . . . . . . 9 |- ((U.J e. _V /\ T C_ U.J) -> T e. _V)
4		uniexg 3795	. . . . . . . . 9 |- (J e. Top -> U.J e. _V)
5		subsubtop.1	. . . . . . . . . . 11 |- X = U.J
6	5	sseq2i 2642	. . . . . . . . . 10 |- (T C_ X <-> T C_ U.J)
7	6	biimpi 168	. . . . . . . . 9 |- (T C_ X -> T C_ U.J)
8	3, 4, 7	syl2an 503	. . . . . . . 8 |- ((J e. Top /\ T C_ X) -> T e. _V)
9	8	3adant2 895	. . . . . . 7 |- ((J e. Top /\ S C_ T /\ T C_ X) -> T e. _V)
10		visset 2295	. . . . . . . 8 |- s e. _V
11		issubspt 10247	. . . . . . . 8 |- ((J e. Top /\ s e. _V /\ T e. _V) -> (s e. (subSp` <.T, J>.) <-> E.r e. J s = (r i^i T)))
12	10, 11	mp3an2 1179	. . . . . . 7 |- ((J e. Top /\ T e. _V) -> (s e. (subSp` <.T, J>.) <-> E.r e. J s = (r i^i T)))
13	1, 9, 12	syl11anc 524	. . . . . 6 |- ((J e. Top /\ S C_ T /\ T C_ X) -> (s e. (subSp` <.T, J>.) <-> E.r e. J s = (r i^i T)))
14		simpllr 453	. . . . . . . . 9 |- (((((J e. Top /\ S C_ T /\ T C_ X) /\ r e. J) /\ s = (r i^i T)) /\ o = (s i^i S)) -> r e. J)
15		eqtr 1904	. . . . . . . . . . . . 13 |- ((o = (s i^i S) /\ (s i^i S) = ((r i^i T) i^i S)) -> o = ((r i^i T) i^i S))
16	15	ancoms 484	. . . . . . . . . . . 12 |- (((s i^i S) = ((r i^i T) i^i S) /\ o = (s i^i S)) -> o = ((r i^i T) i^i S))
17		ineq1 2789	. . . . . . . . . . . 12 |- (s = (r i^i T) -> (s i^i S) = ((r i^i T) i^i S))
18	16, 17	sylan 497	. . . . . . . . . . 11 |- ((s = (r i^i T) /\ o = (s i^i S)) -> o = ((r i^i T) i^i S))
19	18	adantll 428	. . . . . . . . . 10 |- (((((J e. Top /\ S C_ T /\ T C_ X) /\ r e. J) /\ s = (r i^i T)) /\ o = (s i^i S)) -> o = ((r i^i T) i^i S))
20		df-ss 2605	. . . . . . . . . . . . . . . . 17 |- (S C_ T <-> (S i^i T) = S)
21	20	biimpi 168	. . . . . . . . . . . . . . . 16 |- (S C_ T -> (S i^i T) = S)
22		incom 2787	. . . . . . . . . . . . . . . 16 |- (T i^i S) = (S i^i T)
23	21, 22	syl5eq 1940	. . . . . . . . . . . . . . 15 |- (S C_ T -> (T i^i S) = S)
24	23	3ad2ant2 898	. . . . . . . . . . . . . 14 |- ((J e. Top /\ S C_ T /\ T C_ X) -> (T i^i S) = S)
25	24	adantr 425	. . . . . . . . . . . . 13 |- (((J e. Top /\ S C_ T /\ T C_ X) /\ r e. J) -> (T i^i S) = S)
26	25	ad2antrr 440	. . . . . . . . . . . 12 |- (((((J e. Top /\ S C_ T /\ T C_ X) /\ r e. J) /\ s = (r i^i T)) /\ o = (s i^i S)) -> (T i^i S) = S)
27	26	ineq2d 2796	. . . . . . . . . . 11 |- (((((J e. Top /\ S C_ T /\ T C_ X) /\ r e. J) /\ s = (r i^i T)) /\ o = (s i^i S)) -> (r i^i (T i^i S)) = (r i^i S))
28		inass 2804	. . . . . . . . . . 11 |- ((r i^i T) i^i S) = (r i^i (T i^i S))
29	27, 28	syl5eq 1940	. . . . . . . . . 10 |- (((((J e. Top /\ S C_ T /\ T C_ X) /\ r e. J) /\ s = (r i^i T)) /\ o = (s i^i S)) -> ((r i^i T) i^i S) = (r i^i S))
30	19, 29	eqtrd 1925	. . . . . . . . 9 |- (((((J e. Top /\ S C_ T /\ T C_ X) /\ r e. J) /\ s = (r i^i T)) /\ o = (s i^i S)) -> o = (r i^i S))
31		ineq1 2789	. . . . . . . . . . 11 |- (t = r -> (t i^i S) = (r i^i S))
32	31	eqeq2d 1895	. . . . . . . . . 10 |- (t = r -> (o = (t i^i S) <-> o = (r i^i S)))
33	32	rcla4ev 2381	. . . . . . . . 9 |- ((r e. J /\ o = (r i^i S)) -> E.t e. J o = (t i^i S))
34	14, 30, 33	syl11anc 524	. . . . . . . 8 |- (((((J e. Top /\ S C_ T /\ T C_ X) /\ r e. J) /\ s = (r i^i T)) /\ o = (s i^i S)) -> E.t e. J o = (t i^i S))
35	34	exp31 407	. . . . . . 7 |- (((J e. Top /\ S C_ T /\ T C_ X) /\ r e. J) -> (s = (r i^i T) -> (o = (s i^i S) -> E.t e. J o = (t i^i S))))
36	35	r19.23adva 2216	. . . . . 6 |- ((J e. Top /\ S C_ T /\ T C_ X) -> (E.r e. J s = (r i^i T) -> (o = (s i^i S) -> E.t e. J o = (t i^i S))))
37	13, 36	sylbid 220	. . . . 5 |- ((J e. Top /\ S C_ T /\ T C_ X) -> (s e. (subSp` <.T, J>.) -> (o = (s i^i S) -> E.t e. J o = (t i^i S))))
38	37	r19.23adv 2215	. . . 4 |- ((J e. Top /\ S C_ T /\ T C_ X) -> (E.s e. (subSp` <.T, J>.)o = (s i^i S) -> E.t e. J o = (t i^i S)))
39		eqid 1884	. . . . . . . . . 10 |- (t i^i T) = (t i^i T)
40	5	elsubsp 10248	. . . . . . . . . 10 |- (((J e. Top /\ T C_ X) /\ (t e. J /\ (t i^i T) = (t i^i T))) -> (t i^i T) e. (subSp` <.T, J>.))
41	39, 40	mpanr2 776	. . . . . . . . 9 |- (((J e. Top /\ T C_ X) /\ t e. J) -> (t i^i T) e. (subSp` <.T, J>.))
42	41	3adantl2 1033	. . . . . . . 8 |- (((J e. Top /\ S C_ T /\ T C_ X) /\ t e. J) -> (t i^i T) e. (subSp` <.T, J>.))
43	42	adantr 425	. . . . . . 7 |- ((((J e. Top /\ S C_ T /\ T C_ X) /\ t e. J) /\ o = (t i^i S)) -> (t i^i T) e. (subSp` <.T, J>.))
44	24	ineq2d 2796	. . . . . . . . . . 11 |- ((J e. Top /\ S C_ T /\ T C_ X) -> (t i^i (T i^i S)) = (t i^i S))
45	44	adantr 425	. . . . . . . . . 10 |- (((J e. Top /\ S C_ T /\ T C_ X) /\ t e. J) -> (t i^i (T i^i S)) = (t i^i S))
46	45	eqeq2d 1895	. . . . . . . . 9 |- (((J e. Top /\ S C_ T /\ T C_ X) /\ t e. J) -> (o = (t i^i (T i^i S)) <-> o = (t i^i S)))
47	46	biimpar 461	. . . . . . . 8 |- ((((J e. Top /\ S C_ T /\ T C_ X) /\ t e. J) /\ o = (t i^i S)) -> o = (t i^i (T i^i S)))
48		inass 2804	. . . . . . . 8 |- ((t i^i T) i^i S) = (t i^i (T i^i S))
49	47, 48	syl6eqr 1946	. . . . . . 7 |- ((((J e. Top /\ S C_ T /\ T C_ X) /\ t e. J) /\ o = (t i^i S)) -> o = ((t i^i T) i^i S))
50		ineq1 2789	. . . . . . . . 9 |- (s = (t i^i T) -> (s i^i S) = ((t i^i T) i^i S))
51	50	eqeq2d 1895	. . . . . . . 8 |- (s = (t i^i T) -> (o = (s i^i S) <-> o = ((t i^i T) i^i S)))
52	51	rcla4ev 2381	. . . . . . 7 |- (((t i^i T) e. (subSp` <.T, J>.) /\ o = ((t i^i T) i^i S)) -> E.s e. (subSp` <.T, J>.)o = (s i^i S))
53	43, 49, 52	syl11anc 524	. . . . . 6 |- ((((J e. Top /\ S C_ T /\ T C_ X) /\ t e. J) /\ o = (t i^i S)) -> E.s e. (subSp` <.T, J>.)o = (s i^i S))
54	53	ex 402	. . . . 5 |- (((J e. Top /\ S C_ T /\ T C_ X) /\ t e. J) -> (o = (t i^i S) -> E.s e. (subSp` <.T, J>.)o = (s i^i S)))
55	54	r19.23adva 2216	. . . 4 |- ((J e. Top /\ S C_ T /\ T C_ X) -> (E.t e. J o = (t i^i S) -> E.s e. (subSp` <.T, J>.)o = (s i^i S)))
56	38, 55	impbid 574	. . 3 |- ((J e. Top /\ S C_ T /\ T C_ X) -> (E.s e. (subSp` <.T, J>.)o = (s i^i S) <-> E.t e. J o = (t i^i S)))
57		stoig3 10253	. . . . . 6 |- ((J e. Top /\ T C_ U.J) -> (subSp` <.T, J>.) e. Top)
58	57, 6	sylan2b 501	. . . . 5 |- ((J e. Top /\ T C_ X) -> (subSp` <.T, J>.) e. Top)
59	58	3adant2 895	. . . 4 |- ((J e. Top /\ S C_ T /\ T C_ X) -> (subSp` <.T, J>.) e. Top)
60		ssexg 3457	. . . . . . 7 |- ((S C_ U.J /\ U.J e. _V) -> S e. _V)
61	60	ancoms 484	. . . . . 6 |- ((U.J e. _V /\ S C_ U.J) -> S e. _V)
62		sstr 2625	. . . . . . 7 |- ((S C_ T /\ T C_ X) -> S C_ X)
63	62, 5	syl6ss 2663	. . . . . 6 |- ((S C_ T /\ T C_ X) -> S C_ U.J)
64	61, 4, 63	syl2an 503	. . . . 5 |- ((J e. Top /\ (S C_ T /\ T C_ X)) -> S e. _V)
65	64	3impb 1063	. . . 4 |- ((J e. Top /\ S C_ T /\ T C_ X) -> S e. _V)
66		visset 2295	. . . . 5 |- o e. _V
67		issubspt 10247	. . . . 5 |- (((subSp` <.T, J>.) e. Top /\ o e. _V /\ S e. _V) -> (o e. (subSp` <.S, (subSp` <.T, J>.)>.) <-> E.s e. (subSp` <.T, J>.)o = (s i^i S)))
68	66, 67	mp3an2 1179	. . . 4 |- (((subSp` <.T, J>.) e. Top /\ S e. _V) -> (o e. (subSp` <.S, (subSp` <.T, J>.)>.) <-> E.s e. (subSp` <.T, J>.)o = (s i^i S)))
69	59, 65, 68	syl11anc 524	. . 3 |- ((J e. Top /\ S C_ T /\ T C_ X) -> (o e. (subSp` <.S, (subSp` <.T, J>.)>.) <-> E.s e. (subSp` <.T, J>.)o = (s i^i S)))
70		issubspt 10247	. . . . 5 |- ((J e. Top /\ o e. _V /\ S e. _V) -> (o e. (subSp` <.S, J>.) <-> E.t e. J o = (t i^i S)))
71	66, 70	mp3an2 1179	. . . 4 |- ((J e. Top /\ S e. _V) -> (o e. (subSp` <.S, J>.) <-> E.t e. J o = (t i^i S)))
72	1, 65, 71	syl11anc 524	. . 3 |- ((J e. Top /\ S C_ T /\ T C_ X) -> (o e. (subSp` <.S, J>.) <-> E.t e. J o = (t i^i S)))
73	56, 69, 72	3bitr4d 609	. 2 |- ((J e. Top /\ S C_ T /\ T C_ X) -> (o e. (subSp` <.S, (subSp` <.T, J>.)>.) <-> o e. (subSp` <.S, J>.)))
74	73	eqrdv 1882	1 |- ((J e. Top /\ S C_ T /\ T C_ X) -> (subSp` <.S, (subSp` <.T, J>.)>.) = (subSp` <.S, J>.))

Syntax hints:   -> wi 3   <-> wb 163   /\ wa 240   /\ w3a 858   = wceq 1298   e. wcel 1300  E.wrex 2106  _Vcvv 2292   i^i cin 2592   C_ wss 2593  <.cop 3046  U.cuni 3177  ` cfv 3998  Topctop 8857  subSpcsubsp 10242

This theorem is referenced by:  ivthALT 15454

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-subsp 10243

Copyright terms: Public domain