Step | Hyp | Ref
| Expression |
1 | | fveq2 6906 |
. . . 4
⊢ (𝑚 = 𝑁 → (𝐿‘𝑚) = (𝐿‘𝑁)) |
2 | 1 | eleq1d 2823 |
. . 3
⊢ (𝑚 = 𝑁 → ((𝐿‘𝑚) ∈ 𝐶 ↔ (𝐿‘𝑁) ∈ 𝐶)) |
3 | | fveq2 6906 |
. . . . . . 7
⊢ (𝑖 = 0 → (𝐿‘𝑖) = (𝐿‘0)) |
4 | 3 | eleq1d 2823 |
. . . . . 6
⊢ (𝑖 = 0 → ((𝐿‘𝑖) ∈ 𝐶 ↔ (𝐿‘0) ∈ 𝐶)) |
5 | | fveq2 6906 |
. . . . . . 7
⊢ (𝑖 = 𝑛 → (𝐿‘𝑖) = (𝐿‘𝑛)) |
6 | 5 | eleq1d 2823 |
. . . . . 6
⊢ (𝑖 = 𝑛 → ((𝐿‘𝑖) ∈ 𝐶 ↔ (𝐿‘𝑛) ∈ 𝐶)) |
7 | | fveq2 6906 |
. . . . . . 7
⊢ (𝑖 = (𝑛 + 1) → (𝐿‘𝑖) = (𝐿‘(𝑛 + 1))) |
8 | 7 | eleq1d 2823 |
. . . . . 6
⊢ (𝑖 = (𝑛 + 1) → ((𝐿‘𝑖) ∈ 𝐶 ↔ (𝐿‘(𝑛 + 1)) ∈ 𝐶)) |
9 | | fveq2 6906 |
. . . . . . 7
⊢ (𝑖 = 𝑚 → (𝐿‘𝑖) = (𝐿‘𝑚)) |
10 | 9 | eleq1d 2823 |
. . . . . 6
⊢ (𝑖 = 𝑚 → ((𝐿‘𝑖) ∈ 𝐶 ↔ (𝐿‘𝑚) ∈ 𝐶)) |
11 | | zrhcntr.4 |
. . . . . . . . 9
⊢ (𝜑 → 𝑅 ∈ Ring) |
12 | | zrhcntr.3 |
. . . . . . . . . 10
⊢ 𝐿 = (ℤRHom‘𝑅) |
13 | | eqid 2734 |
. . . . . . . . . 10
⊢
(0g‘𝑅) = (0g‘𝑅) |
14 | 12, 13 | zrh0 21541 |
. . . . . . . . 9
⊢ (𝑅 ∈ Ring → (𝐿‘0) =
(0g‘𝑅)) |
15 | 11, 14 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (𝐿‘0) = (0g‘𝑅)) |
16 | | eqid 2734 |
. . . . . . . . . 10
⊢
(Base‘𝑅) =
(Base‘𝑅) |
17 | 16, 13 | ring0cl 20280 |
. . . . . . . . 9
⊢ (𝑅 ∈ Ring →
(0g‘𝑅)
∈ (Base‘𝑅)) |
18 | 11, 17 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (0g‘𝑅) ∈ (Base‘𝑅)) |
19 | 15, 18 | eqeltrd 2838 |
. . . . . . 7
⊢ (𝜑 → (𝐿‘0) ∈ (Base‘𝑅)) |
20 | | eqid 2734 |
. . . . . . . . . . 11
⊢
(.r‘𝑅) = (.r‘𝑅) |
21 | 11 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → 𝑅 ∈ Ring) |
22 | | simpr 484 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → 𝑥 ∈ (Base‘𝑅)) |
23 | 16, 20, 13, 21, 22 | ringlzd 20308 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → ((0g‘𝑅)(.r‘𝑅)𝑥) = (0g‘𝑅)) |
24 | 16, 20, 13, 21, 22 | ringrzd 20309 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → (𝑥(.r‘𝑅)(0g‘𝑅)) = (0g‘𝑅)) |
25 | 23, 24 | eqtr4d 2777 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → ((0g‘𝑅)(.r‘𝑅)𝑥) = (𝑥(.r‘𝑅)(0g‘𝑅))) |
26 | 15 | oveq1d 7445 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝐿‘0)(.r‘𝑅)𝑥) = ((0g‘𝑅)(.r‘𝑅)𝑥)) |
27 | 26 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → ((𝐿‘0)(.r‘𝑅)𝑥) = ((0g‘𝑅)(.r‘𝑅)𝑥)) |
28 | 15 | oveq2d 7446 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑥(.r‘𝑅)(𝐿‘0)) = (𝑥(.r‘𝑅)(0g‘𝑅))) |
29 | 28 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → (𝑥(.r‘𝑅)(𝐿‘0)) = (𝑥(.r‘𝑅)(0g‘𝑅))) |
30 | 25, 27, 29 | 3eqtr4d 2784 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝑅)) → ((𝐿‘0)(.r‘𝑅)𝑥) = (𝑥(.r‘𝑅)(𝐿‘0))) |
31 | 30 | ralrimiva 3143 |
. . . . . . 7
⊢ (𝜑 → ∀𝑥 ∈ (Base‘𝑅)((𝐿‘0)(.r‘𝑅)𝑥) = (𝑥(.r‘𝑅)(𝐿‘0))) |
32 | | zrhcntr.1 |
. . . . . . . . 9
⊢ 𝑀 = (mulGrp‘𝑅) |
33 | 32, 16 | mgpbas 20157 |
. . . . . . . 8
⊢
(Base‘𝑅) =
(Base‘𝑀) |
34 | 32, 20 | mgpplusg 20155 |
. . . . . . . 8
⊢
(.r‘𝑅) = (+g‘𝑀) |
35 | | zrhcntr.2 |
. . . . . . . 8
⊢ 𝐶 = (Cntr‘𝑀) |
36 | 33, 34, 35 | elcntr 19360 |
. . . . . . 7
⊢ ((𝐿‘0) ∈ 𝐶 ↔ ((𝐿‘0) ∈ (Base‘𝑅) ∧ ∀𝑥 ∈ (Base‘𝑅)((𝐿‘0)(.r‘𝑅)𝑥) = (𝑥(.r‘𝑅)(𝐿‘0)))) |
37 | 19, 31, 36 | sylanbrc 583 |
. . . . . 6
⊢ (𝜑 → (𝐿‘0) ∈ 𝐶) |
38 | 12 | zrhrhm 21539 |
. . . . . . . . . . 11
⊢ (𝑅 ∈ Ring → 𝐿 ∈ (ℤring
RingHom 𝑅)) |
39 | | rhmghm 20500 |
. . . . . . . . . . 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 12636 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ (𝐿‘𝑛) ∈ 𝐶) → 𝑛 ∈ ℤ) |
44 | | 1zzd 12645 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ (𝐿‘𝑛) ∈ 𝐶) → 1 ∈ ℤ) |
45 | | zringbas 21481 |
. . . . . . . . . 10
⊢ ℤ =
(Base‘ℤring) |
46 | | zringplusg 21482 |
. . . . . . . . . 10
⊢ + =
(+g‘ℤring) |
47 | | eqid 2734 |
. . . . . . . . . 10
⊢
(+g‘𝑅) = (+g‘𝑅) |
48 | 45, 46, 47 | ghmlin 19251 |
. . . . . . . . 9
⊢ ((𝐿 ∈ (ℤring
GrpHom 𝑅) ∧ 𝑛 ∈ ℤ ∧ 1 ∈
ℤ) → (𝐿‘(𝑛 + 1)) = ((𝐿‘𝑛)(+g‘𝑅)(𝐿‘1))) |
49 | 41, 43, 44, 48 | syl3anc 1370 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ (𝐿‘𝑛) ∈ 𝐶) → (𝐿‘(𝑛 + 1)) = ((𝐿‘𝑛)(+g‘𝑅)(𝐿‘1))) |
50 | | eqid 2734 |
. . . . . . . . . . . 12
⊢
(1r‘𝑅) = (1r‘𝑅) |
51 | 12, 50 | zrh1 21540 |
. . . . . . . . . . 11
⊢ (𝑅 ∈ Ring → (𝐿‘1) =
(1r‘𝑅)) |
52 | 11, 51 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐿‘1) = (1r‘𝑅)) |
53 | 52 | ad2antrr 726 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ (𝐿‘𝑛) ∈ 𝐶) → (𝐿‘1) = (1r‘𝑅)) |
54 | 53 | oveq2d 7446 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ (𝐿‘𝑛) ∈ 𝐶) → ((𝐿‘𝑛)(+g‘𝑅)(𝐿‘1)) = ((𝐿‘𝑛)(+g‘𝑅)(1r‘𝑅))) |
55 | 49, 54 | eqtrd 2774 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ (𝐿‘𝑛) ∈ 𝐶) → (𝐿‘(𝑛 + 1)) = ((𝐿‘𝑛)(+g‘𝑅)(1r‘𝑅))) |
56 | 11 | ringgrpd 20259 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑅 ∈ Grp) |
57 | 56 | ad2antrr 726 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ (𝐿‘𝑛) ∈ 𝐶) → 𝑅 ∈ Grp) |
58 | 33 | cntrss 19361 |
. . . . . . . . . . . 12
⊢
(Cntr‘𝑀)
⊆ (Base‘𝑅) |
59 | 35, 58 | eqsstri 4029 |
. . . . . . . . . . 11
⊢ 𝐶 ⊆ (Base‘𝑅) |
60 | 59 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → 𝐶 ⊆ (Base‘𝑅)) |
61 | 60 | sselda 3994 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ (𝐿‘𝑛) ∈ 𝐶) → (𝐿‘𝑛) ∈ (Base‘𝑅)) |
62 | 16, 50 | ringidcl 20279 |
. . . . . . . . . . 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 18977 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ (𝐿‘𝑛) ∈ 𝐶) → ((𝐿‘𝑛)(+g‘𝑅)(1r‘𝑅)) ∈ (Base‘𝑅)) |
66 | 33, 34, 35 | cntri 19362 |
. . . . . . . . . . . 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 20285 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ (𝐿‘𝑛) ∈ 𝐶) ∧ 𝑥 ∈ (Base‘𝑅)) → ((1r‘𝑅)(.r‘𝑅)𝑥) = 𝑥) |
71 | 16, 20, 50, 68, 69 | ringridmd 20286 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ (𝐿‘𝑛) ∈ 𝐶) ∧ 𝑥 ∈ (Base‘𝑅)) → (𝑥(.r‘𝑅)(1r‘𝑅)) = 𝑥) |
72 | 70, 71 | eqtr4d 2777 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ (𝐿‘𝑛) ∈ 𝐶) ∧ 𝑥 ∈ (Base‘𝑅)) → ((1r‘𝑅)(.r‘𝑅)𝑥) = (𝑥(.r‘𝑅)(1r‘𝑅))) |
73 | 67, 72 | oveq12d 7448 |
. . . . . . . . . 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 33219 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ (𝐿‘𝑛) ∈ 𝐶) ∧ 𝑥 ∈ (Base‘𝑅)) → (((𝐿‘𝑛)(+g‘𝑅)(1r‘𝑅))(.r‘𝑅)𝑥) = (((𝐿‘𝑛)(.r‘𝑅)𝑥)(+g‘𝑅)((1r‘𝑅)(.r‘𝑅)𝑥))) |
77 | 16, 47, 20, 68, 69, 74, 75 | ringdid 33218 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ (𝐿‘𝑛) ∈ 𝐶) ∧ 𝑥 ∈ (Base‘𝑅)) → (𝑥(.r‘𝑅)((𝐿‘𝑛)(+g‘𝑅)(1r‘𝑅))) = ((𝑥(.r‘𝑅)(𝐿‘𝑛))(+g‘𝑅)(𝑥(.r‘𝑅)(1r‘𝑅)))) |
78 | 73, 76, 77 | 3eqtr4d 2784 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ (𝐿‘𝑛) ∈ 𝐶) ∧ 𝑥 ∈ (Base‘𝑅)) → (((𝐿‘𝑛)(+g‘𝑅)(1r‘𝑅))(.r‘𝑅)𝑥) = (𝑥(.r‘𝑅)((𝐿‘𝑛)(+g‘𝑅)(1r‘𝑅)))) |
79 | 78 | ralrimiva 3143 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ (𝐿‘𝑛) ∈ 𝐶) → ∀𝑥 ∈ (Base‘𝑅)(((𝐿‘𝑛)(+g‘𝑅)(1r‘𝑅))(.r‘𝑅)𝑥) = (𝑥(.r‘𝑅)((𝐿‘𝑛)(+g‘𝑅)(1r‘𝑅)))) |
80 | 33, 34, 35 | elcntr 19360 |
. . . . . . . 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 2838 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ (𝐿‘𝑛) ∈ 𝐶) → (𝐿‘(𝑛 + 1)) ∈ 𝐶) |
83 | 4, 6, 8, 10, 37, 82 | nn0indd 12712 |
. . . . 5
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → (𝐿‘𝑚) ∈ 𝐶) |
84 | 83 | ralrimiva 3143 |
. . . 4
⊢ (𝜑 → ∀𝑚 ∈ ℕ0 (𝐿‘𝑚) ∈ 𝐶) |
85 | 84 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ 𝑁 ∈ ℕ0) →
∀𝑚 ∈
ℕ0 (𝐿‘𝑚) ∈ 𝐶) |
86 | | simpr 484 |
. . 3
⊢ ((𝜑 ∧ 𝑁 ∈ ℕ0) → 𝑁 ∈
ℕ0) |
87 | 2, 85, 86 | rspcdva 3622 |
. 2
⊢ ((𝜑 ∧ 𝑁 ∈ ℕ0) → (𝐿‘𝑁) ∈ 𝐶) |
88 | 45, 16 | rhmf 20501 |
. . . . . 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 7104 |
. . 3
⊢ ((𝜑 ∧ -𝑁 ∈ ℕ0) → (𝐿‘𝑁) ∈ (Base‘𝑅)) |
94 | | eqid 2734 |
. . . . . 6
⊢
(invg‘𝑅) = (invg‘𝑅) |
95 | 11 | ad2antrr 726 |
. . . . . 6
⊢ (((𝜑 ∧ -𝑁 ∈ ℕ0) ∧ 𝑥 ∈ (Base‘𝑅)) → 𝑅 ∈ Ring) |
96 | | fveq2 6906 |
. . . . . . . . . . 11
⊢ (𝑚 = -𝑁 → (𝐿‘𝑚) = (𝐿‘-𝑁)) |
97 | 96 | eleq1d 2823 |
. . . . . . . . . 10
⊢ (𝑚 = -𝑁 → ((𝐿‘𝑚) ∈ 𝐶 ↔ (𝐿‘-𝑁) ∈ 𝐶)) |
98 | 84 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ -𝑁 ∈ ℕ0) →
∀𝑚 ∈
ℕ0 (𝐿‘𝑚) ∈ 𝐶) |
99 | | simpr 484 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ -𝑁 ∈ ℕ0) → -𝑁 ∈
ℕ0) |
100 | 97, 98, 99 | rspcdva 3622 |
. . . . . . . . 9
⊢ ((𝜑 ∧ -𝑁 ∈ ℕ0) → (𝐿‘-𝑁) ∈ 𝐶) |
101 | 33, 34, 35 | elcntr 19360 |
. . . . . . . . 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 20317 |
. . . . 5
⊢ (((𝜑 ∧ -𝑁 ∈ ℕ0) ∧ 𝑥 ∈ (Base‘𝑅)) →
(((invg‘𝑅)‘(𝐿‘-𝑁))(.r‘𝑅)𝑥) = ((invg‘𝑅)‘((𝐿‘-𝑁)(.r‘𝑅)𝑥))) |
107 | 91 | zcnd 12720 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑁 ∈ ℂ) |
108 | 107 | ad2antrr 726 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ -𝑁 ∈ ℕ0) ∧ 𝑥 ∈ (Base‘𝑅)) → 𝑁 ∈ ℂ) |
109 | 108 | negnegd 11608 |
. . . . . . . . 9
⊢ (((𝜑 ∧ -𝑁 ∈ ℕ0) ∧ 𝑥 ∈ (Base‘𝑅)) → --𝑁 = 𝑁) |
110 | 91 | znegcld 12721 |
. . . . . . . . . . 11
⊢ (𝜑 → -𝑁 ∈ ℤ) |
111 | | zringinvg 21493 |
. . . . . . . . . . 11
⊢ (-𝑁 ∈ ℤ → --𝑁 =
((invg‘ℤring)‘-𝑁)) |
112 | 110, 111 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → --𝑁 =
((invg‘ℤring)‘-𝑁)) |
113 | 112 | ad2antrr 726 |
. . . . . . . . 9
⊢ (((𝜑 ∧ -𝑁 ∈ ℕ0) ∧ 𝑥 ∈ (Base‘𝑅)) → --𝑁 =
((invg‘ℤring)‘-𝑁)) |
114 | 109, 113 | eqtr3d 2776 |
. . . . . . . 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 2734 |
. . . . . . . . 9
⊢
(invg‘ℤring) =
(invg‘ℤring) |
119 | 45, 118, 94 | ghminv 19253 |
. . . . . . . 8
⊢ ((𝐿 ∈ (ℤring
GrpHom 𝑅) ∧ -𝑁 ∈ ℤ) → (𝐿‘((invg‘ℤring)‘-𝑁)) = ((invg‘𝑅)‘(𝐿‘-𝑁))) |
120 | 116, 117,
119 | syl2anc 584 |
. . . . . . 7
⊢ (((𝜑 ∧ -𝑁 ∈ ℕ0) ∧ 𝑥 ∈ (Base‘𝑅)) → (𝐿‘((invg‘ℤring)‘-𝑁)) = ((invg‘𝑅)‘(𝐿‘-𝑁))) |
121 | 115, 120 | eqtrd 2774 |
. . . . . 6
⊢ (((𝜑 ∧ -𝑁 ∈ ℕ0) ∧ 𝑥 ∈ (Base‘𝑅)) → (𝐿‘𝑁) = ((invg‘𝑅)‘(𝐿‘-𝑁))) |
122 | 121 | oveq1d 7445 |
. . . . 5
⊢ (((𝜑 ∧ -𝑁 ∈ ℕ0) ∧ 𝑥 ∈ (Base‘𝑅)) → ((𝐿‘𝑁)(.r‘𝑅)𝑥) = (((invg‘𝑅)‘(𝐿‘-𝑁))(.r‘𝑅)𝑥)) |
123 | 16, 20, 94, 95, 105, 104 | ringmneg2 20318 |
. . . . . 6
⊢ (((𝜑 ∧ -𝑁 ∈ ℕ0) ∧ 𝑥 ∈ (Base‘𝑅)) → (𝑥(.r‘𝑅)((invg‘𝑅)‘(𝐿‘-𝑁))) = ((invg‘𝑅)‘(𝑥(.r‘𝑅)(𝐿‘-𝑁)))) |
124 | 121 | oveq2d 7446 |
. . . . . 6
⊢ (((𝜑 ∧ -𝑁 ∈ ℕ0) ∧ 𝑥 ∈ (Base‘𝑅)) → (𝑥(.r‘𝑅)(𝐿‘𝑁)) = (𝑥(.r‘𝑅)((invg‘𝑅)‘(𝐿‘-𝑁)))) |
125 | 102 | simprd 495 |
. . . . . . . 8
⊢ ((𝜑 ∧ -𝑁 ∈ ℕ0) →
∀𝑥 ∈
(Base‘𝑅)((𝐿‘-𝑁)(.r‘𝑅)𝑥) = (𝑥(.r‘𝑅)(𝐿‘-𝑁))) |
126 | 125 | r19.21bi 3248 |
. . . . . . 7
⊢ (((𝜑 ∧ -𝑁 ∈ ℕ0) ∧ 𝑥 ∈ (Base‘𝑅)) → ((𝐿‘-𝑁)(.r‘𝑅)𝑥) = (𝑥(.r‘𝑅)(𝐿‘-𝑁))) |
127 | 126 | fveq2d 6910 |
. . . . . 6
⊢ (((𝜑 ∧ -𝑁 ∈ ℕ0) ∧ 𝑥 ∈ (Base‘𝑅)) →
((invg‘𝑅)‘((𝐿‘-𝑁)(.r‘𝑅)𝑥)) = ((invg‘𝑅)‘(𝑥(.r‘𝑅)(𝐿‘-𝑁)))) |
128 | 123, 124,
127 | 3eqtr4d 2784 |
. . . . 5
⊢ (((𝜑 ∧ -𝑁 ∈ ℕ0) ∧ 𝑥 ∈ (Base‘𝑅)) → (𝑥(.r‘𝑅)(𝐿‘𝑁)) = ((invg‘𝑅)‘((𝐿‘-𝑁)(.r‘𝑅)𝑥))) |
129 | 106, 122,
128 | 3eqtr4d 2784 |
. . . 4
⊢ (((𝜑 ∧ -𝑁 ∈ ℕ0) ∧ 𝑥 ∈ (Base‘𝑅)) → ((𝐿‘𝑁)(.r‘𝑅)𝑥) = (𝑥(.r‘𝑅)(𝐿‘𝑁))) |
130 | 129 | ralrimiva 3143 |
. . 3
⊢ ((𝜑 ∧ -𝑁 ∈ ℕ0) →
∀𝑥 ∈
(Base‘𝑅)((𝐿‘𝑁)(.r‘𝑅)𝑥) = (𝑥(.r‘𝑅)(𝐿‘𝑁))) |
131 | 33, 34, 35 | elcntr 19360 |
. . 3
⊢ ((𝐿‘𝑁) ∈ 𝐶 ↔ ((𝐿‘𝑁) ∈ (Base‘𝑅) ∧ ∀𝑥 ∈ (Base‘𝑅)((𝐿‘𝑁)(.r‘𝑅)𝑥) = (𝑥(.r‘𝑅)(𝐿‘𝑁)))) |
132 | 93, 130, 131 | sylanbrc 583 |
. 2
⊢ ((𝜑 ∧ -𝑁 ∈ ℕ0) → (𝐿‘𝑁) ∈ 𝐶) |
133 | | elznn0 12625 |
. . . 4
⊢ (𝑁 ∈ ℤ ↔ (𝑁 ∈ ℝ ∧ (𝑁 ∈ ℕ0 ∨
-𝑁 ∈
ℕ0))) |
134 | 91, 133 | sylib 218 |
. . 3
⊢ (𝜑 → (𝑁 ∈ ℝ ∧ (𝑁 ∈ ℕ0 ∨ -𝑁 ∈
ℕ0))) |
135 | 134 | simprd 495 |
. 2
⊢ (𝜑 → (𝑁 ∈ ℕ0 ∨ -𝑁 ∈
ℕ0)) |
136 | 87, 132, 135 | mpjaodan 960 |
1
⊢ (𝜑 → (𝐿‘𝑁) ∈ 𝐶) |