sspval - Metamath Proof Explorer

Metamath Proof Explorer

< Previous Next >
Related theorems
GIF version

Theorem sspval 8378

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 ∈ NrmCVec → H = {w ∈ 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 3730	. . . . . . 7 ⊢ (u = U → ( +_v ‘u) = ( +_v ‘U))
2		sspval.g	. . . . . . 7 ⊢ G = ( +_v ‘U)
3	1, 2	syl6eqr 1528	. . . . . 6 ⊢ (u = U → ( +_v ‘u) = G)
4	3	sseq2d 2092	. . . . 5 ⊢ (u = U → (( +_v ‘w) ⊆ ( +_v ‘u) ↔ ( +_v ‘w) ⊆ G))
5		fveq2 3730	. . . . . . 7 ⊢ (u = U → ( ·_s ‘u) = ( ·_s ‘U))
6		sspval.s	. . . . . . 7 ⊢ S = ( ·_s ‘U)
7	5, 6	syl6eqr 1528	. . . . . 6 ⊢ (u = U → ( ·_s ‘u) = S)
8	7	sseq2d 2092	. . . . 5 ⊢ (u = U → (( ·_s ‘w) ⊆ ( ·_s ‘u) ↔ ( ·_s ‘w) ⊆ S))
9		fveq2 3730	. . . . . . 7 ⊢ (u = U → (norm ‘u) = (norm ‘U))
10		sspval.n	. . . . . . 7 ⊢ N = (norm ‘U)
11	9, 10	syl6eqr 1528	. . . . . 6 ⊢ (u = U → (norm ‘u) = N)
12	11	sseq2d 2092	. . . . 5 ⊢ (u = U → ((norm ‘w) ⊆ (norm ‘u) ↔ (norm ‘w) ⊆ N))
13	4, 8, 12	3anbi123d 895	. . . 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 1810	. . 3 ⊢ (u = U → {w ∈ NrmCVec∣(( +_v ‘w) ⊆ ( +_v ‘u) ⋀ ( ·_s ‘w) ⊆ ( ·_s ‘u) ⋀ (norm ‘w) ⊆ (norm ‘u))} = {w ∈ NrmCVec∣(( +_v ‘w) ⊆ G ⋀ ( ·_s ‘w) ⊆ S ⋀ (norm ‘w) ⊆ N)})
15		df-ssp 8377	. . 3 ⊢ SubSp = {⟨u, s⟩∣(u ∈ NrmCVec ⋀ s = {w ∈ NrmCVec∣(( +_v ‘w) ⊆ ( +_v ‘u) ⋀ ( ·_s ‘w) ⊆ ( ·_s ‘u) ⋀ (norm ‘w) ⊆ (norm ‘u))})}
16		fvex 3738	. . . . . . . 8 ⊢ ( +_v ‘U) ∈ V
17	2, 16	eqeltr 1547	. . . . . . 7 ⊢ G ∈ V
18	17	pwex 2751	. . . . . 6 ⊢ ℘G ∈ V
19		fvex 3738	. . . . . . . 8 ⊢ ( ·_s ‘U) ∈ V
20	6, 19	eqeltr 1547	. . . . . . 7 ⊢ S ∈ V
21	20	pwex 2751	. . . . . 6 ⊢ ℘S ∈ V
22	18, 21	xpex 3266	. . . . 5 ⊢ (℘G × ℘S) ∈ V
23		fvex 3738	. . . . . . 7 ⊢ (norm ‘U) ∈ V
24	10, 23	eqeltr 1547	. . . . . 6 ⊢ N ∈ V
25	24	pwex 2751	. . . . 5 ⊢ ℘N ∈ V
26	22, 25	xpex 3266	. . . 4 ⊢ ((℘G × ℘S) × ℘N) ∈ V
27		eqid 1478	. . . . . . . . 9 ⊢ (1^st ‘u) = (1^st ‘u)
28		eqid 1478	. . . . . . . . . . 11 ⊢ (norm ‘u) = (norm ‘u)
29	28	nmfval 8222	. . . . . . . . . 10 ⊢ (norm ‘u) = (2^nd ‘u)
30	29	eqcomi 1482	. . . . . . . . 9 ⊢ (2^nd ‘u) = (norm ‘u)
31	27, 30	nvop2 8223	. . . . . . . 8 ⊢ (u ∈ NrmCVec → u = ⟨(1^st ‘u), (2^nd ‘u)⟩)
32	31	adantr 391	. . . . . . 7 ⊢ ((u ∈ NrmCVec ⋀ ((( +_v ‘u) ∈ ℘G ⋀ ( ·_s ‘u) ∈ ℘S) ⋀ (norm ‘u) ∈ ℘N)) → u = ⟨(1^st ‘u), (2^nd ‘u)⟩)
33		eqid 1478	. . . . . . . . . . . . 13 ⊢ ( +_v ‘u) = ( +_v ‘u)
34	33	vafval 8218	. . . . . . . . . . . 12 ⊢ ( +_v ‘u) = (1^st ‘(1^st ‘u))
35	34	eqcomi 1482	. . . . . . . . . . 11 ⊢ (1^st ‘(1^st ‘u)) = ( +_v ‘u)
36		eqid 1478	. . . . . . . . . . . . 13 ⊢ ( ·_s ‘u) = ( ·_s ‘u)
37	36	smfval 8220	. . . . . . . . . . . 12 ⊢ ( ·_s ‘u) = (2^nd ‘(1^st ‘u))
38	37	eqcomi 1482	. . . . . . . . . . 11 ⊢ (2^nd ‘(1^st ‘u)) = ( ·_s ‘u)
39	27, 35, 38	nvvop 8224	. . . . . . . . . 10 ⊢ (u ∈ NrmCVec → (1^st ‘u) = ⟨(1^st ‘(1^st ‘u)), (2^nd ‘(1^st ‘u))⟩)
40	39	adantr 391	. . . . . . . . 9 ⊢ ((u ∈ NrmCVec ⋀ ((( +_v ‘u) ∈ ℘G ⋀ ( ·_s ‘u) ∈ ℘S) ⋀ (norm ‘u) ∈ ℘N)) → (1^st ‘u) = ⟨(1^st ‘(1^st ‘u)), (2^nd ‘(1^st ‘u))⟩)
41	34	eleq1i 1540	. . . . . . . . . . . . 13 ⊢ (( +_v ‘u) ∈ ℘G ↔ (1^st ‘(1^st ‘u)) ∈ ℘G)
42	41	biimp 151	. . . . . . . . . . . 12 ⊢ (( +_v ‘u) ∈ ℘G → (1^st ‘(1^st ‘u)) ∈ ℘G)
43	42	ad2antrr 406	. . . . . . . . . . 11 ⊢ (((( +_v ‘u) ∈ ℘G ⋀ ( ·_s ‘u) ∈ ℘S) ⋀ (norm ‘u) ∈ ℘N) → (1^st ‘(1^st ‘u)) ∈ ℘G)
44	43	adantl 390	. . . . . . . . . 10 ⊢ ((u ∈ NrmCVec ⋀ ((( +_v ‘u) ∈ ℘G ⋀ ( ·_s ‘u) ∈ ℘S) ⋀ (norm ‘u) ∈ ℘N)) → (1^st ‘(1^st ‘u)) ∈ ℘G)
45	37	eleq1i 1540	. . . . . . . . . . . . 13 ⊢ (( ·_s ‘u) ∈ ℘S ↔ (2^nd ‘(1^st ‘u)) ∈ ℘S)
46	45	biimp 151	. . . . . . . . . . . 12 ⊢ (( ·_s ‘u) ∈ ℘S → (2^nd ‘(1^st ‘u)) ∈ ℘S)
47	46	ad2antlr 407	. . . . . . . . . . 11 ⊢ (((( +_v ‘u) ∈ ℘G ⋀ ( ·_s ‘u) ∈ ℘S) ⋀ (norm ‘u) ∈ ℘N) → (2^nd ‘(1^st ‘u)) ∈ ℘S)
48	47	adantl 390	. . . . . . . . . 10 ⊢ ((u ∈ NrmCVec ⋀ ((( +_v ‘u) ∈ ℘G ⋀ ( ·_s ‘u) ∈ ℘S) ⋀ (norm ‘u) ∈ ℘N)) → (2^nd ‘(1^st ‘u)) ∈ ℘S)
49	44, 48	jca 288	. . . . . . . . 9 ⊢ ((u ∈ NrmCVec ⋀ ((( +_v ‘u) ∈ ℘G ⋀ ( ·_s ‘u) ∈ ℘S) ⋀ (norm ‘u) ∈ ℘N)) → ((1^st ‘(1^st ‘u)) ∈ ℘G ⋀ (2^nd ‘(1^st ‘u)) ∈ ℘S))
50	40, 49	jca 288	. . . . . . . 8 ⊢ ((u ∈ NrmCVec ⋀ ((( +_v ‘u) ∈ ℘G ⋀ ( ·_s ‘u) ∈ ℘S) ⋀ (norm ‘u) ∈ ℘N)) → ((1^st ‘u) = ⟨(1^st ‘(1^st ‘u)), (2^nd ‘(1^st ‘u))⟩ ⋀ ((1^st ‘(1^st ‘u)) ∈ ℘G ⋀ (2^nd ‘(1^st ‘u)) ∈ ℘S)))
51	29	eleq1i 1540	. . . . . . . . . 10 ⊢ ((norm ‘u) ∈ ℘N ↔ (2^nd ‘u) ∈ ℘N)
52	51	biimp 151	. . . . . . . . 9 ⊢ ((norm ‘u) ∈ ℘N → (2^nd ‘u) ∈ ℘N)
53	52	ad2antll 409	. . . . . . . 8 ⊢ ((u ∈ NrmCVec ⋀ ((( +_v ‘u) ∈ ℘G ⋀ ( ·_s ‘u) ∈ ℘S) ⋀ (norm ‘u) ∈ ℘N)) → (2^nd ‘u) ∈ ℘N)
54	50, 53	jca 288	. . . . . . 7 ⊢ ((u ∈ NrmCVec ⋀ ((( +_v ‘u) ∈ ℘G ⋀ ( ·_s ‘u) ∈ ℘S) ⋀ (norm ‘u) ∈ ℘N)) → (((1^st ‘u) = ⟨(1^st ‘(1^st ‘u)), (2^nd ‘(1^st ‘u))⟩ ⋀ ((1^st ‘(1^st ‘u)) ∈ ℘G ⋀ (2^nd ‘(1^st ‘u)) ∈ ℘S)) ⋀ (2^nd ‘u) ∈ ℘N))
55	32, 54	jca 288	. . . . . 6 ⊢ ((u ∈ NrmCVec ⋀ ((( +_v ‘u) ∈ ℘G ⋀ ( ·_s ‘u) ∈ ℘S) ⋀ (norm ‘u) ∈ ℘N)) → (u = ⟨(1^st ‘u), (2^nd ‘u)⟩ ⋀ (((1^st ‘u) = ⟨(1^st ‘(1^st ‘u)), (2^nd ‘(1^st ‘u))⟩ ⋀ ((1^st ‘(1^st ‘u)) ∈ ℘G ⋀ (2^nd ‘(1^st ‘u)) ∈ ℘S)) ⋀ (2^nd ‘u) ∈ ℘N)))
56		fveq2 3730	. . . . . . . . . 10 ⊢ (w = u → ( +_v ‘w) = ( +_v ‘u))
57	56	sseq1d 2091	. . . . . . . . 9 ⊢ (w = u → (( +_v ‘w) ⊆ G ↔ ( +_v ‘u) ⊆ G))
58		fveq2 3730	. . . . . . . . . 10 ⊢ (w = u → ( ·_s ‘w) = ( ·_s ‘u))
59	58	sseq1d 2091	. . . . . . . . 9 ⊢ (w = u → (( ·_s ‘w) ⊆ S ↔ ( ·_s ‘u) ⊆ S))
60		fveq2 3730	. . . . . . . . . 10 ⊢ (w = u → (norm ‘w) = (norm ‘u))
61	60	sseq1d 2091	. . . . . . . . 9 ⊢ (w = u → ((norm ‘w) ⊆ N ↔ (norm ‘u) ⊆ N))
62	57, 59, 61	3anbi123d 895	. . . . . . . 8 ⊢ (w = u → ((( +_v ‘w) ⊆ G ⋀ ( ·_s ‘w) ⊆ S ⋀ (norm ‘w) ⊆ N) ↔ (( +_v ‘u) ⊆ G ⋀ ( ·_s ‘u) ⊆ S ⋀ (norm ‘u) ⊆ N)))
63		fvex 3738	. . . . . . . . . . 11 ⊢ ( +_v ‘u) ∈ V
64	63	elpw 2408	. . . . . . . . . 10 ⊢ (( +_v ‘u) ∈ ℘G ↔ ( +_v ‘u) ⊆ G)
65		fvex 3738	. . . . . . . . . . 11 ⊢ ( ·_s ‘u) ∈ V
66	65	elpw 2408	. . . . . . . . . 10 ⊢ (( ·_s ‘u) ∈ ℘S ↔ ( ·_s ‘u) ⊆ S)
67		fvex 3738	. . . . . . . . . . 11 ⊢ (norm ‘u) ∈ V
68	67	elpw 2408	. . . . . . . . . 10 ⊢ ((norm ‘u) ∈ ℘N ↔ (norm ‘u) ⊆ N)
69	64, 66, 68	3anbi123i 824	. . . . . . . . 9 ⊢ ((( +_v ‘u) ∈ ℘G ⋀ ( ·_s ‘u) ∈ ℘S ⋀ (norm ‘u) ∈ ℘N) ↔ (( +_v ‘u) ⊆ G ⋀ ( ·_s ‘u) ⊆ S ⋀ (norm ‘u) ⊆ N))
70		df-3an 779	. . . . . . . . 9 ⊢ ((( +_v ‘u) ∈ ℘G ⋀ ( ·_s ‘u) ∈ ℘S ⋀ (norm ‘u) ∈ ℘N) ↔ ((( +_v ‘u) ∈ ℘G ⋀ ( ·_s ‘u) ∈ ℘S) ⋀ (norm ‘u) ∈ ℘N))
71	69, 70	bitr3 175	. . . . . . . 8 ⊢ ((( +_v ‘u) ⊆ G ⋀ ( ·_s ‘u) ⊆ S ⋀ (norm ‘u) ⊆ N) ↔ ((( +_v ‘u) ∈ ℘G ⋀ ( ·_s ‘u) ∈ ℘S) ⋀ (norm ‘u) ∈ ℘N))
72	62, 71	syl6bb 538	. . . . . . 7 ⊢ (w = u → ((( +_v ‘w) ⊆ G ⋀ ( ·_s ‘w) ⊆ S ⋀ (norm ‘w) ⊆ N) ↔ ((( +_v ‘u) ∈ ℘G ⋀ ( ·_s ‘u) ∈ ℘S) ⋀ (norm ‘u) ∈ ℘N)))
73	72	elrab 1908	. . . . . 6 ⊢ (u ∈ {w ∈ NrmCVec∣(( +_v ‘w) ⊆ G ⋀ ( ·_s ‘w) ⊆ S ⋀ (norm ‘w) ⊆ N)} ↔ (u ∈ NrmCVec ⋀ ((( +_v ‘u) ∈ ℘G ⋀ ( ·_s ‘u) ∈ ℘S) ⋀ (norm ‘u) ∈ ℘N)))
74		elxp6 4108	. . . . . . 7 ⊢ (u ∈ ((℘G × ℘S) × ℘N) ↔ (u = ⟨(1^st ‘u), (2^nd ‘u)⟩ ⋀ ((1^st ‘u) ∈ (℘G × ℘S) ⋀ (2^nd ‘u) ∈ ℘N)))
75		elxp6 4108	. . . . . . . . 9 ⊢ ((1^st ‘u) ∈ (℘G × ℘S) ↔ ((1^st ‘u) = ⟨(1^st ‘(1^st ‘u)), (2^nd ‘(1^st ‘u))⟩ ⋀ ((1^st ‘(1^st ‘u)) ∈ ℘G ⋀ (2^nd ‘(1^st ‘u)) ∈ ℘S)))
76	75	anbi1i 483	. . . . . . . 8 ⊢ (((1^st ‘u) ∈ (℘G × ℘S) ⋀ (2^nd ‘u) ∈ ℘N) ↔ (((1^st ‘u) = ⟨(1^st ‘(1^st ‘u)), (2^nd ‘(1^st ‘u))⟩ ⋀ ((1^st ‘(1^st ‘u)) ∈ ℘G ⋀ (2^nd ‘(1^st ‘u)) ∈ ℘S)) ⋀ (2^nd ‘u) ∈ ℘N))
77	76	anbi2i 482	. . . . . . 7 ⊢ ((u = ⟨(1^st ‘u), (2^nd ‘u)⟩ ⋀ ((1^st ‘u) ∈ (℘G × ℘S) ⋀ (2^nd ‘u) ∈ ℘N)) ↔ (u = ⟨(1^st ‘u), (2^nd ‘u)⟩ ⋀ (((1^st ‘u) = ⟨(1^st ‘(1^st ‘u)), (2^nd ‘(1^st ‘u))⟩ ⋀ ((1^st ‘(1^st ‘u)) ∈ ℘G ⋀ (2^nd ‘(1^st ‘u)) ∈ ℘S)) ⋀ (2^nd ‘u) ∈ ℘N)))
78	74, 77	bitr 173	. . . . . 6 ⊢ (u ∈ ((℘G × ℘S) × ℘N) ↔ (u = ⟨(1^st ‘u), (2^nd ‘u)⟩ ⋀ (((1^st ‘u) = ⟨(1^st ‘(1^st ‘u)), (2^nd ‘(1^st ‘u))⟩ ⋀ ((1^st ‘(1^st ‘u)) ∈ ℘G ⋀ (2^nd ‘(1^st ‘u)) ∈ ℘S)) ⋀ (2^nd ‘u) ∈ ℘N)))
79	55, 73, 78	3imtr4 219	. . . . 5 ⊢ (u ∈ {w ∈ NrmCVec∣(( +_v ‘w) ⊆ G ⋀ ( ·_s ‘w) ⊆ S ⋀ (norm ‘w) ⊆ N)} → u ∈ ((℘G × ℘S) × ℘N))
80	79	ssriv 2072	. . . 4 ⊢ {w ∈ NrmCVec∣(( +_v ‘w) ⊆ G ⋀ ( ·_s ‘w) ⊆ S ⋀ (norm ‘w) ⊆ N)} ⊆ ((℘G × ℘S) × ℘N)
81	26, 80	ssexi 2725	. . 3 ⊢ {w ∈ NrmCVec∣(( +_v ‘w) ⊆ G ⋀ ( ·_s ‘w) ⊆ S ⋀ (norm ‘w) ⊆ N)} ∈ V
82	14, 15, 81	fvopab4 3786	. 2 ⊢ (U ∈ NrmCVec → (SubSp ‘U) = {w ∈ NrmCVec∣(( +_v ‘w) ⊆ G ⋀ ( ·_s ‘w) ⊆ S ⋀ (norm ‘w) ⊆ N)})
83		sspval.h	. 2 ⊢ H = (SubSp ‘U)
84	82, 83	syl5eq 1522	1 ⊢ (U ∈ NrmCVec → H = {w ∈ NrmCVec∣(( +_v ‘w) ⊆ G ⋀ ( ·_s ‘w) ⊆ S ⋀ (norm ‘w) ⊆ N)})

Colors of variables: wff set class

Syntax hints: → wi 3 ⋀ wa 223 ⋀ w3a 777 = wceq 958 ∈ wcel 960 {crab 1651 Vcvv 1814 ⊆ wss 2050 ℘cpw 2405 ⟨cop 2415 × cxp 3174 ‘cfv 3188 1^st c1st 4083 2^nd c2nd 4084 NrmCVeccnv 8199 +_v cpv 8200 ·_s cns 8202 normcnm 8205 SubSpcss 8376

This theorem is referenced by: isssp 8379

This theorem was proved from axioms: ax-1 4 ax-2 5 ax-3 6 ax-mp 7 ax-7 964 ax-gen 965 ax-8 966 ax-9 967 ax-10 968 ax-11 969 ax-12 970 ax-13 971 ax-14 972 ax-17 973 ax-4 975 ax-5o 977 ax-6o 980 ax-9o 1125 ax-10o 1142 ax-16 1212 ax-11o 1220 ax-ext 1462 ax-sep 2708 ax-nul 2715 ax-pow 2748 ax-pr 2785 ax-un 2872

This theorem depends on definitions: df-bi 147 df-or 224 df-an 225 df-3an 779 df-ex 983 df-sb 1174 df-eu 1384 df-mo 1385 df-clab 1467 df-cleq 1472 df-clel 1475 df-ne 1590 df-ral 1652 df-rex 1653 df-rab 1655 df-v 1815 df-dif 2052 df-un 2053 df-in 2054 df-ss 2056 df-nul 2284 df-pw 2406 df-sn 2416 df-pr 2417 df-op 2420 df-uni 2508 df-br 2625 df-opab 2672 df-id 2841 df-xp 3190 df-rel 3191 df-cnv 3192 df-co 3193 df-dm 3194 df-rn 3195 df-res 3196 df-ima 3197 df-fun 3198 df-fn 3199 df-f 3200 df-fo 3202 df-fv 3204 df-oprab 3972 df-1st 4085 df-2nd 4086 df-nv 8207 df-va 8210 df-sm 8212 df-nm 8215 df-ssp 8377