This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem isssp

Description: The predicate "is a subspace." (Contributed by NM, 26-Jan-2008) (New usage is discouraged.)

Ref Expression
Hypotheses isssp.g ⊢ 𝐺 = ( +𝑣 ‘ 𝑈 )
isssp.f ⊢ 𝐹 = ( +𝑣 ‘ 𝑊 )
isssp.s ⊢ 𝑆 = ( ·𝑠OLD ‘ 𝑈 )
isssp.r ⊢ 𝑅 = ( ·𝑠OLD ‘ 𝑊 )
isssp.n ⊢ 𝑁 = ( normCV ‘ 𝑈 )
isssp.m ⊢ 𝑀 = ( normCV ‘ 𝑊 )
isssp.h ⊢ 𝐻 = ( SubSp ‘ 𝑈 )
Assertion isssp ( 𝑈 ∈ NrmCVec → ( 𝑊 ∈ 𝐻 ↔ ( 𝑊 ∈ NrmCVec ∧ ( 𝐹 ⊆ 𝐺 ∧ 𝑅 ⊆ 𝑆 ∧ 𝑀 ⊆ 𝑁 ) ) ) )

Proof

Step Hyp Ref Expression
1 isssp.g ⊢ 𝐺 = ( +𝑣 ‘ 𝑈 )
2 isssp.f ⊢ 𝐹 = ( +𝑣 ‘ 𝑊 )
3 isssp.s ⊢ 𝑆 = ( ·𝑠OLD ‘ 𝑈 )
4 isssp.r ⊢ 𝑅 = ( ·𝑠OLD ‘ 𝑊 )
5 isssp.n ⊢ 𝑁 = ( normCV ‘ 𝑈 )
6 isssp.m ⊢ 𝑀 = ( normCV ‘ 𝑊 )
7 isssp.h ⊢ 𝐻 = ( SubSp ‘ 𝑈 )
8 1 3 5 7 sspval ⊢ ( 𝑈 ∈ NrmCVec → 𝐻 = { 𝑤 ∈ NrmCVec ∣ ( ( +𝑣 ‘ 𝑤 ) ⊆ 𝐺 ∧ ( ·𝑠OLD ‘ 𝑤 ) ⊆ 𝑆 ∧ ( normCV ‘ 𝑤 ) ⊆ 𝑁 ) } )
9 8 eleq2d ⊢ ( 𝑈 ∈ NrmCVec → ( 𝑊 ∈ 𝐻 ↔ 𝑊 ∈ { 𝑤 ∈ NrmCVec ∣ ( ( +𝑣 ‘ 𝑤 ) ⊆ 𝐺 ∧ ( ·𝑠OLD ‘ 𝑤 ) ⊆ 𝑆 ∧ ( normCV ‘ 𝑤 ) ⊆ 𝑁 ) } ) )
10 fveq2 ⊢ ( 𝑤 = 𝑊 → ( +𝑣 ‘ 𝑤 ) = ( +𝑣 ‘ 𝑊 ) )
11 10 2 eqtr4di ⊢ ( 𝑤 = 𝑊 → ( +𝑣 ‘ 𝑤 ) = 𝐹 )
12 11 sseq1d ⊢ ( 𝑤 = 𝑊 → ( ( +𝑣 ‘ 𝑤 ) ⊆ 𝐺 ↔ 𝐹 ⊆ 𝐺 ) )
13 fveq2 ⊢ ( 𝑤 = 𝑊 → ( ·𝑠OLD ‘ 𝑤 ) = ( ·𝑠OLD ‘ 𝑊 ) )
14 13 4 eqtr4di ⊢ ( 𝑤 = 𝑊 → ( ·𝑠OLD ‘ 𝑤 ) = 𝑅 )
15 14 sseq1d ⊢ ( 𝑤 = 𝑊 → ( ( ·𝑠OLD ‘ 𝑤 ) ⊆ 𝑆 ↔ 𝑅 ⊆ 𝑆 ) )
16 fveq2 ⊢ ( 𝑤 = 𝑊 → ( normCV ‘ 𝑤 ) = ( normCV ‘ 𝑊 ) )
17 16 6 eqtr4di ⊢ ( 𝑤 = 𝑊 → ( normCV ‘ 𝑤 ) = 𝑀 )
18 17 sseq1d ⊢ ( 𝑤 = 𝑊 → ( ( normCV ‘ 𝑤 ) ⊆ 𝑁 ↔ 𝑀 ⊆ 𝑁 ) )
19 12 15 18 3anbi123d ⊢ ( 𝑤 = 𝑊 → ( ( ( +𝑣 ‘ 𝑤 ) ⊆ 𝐺 ∧ ( ·𝑠OLD ‘ 𝑤 ) ⊆ 𝑆 ∧ ( normCV ‘ 𝑤 ) ⊆ 𝑁 ) ↔ ( 𝐹 ⊆ 𝐺 ∧ 𝑅 ⊆ 𝑆 ∧ 𝑀 ⊆ 𝑁 ) ) )
20 19 elrab ⊢ ( 𝑊 ∈ { 𝑤 ∈ NrmCVec ∣ ( ( +𝑣 ‘ 𝑤 ) ⊆ 𝐺 ∧ ( ·𝑠OLD ‘ 𝑤 ) ⊆ 𝑆 ∧ ( normCV ‘ 𝑤 ) ⊆ 𝑁 ) } ↔ ( 𝑊 ∈ NrmCVec ∧ ( 𝐹 ⊆ 𝐺 ∧ 𝑅 ⊆ 𝑆 ∧ 𝑀 ⊆ 𝑁 ) ) )
21 9 20 bitrdi ⊢ ( 𝑈 ∈ NrmCVec → ( 𝑊 ∈ 𝐻 ↔ ( 𝑊 ∈ NrmCVec ∧ ( 𝐹 ⊆ 𝐺 ∧ 𝑅 ⊆ 𝑆 ∧ 𝑀 ⊆ 𝑁 ) ) ) )