| Step | Hyp | Ref
| Expression |
| 1 | | idomnnzpownz.4 |
. . 3
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
| 2 | 1 | ancli 548 |
. 2
⊢ (𝜑 → (𝜑 ∧ 𝑁 ∈
ℕ0)) |
| 3 | | oveq1 7438 |
. . . 4
⊢ (𝑥 = 0 → (𝑥 ↑ 𝐴) = (0 ↑ 𝐴)) |
| 4 | 3 | neeq1d 3000 |
. . 3
⊢ (𝑥 = 0 → ((𝑥 ↑ 𝐴) ≠ (0g‘𝑅) ↔ (0 ↑ 𝐴) ≠ (0g‘𝑅))) |
| 5 | | oveq1 7438 |
. . . 4
⊢ (𝑥 = 𝑦 → (𝑥 ↑ 𝐴) = (𝑦 ↑ 𝐴)) |
| 6 | 5 | neeq1d 3000 |
. . 3
⊢ (𝑥 = 𝑦 → ((𝑥 ↑ 𝐴) ≠ (0g‘𝑅) ↔ (𝑦 ↑ 𝐴) ≠ (0g‘𝑅))) |
| 7 | | oveq1 7438 |
. . . 4
⊢ (𝑥 = (𝑦 + 1) → (𝑥 ↑ 𝐴) = ((𝑦 + 1) ↑ 𝐴)) |
| 8 | 7 | neeq1d 3000 |
. . 3
⊢ (𝑥 = (𝑦 + 1) → ((𝑥 ↑ 𝐴) ≠ (0g‘𝑅) ↔ ((𝑦 + 1) ↑ 𝐴) ≠ (0g‘𝑅))) |
| 9 | | oveq1 7438 |
. . . 4
⊢ (𝑥 = 𝑁 → (𝑥 ↑ 𝐴) = (𝑁 ↑ 𝐴)) |
| 10 | 9 | neeq1d 3000 |
. . 3
⊢ (𝑥 = 𝑁 → ((𝑥 ↑ 𝐴) ≠ (0g‘𝑅) ↔ (𝑁 ↑ 𝐴) ≠ (0g‘𝑅))) |
| 11 | | idomnnzpownz.2 |
. . . . . . 7
⊢ (𝜑 → 𝐴 ∈ (Base‘𝑅)) |
| 12 | | eqid 2737 |
. . . . . . . 8
⊢
(mulGrp‘𝑅) =
(mulGrp‘𝑅) |
| 13 | | eqid 2737 |
. . . . . . . 8
⊢
(Base‘𝑅) =
(Base‘𝑅) |
| 14 | 12, 13 | mgpbas 20142 |
. . . . . . 7
⊢
(Base‘𝑅) =
(Base‘(mulGrp‘𝑅)) |
| 15 | 11, 14 | eleqtrdi 2851 |
. . . . . 6
⊢ (𝜑 → 𝐴 ∈ (Base‘(mulGrp‘𝑅))) |
| 16 | | eqid 2737 |
. . . . . . 7
⊢
(Base‘(mulGrp‘𝑅)) = (Base‘(mulGrp‘𝑅)) |
| 17 | | eqid 2737 |
. . . . . . 7
⊢
(0g‘(mulGrp‘𝑅)) =
(0g‘(mulGrp‘𝑅)) |
| 18 | | idomnnzpownz.5 |
. . . . . . 7
⊢ ↑ =
(.g‘(mulGrp‘𝑅)) |
| 19 | 16, 17, 18 | mulg0 19092 |
. . . . . 6
⊢ (𝐴 ∈
(Base‘(mulGrp‘𝑅)) → (0 ↑ 𝐴) = (0g‘(mulGrp‘𝑅))) |
| 20 | 15, 19 | syl 17 |
. . . . 5
⊢ (𝜑 → (0 ↑ 𝐴) = (0g‘(mulGrp‘𝑅))) |
| 21 | | eqid 2737 |
. . . . . 6
⊢
(1r‘𝑅) = (1r‘𝑅) |
| 22 | 12, 21 | ringidval 20180 |
. . . . 5
⊢
(1r‘𝑅) = (0g‘(mulGrp‘𝑅)) |
| 23 | 20, 22 | eqtr4di 2795 |
. . . 4
⊢ (𝜑 → (0 ↑ 𝐴) = (1r‘𝑅)) |
| 24 | | idomnnzpownz.1 |
. . . . 5
⊢ (𝜑 → 𝑅 ∈ IDomn) |
| 25 | | isidom 20725 |
. . . . . 6
⊢ (𝑅 ∈ IDomn ↔ (𝑅 ∈ CRing ∧ 𝑅 ∈ Domn)) |
| 26 | 25 | simprbi 496 |
. . . . 5
⊢ (𝑅 ∈ IDomn → 𝑅 ∈ Domn) |
| 27 | | domnnzr 20706 |
. . . . 5
⊢ (𝑅 ∈ Domn → 𝑅 ∈ NzRing) |
| 28 | | eqid 2737 |
. . . . . 6
⊢
(0g‘𝑅) = (0g‘𝑅) |
| 29 | 21, 28 | nzrnz 20515 |
. . . . 5
⊢ (𝑅 ∈ NzRing →
(1r‘𝑅)
≠ (0g‘𝑅)) |
| 30 | 24, 26, 27, 29 | 4syl 19 |
. . . 4
⊢ (𝜑 → (1r‘𝑅) ≠
(0g‘𝑅)) |
| 31 | 23, 30 | eqnetrd 3008 |
. . 3
⊢ (𝜑 → (0 ↑ 𝐴) ≠ (0g‘𝑅)) |
| 32 | 24 | idomringd 20728 |
. . . . . . . 8
⊢ (𝜑 → 𝑅 ∈ Ring) |
| 33 | 12 | ringmgp 20236 |
. . . . . . . 8
⊢ (𝑅 ∈ Ring →
(mulGrp‘𝑅) ∈
Mnd) |
| 34 | 32, 33 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (mulGrp‘𝑅) ∈ Mnd) |
| 35 | 34 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ ℕ0) →
(mulGrp‘𝑅) ∈
Mnd) |
| 36 | 35 | adantr 480 |
. . . . 5
⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑦 ↑ 𝐴) ≠ (0g‘𝑅)) → (mulGrp‘𝑅) ∈ Mnd) |
| 37 | | simplr 769 |
. . . . 5
⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑦 ↑ 𝐴) ≠ (0g‘𝑅)) → 𝑦 ∈ ℕ0) |
| 38 | 15 | ad2antrr 726 |
. . . . 5
⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑦 ↑ 𝐴) ≠ (0g‘𝑅)) → 𝐴 ∈ (Base‘(mulGrp‘𝑅))) |
| 39 | | eqid 2737 |
. . . . . 6
⊢
(+g‘(mulGrp‘𝑅)) =
(+g‘(mulGrp‘𝑅)) |
| 40 | 16, 18, 39 | mulgnn0p1 19103 |
. . . . 5
⊢
(((mulGrp‘𝑅)
∈ Mnd ∧ 𝑦 ∈
ℕ0 ∧ 𝐴
∈ (Base‘(mulGrp‘𝑅))) → ((𝑦 + 1) ↑ 𝐴) = ((𝑦 ↑ 𝐴)(+g‘(mulGrp‘𝑅))𝐴)) |
| 41 | 36, 37, 38, 40 | syl3anc 1373 |
. . . 4
⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑦 ↑ 𝐴) ≠ (0g‘𝑅)) → ((𝑦 + 1) ↑ 𝐴) = ((𝑦 ↑ 𝐴)(+g‘(mulGrp‘𝑅))𝐴)) |
| 42 | | eqid 2737 |
. . . . . . . . 9
⊢
(.r‘𝑅) = (.r‘𝑅) |
| 43 | 12, 42 | mgpplusg 20141 |
. . . . . . . 8
⊢
(.r‘𝑅) = (+g‘(mulGrp‘𝑅)) |
| 44 | 43 | a1i 11 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑦 ↑ 𝐴) ≠ (0g‘𝑅)) →
(.r‘𝑅) =
(+g‘(mulGrp‘𝑅))) |
| 45 | 44 | eqcomd 2743 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑦 ↑ 𝐴) ≠ (0g‘𝑅)) →
(+g‘(mulGrp‘𝑅)) = (.r‘𝑅)) |
| 46 | 45 | oveqd 7448 |
. . . . 5
⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑦 ↑ 𝐴) ≠ (0g‘𝑅)) → ((𝑦 ↑ 𝐴)(+g‘(mulGrp‘𝑅))𝐴) = ((𝑦 ↑ 𝐴)(.r‘𝑅)𝐴)) |
| 47 | 24, 26 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝑅 ∈ Domn) |
| 48 | 47 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ ℕ0) → 𝑅 ∈ Domn) |
| 49 | 48 | adantr 480 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑦 ↑ 𝐴) ≠ (0g‘𝑅)) → 𝑅 ∈ Domn) |
| 50 | 16, 18 | mulgnn0cl 19108 |
. . . . . . . . 9
⊢
(((mulGrp‘𝑅)
∈ Mnd ∧ 𝑦 ∈
ℕ0 ∧ 𝐴
∈ (Base‘(mulGrp‘𝑅))) → (𝑦 ↑ 𝐴) ∈ (Base‘(mulGrp‘𝑅))) |
| 51 | 36, 37, 38, 50 | syl3anc 1373 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑦 ↑ 𝐴) ≠ (0g‘𝑅)) → (𝑦 ↑ 𝐴) ∈ (Base‘(mulGrp‘𝑅))) |
| 52 | 14 | eqcomi 2746 |
. . . . . . . . 9
⊢
(Base‘(mulGrp‘𝑅)) = (Base‘𝑅) |
| 53 | 52 | a1i 11 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑦 ↑ 𝐴) ≠ (0g‘𝑅)) →
(Base‘(mulGrp‘𝑅)) = (Base‘𝑅)) |
| 54 | 51, 53 | eleqtrd 2843 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑦 ↑ 𝐴) ≠ (0g‘𝑅)) → (𝑦 ↑ 𝐴) ∈ (Base‘𝑅)) |
| 55 | | simpr 484 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑦 ↑ 𝐴) ≠ (0g‘𝑅)) → (𝑦 ↑ 𝐴) ≠ (0g‘𝑅)) |
| 56 | 54, 55 | jca 511 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑦 ↑ 𝐴) ≠ (0g‘𝑅)) → ((𝑦 ↑ 𝐴) ∈ (Base‘𝑅) ∧ (𝑦 ↑ 𝐴) ≠ (0g‘𝑅))) |
| 57 | | idomnnzpownz.3 |
. . . . . . . . 9
⊢ (𝜑 → 𝐴 ≠ (0g‘𝑅)) |
| 58 | 11, 57 | jca 511 |
. . . . . . . 8
⊢ (𝜑 → (𝐴 ∈ (Base‘𝑅) ∧ 𝐴 ≠ (0g‘𝑅))) |
| 59 | 58 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ ℕ0) → (𝐴 ∈ (Base‘𝑅) ∧ 𝐴 ≠ (0g‘𝑅))) |
| 60 | 59 | adantr 480 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑦 ↑ 𝐴) ≠ (0g‘𝑅)) → (𝐴 ∈ (Base‘𝑅) ∧ 𝐴 ≠ (0g‘𝑅))) |
| 61 | 13, 42, 28 | domnmuln0 20709 |
. . . . . 6
⊢ ((𝑅 ∈ Domn ∧ ((𝑦 ↑ 𝐴) ∈ (Base‘𝑅) ∧ (𝑦 ↑ 𝐴) ≠ (0g‘𝑅)) ∧ (𝐴 ∈ (Base‘𝑅) ∧ 𝐴 ≠ (0g‘𝑅))) → ((𝑦 ↑ 𝐴)(.r‘𝑅)𝐴) ≠ (0g‘𝑅)) |
| 62 | 49, 56, 60, 61 | syl3anc 1373 |
. . . . 5
⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑦 ↑ 𝐴) ≠ (0g‘𝑅)) → ((𝑦 ↑ 𝐴)(.r‘𝑅)𝐴) ≠ (0g‘𝑅)) |
| 63 | 46, 62 | eqnetrd 3008 |
. . . 4
⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑦 ↑ 𝐴) ≠ (0g‘𝑅)) → ((𝑦 ↑ 𝐴)(+g‘(mulGrp‘𝑅))𝐴) ≠ (0g‘𝑅)) |
| 64 | 41, 63 | eqnetrd 3008 |
. . 3
⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑦 ↑ 𝐴) ≠ (0g‘𝑅)) → ((𝑦 + 1) ↑ 𝐴) ≠ (0g‘𝑅)) |
| 65 | 4, 6, 8, 10, 31, 64 | nn0indd 12715 |
. 2
⊢ ((𝜑 ∧ 𝑁 ∈ ℕ0) → (𝑁 ↑ 𝐴) ≠ (0g‘𝑅)) |
| 66 | 2, 65 | syl 17 |
1
⊢ (𝜑 → (𝑁 ↑ 𝐴) ≠ (0g‘𝑅)) |