Metamath Proof Explorer

Theorem baerlem5alem1

Description: Lemma for baerlem5a . (Contributed by NM, 13-Apr-2015)

Ref Expression
Hypotheses baerlem3.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
baerlem3.m ⊢ − = ( -g ‘ 𝑊 )
baerlem3.o ⊢ 0 = ( 0g ‘ 𝑊 )
baerlem3.s ⊢ ⊕ = ( LSSum ‘ 𝑊 )
baerlem3.n ⊢ 𝑁 = ( LSpan ‘ 𝑊 )
baerlem3.w ⊢ ( 𝜑 → 𝑊 ∈ LVec )
baerlem3.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
baerlem3.c ⊢ ( 𝜑 → ¬ 𝑋 ∈ ( 𝑁 ‘ { 𝑌 , 𝑍 } ) )
baerlem3.d ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑌 } ) ≠ ( 𝑁 ‘ { 𝑍 } ) )
baerlem3.y ⊢ ( 𝜑 → 𝑌 ∈ ( 𝑉 ∖ { 0 } ) )
baerlem3.z ⊢ ( 𝜑 → 𝑍 ∈ ( 𝑉 ∖ { 0 } ) )
baerlem3.p ⊢ + = ( +g ‘ 𝑊 )
baerlem3.t ⊢ · = ( ·𝑠 ‘ 𝑊 )
baerlem3.r ⊢ 𝑅 = ( Scalar ‘ 𝑊 )
baerlem3.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
baerlem3.a ⊢ ⨣ = ( +g ‘ 𝑅 )
baerlem3.l ⊢ 𝐿 = ( -g ‘ 𝑅 )
baerlem3.q ⊢ 𝑄 = ( 0g ‘ 𝑅 )
baerlem3.i ⊢ 𝐼 = ( invg ‘ 𝑅 )
baerlem5a.a1 ⊢ ( 𝜑 → 𝑎 ∈ 𝐵 )
baerlem5a.b1 ⊢ ( 𝜑 → 𝑏 ∈ 𝐵 )
baerlem5a.d1 ⊢ ( 𝜑 → 𝑑 ∈ 𝐵 )
baerlem5a.e1 ⊢ ( 𝜑 → 𝑒 ∈ 𝐵 )
baerlem5a.j1 ⊢ ( 𝜑 → 𝑗 = ( ( 𝑎 · ( 𝑋 − 𝑌 ) ) + ( 𝑏 · 𝑍 ) ) )
baerlem5a.j2 ⊢ ( 𝜑 → 𝑗 = ( ( 𝑑 · ( 𝑋 − 𝑍 ) ) + ( 𝑒 · 𝑌 ) ) )
Assertion baerlem5alem1 ( 𝜑 → 𝑗 = ( 𝑎 · ( 𝑋 − ( 𝑌 + 𝑍 ) ) ) )

Proof

