Step | Hyp | Ref
| Expression |
1 | | oveq1 7416 |
. . . . 5
β’ (π₯ = 0 β (π₯ β π΅) = (0 β π΅)) |
2 | | oveq1 7416 |
. . . . 5
β’ (π₯ = 0 β (π₯ Β· π΅) = (0 Β· π΅)) |
3 | 1, 2 | eqeq12d 2749 |
. . . 4
β’ (π₯ = 0 β ((π₯ β π΅) = (π₯ Β· π΅) β (0 β π΅) = (0 Β· π΅))) |
4 | | oveq1 7416 |
. . . . 5
β’ (π₯ = π¦ β (π₯ β π΅) = (π¦ β π΅)) |
5 | | oveq1 7416 |
. . . . 5
β’ (π₯ = π¦ β (π₯ Β· π΅) = (π¦ Β· π΅)) |
6 | 4, 5 | eqeq12d 2749 |
. . . 4
β’ (π₯ = π¦ β ((π₯ β π΅) = (π₯ Β· π΅) β (π¦ β π΅) = (π¦ Β· π΅))) |
7 | | oveq1 7416 |
. . . . 5
β’ (π₯ = (π¦ + 1) β (π₯ β π΅) = ((π¦ + 1) β π΅)) |
8 | | oveq1 7416 |
. . . . 5
β’ (π₯ = (π¦ + 1) β (π₯ Β· π΅) = ((π¦ + 1) Β· π΅)) |
9 | 7, 8 | eqeq12d 2749 |
. . . 4
β’ (π₯ = (π¦ + 1) β ((π₯ β π΅) = (π₯ Β· π΅) β ((π¦ + 1) β π΅) = ((π¦ + 1) Β· π΅))) |
10 | | oveq1 7416 |
. . . . 5
β’ (π₯ = -π¦ β (π₯ β π΅) = (-π¦ β π΅)) |
11 | | oveq1 7416 |
. . . . 5
β’ (π₯ = -π¦ β (π₯ Β· π΅) = (-π¦ Β· π΅)) |
12 | 10, 11 | eqeq12d 2749 |
. . . 4
β’ (π₯ = -π¦ β ((π₯ β π΅) = (π₯ Β· π΅) β (-π¦ β π΅) = (-π¦ Β· π΅))) |
13 | | oveq1 7416 |
. . . . 5
β’ (π₯ = π΄ β (π₯ β π΅) = (π΄ β π΅)) |
14 | | oveq1 7416 |
. . . . 5
β’ (π₯ = π΄ β (π₯ Β· π΅) = (π΄ Β· π΅)) |
15 | 13, 14 | eqeq12d 2749 |
. . . 4
β’ (π₯ = π΄ β ((π₯ β π΅) = (π₯ Β· π΅) β (π΄ β π΅) = (π΄ Β· π΅))) |
16 | | clmmulg.1 |
. . . . . . 7
β’ π = (Baseβπ) |
17 | | eqid 2733 |
. . . . . . 7
β’
(0gβπ) = (0gβπ) |
18 | | clmmulg.2 |
. . . . . . 7
β’ β =
(.gβπ) |
19 | 16, 17, 18 | mulg0 18957 |
. . . . . 6
β’ (π΅ β π β (0 β π΅) = (0gβπ)) |
20 | 19 | adantl 483 |
. . . . 5
β’ ((π β βMod β§ π΅ β π) β (0 β π΅) = (0gβπ)) |
21 | | eqid 2733 |
. . . . . 6
β’
(Scalarβπ) =
(Scalarβπ) |
22 | | clmmulg.3 |
. . . . . 6
β’ Β· = (
Β·π βπ) |
23 | 16, 21, 22, 17 | clm0vs 24611 |
. . . . 5
β’ ((π β βMod β§ π΅ β π) β (0 Β· π΅) = (0gβπ)) |
24 | 20, 23 | eqtr4d 2776 |
. . . 4
β’ ((π β βMod β§ π΅ β π) β (0 β π΅) = (0 Β· π΅)) |
25 | | oveq1 7416 |
. . . . . 6
β’ ((π¦ β π΅) = (π¦ Β· π΅) β ((π¦ β π΅)(+gβπ)π΅) = ((π¦ Β· π΅)(+gβπ)π΅)) |
26 | | clmgrp 24584 |
. . . . . . . . . 10
β’ (π β βMod β π β Grp) |
27 | 26 | grpmndd 18832 |
. . . . . . . . 9
β’ (π β βMod β π β Mnd) |
28 | 27 | ad2antrr 725 |
. . . . . . . 8
β’ (((π β βMod β§ π΅ β π) β§ π¦ β β0) β π β Mnd) |
29 | | simpr 486 |
. . . . . . . 8
β’ (((π β βMod β§ π΅ β π) β§ π¦ β β0) β π¦ β
β0) |
30 | | simplr 768 |
. . . . . . . 8
β’ (((π β βMod β§ π΅ β π) β§ π¦ β β0) β π΅ β π) |
31 | | eqid 2733 |
. . . . . . . . 9
β’
(+gβπ) = (+gβπ) |
32 | 16, 18, 31 | mulgnn0p1 18965 |
. . . . . . . 8
β’ ((π β Mnd β§ π¦ β β0
β§ π΅ β π) β ((π¦ + 1) β π΅) = ((π¦ β π΅)(+gβπ)π΅)) |
33 | 28, 29, 30, 32 | syl3anc 1372 |
. . . . . . 7
β’ (((π β βMod β§ π΅ β π) β§ π¦ β β0) β ((π¦ + 1) β π΅) = ((π¦ β π΅)(+gβπ)π΅)) |
34 | | simpll 766 |
. . . . . . . . 9
β’ (((π β βMod β§ π΅ β π) β§ π¦ β β0) β π β
βMod) |
35 | | eqid 2733 |
. . . . . . . . . . . 12
β’
(Baseβ(Scalarβπ)) = (Baseβ(Scalarβπ)) |
36 | 21, 35 | clmzss 24594 |
. . . . . . . . . . 11
β’ (π β βMod β
β€ β (Baseβ(Scalarβπ))) |
37 | 36 | ad2antrr 725 |
. . . . . . . . . 10
β’ (((π β βMod β§ π΅ β π) β§ π¦ β β0) β β€
β (Baseβ(Scalarβπ))) |
38 | | nn0z 12583 |
. . . . . . . . . . 11
β’ (π¦ β β0
β π¦ β
β€) |
39 | 38 | adantl 483 |
. . . . . . . . . 10
β’ (((π β βMod β§ π΅ β π) β§ π¦ β β0) β π¦ β
β€) |
40 | 37, 39 | sseldd 3984 |
. . . . . . . . 9
β’ (((π β βMod β§ π΅ β π) β§ π¦ β β0) β π¦ β
(Baseβ(Scalarβπ))) |
41 | | 1zzd 12593 |
. . . . . . . . . 10
β’ (((π β βMod β§ π΅ β π) β§ π¦ β β0) β 1 β
β€) |
42 | 37, 41 | sseldd 3984 |
. . . . . . . . 9
β’ (((π β βMod β§ π΅ β π) β§ π¦ β β0) β 1 β
(Baseβ(Scalarβπ))) |
43 | 16, 21, 22, 35, 31 | clmvsdir 24607 |
. . . . . . . . 9
β’ ((π β βMod β§ (π¦ β
(Baseβ(Scalarβπ)) β§ 1 β
(Baseβ(Scalarβπ)) β§ π΅ β π)) β ((π¦ + 1) Β· π΅) = ((π¦ Β· π΅)(+gβπ)(1 Β· π΅))) |
44 | 34, 40, 42, 30, 43 | syl13anc 1373 |
. . . . . . . 8
β’ (((π β βMod β§ π΅ β π) β§ π¦ β β0) β ((π¦ + 1) Β· π΅) = ((π¦ Β· π΅)(+gβπ)(1 Β· π΅))) |
45 | 16, 22 | clmvs1 24609 |
. . . . . . . . . 10
β’ ((π β βMod β§ π΅ β π) β (1 Β· π΅) = π΅) |
46 | 45 | adantr 482 |
. . . . . . . . 9
β’ (((π β βMod β§ π΅ β π) β§ π¦ β β0) β (1 Β· π΅) = π΅) |
47 | 46 | oveq2d 7425 |
. . . . . . . 8
β’ (((π β βMod β§ π΅ β π) β§ π¦ β β0) β ((π¦ Β· π΅)(+gβπ)(1 Β· π΅)) = ((π¦ Β· π΅)(+gβπ)π΅)) |
48 | 44, 47 | eqtrd 2773 |
. . . . . . 7
β’ (((π β βMod β§ π΅ β π) β§ π¦ β β0) β ((π¦ + 1) Β· π΅) = ((π¦ Β· π΅)(+gβπ)π΅)) |
49 | 33, 48 | eqeq12d 2749 |
. . . . . 6
β’ (((π β βMod β§ π΅ β π) β§ π¦ β β0) β (((π¦ + 1) β π΅) = ((π¦ + 1) Β· π΅) β ((π¦ β π΅)(+gβπ)π΅) = ((π¦ Β· π΅)(+gβπ)π΅))) |
50 | 25, 49 | imbitrrid 245 |
. . . . 5
β’ (((π β βMod β§ π΅ β π) β§ π¦ β β0) β ((π¦ β π΅) = (π¦ Β· π΅) β ((π¦ + 1) β π΅) = ((π¦ + 1) Β· π΅))) |
51 | 50 | ex 414 |
. . . 4
β’ ((π β βMod β§ π΅ β π) β (π¦ β β0 β ((π¦ β π΅) = (π¦ Β· π΅) β ((π¦ + 1) β π΅) = ((π¦ + 1) Β· π΅)))) |
52 | | fveq2 6892 |
. . . . . 6
β’ ((π¦ β π΅) = (π¦ Β· π΅) β ((invgβπ)β(π¦ β π΅)) = ((invgβπ)β(π¦ Β· π΅))) |
53 | 26 | ad2antrr 725 |
. . . . . . . 8
β’ (((π β βMod β§ π΅ β π) β§ π¦ β β) β π β Grp) |
54 | | nnz 12579 |
. . . . . . . . 9
β’ (π¦ β β β π¦ β
β€) |
55 | 54 | adantl 483 |
. . . . . . . 8
β’ (((π β βMod β§ π΅ β π) β§ π¦ β β) β π¦ β β€) |
56 | | simplr 768 |
. . . . . . . 8
β’ (((π β βMod β§ π΅ β π) β§ π¦ β β) β π΅ β π) |
57 | | eqid 2733 |
. . . . . . . . 9
β’
(invgβπ) = (invgβπ) |
58 | 16, 18, 57 | mulgneg 18972 |
. . . . . . . 8
β’ ((π β Grp β§ π¦ β β€ β§ π΅ β π) β (-π¦ β π΅) = ((invgβπ)β(π¦ β π΅))) |
59 | 53, 55, 56, 58 | syl3anc 1372 |
. . . . . . 7
β’ (((π β βMod β§ π΅ β π) β§ π¦ β β) β (-π¦ β π΅) = ((invgβπ)β(π¦ β π΅))) |
60 | | simpll 766 |
. . . . . . . . 9
β’ (((π β βMod β§ π΅ β π) β§ π¦ β β) β π β βMod) |
61 | 36 | ad2antrr 725 |
. . . . . . . . . 10
β’ (((π β βMod β§ π΅ β π) β§ π¦ β β) β β€ β
(Baseβ(Scalarβπ))) |
62 | 61, 55 | sseldd 3984 |
. . . . . . . . 9
β’ (((π β βMod β§ π΅ β π) β§ π¦ β β) β π¦ β (Baseβ(Scalarβπ))) |
63 | 16, 21, 22, 57, 35, 60, 56, 62 | clmvsneg 24616 |
. . . . . . . 8
β’ (((π β βMod β§ π΅ β π) β§ π¦ β β) β
((invgβπ)β(π¦ Β· π΅)) = (-π¦ Β· π΅)) |
64 | 63 | eqcomd 2739 |
. . . . . . 7
β’ (((π β βMod β§ π΅ β π) β§ π¦ β β) β (-π¦ Β· π΅) = ((invgβπ)β(π¦ Β· π΅))) |
65 | 59, 64 | eqeq12d 2749 |
. . . . . 6
β’ (((π β βMod β§ π΅ β π) β§ π¦ β β) β ((-π¦ β π΅) = (-π¦ Β· π΅) β ((invgβπ)β(π¦ β π΅)) = ((invgβπ)β(π¦ Β· π΅)))) |
66 | 52, 65 | imbitrrid 245 |
. . . . 5
β’ (((π β βMod β§ π΅ β π) β§ π¦ β β) β ((π¦ β π΅) = (π¦ Β· π΅) β (-π¦ β π΅) = (-π¦ Β· π΅))) |
67 | 66 | ex 414 |
. . . 4
β’ ((π β βMod β§ π΅ β π) β (π¦ β β β ((π¦ β π΅) = (π¦ Β· π΅) β (-π¦ β π΅) = (-π¦ Β· π΅)))) |
68 | 3, 6, 9, 12, 15, 24, 51, 67 | zindd 12663 |
. . 3
β’ ((π β βMod β§ π΅ β π) β (π΄ β β€ β (π΄ β π΅) = (π΄ Β· π΅))) |
69 | 68 | 3impia 1118 |
. 2
β’ ((π β βMod β§ π΅ β π β§ π΄ β β€) β (π΄ β π΅) = (π΄ Β· π΅)) |
70 | 69 | 3com23 1127 |
1
β’ ((π β βMod β§ π΄ β β€ β§ π΅ β π) β (π΄ β π΅) = (π΄ Β· π΅)) |