| Step | Hyp | Ref
| Expression |
| 1 | | fveq2 6906 |
. . . 4
⊢ (𝑚 = 𝑁 → (𝐿‘𝑚) = (𝐿‘𝑁)) |
| 2 | 1 | eleq1d 2826 |
. . 3
⊢ (𝑚 = 𝑁 → ((𝐿‘𝑚) ∈ 𝐶 ↔ (𝐿‘𝑁) ∈ 𝐶)) |
| 3 | | fveq2 6906 |
. . . . . . 7
⊢ (𝑖 = 0 → (𝐿‘𝑖) = (𝐿‘0)) |
| 4 | 3 | eleq1d 2826 |
. . . . . 6
⊢ (𝑖 = 0 → ((𝐿‘𝑖) ∈ 𝐶 ↔ (𝐿‘0) ∈ 𝐶)) |
| 5 | | fveq2 6906 |
. . . . . . 7
⊢ (𝑖 = 𝑛 → (𝐿‘𝑖) = (𝐿‘𝑛)) |
| 6 | 5 | eleq1d 2826 |
. . . . . 6
⊢ (𝑖 = 𝑛 → ((𝐿‘𝑖) ∈ 𝐶 ↔ (𝐿‘𝑛) ∈ 𝐶)) |
| 7 | | fveq2 6906 |
. . . . . . 7
⊢ (𝑖 = (𝑛 + 1) → (𝐿‘𝑖) = (𝐿‘(𝑛 + 1))) |
| 8 | 7 | eleq1d 2826 |
. . . . . 6
⊢ (𝑖 = (𝑛 + 1) → ((𝐿‘𝑖) ∈ 𝐶 ↔ (𝐿‘(𝑛 + 1)) ∈ 𝐶)) |
| 9 | | fveq2 6906 |
. . . . . . 7
⊢ (𝑖 = 𝑚 → (𝐿‘𝑖) = (𝐿‘𝑚)) |
| 10 | 9 | eleq1d 2826 |
. . . . . 6
⊢ (𝑖 = 𝑚 → ((𝐿‘𝑖) ∈ 𝐶 ↔ (𝐿‘𝑚) ∈ 𝐶)) |
| 11 | | zrhcntr.4 |
. . . . . . . . 9
⊢ (𝜑 → 𝑅 ∈ Ring) |
| 12 | | zrhcntr.3 |
. . . . . . . . . 10
⊢ 𝐿 = (ℤRHom‘𝑅) |
| 13 | | eqid 2737 |
. . . . . . . . . 10
⊢
(0g‘𝑅) = (0g‘𝑅) |
| 14 | 12, 13 | zrh0 21524 |
. . . . . . . . 9
⊢ (𝑅 ∈ Ring → (𝐿‘0) =
(0g‘𝑅)) |
| 15 | 11, 14 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (𝐿‘0) = (0g‘𝑅)) |
| 16 | | eqid 2737 |
. . . . . . . . . 10
⊢
(Base‘𝑅) =
(Base‘𝑅) |
| 17 | 16, 13 | ring0cl 20264 |
. . . . . . . . 9
⊢ (𝑅 ∈ Ring →
(0g‘𝑅)
∈ (Base‘𝑅)) |
| 18 | 11, 17 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (0g‘𝑅) ∈ (Base‘𝑅)) |
| 19 | 15, 18 | eqeltrd 2841 |
. . . . . . 7
⊢ (𝜑 → (𝐿‘0) ∈ (Base‘𝑅)) |
| 20 | | eqid 2737 |
. . . . . . . . . . 11
⊢
(.r‘𝑅) = (.r‘𝑅) |
| 21 | 11 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → 𝑅 ∈ Ring) |
| 22 | | simpr 484 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → 𝑥 ∈ (Base‘𝑅)) |
| 23 | 16, 20, 13, 21, 22 | ringlzd 20292 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → ((0g‘𝑅)(.r‘𝑅)𝑥) = (0g‘𝑅)) |
| 24 | 16, 20, 13, 21, 22 | ringrzd 20293 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → (𝑥(.r‘𝑅)(0g‘𝑅)) = (0g‘𝑅)) |
| 25 | 23, 24 | eqtr4d 2780 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → ((0g‘𝑅)(.r‘𝑅)𝑥) = (𝑥(.r‘𝑅)(0g‘𝑅))) |
| 26 | 15 | oveq1d 7446 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝐿‘0)(.r‘𝑅)𝑥) = ((0g‘𝑅)(.r‘𝑅)𝑥)) |
| 27 | 26 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → ((𝐿‘0)(.r‘𝑅)𝑥) = ((0g‘𝑅)(.r‘𝑅)𝑥)) |
| 28 | 15 | oveq2d 7447 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑥(.r‘𝑅)(𝐿‘0)) = (𝑥(.r‘𝑅)(0g‘𝑅))) |
| 29 | 28 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → (𝑥(.r‘𝑅)(𝐿‘0)) = (𝑥(.r‘𝑅)(0g‘𝑅))) |
| 30 | 25, 27, 29 | 3eqtr4d 2787 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → ((𝐿‘0)(.r‘𝑅)𝑥) = (𝑥(.r‘𝑅)(𝐿‘0))) |
| 31 | 30 | ralrimiva 3146 |
. . . . . . 7
⊢ (𝜑 → ∀𝑥 ∈ (Base‘𝑅)((𝐿‘0)(.r‘𝑅)𝑥) = (𝑥(.r‘𝑅)(𝐿‘0))) |
| 32 | | zrhcntr.1 |
. . . . . . . . 9
⊢ 𝑀 = (mulGrp‘𝑅) |
| 33 | 32, 16 | mgpbas 20142 |
. . . . . . . 8
⊢
(Base‘𝑅) =
(Base‘𝑀) |
| 34 | 32, 20 | mgpplusg 20141 |
. . . . . . . 8
⊢
(.r‘𝑅) = (+g‘𝑀) |
| 35 | | zrhcntr.2 |
. . . . . . . 8
⊢ 𝐶 = (Cntr‘𝑀) |
| 36 | 33, 34, 35 | elcntr 19348 |
. . . . . . 7
⊢ ((𝐿‘0) ∈ 𝐶 ↔ ((𝐿‘0) ∈ (Base‘𝑅) ∧ ∀𝑥 ∈ (Base‘𝑅)((𝐿‘0)(.r‘𝑅)𝑥) = (𝑥(.r‘𝑅)(𝐿‘0)))) |
| 37 | 19, 31, 36 | sylanbrc 583 |
. . . . . 6
⊢ (𝜑 → (𝐿‘0) ∈ 𝐶) |
| 38 | 12 | zrhrhm 21522 |
. . . . . . . . . . 11
⊢ (𝑅 ∈ Ring → 𝐿 ∈ (ℤring
RingHom 𝑅)) |
| 39 | | rhmghm 20484 |
. . . . . . . . . . 11
⊢ (𝐿 ∈ (ℤring
RingHom 𝑅) → 𝐿 ∈ (ℤring
GrpHom 𝑅)) |
| 40 | 11, 38, 39 | 3syl 18 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐿 ∈ (ℤring GrpHom 𝑅)) |
| 41 | 40 | ad2antrr 726 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ (𝐿‘𝑛) ∈ 𝐶) → 𝐿 ∈ (ℤring GrpHom 𝑅)) |
| 42 | | simplr 769 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ (𝐿‘𝑛) ∈ 𝐶) → 𝑛 ∈ ℕ0) |
| 43 | 42 | nn0zd 12639 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ (𝐿‘𝑛) ∈ 𝐶) → 𝑛 ∈ ℤ) |
| 44 | | 1zzd 12648 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ (𝐿‘𝑛) ∈ 𝐶) → 1 ∈ ℤ) |
| 45 | | zringbas 21464 |
. . . . . . . . . 10
⊢ ℤ =
(Base‘ℤring) |
| 46 | | zringplusg 21465 |
. . . . . . . . . 10
⊢ + =
(+g‘ℤring) |
| 47 | | eqid 2737 |
. . . . . . . . . 10
⊢
(+g‘𝑅) = (+g‘𝑅) |
| 48 | 45, 46, 47 | ghmlin 19239 |
. . . . . . . . 9
⊢ ((𝐿 ∈ (ℤring
GrpHom 𝑅) ∧ 𝑛 ∈ ℤ ∧ 1 ∈
ℤ) → (𝐿‘(𝑛 + 1)) = ((𝐿‘𝑛)(+g‘𝑅)(𝐿‘1))) |
| 49 | 41, 43, 44, 48 | syl3anc 1373 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ (𝐿‘𝑛) ∈ 𝐶) → (𝐿‘(𝑛 + 1)) = ((𝐿‘𝑛)(+g‘𝑅)(𝐿‘1))) |
| 50 | | eqid 2737 |
. . . . . . . . . . . 12
⊢
(1r‘𝑅) = (1r‘𝑅) |
| 51 | 12, 50 | zrh1 21523 |
. . . . . . . . . . 11
⊢ (𝑅 ∈ Ring → (𝐿‘1) =
(1r‘𝑅)) |
| 52 | 11, 51 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐿‘1) = (1r‘𝑅)) |
| 53 | 52 | ad2antrr 726 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ (𝐿‘𝑛) ∈ 𝐶) → (𝐿‘1) = (1r‘𝑅)) |
| 54 | 53 | oveq2d 7447 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ (𝐿‘𝑛) ∈ 𝐶) → ((𝐿‘𝑛)(+g‘𝑅)(𝐿‘1)) = ((𝐿‘𝑛)(+g‘𝑅)(1r‘𝑅))) |
| 55 | 49, 54 | eqtrd 2777 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ (𝐿‘𝑛) ∈ 𝐶) → (𝐿‘(𝑛 + 1)) = ((𝐿‘𝑛)(+g‘𝑅)(1r‘𝑅))) |
| 56 | 11 | ringgrpd 20239 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑅 ∈ Grp) |
| 57 | 56 | ad2antrr 726 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ (𝐿‘𝑛) ∈ 𝐶) → 𝑅 ∈ Grp) |
| 58 | 33 | cntrss 19349 |
. . . . . . . . . . . 12
⊢
(Cntr‘𝑀)
⊆ (Base‘𝑅) |
| 59 | 35, 58 | eqsstri 4030 |
. . . . . . . . . . 11
⊢ 𝐶 ⊆ (Base‘𝑅) |
| 60 | 59 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → 𝐶 ⊆ (Base‘𝑅)) |
| 61 | 60 | sselda 3983 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ (𝐿‘𝑛) ∈ 𝐶) → (𝐿‘𝑛) ∈ (Base‘𝑅)) |
| 62 | 16, 50 | ringidcl 20262 |
. . . . . . . . . . 11
⊢ (𝑅 ∈ Ring →
(1r‘𝑅)
∈ (Base‘𝑅)) |
| 63 | 11, 62 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (1r‘𝑅) ∈ (Base‘𝑅)) |
| 64 | 63 | ad2antrr 726 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ (𝐿‘𝑛) ∈ 𝐶) → (1r‘𝑅) ∈ (Base‘𝑅)) |
| 65 | 16, 47, 57, 61, 64 | grpcld 18965 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ (𝐿‘𝑛) ∈ 𝐶) → ((𝐿‘𝑛)(+g‘𝑅)(1r‘𝑅)) ∈ (Base‘𝑅)) |
| 66 | 33, 34, 35 | cntri 19350 |
. . . . . . . . . . . 12
⊢ (((𝐿‘𝑛) ∈ 𝐶 ∧ 𝑥 ∈ (Base‘𝑅)) → ((𝐿‘𝑛)(.r‘𝑅)𝑥) = (𝑥(.r‘𝑅)(𝐿‘𝑛))) |
| 67 | 66 | adantll 714 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ (𝐿‘𝑛) ∈ 𝐶) ∧ 𝑥 ∈ (Base‘𝑅)) → ((𝐿‘𝑛)(.r‘𝑅)𝑥) = (𝑥(.r‘𝑅)(𝐿‘𝑛))) |
| 68 | 11 | ad3antrrr 730 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ (𝐿‘𝑛) ∈ 𝐶) ∧ 𝑥 ∈ (Base‘𝑅)) → 𝑅 ∈ Ring) |
| 69 | | simpr 484 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ (𝐿‘𝑛) ∈ 𝐶) ∧ 𝑥 ∈ (Base‘𝑅)) → 𝑥 ∈ (Base‘𝑅)) |
| 70 | 16, 20, 50, 68, 69 | ringlidmd 20269 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ (𝐿‘𝑛) ∈ 𝐶) ∧ 𝑥 ∈ (Base‘𝑅)) → ((1r‘𝑅)(.r‘𝑅)𝑥) = 𝑥) |
| 71 | 16, 20, 50, 68, 69 | ringridmd 20270 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ (𝐿‘𝑛) ∈ 𝐶) ∧ 𝑥 ∈ (Base‘𝑅)) → (𝑥(.r‘𝑅)(1r‘𝑅)) = 𝑥) |
| 72 | 70, 71 | eqtr4d 2780 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ (𝐿‘𝑛) ∈ 𝐶) ∧ 𝑥 ∈ (Base‘𝑅)) → ((1r‘𝑅)(.r‘𝑅)𝑥) = (𝑥(.r‘𝑅)(1r‘𝑅))) |
| 73 | 67, 72 | oveq12d 7449 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ (𝐿‘𝑛) ∈ 𝐶) ∧ 𝑥 ∈ (Base‘𝑅)) → (((𝐿‘𝑛)(.r‘𝑅)𝑥)(+g‘𝑅)((1r‘𝑅)(.r‘𝑅)𝑥)) = ((𝑥(.r‘𝑅)(𝐿‘𝑛))(+g‘𝑅)(𝑥(.r‘𝑅)(1r‘𝑅)))) |
| 74 | 61 | adantr 480 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ (𝐿‘𝑛) ∈ 𝐶) ∧ 𝑥 ∈ (Base‘𝑅)) → (𝐿‘𝑛) ∈ (Base‘𝑅)) |
| 75 | 68, 62 | syl 17 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ (𝐿‘𝑛) ∈ 𝐶) ∧ 𝑥 ∈ (Base‘𝑅)) → (1r‘𝑅) ∈ (Base‘𝑅)) |
| 76 | 16, 47, 20, 68, 74, 75, 69 | ringdird 20261 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ (𝐿‘𝑛) ∈ 𝐶) ∧ 𝑥 ∈ (Base‘𝑅)) → (((𝐿‘𝑛)(+g‘𝑅)(1r‘𝑅))(.r‘𝑅)𝑥) = (((𝐿‘𝑛)(.r‘𝑅)𝑥)(+g‘𝑅)((1r‘𝑅)(.r‘𝑅)𝑥))) |
| 77 | 16, 47, 20, 68, 69, 74, 75 | ringdid 20260 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ (𝐿‘𝑛) ∈ 𝐶) ∧ 𝑥 ∈ (Base‘𝑅)) → (𝑥(.r‘𝑅)((𝐿‘𝑛)(+g‘𝑅)(1r‘𝑅))) = ((𝑥(.r‘𝑅)(𝐿‘𝑛))(+g‘𝑅)(𝑥(.r‘𝑅)(1r‘𝑅)))) |
| 78 | 73, 76, 77 | 3eqtr4d 2787 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ (𝐿‘𝑛) ∈ 𝐶) ∧ 𝑥 ∈ (Base‘𝑅)) → (((𝐿‘𝑛)(+g‘𝑅)(1r‘𝑅))(.r‘𝑅)𝑥) = (𝑥(.r‘𝑅)((𝐿‘𝑛)(+g‘𝑅)(1r‘𝑅)))) |
| 79 | 78 | ralrimiva 3146 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ (𝐿‘𝑛) ∈ 𝐶) → ∀𝑥 ∈ (Base‘𝑅)(((𝐿‘𝑛)(+g‘𝑅)(1r‘𝑅))(.r‘𝑅)𝑥) = (𝑥(.r‘𝑅)((𝐿‘𝑛)(+g‘𝑅)(1r‘𝑅)))) |
| 80 | 33, 34, 35 | elcntr 19348 |
. . . . . . . 8
⊢ (((𝐿‘𝑛)(+g‘𝑅)(1r‘𝑅)) ∈ 𝐶 ↔ (((𝐿‘𝑛)(+g‘𝑅)(1r‘𝑅)) ∈ (Base‘𝑅) ∧ ∀𝑥 ∈ (Base‘𝑅)(((𝐿‘𝑛)(+g‘𝑅)(1r‘𝑅))(.r‘𝑅)𝑥) = (𝑥(.r‘𝑅)((𝐿‘𝑛)(+g‘𝑅)(1r‘𝑅))))) |
| 81 | 65, 79, 80 | sylanbrc 583 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ (𝐿‘𝑛) ∈ 𝐶) → ((𝐿‘𝑛)(+g‘𝑅)(1r‘𝑅)) ∈ 𝐶) |
| 82 | 55, 81 | eqeltrd 2841 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ (𝐿‘𝑛) ∈ 𝐶) → (𝐿‘(𝑛 + 1)) ∈ 𝐶) |
| 83 | 4, 6, 8, 10, 37, 82 | nn0indd 12715 |
. . . . 5
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → (𝐿‘𝑚) ∈ 𝐶) |
| 84 | 83 | ralrimiva 3146 |
. . . 4
⊢ (𝜑 → ∀𝑚 ∈ ℕ0 (𝐿‘𝑚) ∈ 𝐶) |
| 85 | 84 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ 𝑁 ∈ ℕ0) →
∀𝑚 ∈
ℕ0 (𝐿‘𝑚) ∈ 𝐶) |
| 86 | | simpr 484 |
. . 3
⊢ ((𝜑 ∧ 𝑁 ∈ ℕ0) → 𝑁 ∈
ℕ0) |
| 87 | 2, 85, 86 | rspcdva 3623 |
. 2
⊢ ((𝜑 ∧ 𝑁 ∈ ℕ0) → (𝐿‘𝑁) ∈ 𝐶) |
| 88 | 45, 16 | rhmf 20485 |
. . . . . 6
⊢ (𝐿 ∈ (ℤring
RingHom 𝑅) → 𝐿:ℤ⟶(Base‘𝑅)) |
| 89 | 11, 38, 88 | 3syl 18 |
. . . . 5
⊢ (𝜑 → 𝐿:ℤ⟶(Base‘𝑅)) |
| 90 | 89 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ -𝑁 ∈ ℕ0) → 𝐿:ℤ⟶(Base‘𝑅)) |
| 91 | | zrhcntr.5 |
. . . . 5
⊢ (𝜑 → 𝑁 ∈ ℤ) |
| 92 | 91 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ -𝑁 ∈ ℕ0) → 𝑁 ∈
ℤ) |
| 93 | 90, 92 | ffvelcdmd 7105 |
. . 3
⊢ ((𝜑 ∧ -𝑁 ∈ ℕ0) → (𝐿‘𝑁) ∈ (Base‘𝑅)) |
| 94 | | eqid 2737 |
. . . . . 6
⊢
(invg‘𝑅) = (invg‘𝑅) |
| 95 | 11 | ad2antrr 726 |
. . . . . 6
⊢ (((𝜑 ∧ -𝑁 ∈ ℕ0) ∧ 𝑥 ∈ (Base‘𝑅)) → 𝑅 ∈ Ring) |
| 96 | | fveq2 6906 |
. . . . . . . . . . 11
⊢ (𝑚 = -𝑁 → (𝐿‘𝑚) = (𝐿‘-𝑁)) |
| 97 | 96 | eleq1d 2826 |
. . . . . . . . . 10
⊢ (𝑚 = -𝑁 → ((𝐿‘𝑚) ∈ 𝐶 ↔ (𝐿‘-𝑁) ∈ 𝐶)) |
| 98 | 84 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ -𝑁 ∈ ℕ0) →
∀𝑚 ∈
ℕ0 (𝐿‘𝑚) ∈ 𝐶) |
| 99 | | simpr 484 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ -𝑁 ∈ ℕ0) → -𝑁 ∈
ℕ0) |
| 100 | 97, 98, 99 | rspcdva 3623 |
. . . . . . . . 9
⊢ ((𝜑 ∧ -𝑁 ∈ ℕ0) → (𝐿‘-𝑁) ∈ 𝐶) |
| 101 | 33, 34, 35 | elcntr 19348 |
. . . . . . . . 9
⊢ ((𝐿‘-𝑁) ∈ 𝐶 ↔ ((𝐿‘-𝑁) ∈ (Base‘𝑅) ∧ ∀𝑥 ∈ (Base‘𝑅)((𝐿‘-𝑁)(.r‘𝑅)𝑥) = (𝑥(.r‘𝑅)(𝐿‘-𝑁)))) |
| 102 | 100, 101 | sylib 218 |
. . . . . . . 8
⊢ ((𝜑 ∧ -𝑁 ∈ ℕ0) → ((𝐿‘-𝑁) ∈ (Base‘𝑅) ∧ ∀𝑥 ∈ (Base‘𝑅)((𝐿‘-𝑁)(.r‘𝑅)𝑥) = (𝑥(.r‘𝑅)(𝐿‘-𝑁)))) |
| 103 | 102 | simpld 494 |
. . . . . . 7
⊢ ((𝜑 ∧ -𝑁 ∈ ℕ0) → (𝐿‘-𝑁) ∈ (Base‘𝑅)) |
| 104 | 103 | adantr 480 |
. . . . . 6
⊢ (((𝜑 ∧ -𝑁 ∈ ℕ0) ∧ 𝑥 ∈ (Base‘𝑅)) → (𝐿‘-𝑁) ∈ (Base‘𝑅)) |
| 105 | | simpr 484 |
. . . . . 6
⊢ (((𝜑 ∧ -𝑁 ∈ ℕ0) ∧ 𝑥 ∈ (Base‘𝑅)) → 𝑥 ∈ (Base‘𝑅)) |
| 106 | 16, 20, 94, 95, 104, 105 | ringmneg1 20301 |
. . . . 5
⊢ (((𝜑 ∧ -𝑁 ∈ ℕ0) ∧ 𝑥 ∈ (Base‘𝑅)) →
(((invg‘𝑅)‘(𝐿‘-𝑁))(.r‘𝑅)𝑥) = ((invg‘𝑅)‘((𝐿‘-𝑁)(.r‘𝑅)𝑥))) |
| 107 | 91 | zcnd 12723 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑁 ∈ ℂ) |
| 108 | 107 | ad2antrr 726 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ -𝑁 ∈ ℕ0) ∧ 𝑥 ∈ (Base‘𝑅)) → 𝑁 ∈ ℂ) |
| 109 | 108 | negnegd 11611 |
. . . . . . . . 9
⊢ (((𝜑 ∧ -𝑁 ∈ ℕ0) ∧ 𝑥 ∈ (Base‘𝑅)) → --𝑁 = 𝑁) |
| 110 | 91 | znegcld 12724 |
. . . . . . . . . . 11
⊢ (𝜑 → -𝑁 ∈ ℤ) |
| 111 | | zringinvg 21476 |
. . . . . . . . . . 11
⊢ (-𝑁 ∈ ℤ → --𝑁 =
((invg‘ℤring)‘-𝑁)) |
| 112 | 110, 111 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → --𝑁 =
((invg‘ℤring)‘-𝑁)) |
| 113 | 112 | ad2antrr 726 |
. . . . . . . . 9
⊢ (((𝜑 ∧ -𝑁 ∈ ℕ0) ∧ 𝑥 ∈ (Base‘𝑅)) → --𝑁 =
((invg‘ℤring)‘-𝑁)) |
| 114 | 109, 113 | eqtr3d 2779 |
. . . . . . . 8
⊢ (((𝜑 ∧ -𝑁 ∈ ℕ0) ∧ 𝑥 ∈ (Base‘𝑅)) → 𝑁 =
((invg‘ℤring)‘-𝑁)) |
| 115 | 114 | fveq2d 6910 |
. . . . . . 7
⊢ (((𝜑 ∧ -𝑁 ∈ ℕ0) ∧ 𝑥 ∈ (Base‘𝑅)) → (𝐿‘𝑁) = (𝐿‘((invg‘ℤring)‘-𝑁))) |
| 116 | 95, 38, 39 | 3syl 18 |
. . . . . . . 8
⊢ (((𝜑 ∧ -𝑁 ∈ ℕ0) ∧ 𝑥 ∈ (Base‘𝑅)) → 𝐿 ∈ (ℤring GrpHom 𝑅)) |
| 117 | 110 | ad2antrr 726 |
. . . . . . . 8
⊢ (((𝜑 ∧ -𝑁 ∈ ℕ0) ∧ 𝑥 ∈ (Base‘𝑅)) → -𝑁 ∈ ℤ) |
| 118 | | eqid 2737 |
. . . . . . . . 9
⊢
(invg‘ℤring) =
(invg‘ℤring) |
| 119 | 45, 118, 94 | ghminv 19241 |
. . . . . . . 8
⊢ ((𝐿 ∈ (ℤring
GrpHom 𝑅) ∧ -𝑁 ∈ ℤ) → (𝐿‘((invg‘ℤring)‘-𝑁)) = ((invg‘𝑅)‘(𝐿‘-𝑁))) |
| 120 | 116, 117,
119 | syl2anc 584 |
. . . . . . 7
⊢ (((𝜑 ∧ -𝑁 ∈ ℕ0) ∧ 𝑥 ∈ (Base‘𝑅)) → (𝐿‘((invg‘ℤring)‘-𝑁)) = ((invg‘𝑅)‘(𝐿‘-𝑁))) |
| 121 | 115, 120 | eqtrd 2777 |
. . . . . 6
⊢ (((𝜑 ∧ -𝑁 ∈ ℕ0) ∧ 𝑥 ∈ (Base‘𝑅)) → (𝐿‘𝑁) = ((invg‘𝑅)‘(𝐿‘-𝑁))) |
| 122 | 121 | oveq1d 7446 |
. . . . 5
⊢ (((𝜑 ∧ -𝑁 ∈ ℕ0) ∧ 𝑥 ∈ (Base‘𝑅)) → ((𝐿‘𝑁)(.r‘𝑅)𝑥) = (((invg‘𝑅)‘(𝐿‘-𝑁))(.r‘𝑅)𝑥)) |
| 123 | 16, 20, 94, 95, 105, 104 | ringmneg2 20302 |
. . . . . 6
⊢ (((𝜑 ∧ -𝑁 ∈ ℕ0) ∧ 𝑥 ∈ (Base‘𝑅)) → (𝑥(.r‘𝑅)((invg‘𝑅)‘(𝐿‘-𝑁))) = ((invg‘𝑅)‘(𝑥(.r‘𝑅)(𝐿‘-𝑁)))) |
| 124 | 121 | oveq2d 7447 |
. . . . . 6
⊢ (((𝜑 ∧ -𝑁 ∈ ℕ0) ∧ 𝑥 ∈ (Base‘𝑅)) → (𝑥(.r‘𝑅)(𝐿‘𝑁)) = (𝑥(.r‘𝑅)((invg‘𝑅)‘(𝐿‘-𝑁)))) |
| 125 | 102 | simprd 495 |
. . . . . . . 8
⊢ ((𝜑 ∧ -𝑁 ∈ ℕ0) →
∀𝑥 ∈
(Base‘𝑅)((𝐿‘-𝑁)(.r‘𝑅)𝑥) = (𝑥(.r‘𝑅)(𝐿‘-𝑁))) |
| 126 | 125 | r19.21bi 3251 |
. . . . . . 7
⊢ (((𝜑 ∧ -𝑁 ∈ ℕ0) ∧ 𝑥 ∈ (Base‘𝑅)) → ((𝐿‘-𝑁)(.r‘𝑅)𝑥) = (𝑥(.r‘𝑅)(𝐿‘-𝑁))) |
| 127 | 126 | fveq2d 6910 |
. . . . . 6
⊢ (((𝜑 ∧ -𝑁 ∈ ℕ0) ∧ 𝑥 ∈ (Base‘𝑅)) →
((invg‘𝑅)‘((𝐿‘-𝑁)(.r‘𝑅)𝑥)) = ((invg‘𝑅)‘(𝑥(.r‘𝑅)(𝐿‘-𝑁)))) |
| 128 | 123, 124,
127 | 3eqtr4d 2787 |
. . . . 5
⊢ (((𝜑 ∧ -𝑁 ∈ ℕ0) ∧ 𝑥 ∈ (Base‘𝑅)) → (𝑥(.r‘𝑅)(𝐿‘𝑁)) = ((invg‘𝑅)‘((𝐿‘-𝑁)(.r‘𝑅)𝑥))) |
| 129 | 106, 122,
128 | 3eqtr4d 2787 |
. . . 4
⊢ (((𝜑 ∧ -𝑁 ∈ ℕ0) ∧ 𝑥 ∈ (Base‘𝑅)) → ((𝐿‘𝑁)(.r‘𝑅)𝑥) = (𝑥(.r‘𝑅)(𝐿‘𝑁))) |
| 130 | 129 | ralrimiva 3146 |
. . 3
⊢ ((𝜑 ∧ -𝑁 ∈ ℕ0) →
∀𝑥 ∈
(Base‘𝑅)((𝐿‘𝑁)(.r‘𝑅)𝑥) = (𝑥(.r‘𝑅)(𝐿‘𝑁))) |
| 131 | 33, 34, 35 | elcntr 19348 |
. . 3
⊢ ((𝐿‘𝑁) ∈ 𝐶 ↔ ((𝐿‘𝑁) ∈ (Base‘𝑅) ∧ ∀𝑥 ∈ (Base‘𝑅)((𝐿‘𝑁)(.r‘𝑅)𝑥) = (𝑥(.r‘𝑅)(𝐿‘𝑁)))) |
| 132 | 93, 130, 131 | sylanbrc 583 |
. 2
⊢ ((𝜑 ∧ -𝑁 ∈ ℕ0) → (𝐿‘𝑁) ∈ 𝐶) |
| 133 | | elznn0 12628 |
. . . 4
⊢ (𝑁 ∈ ℤ ↔ (𝑁 ∈ ℝ ∧ (𝑁 ∈ ℕ0 ∨
-𝑁 ∈
ℕ0))) |
| 134 | 91, 133 | sylib 218 |
. . 3
⊢ (𝜑 → (𝑁 ∈ ℝ ∧ (𝑁 ∈ ℕ0 ∨ -𝑁 ∈
ℕ0))) |
| 135 | 134 | simprd 495 |
. 2
⊢ (𝜑 → (𝑁 ∈ ℕ0 ∨ -𝑁 ∈
ℕ0)) |
| 136 | 87, 132, 135 | mpjaodan 961 |
1
⊢ (𝜑 → (𝐿‘𝑁) ∈ 𝐶) |