Step Hyp Ref Expression
1 baerlem3.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
2 baerlem3.m ⊢ − = ( -g ‘ 𝑊 )
3 baerlem3.o ⊢ 0 = ( 0g ‘ 𝑊 )
4 baerlem3.s ⊢ ⊕ = ( LSSum ‘ 𝑊 )
5 baerlem3.n ⊢ 𝑁 = ( LSpan ‘ 𝑊 )
6 baerlem3.w ⊢ ( 𝜑 → 𝑊 ∈ LVec )
7 baerlem3.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
8 baerlem3.c ⊢ ( 𝜑 → ¬ 𝑋 ∈ ( 𝑁 ‘ { 𝑌 , 𝑍 } ) )
9 baerlem3.d ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑌 } ) ≠ ( 𝑁 ‘ { 𝑍 } ) )
10 baerlem3.y ⊢ ( 𝜑 → 𝑌 ∈ ( 𝑉 ∖ { 0 } ) )
11 baerlem3.z ⊢ ( 𝜑 → 𝑍 ∈ ( 𝑉 ∖ { 0 } ) )
12 baerlem3.p ⊢ + = ( +g ‘ 𝑊 )
13 baerlem3.t ⊢ · = ( ·𝑠 ‘ 𝑊 )
14 baerlem3.r ⊢ 𝑅 = ( Scalar ‘ 𝑊 )
15 baerlem3.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
16 baerlem3.a ⊢ ⨣ = ( +g ‘ 𝑅 )
17 baerlem3.l ⊢ 𝐿 = ( -g ‘ 𝑅 )
18 baerlem3.q ⊢ 𝑄 = ( 0g ‘ 𝑅 )
19 baerlem3.i ⊢ 𝐼 = ( invg ‘ 𝑅 )
20 baerlem5a.a1 ⊢ ( 𝜑 → 𝑎 ∈ 𝐵 )
21 baerlem5a.b1 ⊢ ( 𝜑 → 𝑏 ∈ 𝐵 )
22 baerlem5a.d1 ⊢ ( 𝜑 → 𝑑 ∈ 𝐵 )
23 baerlem5a.e1 ⊢ ( 𝜑 → 𝑒 ∈ 𝐵 )
24 baerlem5a.j1 ⊢ ( 𝜑 → 𝑗 = ( ( 𝑎 · ( 𝑋 − 𝑌 ) ) + ( 𝑏 · 𝑍 ) ) )
25 baerlem5a.j2 ⊢ ( 𝜑 → 𝑗 = ( ( 𝑑 · ( 𝑋 − 𝑍 ) ) + ( 𝑒 · 𝑌 ) ) )
26 lveclmod ⊢ ( 𝑊 ∈ LVec → 𝑊 ∈ LMod )
27 6 26 syl ⊢ ( 𝜑 → 𝑊 ∈ LMod )
28 10 eldifad ⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
29 1 13 14 15 2 27 20 7 28 lmodsubdi ⊢ ( 𝜑 → ( 𝑎 · ( 𝑋 − 𝑌 ) ) = ( ( 𝑎 · 𝑋 ) − ( 𝑎 · 𝑌 ) ) )
30 1 14 13 15 lmodvscl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑎 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ) → ( 𝑎 · 𝑋 ) ∈ 𝑉 )
31 27 20 7 30 syl3anc ⊢ ( 𝜑 → ( 𝑎 · 𝑋 ) ∈ 𝑉 )
32 1 12 2 13 14 15 19 27 20 31 28 lmodsubvs ⊢ ( 𝜑 → ( ( 𝑎 · 𝑋 ) − ( 𝑎 · 𝑌 ) ) = ( ( 𝑎 · 𝑋 ) + ( ( 𝐼 ‘ 𝑎 ) · 𝑌 ) ) )
33 29 32 eqtrd ⊢ ( 𝜑 → ( 𝑎 · ( 𝑋 − 𝑌 ) ) = ( ( 𝑎 · 𝑋 ) + ( ( 𝐼 ‘ 𝑎 ) · 𝑌 ) ) )
34 33 oveq1d ⊢ ( 𝜑 → ( ( 𝑎 · ( 𝑋 − 𝑌 ) ) + ( 𝑏 · 𝑍 ) ) = ( ( ( 𝑎 · 𝑋 ) + ( ( 𝐼 ‘ 𝑎 ) · 𝑌 ) ) + ( 𝑏 · 𝑍 ) ) )
35 14 lmodring ⊢ ( 𝑊 ∈ LMod → 𝑅 ∈ Ring )
36 ringgrp ⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ Grp )
37 27 35 36 3syl ⊢ ( 𝜑 → 𝑅 ∈ Grp )
38 15 19 grpinvcl ⊢ ( ( 𝑅 ∈ Grp ∧ 𝑎 ∈ 𝐵 ) → ( 𝐼 ‘ 𝑎 ) ∈ 𝐵 )
39 37 20 38 syl2anc ⊢ ( 𝜑 → ( 𝐼 ‘ 𝑎 ) ∈ 𝐵 )
40 1 14 13 15 lmodvscl ⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝐼 ‘ 𝑎 ) ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) → ( ( 𝐼 ‘ 𝑎 ) · 𝑌 ) ∈ 𝑉 )
41 27 39 28 40 syl3anc ⊢ ( 𝜑 → ( ( 𝐼 ‘ 𝑎 ) · 𝑌 ) ∈ 𝑉 )
42 11 eldifad ⊢ ( 𝜑 → 𝑍 ∈ 𝑉 )
43 1 14 13 15 lmodvscl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑏 ∈ 𝐵 ∧ 𝑍 ∈ 𝑉 ) → ( 𝑏 · 𝑍 ) ∈ 𝑉 )
44 27 21 42 43 syl3anc ⊢ ( 𝜑 → ( 𝑏 · 𝑍 ) ∈ 𝑉 )
45 1 12 lmodass ⊢ ( ( 𝑊 ∈ LMod ∧ ( ( 𝑎 · 𝑋 ) ∈ 𝑉 ∧ ( ( 𝐼 ‘ 𝑎 ) · 𝑌 ) ∈ 𝑉 ∧ ( 𝑏 · 𝑍 ) ∈ 𝑉 ) ) → ( ( ( 𝑎 · 𝑋 ) + ( ( 𝐼 ‘ 𝑎 ) · 𝑌 ) ) + ( 𝑏 · 𝑍 ) ) = ( ( 𝑎 · 𝑋 ) + ( ( ( 𝐼 ‘ 𝑎 ) · 𝑌 ) + ( 𝑏 · 𝑍 ) ) ) )
46 27 31 41 44 45 syl13anc ⊢ ( 𝜑 → ( ( ( 𝑎 · 𝑋 ) + ( ( 𝐼 ‘ 𝑎 ) · 𝑌 ) ) + ( 𝑏 · 𝑍 ) ) = ( ( 𝑎 · 𝑋 ) + ( ( ( 𝐼 ‘ 𝑎 ) · 𝑌 ) + ( 𝑏 · 𝑍 ) ) ) )
47 24 34 46 3eqtrd ⊢ ( 𝜑 → 𝑗 = ( ( 𝑎 · 𝑋 ) + ( ( ( 𝐼 ‘ 𝑎 ) · 𝑌 ) + ( 𝑏 · 𝑍 ) ) ) )
48 1 12 lmodvacl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑉 ) → ( 𝑌 + 𝑍 ) ∈ 𝑉 )
49 27 28 42 48 syl3anc ⊢ ( 𝜑 → ( 𝑌 + 𝑍 ) ∈ 𝑉 )
50 1 14 13 15 lmodvscl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑎 ∈ 𝐵 ∧ ( 𝑌 + 𝑍 ) ∈ 𝑉 ) → ( 𝑎 · ( 𝑌 + 𝑍 ) ) ∈ 𝑉 )
51 27 20 49 50 syl3anc ⊢ ( 𝜑 → ( 𝑎 · ( 𝑌 + 𝑍 ) ) ∈ 𝑉 )
52 eqid ⊢ ( invg ‘ 𝑊 ) = ( invg ‘ 𝑊 )
53 1 12 52 2 grpsubval ⊢ ( ( ( 𝑎 · 𝑋 ) ∈ 𝑉 ∧ ( 𝑎 · ( 𝑌 + 𝑍 ) ) ∈ 𝑉 ) → ( ( 𝑎 · 𝑋 ) − ( 𝑎 · ( 𝑌 + 𝑍 ) ) ) = ( ( 𝑎 · 𝑋 ) + ( ( invg ‘ 𝑊 ) ‘ ( 𝑎 · ( 𝑌 + 𝑍 ) ) ) ) )
54 31 51 53 syl2anc ⊢ ( 𝜑 → ( ( 𝑎 · 𝑋 ) − ( 𝑎 · ( 𝑌 + 𝑍 ) ) ) = ( ( 𝑎 · 𝑋 ) + ( ( invg ‘ 𝑊 ) ‘ ( 𝑎 · ( 𝑌 + 𝑍 ) ) ) ) )
55 1 13 14 15 2 27 20 7 49 lmodsubdi ⊢ ( 𝜑 → ( 𝑎 · ( 𝑋 − ( 𝑌 + 𝑍 ) ) ) = ( ( 𝑎 · 𝑋 ) − ( 𝑎 · ( 𝑌 + 𝑍 ) ) ) )
56 1 12 14 13 15 lmodvsdi ⊢ ( ( 𝑊 ∈ LMod ∧ ( ( 𝐼 ‘ 𝑎 ) ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑉 ) ) → ( ( 𝐼 ‘ 𝑎 ) · ( 𝑌 + 𝑍 ) ) = ( ( ( 𝐼 ‘ 𝑎 ) · 𝑌 ) + ( ( 𝐼 ‘ 𝑎 ) · 𝑍 ) ) )
57 27 39 28 42 56 syl13anc ⊢ ( 𝜑 → ( ( 𝐼 ‘ 𝑎 ) · ( 𝑌 + 𝑍 ) ) = ( ( ( 𝐼 ‘ 𝑎 ) · 𝑌 ) + ( ( 𝐼 ‘ 𝑎 ) · 𝑍 ) ) )
58 1 14 13 52 15 19 27 49 20 lmodvsneg ⊢ ( 𝜑 → ( ( invg ‘ 𝑊 ) ‘ ( 𝑎 · ( 𝑌 + 𝑍 ) ) ) = ( ( 𝐼 ‘ 𝑎 ) · ( 𝑌 + 𝑍 ) ) )
59 15 19 grpinvcl ⊢ ( ( 𝑅 ∈ Grp ∧ 𝑑 ∈ 𝐵 ) → ( 𝐼 ‘ 𝑑 ) ∈ 𝐵 )
60 37 22 59 syl2anc ⊢ ( 𝜑 → ( 𝐼 ‘ 𝑑 ) ∈ 𝐵 )
61 eqid ⊢ ( LSubSp ‘ 𝑊 ) = ( LSubSp ‘ 𝑊 )
62 1 61 5 27 28 42 lspprcl ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑌 , 𝑍 } ) ∈ ( LSubSp ‘ 𝑊 ) )
63 1 12 13 14 15 5 27 39 21 28 42 lsppreli ⊢ ( 𝜑 → ( ( ( 𝐼 ‘ 𝑎 ) · 𝑌 ) + ( 𝑏 · 𝑍 ) ) ∈ ( 𝑁 ‘ { 𝑌 , 𝑍 } ) )
64 1 12 13 14 15 5 27 23 60 28 42 lsppreli ⊢ ( 𝜑 → ( ( 𝑒 · 𝑌 ) + ( ( 𝐼 ‘ 𝑑 ) · 𝑍 ) ) ∈ ( 𝑁 ‘ { 𝑌 , 𝑍 } ) )
65 1 13 14 15 2 27 22 7 42 lmodsubdi ⊢ ( 𝜑 → ( 𝑑 · ( 𝑋 − 𝑍 ) ) = ( ( 𝑑 · 𝑋 ) − ( 𝑑 · 𝑍 ) ) )
66 1 14 13 15 lmodvscl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑑 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ) → ( 𝑑 · 𝑋 ) ∈ 𝑉 )
67 27 22 7 66 syl3anc ⊢ ( 𝜑 → ( 𝑑 · 𝑋 ) ∈ 𝑉 )
68 1 12 2 13 14 15 19 27 22 67 42 lmodsubvs ⊢ ( 𝜑 → ( ( 𝑑 · 𝑋 ) − ( 𝑑 · 𝑍 ) ) = ( ( 𝑑 · 𝑋 ) + ( ( 𝐼 ‘ 𝑑 ) · 𝑍 ) ) )
69 65 68 eqtrd ⊢ ( 𝜑 → ( 𝑑 · ( 𝑋 − 𝑍 ) ) = ( ( 𝑑 · 𝑋 ) + ( ( 𝐼 ‘ 𝑑 ) · 𝑍 ) ) )
70 69 oveq1d ⊢ ( 𝜑 → ( ( 𝑑 · ( 𝑋 − 𝑍 ) ) + ( 𝑒 · 𝑌 ) ) = ( ( ( 𝑑 · 𝑋 ) + ( ( 𝐼 ‘ 𝑑 ) · 𝑍 ) ) + ( 𝑒 · 𝑌 ) ) )
71 lmodabl ⊢ ( 𝑊 ∈ LMod → 𝑊 ∈ Abel )
72 6 26 71 3syl ⊢ ( 𝜑 → 𝑊 ∈ Abel )
73 1 14 13 15 lmodvscl ⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝐼 ‘ 𝑑 ) ∈ 𝐵 ∧ 𝑍 ∈ 𝑉 ) → ( ( 𝐼 ‘ 𝑑 ) · 𝑍 ) ∈ 𝑉 )
74 27 60 42 73 syl3anc ⊢ ( 𝜑 → ( ( 𝐼 ‘ 𝑑 ) · 𝑍 ) ∈ 𝑉 )
75 1 14 13 15 lmodvscl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑒 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) → ( 𝑒 · 𝑌 ) ∈ 𝑉 )
76 27 23 28 75 syl3anc ⊢ ( 𝜑 → ( 𝑒 · 𝑌 ) ∈ 𝑉 )
77 1 12 72 67 74 76 abl32 ⊢ ( 𝜑 → ( ( ( 𝑑 · 𝑋 ) + ( ( 𝐼 ‘ 𝑑 ) · 𝑍 ) ) + ( 𝑒 · 𝑌 ) ) = ( ( ( 𝑑 · 𝑋 ) + ( 𝑒 · 𝑌 ) ) + ( ( 𝐼 ‘ 𝑑 ) · 𝑍 ) ) )
78 1 12 lmodass ⊢ ( ( 𝑊 ∈ LMod ∧ ( ( 𝑑 · 𝑋 ) ∈ 𝑉 ∧ ( 𝑒 · 𝑌 ) ∈ 𝑉 ∧ ( ( 𝐼 ‘ 𝑑 ) · 𝑍 ) ∈ 𝑉 ) ) → ( ( ( 𝑑 · 𝑋 ) + ( 𝑒 · 𝑌 ) ) + ( ( 𝐼 ‘ 𝑑 ) · 𝑍 ) ) = ( ( 𝑑 · 𝑋 ) + ( ( 𝑒 · 𝑌 ) + ( ( 𝐼 ‘ 𝑑 ) · 𝑍 ) ) ) )
79 27 67 76 74 78 syl13anc ⊢ ( 𝜑 → ( ( ( 𝑑 · 𝑋 ) + ( 𝑒 · 𝑌 ) ) + ( ( 𝐼 ‘ 𝑑 ) · 𝑍 ) ) = ( ( 𝑑 · 𝑋 ) + ( ( 𝑒 · 𝑌 ) + ( ( 𝐼 ‘ 𝑑 ) · 𝑍 ) ) ) )
80 70 77 79 3eqtrd ⊢ ( 𝜑 → ( ( 𝑑 · ( 𝑋 − 𝑍 ) ) + ( 𝑒 · 𝑌 ) ) = ( ( 𝑑 · 𝑋 ) + ( ( 𝑒 · 𝑌 ) + ( ( 𝐼 ‘ 𝑑 ) · 𝑍 ) ) ) )
81 25 47 80 3eqtr3d ⊢ ( 𝜑 → ( ( 𝑎 · 𝑋 ) + ( ( ( 𝐼 ‘ 𝑎 ) · 𝑌 ) + ( 𝑏 · 𝑍 ) ) ) = ( ( 𝑑 · 𝑋 ) + ( ( 𝑒 · 𝑌 ) + ( ( 𝐼 ‘ 𝑑 ) · 𝑍 ) ) ) )
82 1 12 14 15 13 61 6 62 7 8 63 64 20 22 81 lvecindp ⊢ ( 𝜑 → ( 𝑎 = 𝑑 ∧ ( ( ( 𝐼 ‘ 𝑎 ) · 𝑌 ) + ( 𝑏 · 𝑍 ) ) = ( ( 𝑒 · 𝑌 ) + ( ( 𝐼 ‘ 𝑑 ) · 𝑍 ) ) ) )
83 82 simprd ⊢ ( 𝜑 → ( ( ( 𝐼 ‘ 𝑎 ) · 𝑌 ) + ( 𝑏 · 𝑍 ) ) = ( ( 𝑒 · 𝑌 ) + ( ( 𝐼 ‘ 𝑑 ) · 𝑍 ) ) )
84 1 12 14 15 13 3 5 6 10 11 39 21 23 60 9 83 lvecindp2 ⊢ ( 𝜑 → ( ( 𝐼 ‘ 𝑎 ) = 𝑒 ∧ 𝑏 = ( 𝐼 ‘ 𝑑 ) ) )
85 84 simprd ⊢ ( 𝜑 → 𝑏 = ( 𝐼 ‘ 𝑑 ) )
86 82 simpld ⊢ ( 𝜑 → 𝑎 = 𝑑 )
87 86 fveq2d ⊢ ( 𝜑 → ( 𝐼 ‘ 𝑎 ) = ( 𝐼 ‘ 𝑑 ) )
88 85 87 eqtr4d ⊢ ( 𝜑 → 𝑏 = ( 𝐼 ‘ 𝑎 ) )
89 88 oveq1d ⊢ ( 𝜑 → ( 𝑏 · 𝑍 ) = ( ( 𝐼 ‘ 𝑎 ) · 𝑍 ) )
90 89 oveq2d ⊢ ( 𝜑 → ( ( ( 𝐼 ‘ 𝑎 ) · 𝑌 ) + ( 𝑏 · 𝑍 ) ) = ( ( ( 𝐼 ‘ 𝑎 ) · 𝑌 ) + ( ( 𝐼 ‘ 𝑎 ) · 𝑍 ) ) )
91 57 58 90 3eqtr4rd ⊢ ( 𝜑 → ( ( ( 𝐼 ‘ 𝑎 ) · 𝑌 ) + ( 𝑏 · 𝑍 ) ) = ( ( invg ‘ 𝑊 ) ‘ ( 𝑎 · ( 𝑌 + 𝑍 ) ) ) )
92 91 oveq2d ⊢ ( 𝜑 → ( ( 𝑎 · 𝑋 ) + ( ( ( 𝐼 ‘ 𝑎 ) · 𝑌 ) + ( 𝑏 · 𝑍 ) ) ) = ( ( 𝑎 · 𝑋 ) + ( ( invg ‘ 𝑊 ) ‘ ( 𝑎 · ( 𝑌 + 𝑍 ) ) ) ) )
93 54 55 92 3eqtr4rd ⊢ ( 𝜑 → ( ( 𝑎 · 𝑋 ) + ( ( ( 𝐼 ‘ 𝑎 ) · 𝑌 ) + ( 𝑏 · 𝑍 ) ) ) = ( 𝑎 · ( 𝑋 − ( 𝑌 + 𝑍 ) ) ) )
94 47 93 eqtrd ⊢ ( 𝜑 → 𝑗 = ( 𝑎 · ( 𝑋 − ( 𝑌 + 𝑍 ) ) ) )