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