Metamath Proof Explorer

Theorem lspabs2

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 ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
lspabs2.y ⊢ ( 𝜑 → 𝑌 ∈ ( 𝑉 ∖ { 0 } ) )
lspabs2.e ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑋 } ) = ( 𝑁 ‘ { ( 𝑋 + 𝑌 ) } ) )
Assertion lspabs2 ( 𝜑 → ( 𝑁 ‘ { 𝑋 } ) = ( 𝑁 ‘ { 𝑌 } ) )

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 lspabs2.y ⊢ ( 𝜑 → 𝑌 ∈ ( 𝑉 ∖ { 0 } ) )
8 lspabs2.e ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑋 } ) = ( 𝑁 ‘ { ( 𝑋 + 𝑌 ) } ) )
9 lveclmod ⊢ ( 𝑊 ∈ LVec → 𝑊 ∈ LMod )
10 5 9 syl ⊢ ( 𝜑 → 𝑊 ∈ LMod )
11 1 4 lspsnsubg ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ) → ( 𝑁 ‘ { 𝑋 } ) ∈ ( SubGrp ‘ 𝑊 ) )
12 10 6 11 syl2anc ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑋 } ) ∈ ( SubGrp ‘ 𝑊 ) )
13 7 eldifad ⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
14 1 4 lspsnsubg ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑌 ∈ 𝑉 ) → ( 𝑁 ‘ { 𝑌 } ) ∈ ( SubGrp ‘ 𝑊 ) )
15 10 13 14 syl2anc ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑌 } ) ∈ ( SubGrp ‘ 𝑊 ) )
16 eqid ⊢ ( LSSum ‘ 𝑊 ) = ( LSSum ‘ 𝑊 )
17 16 lsmub2 ⊢ ( ( ( 𝑁 ‘ { 𝑋 } ) ∈ ( SubGrp ‘ 𝑊 ) ∧ ( 𝑁 ‘ { 𝑌 } ) ∈ ( SubGrp ‘ 𝑊 ) ) → ( 𝑁 ‘ { 𝑌 } ) ⊆ ( ( 𝑁 ‘ { 𝑋 } ) ( LSSum ‘ 𝑊 ) ( 𝑁 ‘ { 𝑌 } ) ) )
18 12 15 17 syl2anc ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑌 } ) ⊆ ( ( 𝑁 ‘ { 𝑋 } ) ( LSSum ‘ 𝑊 ) ( 𝑁 ‘ { 𝑌 } ) ) )
19 8 oveq2d ⊢ ( 𝜑 → ( ( 𝑁 ‘ { 𝑋 } ) ( LSSum ‘ 𝑊 ) ( 𝑁 ‘ { 𝑋 } ) ) = ( ( 𝑁 ‘ { 𝑋 } ) ( LSSum ‘ 𝑊 ) ( 𝑁 ‘ { ( 𝑋 + 𝑌 ) } ) ) )
20 16 lsmidm ⊢ ( ( 𝑁 ‘ { 𝑋 } ) ∈ ( SubGrp ‘ 𝑊 ) → ( ( 𝑁 ‘ { 𝑋 } ) ( LSSum ‘ 𝑊 ) ( 𝑁 ‘ { 𝑋 } ) ) = ( 𝑁 ‘ { 𝑋 } ) )
21 12 20 syl ⊢ ( 𝜑 → ( ( 𝑁 ‘ { 𝑋 } ) ( LSSum ‘ 𝑊 ) ( 𝑁 ‘ { 𝑋 } ) ) = ( 𝑁 ‘ { 𝑋 } ) )
22 1 2 4 10 6 13 lspprabs ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑋 , ( 𝑋 + 𝑌 ) } ) = ( 𝑁 ‘ { 𝑋 , 𝑌 } ) )
23 1 2 lmodvacl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → ( 𝑋 + 𝑌 ) ∈ 𝑉 )
24 10 6 13 23 syl3anc ⊢ ( 𝜑 → ( 𝑋 + 𝑌 ) ∈ 𝑉 )
25 1 4 16 10 6 24 lsmpr ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑋 , ( 𝑋 + 𝑌 ) } ) = ( ( 𝑁 ‘ { 𝑋 } ) ( LSSum ‘ 𝑊 ) ( 𝑁 ‘ { ( 𝑋 + 𝑌 ) } ) ) )
26 1 4 16 10 6 13 lsmpr ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑋 , 𝑌 } ) = ( ( 𝑁 ‘ { 𝑋 } ) ( LSSum ‘ 𝑊 ) ( 𝑁 ‘ { 𝑌 } ) ) )
27 22 25 26 3eqtr3d ⊢ ( 𝜑 → ( ( 𝑁 ‘ { 𝑋 } ) ( LSSum ‘ 𝑊 ) ( 𝑁 ‘ { ( 𝑋 + 𝑌 ) } ) ) = ( ( 𝑁 ‘ { 𝑋 } ) ( LSSum ‘ 𝑊 ) ( 𝑁 ‘ { 𝑌 } ) ) )
28 19 21 27 3eqtr3rd ⊢ ( 𝜑 → ( ( 𝑁 ‘ { 𝑋 } ) ( LSSum ‘ 𝑊 ) ( 𝑁 ‘ { 𝑌 } ) ) = ( 𝑁 ‘ { 𝑋 } ) )
29 18 28 sseqtrd ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑌 } ) ⊆ ( 𝑁 ‘ { 𝑋 } ) )
30 1 3 4 5 7 6 lspsncmp ⊢ ( 𝜑 → ( ( 𝑁 ‘ { 𝑌 } ) ⊆ ( 𝑁 ‘ { 𝑋 } ) ↔ ( 𝑁 ‘ { 𝑌 } ) = ( 𝑁 ‘ { 𝑋 } ) ) )
31 29 30 mpbid ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑌 } ) = ( 𝑁 ‘ { 𝑋 } ) )
32 31 eqcomd ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑋 } ) = ( 𝑁 ‘ { 𝑌 } ) )