Step | Hyp | Ref
| Expression |
1 | | simp1 1135 |
. . 3
β’ ((π β βMod β§ π΄ β π β§ π΅ β π) β π β βMod) |
2 | | eqid 2731 |
. . . . 5
β’
(Scalarβπ) =
(Scalarβπ) |
3 | | eqid 2731 |
. . . . 5
β’
(Baseβ(Scalarβπ)) = (Baseβ(Scalarβπ)) |
4 | 2, 3 | clmneg1 24830 |
. . . 4
β’ (π β βMod β -1
β (Baseβ(Scalarβπ))) |
5 | 4 | 3ad2ant1 1132 |
. . 3
β’ ((π β βMod β§ π΄ β π β§ π΅ β π) β -1 β
(Baseβ(Scalarβπ))) |
6 | | simp2 1136 |
. . 3
β’ ((π β βMod β§ π΄ β π β§ π΅ β π) β π΄ β π) |
7 | | simpl 482 |
. . . . 5
β’ ((π β βMod β§ π΅ β π) β π β βMod) |
8 | 4 | adantr 480 |
. . . . 5
β’ ((π β βMod β§ π΅ β π) β -1 β
(Baseβ(Scalarβπ))) |
9 | | simpr 484 |
. . . . 5
β’ ((π β βMod β§ π΅ β π) β π΅ β π) |
10 | | clmpm1dir.v |
. . . . . 6
β’ π = (Baseβπ) |
11 | | clmpm1dir.s |
. . . . . 6
β’ Β· = (
Β·π βπ) |
12 | 10, 2, 11, 3 | clmvscl 24836 |
. . . . 5
β’ ((π β βMod β§ -1
β (Baseβ(Scalarβπ)) β§ π΅ β π) β (-1 Β· π΅) β π) |
13 | 7, 8, 9, 12 | syl3anc 1370 |
. . . 4
β’ ((π β βMod β§ π΅ β π) β (-1 Β· π΅) β π) |
14 | 13 | 3adant2 1130 |
. . 3
β’ ((π β βMod β§ π΄ β π β§ π΅ β π) β (-1 Β· π΅) β π) |
15 | | clmpm1dir.a |
. . . 4
β’ + =
(+gβπ) |
16 | 10, 2, 11, 3, 15 | clmvsdi 24840 |
. . 3
β’ ((π β βMod β§ (-1
β (Baseβ(Scalarβπ)) β§ π΄ β π β§ (-1 Β· π΅) β π)) β (-1 Β· (π΄ + (-1 Β· π΅))) = ((-1 Β· π΄) + (-1 Β· (-1 Β· π΅)))) |
17 | 1, 5, 6, 14, 16 | syl13anc 1371 |
. 2
β’ ((π β βMod β§ π΄ β π β§ π΅ β π) β (-1 Β· (π΄ + (-1 Β· π΅))) = ((-1 Β· π΄) + (-1 Β· (-1 Β· π΅)))) |
18 | 10, 11, 15 | clmnegneg 24852 |
. . . 4
β’ ((π β βMod β§ π΅ β π) β (-1 Β· (-1 Β· π΅)) = π΅) |
19 | 18 | 3adant2 1130 |
. . 3
β’ ((π β βMod β§ π΄ β π β§ π΅ β π) β (-1 Β· (-1 Β· π΅)) = π΅) |
20 | 19 | oveq2d 7428 |
. 2
β’ ((π β βMod β§ π΄ β π β§ π΅ β π) β ((-1 Β· π΄) + (-1 Β· (-1 Β· π΅))) = ((-1 Β· π΄) + π΅)) |
21 | | clmabl 24817 |
. . . 4
β’ (π β βMod β π β Abel) |
22 | 21 | 3ad2ant1 1132 |
. . 3
β’ ((π β βMod β§ π΄ β π β§ π΅ β π) β π β Abel) |
23 | | simpl 482 |
. . . . 5
β’ ((π β βMod β§ π΄ β π) β π β βMod) |
24 | 4 | adantr 480 |
. . . . 5
β’ ((π β βMod β§ π΄ β π) β -1 β
(Baseβ(Scalarβπ))) |
25 | | simpr 484 |
. . . . 5
β’ ((π β βMod β§ π΄ β π) β π΄ β π) |
26 | 10, 2, 11, 3 | clmvscl 24836 |
. . . . 5
β’ ((π β βMod β§ -1
β (Baseβ(Scalarβπ)) β§ π΄ β π) β (-1 Β· π΄) β π) |
27 | 23, 24, 25, 26 | syl3anc 1370 |
. . . 4
β’ ((π β βMod β§ π΄ β π) β (-1 Β· π΄) β π) |
28 | 27 | 3adant3 1131 |
. . 3
β’ ((π β βMod β§ π΄ β π β§ π΅ β π) β (-1 Β· π΄) β π) |
29 | | simp3 1137 |
. . 3
β’ ((π β βMod β§ π΄ β π β§ π΅ β π) β π΅ β π) |
30 | 10, 15 | ablcom 19709 |
. . 3
β’ ((π β Abel β§ (-1 Β· π΄) β π β§ π΅ β π) β ((-1 Β· π΄) + π΅) = (π΅ + (-1 Β· π΄))) |
31 | 22, 28, 29, 30 | syl3anc 1370 |
. 2
β’ ((π β βMod β§ π΄ β π β§ π΅ β π) β ((-1 Β· π΄) + π΅) = (π΅ + (-1 Β· π΄))) |
32 | 17, 20, 31 | 3eqtrd 2775 |
1
β’ ((π β βMod β§ π΄ β π β§ π΅ β π) β (-1 Β· (π΄ + (-1 Β· π΅))) = (π΅ + (-1 Β· π΄))) |