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 ‘ 𝑤 ) ⊆ 𝑁 ) } )