Metamath Proof Explorer

Theorem baerlem3lem1

Description: Lemma for baerlem3 . (Contributed by NM, 9-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 ‘ 𝑅 )
baerlem3.a1 ⊢ ( 𝜑 → 𝑎 ∈ 𝐵 )
baerlem3.b1 ⊢ ( 𝜑 → 𝑏 ∈ 𝐵 )
baerlem3.d1 ⊢ ( 𝜑 → 𝑑 ∈ 𝐵 )
baerlem3.e1 ⊢ ( 𝜑 → 𝑒 ∈ 𝐵 )
baerlem3.j1 ⊢ ( 𝜑 → 𝑗 = ( ( 𝑎 · 𝑌 ) + ( 𝑏 · 𝑍 ) ) )
baerlem3.j2 ⊢ ( 𝜑 → 𝑗 = ( ( 𝑑 · ( 𝑋 − 𝑌 ) ) + ( 𝑒 · ( 𝑋 − 𝑍 ) ) ) )
Assertion baerlem3lem1 ( 𝜑 → 𝑗 = ( 𝑎 · ( 𝑌 − 𝑍 ) ) )

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 baerlem3.a1 ⊢ ( 𝜑 → 𝑎 ∈ 𝐵 )
21 baerlem3.b1 ⊢ ( 𝜑 → 𝑏 ∈ 𝐵 )
22 baerlem3.d1 ⊢ ( 𝜑 → 𝑑 ∈ 𝐵 )
23 baerlem3.e1 ⊢ ( 𝜑 → 𝑒 ∈ 𝐵 )
24 baerlem3.j1 ⊢ ( 𝜑 → 𝑗 = ( ( 𝑎 · 𝑌 ) + ( 𝑏 · 𝑍 ) ) )
25 baerlem3.j2 ⊢ ( 𝜑 → 𝑗 = ( ( 𝑑 · ( 𝑋 − 𝑌 ) ) + ( 𝑒 · ( 𝑋 − 𝑍 ) ) ) )
26 lveclmod ⊢ ( 𝑊 ∈ LVec → 𝑊 ∈ LMod )
27 6 26 syl ⊢ ( 𝜑 → 𝑊 ∈ LMod )
28 10 eldifad ⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
29 1 14 13 15 lmodvscl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑎 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) → ( 𝑎 · 𝑌 ) ∈ 𝑉 )
30 27 20 28 29 syl3anc ⊢ ( 𝜑 → ( 𝑎 · 𝑌 ) ∈ 𝑉 )
31 11 eldifad ⊢ ( 𝜑 → 𝑍 ∈ 𝑉 )
32 1 14 13 15 lmodvscl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑎 ∈ 𝐵 ∧ 𝑍 ∈ 𝑉 ) → ( 𝑎 · 𝑍 ) ∈ 𝑉 )
33 27 20 31 32 syl3anc ⊢ ( 𝜑 → ( 𝑎 · 𝑍 ) ∈ 𝑉 )
34 eqid ⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
35 1 12 2 14 13 19 34 lmodvsubval2 ⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝑎 · 𝑌 ) ∈ 𝑉 ∧ ( 𝑎 · 𝑍 ) ∈ 𝑉 ) → ( ( 𝑎 · 𝑌 ) − ( 𝑎 · 𝑍 ) ) = ( ( 𝑎 · 𝑌 ) + ( ( 𝐼 ‘ ( 1r ‘ 𝑅 ) ) · ( 𝑎 · 𝑍 ) ) ) )
36 27 30 33 35 syl3anc ⊢ ( 𝜑 → ( ( 𝑎 · 𝑌 ) − ( 𝑎 · 𝑍 ) ) = ( ( 𝑎 · 𝑌 ) + ( ( 𝐼 ‘ ( 1r ‘ 𝑅 ) ) · ( 𝑎 · 𝑍 ) ) ) )
37 1 13 14 15 2 27 20 28 31 lmodsubdi ⊢ ( 𝜑 → ( 𝑎 · ( 𝑌 − 𝑍 ) ) = ( ( 𝑎 · 𝑌 ) − ( 𝑎 · 𝑍 ) ) )
38 14 lmodring ⊢ ( 𝑊 ∈ LMod → 𝑅 ∈ Ring )
39 27 38 syl ⊢ ( 𝜑 → 𝑅 ∈ Ring )
40 ringgrp ⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ Grp )
41 39 40 syl ⊢ ( 𝜑 → 𝑅 ∈ Grp )
42 14 15 34 lmod1cl ⊢ ( 𝑊 ∈ LMod → ( 1r ‘ 𝑅 ) ∈ 𝐵 )
43 27 42 syl ⊢ ( 𝜑 → ( 1r ‘ 𝑅 ) ∈ 𝐵 )
44 15 19 grpinvcl ⊢ ( ( 𝑅 ∈ Grp ∧ ( 1r ‘ 𝑅 ) ∈ 𝐵 ) → ( 𝐼 ‘ ( 1r ‘ 𝑅 ) ) ∈ 𝐵 )
45 41 43 44 syl2anc ⊢ ( 𝜑 → ( 𝐼 ‘ ( 1r ‘ 𝑅 ) ) ∈ 𝐵 )
46 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
47 1 14 13 15 46 lmodvsass ⊢ ( ( 𝑊 ∈ LMod ∧ ( ( 𝐼 ‘ ( 1r ‘ 𝑅 ) ) ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑍 ∈ 𝑉 ) ) → ( ( ( 𝐼 ‘ ( 1r ‘ 𝑅 ) ) ( .r ‘ 𝑅 ) 𝑎 ) · 𝑍 ) = ( ( 𝐼 ‘ ( 1r ‘ 𝑅 ) ) · ( 𝑎 · 𝑍 ) ) )
48 27 45 20 31 47 syl13anc ⊢ ( 𝜑 → ( ( ( 𝐼 ‘ ( 1r ‘ 𝑅 ) ) ( .r ‘ 𝑅 ) 𝑎 ) · 𝑍 ) = ( ( 𝐼 ‘ ( 1r ‘ 𝑅 ) ) · ( 𝑎 · 𝑍 ) ) )
49 15 46 34 19 39 20 ringnegl ⊢ ( 𝜑 → ( ( 𝐼 ‘ ( 1r ‘ 𝑅 ) ) ( .r ‘ 𝑅 ) 𝑎 ) = ( 𝐼 ‘ 𝑎 ) )
50 ringabl ⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ Abel )
51 39 50 syl ⊢ ( 𝜑 → 𝑅 ∈ Abel )
52 15 16 19 ablinvadd ⊢ ( ( 𝑅 ∈ Abel ∧ 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝐵 ) → ( 𝐼 ‘ ( 𝑑 ⨣ 𝑒 ) ) = ( ( 𝐼 ‘ 𝑑 ) ⨣ ( 𝐼 ‘ 𝑒 ) ) )
53 51 22 23 52 syl3anc ⊢ ( 𝜑 → ( 𝐼 ‘ ( 𝑑 ⨣ 𝑒 ) ) = ( ( 𝐼 ‘ 𝑑 ) ⨣ ( 𝐼 ‘ 𝑒 ) ) )
54 eqid ⊢ ( LSubSp ‘ 𝑊 ) = ( LSubSp ‘ 𝑊 )
55 1 54 5 27 28 31 lspprcl ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑌 , 𝑍 } ) ∈ ( LSubSp ‘ 𝑊 ) )
56 1 12 13 14 15 5 27 20 21 28 31 lsppreli ⊢ ( 𝜑 → ( ( 𝑎 · 𝑌 ) + ( 𝑏 · 𝑍 ) ) ∈ ( 𝑁 ‘ { 𝑌 , 𝑍 } ) )
57 1 12 13 14 15 5 27 22 23 28 31 lsppreli ⊢ ( 𝜑 → ( ( 𝑑 · 𝑌 ) + ( 𝑒 · 𝑍 ) ) ∈ ( 𝑁 ‘ { 𝑌 , 𝑍 } ) )
58 eqid ⊢ ( invg ‘ 𝑊 ) = ( invg ‘ 𝑊 )
59 54 58 lssvnegcl ⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝑁 ‘ { 𝑌 , 𝑍 } ) ∈ ( LSubSp ‘ 𝑊 ) ∧ ( ( 𝑑 · 𝑌 ) + ( 𝑒 · 𝑍 ) ) ∈ ( 𝑁 ‘ { 𝑌 , 𝑍 } ) ) → ( ( invg ‘ 𝑊 ) ‘ ( ( 𝑑 · 𝑌 ) + ( 𝑒 · 𝑍 ) ) ) ∈ ( 𝑁 ‘ { 𝑌 , 𝑍 } ) )
60 27 55 57 59 syl3anc ⊢ ( 𝜑 → ( ( invg ‘ 𝑊 ) ‘ ( ( 𝑑 · 𝑌 ) + ( 𝑒 · 𝑍 ) ) ) ∈ ( 𝑁 ‘ { 𝑌 , 𝑍 } ) )
61 15 18 ring0cl ⊢ ( 𝑅 ∈ Ring → 𝑄 ∈ 𝐵 )
62 39 61 syl ⊢ ( 𝜑 → 𝑄 ∈ 𝐵 )
63 15 16 ringacl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝐵 ) → ( 𝑑 ⨣ 𝑒 ) ∈ 𝐵 )
64 39 22 23 63 syl3anc ⊢ ( 𝜑 → ( 𝑑 ⨣ 𝑒 ) ∈ 𝐵 )
65 1 14 13 18 3 lmod0vs ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ) → ( 𝑄 · 𝑋 ) = 0 )
66 27 7 65 syl2anc ⊢ ( 𝜑 → ( 𝑄 · 𝑋 ) = 0 )
67 66 oveq1d ⊢ ( 𝜑 → ( ( 𝑄 · 𝑋 ) + ( ( 𝑎 · 𝑌 ) + ( 𝑏 · 𝑍 ) ) ) = ( 0 + ( ( 𝑎 · 𝑌 ) + ( 𝑏 · 𝑍 ) ) ) )
68 lmodgrp ⊢ ( 𝑊 ∈ LMod → 𝑊 ∈ Grp )
69 27 68 syl ⊢ ( 𝜑 → 𝑊 ∈ Grp )
70 1 14 13 15 lmodvscl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑏 ∈ 𝐵 ∧ 𝑍 ∈ 𝑉 ) → ( 𝑏 · 𝑍 ) ∈ 𝑉 )
71 27 21 31 70 syl3anc ⊢ ( 𝜑 → ( 𝑏 · 𝑍 ) ∈ 𝑉 )
72 1 12 lmodvacl ⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝑎 · 𝑌 ) ∈ 𝑉 ∧ ( 𝑏 · 𝑍 ) ∈ 𝑉 ) → ( ( 𝑎 · 𝑌 ) + ( 𝑏 · 𝑍 ) ) ∈ 𝑉 )
73 27 30 71 72 syl3anc ⊢ ( 𝜑 → ( ( 𝑎 · 𝑌 ) + ( 𝑏 · 𝑍 ) ) ∈ 𝑉 )
74 1 12 3 grplid ⊢ ( ( 𝑊 ∈ Grp ∧ ( ( 𝑎 · 𝑌 ) + ( 𝑏 · 𝑍 ) ) ∈ 𝑉 ) → ( 0 + ( ( 𝑎 · 𝑌 ) + ( 𝑏 · 𝑍 ) ) ) = ( ( 𝑎 · 𝑌 ) + ( 𝑏 · 𝑍 ) ) )
75 69 73 74 syl2anc ⊢ ( 𝜑 → ( 0 + ( ( 𝑎 · 𝑌 ) + ( 𝑏 · 𝑍 ) ) ) = ( ( 𝑎 · 𝑌 ) + ( 𝑏 · 𝑍 ) ) )
76 lmodabl ⊢ ( 𝑊 ∈ LMod → 𝑊 ∈ Abel )
77 27 76 syl ⊢ ( 𝜑 → 𝑊 ∈ Abel )
78 1 14 13 15 lmodvscl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑑 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ) → ( 𝑑 · 𝑋 ) ∈ 𝑉 )
79 27 22 7 78 syl3anc ⊢ ( 𝜑 → ( 𝑑 · 𝑋 ) ∈ 𝑉 )
80 1 14 13 15 lmodvscl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑒 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ) → ( 𝑒 · 𝑋 ) ∈ 𝑉 )
81 27 23 7 80 syl3anc ⊢ ( 𝜑 → ( 𝑒 · 𝑋 ) ∈ 𝑉 )
82 1 14 13 15 lmodvscl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑑 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) → ( 𝑑 · 𝑌 ) ∈ 𝑉 )
83 27 22 28 82 syl3anc ⊢ ( 𝜑 → ( 𝑑 · 𝑌 ) ∈ 𝑉 )
84 1 14 13 15 lmodvscl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑒 ∈ 𝐵 ∧ 𝑍 ∈ 𝑉 ) → ( 𝑒 · 𝑍 ) ∈ 𝑉 )
85 27 23 31 84 syl3anc ⊢ ( 𝜑 → ( 𝑒 · 𝑍 ) ∈ 𝑉 )
86 1 12 2 ablsub4 ⊢ ( ( 𝑊 ∈ Abel ∧ ( ( 𝑑 · 𝑋 ) ∈ 𝑉 ∧ ( 𝑒 · 𝑋 ) ∈ 𝑉 ) ∧ ( ( 𝑑 · 𝑌 ) ∈ 𝑉 ∧ ( 𝑒 · 𝑍 ) ∈ 𝑉 ) ) → ( ( ( 𝑑 · 𝑋 ) + ( 𝑒 · 𝑋 ) ) − ( ( 𝑑 · 𝑌 ) + ( 𝑒 · 𝑍 ) ) ) = ( ( ( 𝑑 · 𝑋 ) − ( 𝑑 · 𝑌 ) ) + ( ( 𝑒 · 𝑋 ) − ( 𝑒 · 𝑍 ) ) ) )
87 77 79 81 83 85 86 syl122anc ⊢ ( 𝜑 → ( ( ( 𝑑 · 𝑋 ) + ( 𝑒 · 𝑋 ) ) − ( ( 𝑑 · 𝑌 ) + ( 𝑒 · 𝑍 ) ) ) = ( ( ( 𝑑 · 𝑋 ) − ( 𝑑 · 𝑌 ) ) + ( ( 𝑒 · 𝑋 ) − ( 𝑒 · 𝑍 ) ) ) )
88 1 12 14 13 15 16 lmodvsdir ⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ) ) → ( ( 𝑑 ⨣ 𝑒 ) · 𝑋 ) = ( ( 𝑑 · 𝑋 ) + ( 𝑒 · 𝑋 ) ) )
89 27 22 23 7 88 syl13anc ⊢ ( 𝜑 → ( ( 𝑑 ⨣ 𝑒 ) · 𝑋 ) = ( ( 𝑑 · 𝑋 ) + ( 𝑒 · 𝑋 ) ) )
90 89 oveq1d ⊢ ( 𝜑 → ( ( ( 𝑑 ⨣ 𝑒 ) · 𝑋 ) − ( ( 𝑑 · 𝑌 ) + ( 𝑒 · 𝑍 ) ) ) = ( ( ( 𝑑 · 𝑋 ) + ( 𝑒 · 𝑋 ) ) − ( ( 𝑑 · 𝑌 ) + ( 𝑒 · 𝑍 ) ) ) )
91 1 13 14 15 2 27 22 7 28 lmodsubdi ⊢ ( 𝜑 → ( 𝑑 · ( 𝑋 − 𝑌 ) ) = ( ( 𝑑 · 𝑋 ) − ( 𝑑 · 𝑌 ) ) )
92 1 13 14 15 2 27 23 7 31 lmodsubdi ⊢ ( 𝜑 → ( 𝑒 · ( 𝑋 − 𝑍 ) ) = ( ( 𝑒 · 𝑋 ) − ( 𝑒 · 𝑍 ) ) )
93 91 92 oveq12d ⊢ ( 𝜑 → ( ( 𝑑 · ( 𝑋 − 𝑌 ) ) + ( 𝑒 · ( 𝑋 − 𝑍 ) ) ) = ( ( ( 𝑑 · 𝑋 ) − ( 𝑑 · 𝑌 ) ) + ( ( 𝑒 · 𝑋 ) − ( 𝑒 · 𝑍 ) ) ) )
94 25 93 eqtrd ⊢ ( 𝜑 → 𝑗 = ( ( ( 𝑑 · 𝑋 ) − ( 𝑑 · 𝑌 ) ) + ( ( 𝑒 · 𝑋 ) − ( 𝑒 · 𝑍 ) ) ) )
95 87 90 94 3eqtr4rd ⊢ ( 𝜑 → 𝑗 = ( ( ( 𝑑 ⨣ 𝑒 ) · 𝑋 ) − ( ( 𝑑 · 𝑌 ) + ( 𝑒 · 𝑍 ) ) ) )
96 1 14 13 15 lmodvscl ⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝑑 ⨣ 𝑒 ) ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ) → ( ( 𝑑 ⨣ 𝑒 ) · 𝑋 ) ∈ 𝑉 )
97 27 64 7 96 syl3anc ⊢ ( 𝜑 → ( ( 𝑑 ⨣ 𝑒 ) · 𝑋 ) ∈ 𝑉 )
98 1 12 lmodvacl ⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝑑 · 𝑌 ) ∈ 𝑉 ∧ ( 𝑒 · 𝑍 ) ∈ 𝑉 ) → ( ( 𝑑 · 𝑌 ) + ( 𝑒 · 𝑍 ) ) ∈ 𝑉 )
99 27 83 85 98 syl3anc ⊢ ( 𝜑 → ( ( 𝑑 · 𝑌 ) + ( 𝑒 · 𝑍 ) ) ∈ 𝑉 )
100 1 12 58 2 grpsubval ⊢ ( ( ( ( 𝑑 ⨣ 𝑒 ) · 𝑋 ) ∈ 𝑉 ∧ ( ( 𝑑 · 𝑌 ) + ( 𝑒 · 𝑍 ) ) ∈ 𝑉 ) → ( ( ( 𝑑 ⨣ 𝑒 ) · 𝑋 ) − ( ( 𝑑 · 𝑌 ) + ( 𝑒 · 𝑍 ) ) ) = ( ( ( 𝑑 ⨣ 𝑒 ) · 𝑋 ) + ( ( invg ‘ 𝑊 ) ‘ ( ( 𝑑 · 𝑌 ) + ( 𝑒 · 𝑍 ) ) ) ) )
101 97 99 100 syl2anc ⊢ ( 𝜑 → ( ( ( 𝑑 ⨣ 𝑒 ) · 𝑋 ) − ( ( 𝑑 · 𝑌 ) + ( 𝑒 · 𝑍 ) ) ) = ( ( ( 𝑑 ⨣ 𝑒 ) · 𝑋 ) + ( ( invg ‘ 𝑊 ) ‘ ( ( 𝑑 · 𝑌 ) + ( 𝑒 · 𝑍 ) ) ) ) )
102 95 24 101 3eqtr3d ⊢ ( 𝜑 → ( ( 𝑎 · 𝑌 ) + ( 𝑏 · 𝑍 ) ) = ( ( ( 𝑑 ⨣ 𝑒 ) · 𝑋 ) + ( ( invg ‘ 𝑊 ) ‘ ( ( 𝑑 · 𝑌 ) + ( 𝑒 · 𝑍 ) ) ) ) )
103 67 75 102 3eqtrd ⊢ ( 𝜑 → ( ( 𝑄 · 𝑋 ) + ( ( 𝑎 · 𝑌 ) + ( 𝑏 · 𝑍 ) ) ) = ( ( ( 𝑑 ⨣ 𝑒 ) · 𝑋 ) + ( ( invg ‘ 𝑊 ) ‘ ( ( 𝑑 · 𝑌 ) + ( 𝑒 · 𝑍 ) ) ) ) )
104 1 12 14 15 13 54 6 55 7 8 56 60 62 64 103 lvecindp ⊢ ( 𝜑 → ( 𝑄 = ( 𝑑 ⨣ 𝑒 ) ∧ ( ( 𝑎 · 𝑌 ) + ( 𝑏 · 𝑍 ) ) = ( ( invg ‘ 𝑊 ) ‘ ( ( 𝑑 · 𝑌 ) + ( 𝑒 · 𝑍 ) ) ) ) )
105 104 simpld ⊢ ( 𝜑 → 𝑄 = ( 𝑑 ⨣ 𝑒 ) )
106 105 fveq2d ⊢ ( 𝜑 → ( 𝐼 ‘ 𝑄 ) = ( 𝐼 ‘ ( 𝑑 ⨣ 𝑒 ) ) )
107 15 19 grpinvcl ⊢ ( ( 𝑅 ∈ Grp ∧ 𝑑 ∈ 𝐵 ) → ( 𝐼 ‘ 𝑑 ) ∈ 𝐵 )
108 41 22 107 syl2anc ⊢ ( 𝜑 → ( 𝐼 ‘ 𝑑 ) ∈ 𝐵 )
109 15 19 grpinvcl ⊢ ( ( 𝑅 ∈ Grp ∧ 𝑒 ∈ 𝐵 ) → ( 𝐼 ‘ 𝑒 ) ∈ 𝐵 )
110 41 23 109 syl2anc ⊢ ( 𝜑 → ( 𝐼 ‘ 𝑒 ) ∈ 𝐵 )
111 104 simprd ⊢ ( 𝜑 → ( ( 𝑎 · 𝑌 ) + ( 𝑏 · 𝑍 ) ) = ( ( invg ‘ 𝑊 ) ‘ ( ( 𝑑 · 𝑌 ) + ( 𝑒 · 𝑍 ) ) ) )
112 1 12 13 58 14 15 19 27 22 23 28 31 lmodnegadd ⊢ ( 𝜑 → ( ( invg ‘ 𝑊 ) ‘ ( ( 𝑑 · 𝑌 ) + ( 𝑒 · 𝑍 ) ) ) = ( ( ( 𝐼 ‘ 𝑑 ) · 𝑌 ) + ( ( 𝐼 ‘ 𝑒 ) · 𝑍 ) ) )
113 111 112 eqtrd ⊢ ( 𝜑 → ( ( 𝑎 · 𝑌 ) + ( 𝑏 · 𝑍 ) ) = ( ( ( 𝐼 ‘ 𝑑 ) · 𝑌 ) + ( ( 𝐼 ‘ 𝑒 ) · 𝑍 ) ) )
114 1 12 14 15 13 3 5 6 10 11 20 21 108 110 9 113 lvecindp2 ⊢ ( 𝜑 → ( 𝑎 = ( 𝐼 ‘ 𝑑 ) ∧ 𝑏 = ( 𝐼 ‘ 𝑒 ) ) )
115 oveq12 ⊢ ( ( 𝑎 = ( 𝐼 ‘ 𝑑 ) ∧ 𝑏 = ( 𝐼 ‘ 𝑒 ) ) → ( 𝑎 ⨣ 𝑏 ) = ( ( 𝐼 ‘ 𝑑 ) ⨣ ( 𝐼 ‘ 𝑒 ) ) )
116 114 115 syl ⊢ ( 𝜑 → ( 𝑎 ⨣ 𝑏 ) = ( ( 𝐼 ‘ 𝑑 ) ⨣ ( 𝐼 ‘ 𝑒 ) ) )
117 53 106 116 3eqtr4rd ⊢ ( 𝜑 → ( 𝑎 ⨣ 𝑏 ) = ( 𝐼 ‘ 𝑄 ) )
118 18 19 grpinvid ⊢ ( 𝑅 ∈ Grp → ( 𝐼 ‘ 𝑄 ) = 𝑄 )
119 41 118 syl ⊢ ( 𝜑 → ( 𝐼 ‘ 𝑄 ) = 𝑄 )
120 117 119 eqtrd ⊢ ( 𝜑 → ( 𝑎 ⨣ 𝑏 ) = 𝑄 )
121 15 16 18 19 grpinvid1 ⊢ ( ( 𝑅 ∈ Grp ∧ 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) → ( ( 𝐼 ‘ 𝑎 ) = 𝑏 ↔ ( 𝑎 ⨣ 𝑏 ) = 𝑄 ) )
122 41 20 21 121 syl3anc ⊢ ( 𝜑 → ( ( 𝐼 ‘ 𝑎 ) = 𝑏 ↔ ( 𝑎 ⨣ 𝑏 ) = 𝑄 ) )
123 120 122 mpbird ⊢ ( 𝜑 → ( 𝐼 ‘ 𝑎 ) = 𝑏 )
124 49 123 eqtrd ⊢ ( 𝜑 → ( ( 𝐼 ‘ ( 1r ‘ 𝑅 ) ) ( .r ‘ 𝑅 ) 𝑎 ) = 𝑏 )
125 124 oveq1d ⊢ ( 𝜑 → ( ( ( 𝐼 ‘ ( 1r ‘ 𝑅 ) ) ( .r ‘ 𝑅 ) 𝑎 ) · 𝑍 ) = ( 𝑏 · 𝑍 ) )
126 48 125 eqtr3d ⊢ ( 𝜑 → ( ( 𝐼 ‘ ( 1r ‘ 𝑅 ) ) · ( 𝑎 · 𝑍 ) ) = ( 𝑏 · 𝑍 ) )
127 126 oveq2d ⊢ ( 𝜑 → ( ( 𝑎 · 𝑌 ) + ( ( 𝐼 ‘ ( 1r ‘ 𝑅 ) ) · ( 𝑎 · 𝑍 ) ) ) = ( ( 𝑎 · 𝑌 ) + ( 𝑏 · 𝑍 ) ) )
128 24 127 eqtr4d ⊢ ( 𝜑 → 𝑗 = ( ( 𝑎 · 𝑌 ) + ( ( 𝐼 ‘ ( 1r ‘ 𝑅 ) ) · ( 𝑎 · 𝑍 ) ) ) )
129 36 37 128 3eqtr4rd ⊢ ( 𝜑 → 𝑗 = ( 𝑎 · ( 𝑌 − 𝑍 ) ) )