Theorem sspval 8316

Description: The set of all subspaces of a normed complex vector space.

Hypotheses

Ref	Expression
sspval.g	|- G = (+v` U)
sspval.s	|- S = (.s` U)
sspval.n	|- N = (norm` U)
sspval.h	|- H = (SubSp` U)

Assertion

Ref	Expression
sspval	|- (U e. NrmCVec -> H = {w e. NrmCVec | ((+v` w) (_ G /\ (.s` w) (_ S /\ (norm` w) (_ N)})

Distinct variable groups:   w,G   w,N   w,S   w,U

Proof of Theorem sspval

Step	Hyp	Ref	Expression
1		fveq2 3709	. . . . . . 7 |- (u = U -> (+v` u) = (+v` U))
2		sspval.g	. . . . . . 7 |- G = (+v` U)
3	1, 2	syl6eqr 1517	. . . . . 6 |- (u = U -> (+v` u) = G)
4	3	sseq2d 2079	. . . . 5 |- (u = U -> ((+v` w) (_ (+v` u) <-> (+v` w) (_ G))
5		fveq2 3709	. . . . . . 7 |- (u = U -> (.s` u) = (.s` U))
6		sspval.s	. . . . . . 7 |- S = (.s` U)
7	5, 6	syl6eqr 1517	. . . . . 6 |- (u = U -> (.s` u) = S)
8	7	sseq2d 2079	. . . . 5 |- (u = U -> ((.s` w) (_ (.s` u) <-> (.s` w) (_ S))
9		fveq2 3709	. . . . . . 7 |- (u = U -> (norm` u) = (norm` U))
10		sspval.n	. . . . . . 7 |- N = (norm` U)
11	9, 10	syl6eqr 1517	. . . . . 6 |- (u = U -> (norm` u) = N)
12	11	sseq2d 2079	. . . . 5 |- (u = U -> ((norm` w) (_ (norm` u) <-> (norm` w) (_ N))
13	4, 8, 12	3anbi123d 890	. . . 4 |- (u = U -> (((+v` w) (_ (+v` u) /\ (.s` w) (_ (.s` u) /\ (norm` w) (_ (norm` u)) <-> ((+v` w) (_ G /\ (.s` w) (_ S /\ (norm` w) (_ N)))
14	13	rabbisdv 1798	. . 3 |- (u = U -> {w e. NrmCVec | ((+v` w) (_ (+v` u) /\ (.s` w) (_ (.s` u) /\ (norm` w) (_ (norm` u))} = {w e. NrmCVec | ((+v` w) (_ G /\ (.s` w) (_ S /\ (norm` w) (_ N)})
15		df-ssp 8315	. . 3 |- SubSp = {<.u, s>. | (u e. NrmCVec /\ s = {w e. NrmCVec | ((+v` w) (_ (+v` u) /\ (.s` w) (_ (.s` u) /\ (norm` w) (_ (norm` u))})}
16		fvex 3717	. . . . . . . 8 |- (+v` U) e. V
17	2, 16	eqeltr 1536	. . . . . . 7 |- G e. V
18	17	pwex 2735	. . . . . 6 |- P~G e. V
19		fvex 3717	. . . . . . . 8 |- (.s` U) e. V
20	6, 19	eqeltr 1536	. . . . . . 7 |- S e. V
21	20	pwex 2735	. . . . . 6 |- P~S e. V
22	18, 21	xpex 3250	. . . . 5 |- (P~G X. P~S) e. V
23		fvex 3717	. . . . . . 7 |- (norm` U) e. V
24	10, 23	eqeltr 1536	. . . . . 6 |- N e. V
25	24	pwex 2735	. . . . 5 |- P~N e. V
26	22, 25	xpex 3250	. . . 4 |- ((P~G X. P~S) X. P~N) e. V
27		eqid 1468	. . . . . . . . 9 |- (1st` u) = (1st` u)
28		eqid 1468	. . . . . . . . . . 11 |- (norm` u) = (norm` u)
29	28	nmfval 8164	. . . . . . . . . 10 |- (norm` u) = (2nd` u)
30	29	eqcomi 1471	. . . . . . . . 9 |- (2nd` u) = (norm` u)
31	27, 30	nvop2 8165	. . . . . . . 8 |- (u e. NrmCVec -> u = <.(1st` u), (2nd` u)>.)
32	31	adantr 389	. . . . . . 7 |- ((u e. NrmCVec /\ (((+v` u) e. P~G /\ (.s` u) e. P~S) /\ (norm` u) e. P~N)) -> u = <.(1st` u), (2nd` u)>.)
33		eqid 1468	. . . . . . . . . . . . 13 |- (+v` u) = (+v` u)
34	33	vafval 8160	. . . . . . . . . . . 12 |- (+v` u) = (1st` (1st` u))
35	34	eqcomi 1471	. . . . . . . . . . 11 |- (1st` (1st` u)) = (+v` u)
36		eqid 1468	. . . . . . . . . . . . 13 |- (.s` u) = (.s` u)
37	36	smfval 8162	. . . . . . . . . . . 12 |- (.s` u) = (2nd` (1st` u))
38	37	eqcomi 1471	. . . . . . . . . . 11 |- (2nd` (1st` u)) = (.s` u)
39	27, 35, 38	nvvop 8166	. . . . . . . . . 10 |- (u e. NrmCVec -> (1st` u) = <.(1st` (1st` u)), (2nd` (1st` u))>.)
40	39	adantr 389	. . . . . . . . 9 |- ((u e. NrmCVec /\ (((+v` u) e. P~G /\ (.s` u) e. P~S) /\ (norm` u) e. P~N)) -> (1st` u) = <.(1st` (1st` u)), (2nd` (1st` u))>.)
41	34	eleq1i 1529	. . . . . . . . . . . . 13 |- ((+v` u) e. P~G <-> (1st` (1st` u)) e. P~G)
42	41	biimp 151	. . . . . . . . . . . 12 |- ((+v` u) e. P~G -> (1st` (1st` u)) e. P~G)
43	42	ad2antrr 404	. . . . . . . . . . 11 |- ((((+v` u) e. P~G /\ (.s` u) e. P~S) /\ (norm` u) e. P~N) -> (1st` (1st` u)) e. P~G)
44	43	adantl 388	. . . . . . . . . 10 |- ((u e. NrmCVec /\ (((+v` u) e. P~G /\ (.s` u) e. P~S) /\ (norm` u) e. P~N)) -> (1st` (1st` u)) e. P~G)
45	37	eleq1i 1529	. . . . . . . . . . . . 13 |- ((.s` u) e. P~S <-> (2nd` (1st` u)) e. P~S)
46	45	biimp 151	. . . . . . . . . . . 12 |- ((.s` u) e. P~S -> (2nd` (1st` u)) e. P~S)
47	46	ad2antlr 405	. . . . . . . . . . 11 |- ((((+v` u) e. P~G /\ (.s` u) e. P~S) /\ (norm` u) e. P~N) -> (2nd` (1st` u)) e. P~S)
48	47	adantl 388	. . . . . . . . . 10 |- ((u e. NrmCVec /\ (((+v` u) e. P~G /\ (.s` u) e. P~S) /\ (norm` u) e. P~N)) -> (2nd` (1st` u)) e. P~S)
49	44, 48	jca 288	. . . . . . . . 9 |- ((u e. NrmCVec /\ (((+v` u) e. P~G /\ (.s` u) e. P~S) /\ (norm` u) e. P~N)) -> ((1st` (1st` u)) e. P~G /\ (2nd` (1st` u)) e. P~S))
50	40, 49	jca 288	. . . . . . . 8 |- ((u e. NrmCVec /\ (((+v` u) e. P~G /\ (.s` u) e. P~S) /\ (norm` u) e. P~N)) -> ((1st` u) = <.(1st` (1st` u)), (2nd` (1st` u))>. /\ ((1st` (1st` u)) e. P~G /\ (2nd` (1st` u)) e. P~S)))
51	29	eleq1i 1529	. . . . . . . . . 10 |- ((norm` u) e. P~N <-> (2nd` u) e. P~N)
52	51	biimp 151	. . . . . . . . 9 |- ((norm` u) e. P~N -> (2nd` u) e. P~N)
53	52	ad2antll 407	. . . . . . . 8 |- ((u e. NrmCVec /\ (((+v` u) e. P~G /\ (.s` u) e. P~S) /\ (norm` u) e. P~N)) -> (2nd` u) e. P~N)
54	50, 53	jca 288	. . . . . . 7 |- ((u e. NrmCVec /\ (((+v` u) e. P~G /\ (.s` u) e. P~S) /\ (norm` u) e. P~N)) -> (((1st` u) = <.(1st` (1st` u)), (2nd` (1st` u))>. /\ ((1st` (1st` u)) e. P~G /\ (2nd` (1st` u)) e. P~S)) /\ (2nd` u) e. P~N))
55	32, 54	jca 288	. . . . . 6 |- ((u e. NrmCVec /\ (((+v` u) e. P~G /\ (.s` u) e. P~S) /\ (norm` u) e. P~N)) -> (u = <.(1st` u), (2nd` u)>. /\ (((1st` u) = <.(1st` (1st` u)), (2nd` (1st` u))>. /\ ((1st` (1st` u)) e. P~G /\ (2nd` (1st` u)) e. P~S)) /\ (2nd` u) e. P~N)))
56		fveq2 3709	. . . . . . . . . 10 |- (w = u -> (+v` w) = (+v` u))
57	56	sseq1d 2078	. . . . . . . . 9 |- (w = u -> ((+v` w) (_ G <-> (+v` u) (_ G))
58		fveq2 3709	. . . . . . . . . 10 |- (w = u -> (.s` w) = (.s` u))
59	58	sseq1d 2078	. . . . . . . . 9 |- (w = u -> ((.s` w) (_ S <-> (.s` u) (_ S))
60		fveq2 3709	. . . . . . . . . 10 |- (w = u -> (norm` w) = (norm` u))
61	60	sseq1d 2078	. . . . . . . . 9 |- (w = u -> ((norm` w) (_ N <-> (norm` u) (_ N))
62	57, 59, 61	3anbi123d 890	. . . . . . . 8 |- (w = u -> (((+v` w) (_ G /\ (.s` w) (_ S /\ (norm` w) (_ N) <-> ((+v` u) (_ G /\ (.s` u) (_ S /\ (norm` u) (_ N)))
63		fvex 3717	. . . . . . . . . . 11 |- (+v` u) e. V
64	63	elpw 2394	. . . . . . . . . 10 |- ((+v` u) e. P~G <-> (+v` u) (_ G)
65		fvex 3717	. . . . . . . . . . 11 |- (.s` u) e. V
66	65	elpw 2394	. . . . . . . . . 10 |- ((.s` u) e. P~S <-> (.s` u) (_ S)
67		fvex 3717	. . . . . . . . . . 11 |- (norm` u) e. V
68	67	elpw 2394	. . . . . . . . . 10 |- ((norm` u) e. P~N <-> (norm` u) (_ N)
69	64, 66, 68	3anbi123i 820	. . . . . . . . 9 |- (((+v` u) e. P~G /\ (.s` u) e. P~S /\ (norm` u) e.