Step | Hyp | Ref
| Expression |
1 | | oveq1 6556 |
. . . . . 6
⊢ (𝑥 = 0 → (𝑥 · (𝐼‘𝑋)) = (0 · (𝐼‘𝑋))) |
2 | | oveq1 6556 |
. . . . . . 7
⊢ (𝑥 = 0 → (𝑥 · 𝑋) = (0 · 𝑋)) |
3 | 2 | fveq2d 6107 |
. . . . . 6
⊢ (𝑥 = 0 → (𝐼‘(𝑥 · 𝑋)) = (𝐼‘(0 · 𝑋))) |
4 | 1, 3 | eqeq12d 2625 |
. . . . 5
⊢ (𝑥 = 0 → ((𝑥 · (𝐼‘𝑋)) = (𝐼‘(𝑥 · 𝑋)) ↔ (0 · (𝐼‘𝑋)) = (𝐼‘(0 · 𝑋)))) |
5 | | oveq1 6556 |
. . . . . 6
⊢ (𝑥 = 𝑦 → (𝑥 · (𝐼‘𝑋)) = (𝑦 · (𝐼‘𝑋))) |
6 | | oveq1 6556 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → (𝑥 · 𝑋) = (𝑦 · 𝑋)) |
7 | 6 | fveq2d 6107 |
. . . . . 6
⊢ (𝑥 = 𝑦 → (𝐼‘(𝑥 · 𝑋)) = (𝐼‘(𝑦 · 𝑋))) |
8 | 5, 7 | eqeq12d 2625 |
. . . . 5
⊢ (𝑥 = 𝑦 → ((𝑥 · (𝐼‘𝑋)) = (𝐼‘(𝑥 · 𝑋)) ↔ (𝑦 · (𝐼‘𝑋)) = (𝐼‘(𝑦 · 𝑋)))) |
9 | | oveq1 6556 |
. . . . . 6
⊢ (𝑥 = (𝑦 + 1) → (𝑥 · (𝐼‘𝑋)) = ((𝑦 + 1) · (𝐼‘𝑋))) |
10 | | oveq1 6556 |
. . . . . . 7
⊢ (𝑥 = (𝑦 + 1) → (𝑥 · 𝑋) = ((𝑦 + 1) · 𝑋)) |
11 | 10 | fveq2d 6107 |
. . . . . 6
⊢ (𝑥 = (𝑦 + 1) → (𝐼‘(𝑥 · 𝑋)) = (𝐼‘((𝑦 + 1) · 𝑋))) |
12 | 9, 11 | eqeq12d 2625 |
. . . . 5
⊢ (𝑥 = (𝑦 + 1) → ((𝑥 · (𝐼‘𝑋)) = (𝐼‘(𝑥 · 𝑋)) ↔ ((𝑦 + 1) · (𝐼‘𝑋)) = (𝐼‘((𝑦 + 1) · 𝑋)))) |
13 | | oveq1 6556 |
. . . . . 6
⊢ (𝑥 = -𝑦 → (𝑥 · (𝐼‘𝑋)) = (-𝑦 · (𝐼‘𝑋))) |
14 | | oveq1 6556 |
. . . . . . 7
⊢ (𝑥 = -𝑦 → (𝑥 · 𝑋) = (-𝑦 · 𝑋)) |
15 | 14 | fveq2d 6107 |
. . . . . 6
⊢ (𝑥 = -𝑦 → (𝐼‘(𝑥 · 𝑋)) = (𝐼‘(-𝑦 · 𝑋))) |
16 | 13, 15 | eqeq12d 2625 |
. . . . 5
⊢ (𝑥 = -𝑦 → ((𝑥 · (𝐼‘𝑋)) = (𝐼‘(𝑥 · 𝑋)) ↔ (-𝑦 · (𝐼‘𝑋)) = (𝐼‘(-𝑦 · 𝑋)))) |
17 | | oveq1 6556 |
. . . . . 6
⊢ (𝑥 = 𝑁 → (𝑥 · (𝐼‘𝑋)) = (𝑁 · (𝐼‘𝑋))) |
18 | | oveq1 6556 |
. . . . . . 7
⊢ (𝑥 = 𝑁 → (𝑥 · 𝑋) = (𝑁 · 𝑋)) |
19 | 18 | fveq2d 6107 |
. . . . . 6
⊢ (𝑥 = 𝑁 → (𝐼‘(𝑥 · 𝑋)) = (𝐼‘(𝑁 · 𝑋))) |
20 | 17, 19 | eqeq12d 2625 |
. . . . 5
⊢ (𝑥 = 𝑁 → ((𝑥 · (𝐼‘𝑋)) = (𝐼‘(𝑥 · 𝑋)) ↔ (𝑁 · (𝐼‘𝑋)) = (𝐼‘(𝑁 · 𝑋)))) |
21 | | eqid 2610 |
. . . . . . . . 9
⊢
(0g‘𝐺) = (0g‘𝐺) |
22 | | mulginvcom.i |
. . . . . . . . 9
⊢ 𝐼 = (invg‘𝐺) |
23 | 21, 22 | grpinvid 17299 |
. . . . . . . 8
⊢ (𝐺 ∈ Grp → (𝐼‘(0g‘𝐺)) = (0g‘𝐺)) |
24 | 23 | eqcomd 2616 |
. . . . . . 7
⊢ (𝐺 ∈ Grp →
(0g‘𝐺) =
(𝐼‘(0g‘𝐺))) |
25 | 24 | adantr 480 |
. . . . . 6
⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵) → (0g‘𝐺) = (𝐼‘(0g‘𝐺))) |
26 | | mulginvcom.b |
. . . . . . . 8
⊢ 𝐵 = (Base‘𝐺) |
27 | 26, 22 | grpinvcl 17290 |
. . . . . . 7
⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵) → (𝐼‘𝑋) ∈ 𝐵) |
28 | | mulginvcom.t |
. . . . . . . 8
⊢ · =
(.g‘𝐺) |
29 | 26, 21, 28 | mulg0 17369 |
. . . . . . 7
⊢ ((𝐼‘𝑋) ∈ 𝐵 → (0 · (𝐼‘𝑋)) = (0g‘𝐺)) |
30 | 27, 29 | syl 17 |
. . . . . 6
⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵) → (0 · (𝐼‘𝑋)) = (0g‘𝐺)) |
31 | 26, 21, 28 | mulg0 17369 |
. . . . . . . 8
⊢ (𝑋 ∈ 𝐵 → (0 · 𝑋) = (0g‘𝐺)) |
32 | 31 | adantl 481 |
. . . . . . 7
⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵) → (0 · 𝑋) = (0g‘𝐺)) |
33 | 32 | fveq2d 6107 |
. . . . . 6
⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵) → (𝐼‘(0 · 𝑋)) = (𝐼‘(0g‘𝐺))) |
34 | 25, 30, 33 | 3eqtr4d 2654 |
. . . . 5
⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵) → (0 · (𝐼‘𝑋)) = (𝐼‘(0 · 𝑋))) |
35 | | oveq2 6557 |
. . . . . . . . . 10
⊢ ((𝑦 · (𝐼‘𝑋)) = (𝐼‘(𝑦 · 𝑋)) → ((𝐼‘𝑋)(+g‘𝐺)(𝑦 · (𝐼‘𝑋))) = ((𝐼‘𝑋)(+g‘𝐺)(𝐼‘(𝑦 · 𝑋)))) |
36 | 35 | adantl 481 |
. . . . . . . . 9
⊢ (((𝐺 ∈ Grp ∧ 𝑦 ∈ ℕ0
∧ 𝑋 ∈ 𝐵) ∧ (𝑦 · (𝐼‘𝑋)) = (𝐼‘(𝑦 · 𝑋))) → ((𝐼‘𝑋)(+g‘𝐺)(𝑦 · (𝐼‘𝑋))) = ((𝐼‘𝑋)(+g‘𝐺)(𝐼‘(𝑦 · 𝑋)))) |
37 | | grpmnd 17252 |
. . . . . . . . . . . . 13
⊢ (𝐺 ∈ Grp → 𝐺 ∈ Mnd) |
38 | 37 | 3ad2ant1 1075 |
. . . . . . . . . . . 12
⊢ ((𝐺 ∈ Grp ∧ 𝑦 ∈ ℕ0
∧ 𝑋 ∈ 𝐵) → 𝐺 ∈ Mnd) |
39 | | simp2 1055 |
. . . . . . . . . . . 12
⊢ ((𝐺 ∈ Grp ∧ 𝑦 ∈ ℕ0
∧ 𝑋 ∈ 𝐵) → 𝑦 ∈ ℕ0) |
40 | 27 | 3adant2 1073 |
. . . . . . . . . . . 12
⊢ ((𝐺 ∈ Grp ∧ 𝑦 ∈ ℕ0
∧ 𝑋 ∈ 𝐵) → (𝐼‘𝑋) ∈ 𝐵) |
41 | | eqid 2610 |
. . . . . . . . . . . . 13
⊢
(+g‘𝐺) = (+g‘𝐺) |
42 | 26, 28, 41 | mulgnn0p1 17375 |
. . . . . . . . . . . 12
⊢ ((𝐺 ∈ Mnd ∧ 𝑦 ∈ ℕ0
∧ (𝐼‘𝑋) ∈ 𝐵) → ((𝑦 + 1) · (𝐼‘𝑋)) = ((𝑦 · (𝐼‘𝑋))(+g‘𝐺)(𝐼‘𝑋))) |
43 | 38, 39, 40, 42 | syl3anc 1318 |
. . . . . . . . . . 11
⊢ ((𝐺 ∈ Grp ∧ 𝑦 ∈ ℕ0
∧ 𝑋 ∈ 𝐵) → ((𝑦 + 1) · (𝐼‘𝑋)) = ((𝑦 · (𝐼‘𝑋))(+g‘𝐺)(𝐼‘𝑋))) |
44 | | simp1 1054 |
. . . . . . . . . . . 12
⊢ ((𝐺 ∈ Grp ∧ 𝑦 ∈ ℕ0
∧ 𝑋 ∈ 𝐵) → 𝐺 ∈ Grp) |
45 | | nn0z 11277 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ ℕ0
→ 𝑦 ∈
ℤ) |
46 | 45 | 3ad2ant2 1076 |
. . . . . . . . . . . 12
⊢ ((𝐺 ∈ Grp ∧ 𝑦 ∈ ℕ0
∧ 𝑋 ∈ 𝐵) → 𝑦 ∈ ℤ) |
47 | 26, 28, 41 | mulgaddcom 17387 |
. . . . . . . . . . . 12
⊢ ((𝐺 ∈ Grp ∧ 𝑦 ∈ ℤ ∧ (𝐼‘𝑋) ∈ 𝐵) → ((𝑦 · (𝐼‘𝑋))(+g‘𝐺)(𝐼‘𝑋)) = ((𝐼‘𝑋)(+g‘𝐺)(𝑦 · (𝐼‘𝑋)))) |
48 | 44, 46, 40, 47 | syl3anc 1318 |
. . . . . . . . . . 11
⊢ ((𝐺 ∈ Grp ∧ 𝑦 ∈ ℕ0
∧ 𝑋 ∈ 𝐵) → ((𝑦 · (𝐼‘𝑋))(+g‘𝐺)(𝐼‘𝑋)) = ((𝐼‘𝑋)(+g‘𝐺)(𝑦 · (𝐼‘𝑋)))) |
49 | 43, 48 | eqtrd 2644 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ Grp ∧ 𝑦 ∈ ℕ0
∧ 𝑋 ∈ 𝐵) → ((𝑦 + 1) · (𝐼‘𝑋)) = ((𝐼‘𝑋)(+g‘𝐺)(𝑦 · (𝐼‘𝑋)))) |
50 | 49 | adantr 480 |
. . . . . . . . 9
⊢ (((𝐺 ∈ Grp ∧ 𝑦 ∈ ℕ0
∧ 𝑋 ∈ 𝐵) ∧ (𝑦 · (𝐼‘𝑋)) = (𝐼‘(𝑦 · 𝑋))) → ((𝑦 + 1) · (𝐼‘𝑋)) = ((𝐼‘𝑋)(+g‘𝐺)(𝑦 · (𝐼‘𝑋)))) |
51 | 26, 28, 41 | mulgnn0p1 17375 |
. . . . . . . . . . . . 13
⊢ ((𝐺 ∈ Mnd ∧ 𝑦 ∈ ℕ0
∧ 𝑋 ∈ 𝐵) → ((𝑦 + 1) · 𝑋) = ((𝑦 · 𝑋)(+g‘𝐺)𝑋)) |
52 | 37, 51 | syl3an1 1351 |
. . . . . . . . . . . 12
⊢ ((𝐺 ∈ Grp ∧ 𝑦 ∈ ℕ0
∧ 𝑋 ∈ 𝐵) → ((𝑦 + 1) · 𝑋) = ((𝑦 · 𝑋)(+g‘𝐺)𝑋)) |
53 | 52 | fveq2d 6107 |
. . . . . . . . . . 11
⊢ ((𝐺 ∈ Grp ∧ 𝑦 ∈ ℕ0
∧ 𝑋 ∈ 𝐵) → (𝐼‘((𝑦 + 1) · 𝑋)) = (𝐼‘((𝑦 · 𝑋)(+g‘𝐺)𝑋))) |
54 | 26, 28 | mulgcl 17382 |
. . . . . . . . . . . . 13
⊢ ((𝐺 ∈ Grp ∧ 𝑦 ∈ ℤ ∧ 𝑋 ∈ 𝐵) → (𝑦 · 𝑋) ∈ 𝐵) |
55 | 45, 54 | syl3an2 1352 |
. . . . . . . . . . . 12
⊢ ((𝐺 ∈ Grp ∧ 𝑦 ∈ ℕ0
∧ 𝑋 ∈ 𝐵) → (𝑦 · 𝑋) ∈ 𝐵) |
56 | 26, 41, 22 | grpinvadd 17316 |
. . . . . . . . . . . 12
⊢ ((𝐺 ∈ Grp ∧ (𝑦 · 𝑋) ∈ 𝐵 ∧ 𝑋 ∈ 𝐵) → (𝐼‘((𝑦 · 𝑋)(+g‘𝐺)𝑋)) = ((𝐼‘𝑋)(+g‘𝐺)(𝐼‘(𝑦 · 𝑋)))) |
57 | 55, 56 | syld3an2 1365 |
. . . . . . . . . . 11
⊢ ((𝐺 ∈ Grp ∧ 𝑦 ∈ ℕ0
∧ 𝑋 ∈ 𝐵) → (𝐼‘((𝑦 · 𝑋)(+g‘𝐺)𝑋)) = ((𝐼‘𝑋)(+g‘𝐺)(𝐼‘(𝑦 · 𝑋)))) |
58 | 53, 57 | eqtrd 2644 |
. . . . . . . . . 10
⊢ ((𝐺 ∈ Grp ∧ 𝑦 ∈ ℕ0
∧ 𝑋 ∈ 𝐵) → (𝐼‘((𝑦 + 1) · 𝑋)) = ((𝐼‘𝑋)(+g‘𝐺)(𝐼‘(𝑦 · 𝑋)))) |
59 | 58 | adantr 480 |
. . . . . . . . 9
⊢ (((𝐺 ∈ Grp ∧ 𝑦 ∈ ℕ0
∧ 𝑋 ∈ 𝐵) ∧ (𝑦 · (𝐼‘𝑋)) = (𝐼‘(𝑦 · 𝑋))) → (𝐼‘((𝑦 + 1) · 𝑋)) = ((𝐼‘𝑋)(+g‘𝐺)(𝐼‘(𝑦 · 𝑋)))) |
60 | 36, 50, 59 | 3eqtr4d 2654 |
. . . . . . . 8
⊢ (((𝐺 ∈ Grp ∧ 𝑦 ∈ ℕ0
∧ 𝑋 ∈ 𝐵) ∧ (𝑦 · (𝐼‘𝑋)) = (𝐼‘(𝑦 · 𝑋))) → ((𝑦 + 1) · (𝐼‘𝑋)) = (𝐼‘((𝑦 + 1) · 𝑋))) |
61 | 60 | 3exp1 1275 |
. . . . . . 7
⊢ (𝐺 ∈ Grp → (𝑦 ∈ ℕ0
→ (𝑋 ∈ 𝐵 → ((𝑦 · (𝐼‘𝑋)) = (𝐼‘(𝑦 · 𝑋)) → ((𝑦 + 1) · (𝐼‘𝑋)) = (𝐼‘((𝑦 + 1) · 𝑋)))))) |
62 | 61 | com23 84 |
. . . . . 6
⊢ (𝐺 ∈ Grp → (𝑋 ∈ 𝐵 → (𝑦 ∈ ℕ0 → ((𝑦 · (𝐼‘𝑋)) = (𝐼‘(𝑦 · 𝑋)) → ((𝑦 + 1) · (𝐼‘𝑋)) = (𝐼‘((𝑦 + 1) · 𝑋)))))) |
63 | 62 | imp 444 |
. . . . 5
⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵) → (𝑦 ∈ ℕ0 → ((𝑦 · (𝐼‘𝑋)) = (𝐼‘(𝑦 · 𝑋)) → ((𝑦 + 1) · (𝐼‘𝑋)) = (𝐼‘((𝑦 + 1) · 𝑋))))) |
64 | | nnz 11276 |
. . . . . 6
⊢ (𝑦 ∈ ℕ → 𝑦 ∈
ℤ) |
65 | 27 | 3adant2 1073 |
. . . . . . . . . . . 12
⊢ ((𝐺 ∈ Grp ∧ 𝑦 ∈ ℤ ∧ 𝑋 ∈ 𝐵) → (𝐼‘𝑋) ∈ 𝐵) |
66 | 26, 28, 22 | mulgneg 17383 |
. . . . . . . . . . . 12
⊢ ((𝐺 ∈ Grp ∧ 𝑦 ∈ ℤ ∧ (𝐼‘𝑋) ∈ 𝐵) → (-𝑦 · (𝐼‘𝑋)) = (𝐼‘(𝑦 · (𝐼‘𝑋)))) |
67 | 65, 66 | syld3an3 1363 |
. . . . . . . . . . 11
⊢ ((𝐺 ∈ Grp ∧ 𝑦 ∈ ℤ ∧ 𝑋 ∈ 𝐵) → (-𝑦 · (𝐼‘𝑋)) = (𝐼‘(𝑦 · (𝐼‘𝑋)))) |
68 | 67 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝐺 ∈ Grp ∧ 𝑦 ∈ ℤ ∧ 𝑋 ∈ 𝐵) ∧ (𝑦 · (𝐼‘𝑋)) = (𝐼‘(𝑦 · 𝑋))) → (-𝑦 · (𝐼‘𝑋)) = (𝐼‘(𝑦 · (𝐼‘𝑋)))) |
69 | 26, 28, 22 | mulgneg 17383 |
. . . . . . . . . . . . 13
⊢ ((𝐺 ∈ Grp ∧ 𝑦 ∈ ℤ ∧ 𝑋 ∈ 𝐵) → (-𝑦 · 𝑋) = (𝐼‘(𝑦 · 𝑋))) |
70 | 69 | adantr 480 |
. . . . . . . . . . . 12
⊢ (((𝐺 ∈ Grp ∧ 𝑦 ∈ ℤ ∧ 𝑋 ∈ 𝐵) ∧ (𝑦 · (𝐼‘𝑋)) = (𝐼‘(𝑦 · 𝑋))) → (-𝑦 · 𝑋) = (𝐼‘(𝑦 · 𝑋))) |
71 | | simpr 476 |
. . . . . . . . . . . 12
⊢ (((𝐺 ∈ Grp ∧ 𝑦 ∈ ℤ ∧ 𝑋 ∈ 𝐵) ∧ (𝑦 · (𝐼‘𝑋)) = (𝐼‘(𝑦 · 𝑋))) → (𝑦 · (𝐼‘𝑋)) = (𝐼‘(𝑦 · 𝑋))) |
72 | 70, 71 | eqtr4d 2647 |
. . . . . . . . . . 11
⊢ (((𝐺 ∈ Grp ∧ 𝑦 ∈ ℤ ∧ 𝑋 ∈ 𝐵) ∧ (𝑦 · (𝐼‘𝑋)) = (𝐼‘(𝑦 · 𝑋))) → (-𝑦 · 𝑋) = (𝑦 · (𝐼‘𝑋))) |
73 | 72 | fveq2d 6107 |
. . . . . . . . . 10
⊢ (((𝐺 ∈ Grp ∧ 𝑦 ∈ ℤ ∧ 𝑋 ∈ 𝐵) ∧ (𝑦 · (𝐼‘𝑋)) = (𝐼‘(𝑦 · 𝑋))) → (𝐼‘(-𝑦 · 𝑋)) = (𝐼‘(𝑦 · (𝐼‘𝑋)))) |
74 | 68, 73 | eqtr4d 2647 |
. . . . . . . . 9
⊢ (((𝐺 ∈ Grp ∧ 𝑦 ∈ ℤ ∧ 𝑋 ∈ 𝐵) ∧ (𝑦 · (𝐼‘𝑋)) = (𝐼‘(𝑦 · 𝑋))) → (-𝑦 · (𝐼‘𝑋)) = (𝐼‘(-𝑦 · 𝑋))) |
75 | 74 | 3exp1 1275 |
. . . . . . . 8
⊢ (𝐺 ∈ Grp → (𝑦 ∈ ℤ → (𝑋 ∈ 𝐵 → ((𝑦 · (𝐼‘𝑋)) = (𝐼‘(𝑦 · 𝑋)) → (-𝑦 · (𝐼‘𝑋)) = (𝐼‘(-𝑦 · 𝑋)))))) |
76 | 75 | com23 84 |
. . . . . . 7
⊢ (𝐺 ∈ Grp → (𝑋 ∈ 𝐵 → (𝑦 ∈ ℤ → ((𝑦 · (𝐼‘𝑋)) = (𝐼‘(𝑦 · 𝑋)) → (-𝑦 · (𝐼‘𝑋)) = (𝐼‘(-𝑦 · 𝑋)))))) |
77 | 76 | imp 444 |
. . . . . 6
⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵) → (𝑦 ∈ ℤ → ((𝑦 · (𝐼‘𝑋)) = (𝐼‘(𝑦 · 𝑋)) → (-𝑦 · (𝐼‘𝑋)) = (𝐼‘(-𝑦 · 𝑋))))) |
78 | 64, 77 | syl5 33 |
. . . . 5
⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵) → (𝑦 ∈ ℕ → ((𝑦 · (𝐼‘𝑋)) = (𝐼‘(𝑦 · 𝑋)) → (-𝑦 · (𝐼‘𝑋)) = (𝐼‘(-𝑦 · 𝑋))))) |
79 | 4, 8, 12, 16, 20, 34, 63, 78 | zindd 11354 |
. . . 4
⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵) → (𝑁 ∈ ℤ → (𝑁 · (𝐼‘𝑋)) = (𝐼‘(𝑁 · 𝑋)))) |
80 | 79 | ex 449 |
. . 3
⊢ (𝐺 ∈ Grp → (𝑋 ∈ 𝐵 → (𝑁 ∈ ℤ → (𝑁 · (𝐼‘𝑋)) = (𝐼‘(𝑁 · 𝑋))))) |
81 | 80 | com23 84 |
. 2
⊢ (𝐺 ∈ Grp → (𝑁 ∈ ℤ → (𝑋 ∈ 𝐵 → (𝑁 · (𝐼‘𝑋)) = (𝐼‘(𝑁 · 𝑋))))) |
82 | 81 | 3imp 1249 |
1
⊢ ((𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) → (𝑁 · (𝐼‘𝑋)) = (𝐼‘(𝑁 · 𝑋))) |