This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 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 = ( 0g ‘ 𝑊 )
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 = ( 0g ‘ 𝑊 )
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 ellspsn5 ⊢ ( 𝜑 → ( 𝑁 ‘ { ( 𝑋 + 𝑌 ) } ) ⊆ ( ( 𝑁 ‘ { 𝑋 } ) ( 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 ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑋 } ) = ( 𝑁 ‘ { ( 𝑋 + 𝑌 ) } ) )