Theorem hhshsslem2

Description: Lemma for hhsssh . (Contributed by NM, 6-Apr-2008) (New usage is discouraged.)

	Ref	Expression
Hypotheses	hhsst.1	⊢ 𝑈 = ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩
	hhsst.2	⊢ 𝑊 = ⟨ ⟨ ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) , ( ·ℎ ↾ ( ℂ × 𝐻 ) ) ⟩ , ( normℎ ↾ 𝐻 ) ⟩
	hhssp3.3	⊢ 𝑊 ∈ ( SubSp ‘ 𝑈 )
	hhssp3.4	⊢ 𝐻 ⊆ ℋ
Assertion	hhshsslem2	⊢ 𝐻 ∈ Sℋ

Proof

Step	Hyp	Ref	Expression
1		hhsst.1	⊢ 𝑈 = ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩
2		hhsst.2	⊢ 𝑊 = ⟨ ⟨ ( +ℎ ↾ ( 𝐻 × 𝐻 ) ) , ( ·ℎ ↾ ( ℂ × 𝐻 ) ) ⟩ , ( normℎ ↾ 𝐻 ) ⟩
3		hhssp3.3	⊢ 𝑊 ∈ ( SubSp ‘ 𝑈 )
4		hhssp3.4	⊢ 𝐻 ⊆ ℋ
5	1	hhnv	⊢ 𝑈 ∈ NrmCVec
6	1	hh0v	⊢ 0ℎ = ( 0vec ‘ 𝑈 )
7		eqid	⊢ ( 0vec ‘ 𝑊 ) = ( 0vec ‘ 𝑊 )
8		eqid	⊢ ( SubSp ‘ 𝑈 ) = ( SubSp ‘ 𝑈 )
9	6 7 8	sspz	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ ( SubSp ‘ 𝑈 ) ) → ( 0vec ‘ 𝑊 ) = 0ℎ )
10	5 3 9	mp2an	⊢ ( 0vec ‘ 𝑊 ) = 0ℎ
11	8	sspnv	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ ( SubSp ‘ 𝑈 ) ) → 𝑊 ∈ NrmCVec )
12	5 3 11	mp2an	⊢ 𝑊 ∈ NrmCVec
13		eqid	⊢ ( BaseSet ‘ 𝑊 ) = ( BaseSet ‘ 𝑊 )
14	13 7	nvzcl	⊢ ( 𝑊 ∈ NrmCVec → ( 0vec ‘ 𝑊 ) ∈ ( BaseSet ‘ 𝑊 ) )
15	12 14	ax-mp	⊢ ( 0vec ‘ 𝑊 ) ∈ ( BaseSet ‘ 𝑊 )
16	1 2 3 4	hhshsslem1	⊢ 𝐻 = ( BaseSet ‘ 𝑊 )
17	15 16	eleqtrri	⊢ ( 0vec ‘ 𝑊 ) ∈ 𝐻
18	10 17	eqeltrri	⊢ 0ℎ ∈ 𝐻
19	4 18	pm3.2i	⊢ ( 𝐻 ⊆ ℋ ∧ 0ℎ ∈ 𝐻 )
20	1	hhva	⊢ +ℎ = ( +𝑣 ‘ 𝑈 )
21		eqid	⊢ ( +𝑣 ‘ 𝑊 ) = ( +𝑣 ‘ 𝑊 )
22	16 20 21 8	sspgval	⊢ ( ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ ( SubSp ‘ 𝑈 ) ) ∧ ( 𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻 ) ) → ( 𝑥 ( +𝑣 ‘ 𝑊 ) 𝑦 ) = ( 𝑥 +ℎ 𝑦 ) )
23	5 3 22	mpanl12	⊢ ( ( 𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻 ) → ( 𝑥 ( +𝑣 ‘ 𝑊 ) 𝑦 ) = ( 𝑥 +ℎ 𝑦 ) )
24	16 21	nvgcl	⊢ ( ( 𝑊 ∈ NrmCVec ∧ 𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻 ) → ( 𝑥 ( +𝑣 ‘ 𝑊 ) 𝑦 ) ∈ 𝐻 )
25	12 24	mp3an1	⊢ ( ( 𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻 ) → ( 𝑥 ( +𝑣 ‘ 𝑊 ) 𝑦 ) ∈ 𝐻 )
26	23 25	eqeltrrd	⊢ ( ( 𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻 ) → ( 𝑥 +ℎ 𝑦 ) ∈ 𝐻 )
27	26	rgen2	⊢ ∀ 𝑥 ∈ 𝐻 ∀ 𝑦 ∈ 𝐻 ( 𝑥 +ℎ 𝑦 ) ∈ 𝐻
28	1	hhsm	⊢ ·ℎ = ( ·𝑠OLD ‘ 𝑈 )
29		eqid	⊢ ( ·𝑠OLD ‘ 𝑊 ) = ( ·𝑠OLD ‘ 𝑊 )
30	16 28 29 8	sspsval	⊢ ( ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ ( SubSp ‘ 𝑈 ) ) ∧ ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝐻 ) ) → ( 𝑥 ( ·𝑠OLD ‘ 𝑊 ) 𝑦 ) = ( 𝑥 ·ℎ 𝑦 ) )
31	5 3 30	mpanl12	⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝐻 ) → ( 𝑥 ( ·𝑠OLD ‘ 𝑊 ) 𝑦 ) = ( 𝑥 ·ℎ 𝑦 ) )
32	16 29	nvscl	⊢ ( ( 𝑊 ∈ NrmCVec ∧ 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝐻 ) → ( 𝑥 ( ·𝑠OLD ‘ 𝑊 ) 𝑦 ) ∈ 𝐻 )
33	12 32	mp3an1	⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝐻 ) → ( 𝑥 ( ·𝑠OLD ‘ 𝑊 ) 𝑦 ) ∈ 𝐻 )
34	31 33	eqeltrrd	⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ 𝐻 ) → ( 𝑥 ·ℎ 𝑦 ) ∈ 𝐻 )
35	34	rgen2	⊢ ∀ 𝑥 ∈ ℂ ∀ 𝑦 ∈ 𝐻 ( 𝑥 ·ℎ 𝑦 ) ∈ 𝐻
36	27 35	pm3.2i	⊢ ( ∀ 𝑥 ∈ 𝐻 ∀ 𝑦 ∈ 𝐻 ( 𝑥 +ℎ 𝑦 ) ∈ 𝐻 ∧ ∀ 𝑥 ∈ ℂ ∀ 𝑦 ∈ 𝐻 ( 𝑥 ·ℎ 𝑦 ) ∈ 𝐻 )
37		issh2	⊢ ( 𝐻 ∈ Sℋ ↔ ( ( 𝐻 ⊆ ℋ ∧ 0ℎ ∈ 𝐻 ) ∧ ( ∀ 𝑥 ∈ 𝐻 ∀ 𝑦 ∈ 𝐻 ( 𝑥 +ℎ 𝑦 ) ∈ 𝐻 ∧ ∀ 𝑥 ∈ ℂ ∀ 𝑦 ∈ 𝐻 ( 𝑥 ·ℎ 𝑦 ) ∈ 𝐻 ) ) )
38	19 36 37	mpbir2an	⊢ 𝐻 ∈ Sℋ