Metamath Proof Explorer


Theorem sspval

Description: The set of all subspaces of a normed complex vector space. (Contributed by NM, 26-Jan-2008) (Revised by Mario Carneiro, 16-Nov-2013) (New usage is discouraged.)

Ref Expression
Hypotheses sspval.g 𝐺 = ( +𝑣𝑈 )
sspval.s 𝑆 = ( ·𝑠OLD𝑈 )
sspval.n 𝑁 = ( normCV𝑈 )
sspval.h 𝐻 = ( SubSp ‘ 𝑈 )
Assertion sspval ( 𝑈 ∈ NrmCVec → 𝐻 = { 𝑤 ∈ NrmCVec ∣ ( ( +𝑣𝑤 ) ⊆ 𝐺 ∧ ( ·𝑠OLD𝑤 ) ⊆ 𝑆 ∧ ( normCV𝑤 ) ⊆ 𝑁 ) } )

Proof

Step Hyp Ref Expression
1 sspval.g 𝐺 = ( +𝑣𝑈 )
2 sspval.s 𝑆 = ( ·𝑠OLD𝑈 )
3 sspval.n 𝑁 = ( normCV𝑈 )
4 sspval.h 𝐻 = ( SubSp ‘ 𝑈 )
5 fveq2 ( 𝑢 = 𝑈 → ( +𝑣𝑢 ) = ( +𝑣𝑈 ) )
6 5 1 eqtr4di ( 𝑢 = 𝑈 → ( +𝑣𝑢 ) = 𝐺 )
7 6 sseq2d ( 𝑢 = 𝑈 → ( ( +𝑣𝑤 ) ⊆ ( +𝑣𝑢 ) ↔ ( +𝑣𝑤 ) ⊆ 𝐺 ) )
8 fveq2 ( 𝑢 = 𝑈 → ( ·𝑠OLD𝑢 ) = ( ·𝑠OLD𝑈 ) )
9 8 2 eqtr4di ( 𝑢 = 𝑈 → ( ·𝑠OLD𝑢 ) = 𝑆 )
10 9 sseq2d ( 𝑢 = 𝑈 → ( ( ·𝑠OLD𝑤 ) ⊆ ( ·𝑠OLD𝑢 ) ↔ ( ·𝑠OLD𝑤 ) ⊆ 𝑆 ) )
11 fveq2 ( 𝑢 = 𝑈 → ( normCV𝑢 ) = ( normCV𝑈 ) )
12 11 3 eqtr4di ( 𝑢 = 𝑈 → ( normCV𝑢 ) = 𝑁 )
13 12 sseq2d ( 𝑢 = 𝑈 → ( ( normCV𝑤 ) ⊆ ( normCV𝑢 ) ↔ ( normCV𝑤 ) ⊆ 𝑁 ) )
14 7 10 13 3anbi123d ( 𝑢 = 𝑈 → ( ( ( +𝑣𝑤 ) ⊆ ( +𝑣𝑢 ) ∧ ( ·𝑠OLD𝑤 ) ⊆ ( ·𝑠OLD𝑢 ) ∧ ( normCV𝑤 ) ⊆ ( normCV𝑢 ) ) ↔ ( ( +𝑣𝑤 ) ⊆ 𝐺 ∧ ( ·𝑠OLD𝑤 ) ⊆ 𝑆 ∧ ( normCV𝑤 ) ⊆ 𝑁 ) ) )
15 14 rabbidv ( 𝑢 = 𝑈 → { 𝑤 ∈ NrmCVec ∣ ( ( +𝑣𝑤 ) ⊆ ( +𝑣𝑢 ) ∧ ( ·𝑠OLD𝑤 ) ⊆ ( ·𝑠OLD𝑢 ) ∧ ( normCV𝑤 ) ⊆ ( normCV𝑢 ) ) } = { 𝑤 ∈ NrmCVec ∣ ( ( +𝑣𝑤 ) ⊆ 𝐺 ∧ ( ·𝑠OLD𝑤 ) ⊆ 𝑆 ∧ ( normCV𝑤 ) ⊆ 𝑁 ) } )
16 df-ssp SubSp = ( 𝑢 ∈ NrmCVec ↦ { 𝑤 ∈ NrmCVec ∣ ( ( +𝑣𝑤 ) ⊆ ( +𝑣𝑢 ) ∧ ( ·𝑠OLD𝑤 ) ⊆ ( ·𝑠OLD𝑢 ) ∧ ( normCV𝑤 ) ⊆ ( normCV𝑢 ) ) } )
17 1 fvexi 𝐺 ∈ V
18 17 pwex 𝒫 𝐺 ∈ V
19 2 fvexi 𝑆 ∈ V
20 19 pwex 𝒫 𝑆 ∈ V
21 18 20 xpex ( 𝒫 𝐺 × 𝒫 𝑆 ) ∈ V
22 3 fvexi 𝑁 ∈ V
23 22 pwex 𝒫 𝑁 ∈ V
24 21 23 xpex ( ( 𝒫 𝐺 × 𝒫 𝑆 ) × 𝒫 𝑁 ) ∈ V
25 rabss ( { 𝑤 ∈ NrmCVec ∣ ( ( +𝑣𝑤 ) ⊆ 𝐺 ∧ ( ·𝑠OLD𝑤 ) ⊆ 𝑆 ∧ ( normCV𝑤 ) ⊆ 𝑁 ) } ⊆ ( ( 𝒫 𝐺 × 𝒫 𝑆 ) × 𝒫 𝑁 ) ↔ ∀ 𝑤 ∈ NrmCVec ( ( ( +𝑣𝑤 ) ⊆ 𝐺 ∧ ( ·𝑠OLD𝑤 ) ⊆ 𝑆 ∧ ( normCV𝑤 ) ⊆ 𝑁 ) → 𝑤 ∈ ( ( 𝒫 𝐺 × 𝒫 𝑆 ) × 𝒫 𝑁 ) ) )
26 fvex ( +𝑣𝑤 ) ∈ V
27 26 elpw ( ( +𝑣𝑤 ) ∈ 𝒫 𝐺 ↔ ( +𝑣𝑤 ) ⊆ 𝐺 )
28 fvex ( ·𝑠OLD𝑤 ) ∈ V
29 28 elpw ( ( ·𝑠OLD𝑤 ) ∈ 𝒫 𝑆 ↔ ( ·𝑠OLD𝑤 ) ⊆ 𝑆 )
30 opelxpi ( ( ( +𝑣𝑤 ) ∈ 𝒫 𝐺 ∧ ( ·𝑠OLD𝑤 ) ∈ 𝒫 𝑆 ) → ⟨ ( +𝑣𝑤 ) , ( ·𝑠OLD𝑤 ) ⟩ ∈ ( 𝒫 𝐺 × 𝒫 𝑆 ) )
31 27 29 30 syl2anbr ( ( ( +𝑣𝑤 ) ⊆ 𝐺 ∧ ( ·𝑠OLD𝑤 ) ⊆ 𝑆 ) → ⟨ ( +𝑣𝑤 ) , ( ·𝑠OLD𝑤 ) ⟩ ∈ ( 𝒫 𝐺 × 𝒫 𝑆 ) )
32 fvex ( normCV𝑤 ) ∈ V
33 32 elpw ( ( normCV𝑤 ) ∈ 𝒫 𝑁 ↔ ( normCV𝑤 ) ⊆ 𝑁 )
34 33 biimpri ( ( normCV𝑤 ) ⊆ 𝑁 → ( normCV𝑤 ) ∈ 𝒫 𝑁 )
35 opelxpi ( ( ⟨ ( +𝑣𝑤 ) , ( ·𝑠OLD𝑤 ) ⟩ ∈ ( 𝒫 𝐺 × 𝒫 𝑆 ) ∧ ( normCV𝑤 ) ∈ 𝒫 𝑁 ) → ⟨ ⟨ ( +𝑣𝑤 ) , ( ·𝑠OLD𝑤 ) ⟩ , ( normCV𝑤 ) ⟩ ∈ ( ( 𝒫 𝐺 × 𝒫 𝑆 ) × 𝒫 𝑁 ) )
36 31 34 35 syl2an ( ( ( ( +𝑣𝑤 ) ⊆ 𝐺 ∧ ( ·𝑠OLD𝑤 ) ⊆ 𝑆 ) ∧ ( normCV𝑤 ) ⊆ 𝑁 ) → ⟨ ⟨ ( +𝑣𝑤 ) , ( ·𝑠OLD𝑤 ) ⟩ , ( normCV𝑤 ) ⟩ ∈ ( ( 𝒫 𝐺 × 𝒫 𝑆 ) × 𝒫 𝑁 ) )
37 36 3impa ( ( ( +𝑣𝑤 ) ⊆ 𝐺 ∧ ( ·𝑠OLD𝑤 ) ⊆ 𝑆 ∧ ( normCV𝑤 ) ⊆ 𝑁 ) → ⟨ ⟨ ( +𝑣𝑤 ) , ( ·𝑠OLD𝑤 ) ⟩ , ( normCV𝑤 ) ⟩ ∈ ( ( 𝒫 𝐺 × 𝒫 𝑆 ) × 𝒫 𝑁 ) )
38 eqid ( +𝑣𝑤 ) = ( +𝑣𝑤 )
39 eqid ( ·𝑠OLD𝑤 ) = ( ·𝑠OLD𝑤 )
40 eqid ( normCV𝑤 ) = ( normCV𝑤 )
41 38 39 40 nvop ( 𝑤 ∈ NrmCVec → 𝑤 = ⟨ ⟨ ( +𝑣𝑤 ) , ( ·𝑠OLD𝑤 ) ⟩ , ( normCV𝑤 ) ⟩ )
42 41 eleq1d ( 𝑤 ∈ NrmCVec → ( 𝑤 ∈ ( ( 𝒫 𝐺 × 𝒫 𝑆 ) × 𝒫 𝑁 ) ↔ ⟨ ⟨ ( +𝑣𝑤 ) , ( ·𝑠OLD𝑤 ) ⟩ , ( normCV𝑤 ) ⟩ ∈ ( ( 𝒫 𝐺 × 𝒫 𝑆 ) × 𝒫 𝑁 ) ) )
43 37 42 syl5ibr ( 𝑤 ∈ NrmCVec → ( ( ( +𝑣𝑤 ) ⊆ 𝐺 ∧ ( ·𝑠OLD𝑤 ) ⊆ 𝑆 ∧ ( normCV𝑤 ) ⊆ 𝑁 ) → 𝑤 ∈ ( ( 𝒫 𝐺 × 𝒫 𝑆 ) × 𝒫 𝑁 ) ) )
44 25 43 mprgbir { 𝑤 ∈ NrmCVec ∣ ( ( +𝑣𝑤 ) ⊆ 𝐺 ∧ ( ·𝑠OLD𝑤 ) ⊆ 𝑆 ∧ ( normCV𝑤 ) ⊆ 𝑁 ) } ⊆ ( ( 𝒫 𝐺 × 𝒫 𝑆 ) × 𝒫 𝑁 )
45 24 44 ssexi { 𝑤 ∈ NrmCVec ∣ ( ( +𝑣𝑤 ) ⊆ 𝐺 ∧ ( ·𝑠OLD𝑤 ) ⊆ 𝑆 ∧ ( normCV𝑤 ) ⊆ 𝑁 ) } ∈ V
46 15 16 45 fvmpt ( 𝑈 ∈ NrmCVec → ( SubSp ‘ 𝑈 ) = { 𝑤 ∈ NrmCVec ∣ ( ( +𝑣𝑤 ) ⊆ 𝐺 ∧ ( ·𝑠OLD𝑤 ) ⊆ 𝑆 ∧ ( normCV𝑤 ) ⊆ 𝑁 ) } )
47 4 46 syl5eq ( 𝑈 ∈ NrmCVec → 𝐻 = { 𝑤 ∈ NrmCVec ∣ ( ( +𝑣𝑤 ) ⊆ 𝐺 ∧ ( ·𝑠OLD𝑤 ) ⊆ 𝑆 ∧ ( normCV𝑤 ) ⊆ 𝑁 ) } )