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 ∧ ( 𝐹𝐺𝑅𝑆𝑀𝑁 ) ) ) )