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

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