lspabs3

Description: Absorption law for span of vector sum. (Contributed by NM, 30-Apr-2015)

	Ref	Expression
Hypotheses	lspabs2.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
	lspabs2.p	⊢ + = ( +_g ‘ 𝑊 )
	lspabs2.o	⊢ 0 = ( 0_g ‘ 𝑊 )
	lspabs2.n	⊢ 𝑁 = ( LSpan ‘ 𝑊 )
	lspabs2.w	⊢ ( 𝜑 → 𝑊 ∈ LVec )
	lspabs2.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
	lspabs3.y	⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
	lspabs3.xy	⊢ ( 𝜑 → ( 𝑋 + 𝑌 ) ≠ 0 )
	lspabs3.e	⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑋 } ) = ( 𝑁 ‘ { 𝑌 } ) )
Assertion	lspabs3	⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑋 } ) = ( 𝑁 ‘ { ( 𝑋 + 𝑌 ) } ) )

Proof

Step	Hyp	Ref	Expression
1		lspabs2.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
2		lspabs2.p	⊢ + = ( +_g ‘ 𝑊 )
3		lspabs2.o	⊢ 0 = ( 0_g ‘ 𝑊 )
4		lspabs2.n	⊢ 𝑁 = ( LSpan ‘ 𝑊 )
5		lspabs2.w	⊢ ( 𝜑 → 𝑊 ∈ LVec )
6		lspabs2.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
7		lspabs3.y	⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
8		lspabs3.xy	⊢ ( 𝜑 → ( 𝑋 + 𝑌 ) ≠ 0 )
9		lspabs3.e	⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑋 } ) = ( 𝑁 ‘ { 𝑌 } ) )
10		eqid	⊢ ( LSubSp ‘ 𝑊 ) = ( LSubSp ‘ 𝑊 )
11		lveclmod	⊢ ( 𝑊 ∈ LVec → 𝑊 ∈ LMod )
12	5 11	syl	⊢ ( 𝜑 → 𝑊 ∈ LMod )
13	1 10 4	lspsncl	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ) → ( 𝑁 ‘ { 𝑋 } ) ∈ ( LSubSp ‘ 𝑊 ) )
14	12 6 13	syl2anc	⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑋 } ) ∈ ( LSubSp ‘ 𝑊 ) )
15	1 10 4	lspsncl	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑌 ∈ 𝑉 ) → ( 𝑁 ‘ { 𝑌 } ) ∈ ( LSubSp ‘ 𝑊 ) )
16	12 7 15	syl2anc	⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑌 } ) ∈ ( LSubSp ‘ 𝑊 ) )
17		eqid	⊢ ( LSSum ‘ 𝑊 ) = ( LSSum ‘ 𝑊 )
18	10 17	lsmcl	⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝑁 ‘ { 𝑋 } ) ∈ ( LSubSp ‘ 𝑊 ) ∧ ( 𝑁 ‘ { 𝑌 } ) ∈ ( LSubSp ‘ 𝑊 ) ) → ( ( 𝑁 ‘ { 𝑋 } ) ( LSSum ‘ 𝑊 ) ( 𝑁 ‘ { 𝑌 } ) ) ∈ ( LSubSp ‘ 𝑊 ) )
19	12 14 16 18	syl3anc	⊢ ( 𝜑 → ( ( 𝑁 ‘ { 𝑋 } ) ( LSSum ‘ 𝑊 ) ( 𝑁 ‘ { 𝑌 } ) ) ∈ ( LSubSp ‘ 𝑊 ) )
20	1 4	lspsnsubg	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ) → ( 𝑁 ‘ { 𝑋 } ) ∈ ( SubGrp ‘ 𝑊 ) )
21	12 6 20	syl2anc	⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑋 } ) ∈ ( SubGrp ‘ 𝑊 ) )
22	9 21	eqeltrrd	⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑌 } ) ∈ ( SubGrp ‘ 𝑊 ) )
23	1 4	lspsnid	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ) → 𝑋 ∈ ( 𝑁 ‘ { 𝑋 } ) )
24	12 6 23	syl2anc	⊢ ( 𝜑 → 𝑋 ∈ ( 𝑁 ‘ { 𝑋 } ) )
25	1 4	lspsnid	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑌 ∈ 𝑉 ) → 𝑌 ∈ ( 𝑁 ‘ { 𝑌 } ) )
26	12 7 25	syl2anc	⊢ ( 𝜑 → 𝑌 ∈ ( 𝑁 ‘ { 𝑌 } ) )
27	2 17	lsmelvali	⊢ ( ( ( ( 𝑁 ‘ { 𝑋 } ) ∈ ( SubGrp ‘ 𝑊 ) ∧ ( 𝑁 ‘ { 𝑌 } ) ∈ ( SubGrp ‘ 𝑊 ) ) ∧ ( 𝑋 ∈ ( 𝑁 ‘ { 𝑋 } ) ∧ 𝑌 ∈ ( 𝑁 ‘ { 𝑌 } ) ) ) → ( 𝑋 + 𝑌 ) ∈ ( ( 𝑁 ‘ { 𝑋 } ) ( LSSum ‘ 𝑊 ) ( 𝑁 ‘ { 𝑌 } ) ) )
28	21 22 24 26 27	syl22anc	⊢ ( 𝜑 → ( 𝑋 + 𝑌 ) ∈ ( ( 𝑁 ‘ { 𝑋 } ) ( LSSum ‘ 𝑊 ) ( 𝑁 ‘ { 𝑌 } ) ) )
29	10 4 12 19 28	lspsnel5a	⊢ ( 𝜑 → ( 𝑁 ‘ { ( 𝑋 + 𝑌 ) } ) ⊆ ( ( 𝑁 ‘ { 𝑋 } ) ( LSSum ‘ 𝑊 ) ( 𝑁 ‘ { 𝑌 } ) ) )
30	9	oveq2d	⊢ ( 𝜑 → ( ( 𝑁 ‘ { 𝑋 } ) ( LSSum ‘ 𝑊 ) ( 𝑁 ‘ { 𝑋 } ) ) = ( ( 𝑁 ‘ { 𝑋 } ) ( LSSum ‘ 𝑊 ) ( 𝑁 ‘ { 𝑌 } ) ) )
31	17	lsmidm	⊢ ( ( 𝑁 ‘ { 𝑋 } ) ∈ ( SubGrp ‘ 𝑊 ) → ( ( 𝑁 ‘ { 𝑋 } ) ( LSSum ‘ 𝑊 ) ( 𝑁 ‘ { 𝑋 } ) ) = ( 𝑁 ‘ { 𝑋 } ) )
32	21 31	syl	⊢ ( 𝜑 → ( ( 𝑁 ‘ { 𝑋 } ) ( LSSum ‘ 𝑊 ) ( 𝑁 ‘ { 𝑋 } ) ) = ( 𝑁 ‘ { 𝑋 } ) )
33	30 32	eqtr3d	⊢ ( 𝜑 → ( ( 𝑁 ‘ { 𝑋 } ) ( LSSum ‘ 𝑊 ) ( 𝑁 ‘ { 𝑌 } ) ) = ( 𝑁 ‘ { 𝑋 } ) )
34	29 33	sseqtrd	⊢ ( 𝜑 → ( 𝑁 ‘ { ( 𝑋 + 𝑌 ) } ) ⊆ ( 𝑁 ‘ { 𝑋 } ) )
35	1 2	lmodvacl	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → ( 𝑋 + 𝑌 ) ∈ 𝑉 )
36	12 6 7 35	syl3anc	⊢ ( 𝜑 → ( 𝑋 + 𝑌 ) ∈ 𝑉 )
37		eldifsn	⊢ ( ( 𝑋 + 𝑌 ) ∈ ( 𝑉 ∖ { 0 } ) ↔ ( ( 𝑋 + 𝑌 ) ∈ 𝑉 ∧ ( 𝑋 + 𝑌 ) ≠ 0 ) )
38	36 8 37	sylanbrc	⊢ ( 𝜑 → ( 𝑋 + 𝑌 ) ∈ ( 𝑉 ∖ { 0 } ) )
39	1 3 4 5 38 6	lspsncmp	⊢ ( 𝜑 → ( ( 𝑁 ‘ { ( 𝑋 + 𝑌 ) } ) ⊆ ( 𝑁 ‘ { 𝑋 } ) ↔ ( 𝑁 ‘ { ( 𝑋 + 𝑌 ) } ) = ( 𝑁 ‘ { 𝑋 } ) ) )
40	34 39	mpbid	⊢ ( 𝜑 → ( 𝑁 ‘ { ( 𝑋 + 𝑌 ) } ) = ( 𝑁 ‘ { 𝑋 } ) )
41	40	eqcomd	⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑋 } ) = ( 𝑁 ‘ { ( 𝑋 + 𝑌 ) } ) )

Metamath Proof Explorer

Theorem lspabs3

Proof