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 |
⊢ ( 𝜑 → 𝑗 = ( 𝑎 · ( 𝑌 − 𝑍 ) ) ) |