Theorem lssvsubcl

Description: Closure of vector subtraction in a subspace. (Contributed by NM, 31-Mar-2014) (Revised by Mario Carneiro, 19-Jun-2014)

	Ref	Expression
Hypotheses	lssvsubcl.m	⊢ − = ( -g ‘ 𝑊 )
	lssvsubcl.s	⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
Assertion	lssvsubcl	⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) ∧ ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈 ) ) → ( 𝑋 − 𝑌 ) ∈ 𝑈 )

Proof

Step	Hyp	Ref	Expression
1		lssvsubcl.m	⊢ − = ( -g ‘ 𝑊 )
2		lssvsubcl.s	⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
3		simpll	⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) ∧ ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈 ) ) → 𝑊 ∈ LMod )
4		eqid	⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
5	4 2	lssel	⊢ ( ( 𝑈 ∈ 𝑆 ∧ 𝑋 ∈ 𝑈 ) → 𝑋 ∈ ( Base ‘ 𝑊 ) )
6	5	ad2ant2lr	⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) ∧ ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈 ) ) → 𝑋 ∈ ( Base ‘ 𝑊 ) )
7	4 2	lssel	⊢ ( ( 𝑈 ∈ 𝑆 ∧ 𝑌 ∈ 𝑈 ) → 𝑌 ∈ ( Base ‘ 𝑊 ) )
8	7	ad2ant2l	⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) ∧ ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈 ) ) → 𝑌 ∈ ( Base ‘ 𝑊 ) )
9		eqid	⊢ ( +g ‘ 𝑊 ) = ( +g ‘ 𝑊 )
10		eqid	⊢ ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑊 )
11		eqid	⊢ ( ·𝑠 ‘ 𝑊 ) = ( ·𝑠 ‘ 𝑊 )
12		eqid	⊢ ( invg ‘ ( Scalar ‘ 𝑊 ) ) = ( invg ‘ ( Scalar ‘ 𝑊 ) )
13		eqid	⊢ ( 1r ‘ ( Scalar ‘ 𝑊 ) ) = ( 1r ‘ ( Scalar ‘ 𝑊 ) )
14	4 9 1 10 11 12 13	lmodvsubval2	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ ( Base ‘ 𝑊 ) ∧ 𝑌 ∈ ( Base ‘ 𝑊 ) ) → ( 𝑋 − 𝑌 ) = ( 𝑋 ( +g ‘ 𝑊 ) ( ( ( invg ‘ ( Scalar ‘ 𝑊 ) ) ‘ ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ) ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ) )
15	3 6 8 14	syl3anc	⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) ∧ ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈 ) ) → ( 𝑋 − 𝑌 ) = ( 𝑋 ( +g ‘ 𝑊 ) ( ( ( invg ‘ ( Scalar ‘ 𝑊 ) ) ‘ ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ) ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ) )
16	10	lmodfgrp	⊢ ( 𝑊 ∈ LMod → ( Scalar ‘ 𝑊 ) ∈ Grp )
17	3 16	syl	⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) ∧ ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈 ) ) → ( Scalar ‘ 𝑊 ) ∈ Grp )
18		eqid	⊢ ( Base ‘ ( Scalar ‘ 𝑊 ) ) = ( Base ‘ ( Scalar ‘ 𝑊 ) )
19	10 18 13	lmod1cl	⊢ ( 𝑊 ∈ LMod → ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
20	3 19	syl	⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) ∧ ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈 ) ) → ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
21	18 12	grpinvcl	⊢ ( ( ( Scalar ‘ 𝑊 ) ∈ Grp ∧ ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) → ( ( invg ‘ ( Scalar ‘ 𝑊 ) ) ‘ ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ) ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
22	17 20 21	syl2anc	⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) ∧ ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈 ) ) → ( ( invg ‘ ( Scalar ‘ 𝑊 ) ) ‘ ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ) ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
23	4 10 11 18	lmodvscl	⊢ ( ( 𝑊 ∈ LMod ∧ ( ( invg ‘ ( Scalar ‘ 𝑊 ) ) ‘ ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ) ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑌 ∈ ( Base ‘ 𝑊 ) ) → ( ( ( invg ‘ ( Scalar ‘ 𝑊 ) ) ‘ ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ) ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ∈ ( Base ‘ 𝑊 ) )
24	3 22 8 23	syl3anc	⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) ∧ ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈 ) ) → ( ( ( invg ‘ ( Scalar ‘ 𝑊 ) ) ‘ ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ) ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ∈ ( Base ‘ 𝑊 ) )
25	4 9	lmodcom	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ ( Base ‘ 𝑊 ) ∧ ( ( ( invg ‘ ( Scalar ‘ 𝑊 ) ) ‘ ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ) ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ∈ ( Base ‘ 𝑊 ) ) → ( 𝑋 ( +g ‘ 𝑊 ) ( ( ( invg ‘ ( Scalar ‘ 𝑊 ) ) ‘ ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ) ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ) = ( ( ( ( invg ‘ ( Scalar ‘ 𝑊 ) ) ‘ ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ) ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ( +g ‘ 𝑊 ) 𝑋 ) )
26	3 6 24 25	syl3anc	⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) ∧ ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈 ) ) → ( 𝑋 ( +g ‘ 𝑊 ) ( ( ( invg ‘ ( Scalar ‘ 𝑊 ) ) ‘ ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ) ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ) = ( ( ( ( invg ‘ ( Scalar ‘ 𝑊 ) ) ‘ ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ) ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ( +g ‘ 𝑊 ) 𝑋 ) )
27		simplr	⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) ∧ ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈 ) ) → 𝑈 ∈ 𝑆 )
28		simprr	⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) ∧ ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈 ) ) → 𝑌 ∈ 𝑈 )
29		simprl	⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) ∧ ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈 ) ) → 𝑋 ∈ 𝑈 )
30	10 18 9 11 2	lsscl	⊢ ( ( 𝑈 ∈ 𝑆 ∧ ( ( ( invg ‘ ( Scalar ‘ 𝑊 ) ) ‘ ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ) ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑌 ∈ 𝑈 ∧ 𝑋 ∈ 𝑈 ) ) → ( ( ( ( invg ‘ ( Scalar ‘ 𝑊 ) ) ‘ ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ) ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ( +g ‘ 𝑊 ) 𝑋 ) ∈ 𝑈 )
31	27 22 28 29 30	syl13anc	⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) ∧ ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈 ) ) → ( ( ( ( invg ‘ ( Scalar ‘ 𝑊 ) ) ‘ ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ) ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ( +g ‘ 𝑊 ) 𝑋 ) ∈ 𝑈 )
32	26 31	eqeltrd	⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) ∧ ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈 ) ) → ( 𝑋 ( +g ‘ 𝑊 ) ( ( ( invg ‘ ( Scalar ‘ 𝑊 ) ) ‘ ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ) ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ) ∈ 𝑈 )
33	15 32	eqeltrd	⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) ∧ ( 𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑈 ) ) → ( 𝑋 − 𝑌 ) ∈ 𝑈 )