Theorem lssvscl

Description: Closure of scalar product in a subspace. (Contributed by NM, 11-Jan-2014) (Revised by Mario Carneiro, 19-Jun-2014)

	Ref	Expression
Hypotheses	lssvscl.f	⊢ 𝐹 = ( Scalar ‘ 𝑊 )
	lssvscl.t	⊢ · = ( ·𝑠 ‘ 𝑊 )
	lssvscl.b	⊢ 𝐵 = ( Base ‘ 𝐹 )
	lssvscl.s	⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
Assertion	lssvscl	⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈 ) ) → ( 𝑋 · 𝑌 ) ∈ 𝑈 )

Proof

Step	Hyp	Ref	Expression
1		lssvscl.f	⊢ 𝐹 = ( Scalar ‘ 𝑊 )
2		lssvscl.t	⊢ · = ( ·𝑠 ‘ 𝑊 )
3		lssvscl.b	⊢ 𝐵 = ( Base ‘ 𝐹 )
4		lssvscl.s	⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
5		simpll	⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈 ) ) → 𝑊 ∈ LMod )
6		simprl	⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈 ) ) → 𝑋 ∈ 𝐵 )
7		eqid	⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
8	7 4	lssel	⊢ ( ( 𝑈 ∈ 𝑆 ∧ 𝑌 ∈ 𝑈 ) → 𝑌 ∈ ( Base ‘ 𝑊 ) )
9	8	ad2ant2l	⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈 ) ) → 𝑌 ∈ ( Base ‘ 𝑊 ) )
10	7 1 2 3	lmodvscl	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ ( Base ‘ 𝑊 ) ) → ( 𝑋 · 𝑌 ) ∈ ( Base ‘ 𝑊 ) )
11	5 6 9 10	syl3anc	⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈 ) ) → ( 𝑋 · 𝑌 ) ∈ ( Base ‘ 𝑊 ) )
12		eqid	⊢ ( +g ‘ 𝑊 ) = ( +g ‘ 𝑊 )
13		eqid	⊢ ( 0g ‘ 𝑊 ) = ( 0g ‘ 𝑊 )
14	7 12 13	lmod0vrid	⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝑋 · 𝑌 ) ∈ ( Base ‘ 𝑊 ) ) → ( ( 𝑋 · 𝑌 ) ( +g ‘ 𝑊 ) ( 0g ‘ 𝑊 ) ) = ( 𝑋 · 𝑌 ) )
15	5 11 14	syl2anc	⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈 ) ) → ( ( 𝑋 · 𝑌 ) ( +g ‘ 𝑊 ) ( 0g ‘ 𝑊 ) ) = ( 𝑋 · 𝑌 ) )
16		simplr	⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈 ) ) → 𝑈 ∈ 𝑆 )
17		simprr	⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈 ) ) → 𝑌 ∈ 𝑈 )
18	13 4	lss0cl	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) → ( 0g ‘ 𝑊 ) ∈ 𝑈 )
19	18	adantr	⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈 ) ) → ( 0g ‘ 𝑊 ) ∈ 𝑈 )
20	1 3 12 2 4	lsscl	⊢ ( ( 𝑈 ∈ 𝑆 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈 ∧ ( 0g ‘ 𝑊 ) ∈ 𝑈 ) ) → ( ( 𝑋 · 𝑌 ) ( +g ‘ 𝑊 ) ( 0g ‘ 𝑊 ) ) ∈ 𝑈 )
21	16 6 17 19 20	syl13anc	⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈 ) ) → ( ( 𝑋 · 𝑌 ) ( +g ‘ 𝑊 ) ( 0g ‘ 𝑊 ) ) ∈ 𝑈 )
22	15 21	eqeltrrd	⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝑈 ) ) → ( 𝑋 · 𝑌 ) ∈ 𝑈 )