Metamath Proof Explorer


Theorem lspprabs

Description: Absorption of vector sum into span of pair. (Contributed by NM, 27-Apr-2015)

Ref Expression
Hypotheses lspprabs.v 𝑉 = ( Base ‘ 𝑊 )
lspprabs.p + = ( +g𝑊 )
lspprabs.n 𝑁 = ( LSpan ‘ 𝑊 )
lspprabs.w ( 𝜑𝑊 ∈ LMod )
lspprabs.x ( 𝜑𝑋𝑉 )
lspprabs.y ( 𝜑𝑌𝑉 )
Assertion lspprabs ( 𝜑 → ( 𝑁 ‘ { 𝑋 , ( 𝑋 + 𝑌 ) } ) = ( 𝑁 ‘ { 𝑋 , 𝑌 } ) )

Proof

Step Hyp Ref Expression
1 lspprabs.v 𝑉 = ( Base ‘ 𝑊 )
2 lspprabs.p + = ( +g𝑊 )
3 lspprabs.n 𝑁 = ( LSpan ‘ 𝑊 )
4 lspprabs.w ( 𝜑𝑊 ∈ LMod )
5 lspprabs.x ( 𝜑𝑋𝑉 )
6 lspprabs.y ( 𝜑𝑌𝑉 )
7 eqid ( LSubSp ‘ 𝑊 ) = ( LSubSp ‘ 𝑊 )
8 7 lsssssubg ( 𝑊 ∈ LMod → ( LSubSp ‘ 𝑊 ) ⊆ ( SubGrp ‘ 𝑊 ) )
9 4 8 syl ( 𝜑 → ( LSubSp ‘ 𝑊 ) ⊆ ( SubGrp ‘ 𝑊 ) )
10 1 7 3 lspsncl ( ( 𝑊 ∈ LMod ∧ 𝑋𝑉 ) → ( 𝑁 ‘ { 𝑋 } ) ∈ ( LSubSp ‘ 𝑊 ) )
11 4 5 10 syl2anc ( 𝜑 → ( 𝑁 ‘ { 𝑋 } ) ∈ ( LSubSp ‘ 𝑊 ) )
12 9 11 sseldd ( 𝜑 → ( 𝑁 ‘ { 𝑋 } ) ∈ ( SubGrp ‘ 𝑊 ) )
13 1 7 3 lspsncl ( ( 𝑊 ∈ LMod ∧ 𝑌𝑉 ) → ( 𝑁 ‘ { 𝑌 } ) ∈ ( LSubSp ‘ 𝑊 ) )
14 4 6 13 syl2anc ( 𝜑 → ( 𝑁 ‘ { 𝑌 } ) ∈ ( LSubSp ‘ 𝑊 ) )
15 9 14 sseldd ( 𝜑 → ( 𝑁 ‘ { 𝑌 } ) ∈ ( SubGrp ‘ 𝑊 ) )
16 eqid ( LSSum ‘ 𝑊 ) = ( LSSum ‘ 𝑊 )
17 16 lsmub1 ( ( ( 𝑁 ‘ { 𝑋 } ) ∈ ( SubGrp ‘ 𝑊 ) ∧ ( 𝑁 ‘ { 𝑌 } ) ∈ ( SubGrp ‘ 𝑊 ) ) → ( 𝑁 ‘ { 𝑋 } ) ⊆ ( ( 𝑁 ‘ { 𝑋 } ) ( LSSum ‘ 𝑊 ) ( 𝑁 ‘ { 𝑌 } ) ) )
18 12 15 17 syl2anc ( 𝜑 → ( 𝑁 ‘ { 𝑋 } ) ⊆ ( ( 𝑁 ‘ { 𝑋 } ) ( LSSum ‘ 𝑊 ) ( 𝑁 ‘ { 𝑌 } ) ) )
19 7 16 lsmcl ( ( 𝑊 ∈ LMod ∧ ( 𝑁 ‘ { 𝑋 } ) ∈ ( LSubSp ‘ 𝑊 ) ∧ ( 𝑁 ‘ { 𝑌 } ) ∈ ( LSubSp ‘ 𝑊 ) ) → ( ( 𝑁 ‘ { 𝑋 } ) ( LSSum ‘ 𝑊 ) ( 𝑁 ‘ { 𝑌 } ) ) ∈ ( LSubSp ‘ 𝑊 ) )
20 4 11 14 19 syl3anc ( 𝜑 → ( ( 𝑁 ‘ { 𝑋 } ) ( LSSum ‘ 𝑊 ) ( 𝑁 ‘ { 𝑌 } ) ) ∈ ( LSubSp ‘ 𝑊 ) )
21 1 3 lspsnid ( ( 𝑊 ∈ LMod ∧ 𝑋𝑉 ) → 𝑋 ∈ ( 𝑁 ‘ { 𝑋 } ) )
22 4 5 21 syl2anc ( 𝜑𝑋 ∈ ( 𝑁 ‘ { 𝑋 } ) )
23 1 3 lspsnid ( ( 𝑊 ∈ LMod ∧ 𝑌𝑉 ) → 𝑌 ∈ ( 𝑁 ‘ { 𝑌 } ) )
24 4 6 23 syl2anc ( 𝜑𝑌 ∈ ( 𝑁 ‘ { 𝑌 } ) )
25 2 16 lsmelvali ( ( ( ( 𝑁 ‘ { 𝑋 } ) ∈ ( SubGrp ‘ 𝑊 ) ∧ ( 𝑁 ‘ { 𝑌 } ) ∈ ( SubGrp ‘ 𝑊 ) ) ∧ ( 𝑋 ∈ ( 𝑁 ‘ { 𝑋 } ) ∧ 𝑌 ∈ ( 𝑁 ‘ { 𝑌 } ) ) ) → ( 𝑋 + 𝑌 ) ∈ ( ( 𝑁 ‘ { 𝑋 } ) ( LSSum ‘ 𝑊 ) ( 𝑁 ‘ { 𝑌 } ) ) )
26 12 15 22 24 25 syl22anc ( 𝜑 → ( 𝑋 + 𝑌 ) ∈ ( ( 𝑁 ‘ { 𝑋 } ) ( LSSum ‘ 𝑊 ) ( 𝑁 ‘ { 𝑌 } ) ) )
27 7 3 4 20 26 lspsnel5a ( 𝜑 → ( 𝑁 ‘ { ( 𝑋 + 𝑌 ) } ) ⊆ ( ( 𝑁 ‘ { 𝑋 } ) ( LSSum ‘ 𝑊 ) ( 𝑁 ‘ { 𝑌 } ) ) )
28 1 2 lmodvacl ( ( 𝑊 ∈ LMod ∧ 𝑋𝑉𝑌𝑉 ) → ( 𝑋 + 𝑌 ) ∈ 𝑉 )
29 4 5 6 28 syl3anc ( 𝜑 → ( 𝑋 + 𝑌 ) ∈ 𝑉 )
30 1 7 3 lspsncl ( ( 𝑊 ∈ LMod ∧ ( 𝑋 + 𝑌 ) ∈ 𝑉 ) → ( 𝑁 ‘ { ( 𝑋 + 𝑌 ) } ) ∈ ( LSubSp ‘ 𝑊 ) )
31 4 29 30 syl2anc ( 𝜑 → ( 𝑁 ‘ { ( 𝑋 + 𝑌 ) } ) ∈ ( LSubSp ‘ 𝑊 ) )
32 9 31 sseldd ( 𝜑 → ( 𝑁 ‘ { ( 𝑋 + 𝑌 ) } ) ∈ ( SubGrp ‘ 𝑊 ) )
33 9 20 sseldd ( 𝜑 → ( ( 𝑁 ‘ { 𝑋 } ) ( LSSum ‘ 𝑊 ) ( 𝑁 ‘ { 𝑌 } ) ) ∈ ( SubGrp ‘ 𝑊 ) )
34 16 lsmlub ( ( ( 𝑁 ‘ { 𝑋 } ) ∈ ( SubGrp ‘ 𝑊 ) ∧ ( 𝑁 ‘ { ( 𝑋 + 𝑌 ) } ) ∈ ( SubGrp ‘ 𝑊 ) ∧ ( ( 𝑁 ‘ { 𝑋 } ) ( LSSum ‘ 𝑊 ) ( 𝑁 ‘ { 𝑌 } ) ) ∈ ( SubGrp ‘ 𝑊 ) ) → ( ( ( 𝑁 ‘ { 𝑋 } ) ⊆ ( ( 𝑁 ‘ { 𝑋 } ) ( LSSum ‘ 𝑊 ) ( 𝑁 ‘ { 𝑌 } ) ) ∧ ( 𝑁 ‘ { ( 𝑋 + 𝑌 ) } ) ⊆ ( ( 𝑁 ‘ { 𝑋 } ) ( LSSum ‘ 𝑊 ) ( 𝑁 ‘ { 𝑌 } ) ) ) ↔ ( ( 𝑁 ‘ { 𝑋 } ) ( LSSum ‘ 𝑊 ) ( 𝑁 ‘ { ( 𝑋 + 𝑌 ) } ) ) ⊆ ( ( 𝑁 ‘ { 𝑋 } ) ( LSSum ‘ 𝑊 ) ( 𝑁 ‘ { 𝑌 } ) ) ) )
35 12 32 33 34 syl3anc ( 𝜑 → ( ( ( 𝑁 ‘ { 𝑋 } ) ⊆ ( ( 𝑁 ‘ { 𝑋 } ) ( LSSum ‘ 𝑊 ) ( 𝑁 ‘ { 𝑌 } ) ) ∧ ( 𝑁 ‘ { ( 𝑋 + 𝑌 ) } ) ⊆ ( ( 𝑁 ‘ { 𝑋 } ) ( LSSum ‘ 𝑊 ) ( 𝑁 ‘ { 𝑌 } ) ) ) ↔ ( ( 𝑁 ‘ { 𝑋 } ) ( LSSum ‘ 𝑊 ) ( 𝑁 ‘ { ( 𝑋 + 𝑌 ) } ) ) ⊆ ( ( 𝑁 ‘ { 𝑋 } ) ( LSSum ‘ 𝑊 ) ( 𝑁 ‘ { 𝑌 } ) ) ) )
36 18 27 35 mpbi2and ( 𝜑 → ( ( 𝑁 ‘ { 𝑋 } ) ( LSSum ‘ 𝑊 ) ( 𝑁 ‘ { ( 𝑋 + 𝑌 ) } ) ) ⊆ ( ( 𝑁 ‘ { 𝑋 } ) ( LSSum ‘ 𝑊 ) ( 𝑁 ‘ { 𝑌 } ) ) )
37 16 lsmub1 ( ( ( 𝑁 ‘ { 𝑋 } ) ∈ ( SubGrp ‘ 𝑊 ) ∧ ( 𝑁 ‘ { ( 𝑋 + 𝑌 ) } ) ∈ ( SubGrp ‘ 𝑊 ) ) → ( 𝑁 ‘ { 𝑋 } ) ⊆ ( ( 𝑁 ‘ { 𝑋 } ) ( LSSum ‘ 𝑊 ) ( 𝑁 ‘ { ( 𝑋 + 𝑌 ) } ) ) )
38 12 32 37 syl2anc ( 𝜑 → ( 𝑁 ‘ { 𝑋 } ) ⊆ ( ( 𝑁 ‘ { 𝑋 } ) ( LSSum ‘ 𝑊 ) ( 𝑁 ‘ { ( 𝑋 + 𝑌 ) } ) ) )
39 7 16 lsmcl ( ( 𝑊 ∈ LMod ∧ ( 𝑁 ‘ { 𝑋 } ) ∈ ( LSubSp ‘ 𝑊 ) ∧ ( 𝑁 ‘ { ( 𝑋 + 𝑌 ) } ) ∈ ( LSubSp ‘ 𝑊 ) ) → ( ( 𝑁 ‘ { 𝑋 } ) ( LSSum ‘ 𝑊 ) ( 𝑁 ‘ { ( 𝑋 + 𝑌 ) } ) ) ∈ ( LSubSp ‘ 𝑊 ) )
40 4 11 31 39 syl3anc ( 𝜑 → ( ( 𝑁 ‘ { 𝑋 } ) ( LSSum ‘ 𝑊 ) ( 𝑁 ‘ { ( 𝑋 + 𝑌 ) } ) ) ∈ ( LSubSp ‘ 𝑊 ) )
41 eqid ( -g𝑊 ) = ( -g𝑊 )
42 1 3 lspsnid ( ( 𝑊 ∈ LMod ∧ ( 𝑋 + 𝑌 ) ∈ 𝑉 ) → ( 𝑋 + 𝑌 ) ∈ ( 𝑁 ‘ { ( 𝑋 + 𝑌 ) } ) )
43 4 29 42 syl2anc ( 𝜑 → ( 𝑋 + 𝑌 ) ∈ ( 𝑁 ‘ { ( 𝑋 + 𝑌 ) } ) )
44 41 16 32 12 43 22 lsmelvalmi ( 𝜑 → ( ( 𝑋 + 𝑌 ) ( -g𝑊 ) 𝑋 ) ∈ ( ( 𝑁 ‘ { ( 𝑋 + 𝑌 ) } ) ( LSSum ‘ 𝑊 ) ( 𝑁 ‘ { 𝑋 } ) ) )
45 lmodabl ( 𝑊 ∈ LMod → 𝑊 ∈ Abel )
46 4 45 syl ( 𝜑𝑊 ∈ Abel )
47 1 2 41 ablpncan2 ( ( 𝑊 ∈ Abel ∧ 𝑋𝑉𝑌𝑉 ) → ( ( 𝑋 + 𝑌 ) ( -g𝑊 ) 𝑋 ) = 𝑌 )
48 46 5 6 47 syl3anc ( 𝜑 → ( ( 𝑋 + 𝑌 ) ( -g𝑊 ) 𝑋 ) = 𝑌 )
49 16 lsmcom ( ( 𝑊 ∈ Abel ∧ ( 𝑁 ‘ { ( 𝑋 + 𝑌 ) } ) ∈ ( SubGrp ‘ 𝑊 ) ∧ ( 𝑁 ‘ { 𝑋 } ) ∈ ( SubGrp ‘ 𝑊 ) ) → ( ( 𝑁 ‘ { ( 𝑋 + 𝑌 ) } ) ( LSSum ‘ 𝑊 ) ( 𝑁 ‘ { 𝑋 } ) ) = ( ( 𝑁 ‘ { 𝑋 } ) ( LSSum ‘ 𝑊 ) ( 𝑁 ‘ { ( 𝑋 + 𝑌 ) } ) ) )
50 46 32 12 49 syl3anc ( 𝜑 → ( ( 𝑁 ‘ { ( 𝑋 + 𝑌 ) } ) ( LSSum ‘ 𝑊 ) ( 𝑁 ‘ { 𝑋 } ) ) = ( ( 𝑁 ‘ { 𝑋 } ) ( LSSum ‘ 𝑊 ) ( 𝑁 ‘ { ( 𝑋 + 𝑌 ) } ) ) )
51 44 48 50 3eltr3d ( 𝜑𝑌 ∈ ( ( 𝑁 ‘ { 𝑋 } ) ( LSSum ‘ 𝑊 ) ( 𝑁 ‘ { ( 𝑋 + 𝑌 ) } ) ) )
52 7 3 4 40 51 lspsnel5a ( 𝜑 → ( 𝑁 ‘ { 𝑌 } ) ⊆ ( ( 𝑁 ‘ { 𝑋 } ) ( LSSum ‘ 𝑊 ) ( 𝑁 ‘ { ( 𝑋 + 𝑌 ) } ) ) )
53 9 40 sseldd ( 𝜑 → ( ( 𝑁 ‘ { 𝑋 } ) ( LSSum ‘ 𝑊 ) ( 𝑁 ‘ { ( 𝑋 + 𝑌 ) } ) ) ∈ ( SubGrp ‘ 𝑊 ) )
54 16 lsmlub ( ( ( 𝑁 ‘ { 𝑋 } ) ∈ ( SubGrp ‘ 𝑊 ) ∧ ( 𝑁 ‘ { 𝑌 } ) ∈ ( SubGrp ‘ 𝑊 ) ∧ ( ( 𝑁 ‘ { 𝑋 } ) ( LSSum ‘ 𝑊 ) ( 𝑁 ‘ { ( 𝑋 + 𝑌 ) } ) ) ∈ ( SubGrp ‘ 𝑊 ) ) → ( ( ( 𝑁 ‘ { 𝑋 } ) ⊆ ( ( 𝑁 ‘ { 𝑋 } ) ( LSSum ‘ 𝑊 ) ( 𝑁 ‘ { ( 𝑋 + 𝑌 ) } ) ) ∧ ( 𝑁 ‘ { 𝑌 } ) ⊆ ( ( 𝑁 ‘ { 𝑋 } ) ( LSSum ‘ 𝑊 ) ( 𝑁 ‘ { ( 𝑋 + 𝑌 ) } ) ) ) ↔ ( ( 𝑁 ‘ { 𝑋 } ) ( LSSum ‘ 𝑊 ) ( 𝑁 ‘ { 𝑌 } ) ) ⊆ ( ( 𝑁 ‘ { 𝑋 } ) ( LSSum ‘ 𝑊 ) ( 𝑁 ‘ { ( 𝑋 + 𝑌 ) } ) ) ) )
55 12 15 53 54 syl3anc ( 𝜑 → ( ( ( 𝑁 ‘ { 𝑋 } ) ⊆ ( ( 𝑁 ‘ { 𝑋 } ) ( LSSum ‘ 𝑊 ) ( 𝑁 ‘ { ( 𝑋 + 𝑌 ) } ) ) ∧ ( 𝑁 ‘ { 𝑌 } ) ⊆ ( ( 𝑁 ‘ { 𝑋 } ) ( LSSum ‘ 𝑊 ) ( 𝑁 ‘ { ( 𝑋 + 𝑌 ) } ) ) ) ↔ ( ( 𝑁 ‘ { 𝑋 } ) ( LSSum ‘ 𝑊 ) ( 𝑁 ‘ { 𝑌 } ) ) ⊆ ( ( 𝑁 ‘ { 𝑋 } ) ( LSSum ‘ 𝑊 ) ( 𝑁 ‘ { ( 𝑋 + 𝑌 ) } ) ) ) )
56 38 52 55 mpbi2and ( 𝜑 → ( ( 𝑁 ‘ { 𝑋 } ) ( LSSum ‘ 𝑊 ) ( 𝑁 ‘ { 𝑌 } ) ) ⊆ ( ( 𝑁 ‘ { 𝑋 } ) ( LSSum ‘ 𝑊 ) ( 𝑁 ‘ { ( 𝑋 + 𝑌 ) } ) ) )
57 36 56 eqssd ( 𝜑 → ( ( 𝑁 ‘ { 𝑋 } ) ( LSSum ‘ 𝑊 ) ( 𝑁 ‘ { ( 𝑋 + 𝑌 ) } ) ) = ( ( 𝑁 ‘ { 𝑋 } ) ( LSSum ‘ 𝑊 ) ( 𝑁 ‘ { 𝑌 } ) ) )
58 1 3 16 4 5 29 lsmpr ( 𝜑 → ( 𝑁 ‘ { 𝑋 , ( 𝑋 + 𝑌 ) } ) = ( ( 𝑁 ‘ { 𝑋 } ) ( LSSum ‘ 𝑊 ) ( 𝑁 ‘ { ( 𝑋 + 𝑌 ) } ) ) )
59 1 3 16 4 5 6 lsmpr ( 𝜑 → ( 𝑁 ‘ { 𝑋 , 𝑌 } ) = ( ( 𝑁 ‘ { 𝑋 } ) ( LSSum ‘ 𝑊 ) ( 𝑁 ‘ { 𝑌 } ) ) )
60 57 58 59 3eqtr4d ( 𝜑 → ( 𝑁 ‘ { 𝑋 , ( 𝑋 + 𝑌 ) } ) = ( 𝑁 ‘ { 𝑋 , 𝑌 } ) )