Step | Hyp | Ref
| Expression |
1 | | simpl 483 |
. . . . 5
β’ ((π β βMod β§ (πΆ β π β§ π· β π)) β π β βMod) |
2 | | eqid 2732 |
. . . . . . 7
β’
(Scalarβπ) =
(Scalarβπ) |
3 | | eqid 2732 |
. . . . . . 7
β’
(Baseβ(Scalarβπ)) = (Baseβ(Scalarβπ)) |
4 | 2, 3 | clmneg1 24822 |
. . . . . 6
β’ (π β βMod β -1
β (Baseβ(Scalarβπ))) |
5 | 4 | adantr 481 |
. . . . 5
β’ ((π β βMod β§ (πΆ β π β§ π· β π)) β -1 β
(Baseβ(Scalarβπ))) |
6 | | simpl 483 |
. . . . . 6
β’ ((πΆ β π β§ π· β π) β πΆ β π) |
7 | 6 | adantl 482 |
. . . . 5
β’ ((π β βMod β§ (πΆ β π β§ π· β π)) β πΆ β π) |
8 | | simpr 485 |
. . . . . 6
β’ ((πΆ β π β§ π· β π) β π· β π) |
9 | 8 | adantl 482 |
. . . . 5
β’ ((π β βMod β§ (πΆ β π β§ π· β π)) β π· β π) |
10 | | clmpm1dir.v |
. . . . . 6
β’ π = (Baseβπ) |
11 | | clmpm1dir.s |
. . . . . 6
β’ Β· = (
Β·π βπ) |
12 | | clmpm1dir.a |
. . . . . 6
β’ + =
(+gβπ) |
13 | 10, 2, 11, 3, 12 | clmvsdi 24832 |
. . . . 5
β’ ((π β βMod β§ (-1
β (Baseβ(Scalarβπ)) β§ πΆ β π β§ π· β π)) β (-1 Β· (πΆ + π·)) = ((-1 Β· πΆ) + (-1 Β· π·))) |
14 | 1, 5, 7, 9, 13 | syl13anc 1372 |
. . . 4
β’ ((π β βMod β§ (πΆ β π β§ π· β π)) β (-1 Β· (πΆ + π·)) = ((-1 Β· πΆ) + (-1 Β· π·))) |
15 | 14 | 3adant2 1131 |
. . 3
β’ ((π β βMod β§ (π΄ β π β§ π΅ β π) β§ (πΆ β π β§ π· β π)) β (-1 Β· (πΆ + π·)) = ((-1 Β· πΆ) + (-1 Β· π·))) |
16 | 15 | oveq2d 7427 |
. 2
β’ ((π β βMod β§ (π΄ β π β§ π΅ β π) β§ (πΆ β π β§ π· β π)) β ((π΄ + π΅) + (-1 Β· (πΆ + π·))) = ((π΄ + π΅) + ((-1 Β· πΆ) + (-1 Β· π·)))) |
17 | | clmabl 24809 |
. . . . 5
β’ (π β βMod β π β Abel) |
18 | | ablcmn 19696 |
. . . . 5
β’ (π β Abel β π β CMnd) |
19 | 17, 18 | syl 17 |
. . . 4
β’ (π β βMod β π β CMnd) |
20 | 19 | 3ad2ant1 1133 |
. . 3
β’ ((π β βMod β§ (π΄ β π β§ π΅ β π) β§ (πΆ β π β§ π· β π)) β π β CMnd) |
21 | | simp2 1137 |
. . 3
β’ ((π β βMod β§ (π΄ β π β§ π΅ β π) β§ (πΆ β π β§ π· β π)) β (π΄ β π β§ π΅ β π)) |
22 | | simpl 483 |
. . . . . 6
β’ ((π β βMod β§ πΆ β π) β π β βMod) |
23 | 4 | adantr 481 |
. . . . . 6
β’ ((π β βMod β§ πΆ β π) β -1 β
(Baseβ(Scalarβπ))) |
24 | | simpr 485 |
. . . . . 6
β’ ((π β βMod β§ πΆ β π) β πΆ β π) |
25 | 10, 2, 11, 3 | clmvscl 24828 |
. . . . . 6
β’ ((π β βMod β§ -1
β (Baseβ(Scalarβπ)) β§ πΆ β π) β (-1 Β· πΆ) β π) |
26 | 22, 23, 24, 25 | syl3anc 1371 |
. . . . 5
β’ ((π β βMod β§ πΆ β π) β (-1 Β· πΆ) β π) |
27 | | simpl 483 |
. . . . . 6
β’ ((π β βMod β§ π· β π) β π β βMod) |
28 | 4 | adantr 481 |
. . . . . 6
β’ ((π β βMod β§ π· β π) β -1 β
(Baseβ(Scalarβπ))) |
29 | | simpr 485 |
. . . . . 6
β’ ((π β βMod β§ π· β π) β π· β π) |
30 | 10, 2, 11, 3 | clmvscl 24828 |
. . . . . 6
β’ ((π β βMod β§ -1
β (Baseβ(Scalarβπ)) β§ π· β π) β (-1 Β· π·) β π) |
31 | 27, 28, 29, 30 | syl3anc 1371 |
. . . . 5
β’ ((π β βMod β§ π· β π) β (-1 Β· π·) β π) |
32 | 26, 31 | anim12dan 619 |
. . . 4
β’ ((π β βMod β§ (πΆ β π β§ π· β π)) β ((-1 Β· πΆ) β π β§ (-1 Β· π·) β π)) |
33 | 32 | 3adant2 1131 |
. . 3
β’ ((π β βMod β§ (π΄ β π β§ π΅ β π) β§ (πΆ β π β§ π· β π)) β ((-1 Β· πΆ) β π β§ (-1 Β· π·) β π)) |
34 | 10, 12 | cmn4 19710 |
. . 3
β’ ((π β CMnd β§ (π΄ β π β§ π΅ β π) β§ ((-1 Β· πΆ) β π β§ (-1 Β· π·) β π)) β ((π΄ + π΅) + ((-1 Β· πΆ) + (-1 Β· π·))) = ((π΄ + (-1 Β· πΆ)) + (π΅ + (-1 Β· π·)))) |
35 | 20, 21, 33, 34 | syl3anc 1371 |
. 2
β’ ((π β βMod β§ (π΄ β π β§ π΅ β π) β§ (πΆ β π β§ π· β π)) β ((π΄ + π΅) + ((-1 Β· πΆ) + (-1 Β· π·))) = ((π΄ + (-1 Β· πΆ)) + (π΅ + (-1 Β· π·)))) |
36 | 16, 35 | eqtrd 2772 |
1
β’ ((π β βMod β§ (π΄ β π β§ π΅ β π) β§ (πΆ β π β§ π· β π)) β ((π΄ + π΅) + (-1 Β· (πΆ + π·))) = ((π΄ + (-1 Β· πΆ)) + (π΅ + (-1 Β· π·)))) |