Step | Hyp | Ref
| Expression |
1 | | frobrhm.1 |
. 2
⊢ 𝐵 = (Base‘𝑅) |
2 | | eqid 2740 |
. 2
⊢
(1r‘𝑅) = (1r‘𝑅) |
3 | | eqid 2740 |
. 2
⊢
(.r‘𝑅) = (.r‘𝑅) |
4 | | frobrhm.5 |
. . 3
⊢ (𝜑 → 𝑅 ∈ CRing) |
5 | 4 | crngringd 19794 |
. 2
⊢ (𝜑 → 𝑅 ∈ Ring) |
6 | | frobrhm.4 |
. . 3
⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ (𝑃 ↑ 𝑥)) |
7 | | simpr 485 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 = (1r‘𝑅)) → 𝑥 = (1r‘𝑅)) |
8 | 7 | oveq2d 7287 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 = (1r‘𝑅)) → (𝑃 ↑ 𝑥) = (𝑃 ↑
(1r‘𝑅))) |
9 | | eqid 2740 |
. . . . . . . 8
⊢
(mulGrp‘𝑅) =
(mulGrp‘𝑅) |
10 | 9 | ringmgp 19787 |
. . . . . . 7
⊢ (𝑅 ∈ Ring →
(mulGrp‘𝑅) ∈
Mnd) |
11 | 5, 10 | syl 17 |
. . . . . 6
⊢ (𝜑 → (mulGrp‘𝑅) ∈ Mnd) |
12 | | frobrhm.6 |
. . . . . . 7
⊢ (𝜑 → 𝑃 ∈ ℙ) |
13 | | prmnn 16377 |
. . . . . . 7
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℕ) |
14 | | nnnn0 12240 |
. . . . . . 7
⊢ (𝑃 ∈ ℕ → 𝑃 ∈
ℕ0) |
15 | 12, 13, 14 | 3syl 18 |
. . . . . 6
⊢ (𝜑 → 𝑃 ∈
ℕ0) |
16 | 9, 1 | mgpbas 19724 |
. . . . . . 7
⊢ 𝐵 =
(Base‘(mulGrp‘𝑅)) |
17 | | frobrhm.3 |
. . . . . . 7
⊢ ↑ =
(.g‘(mulGrp‘𝑅)) |
18 | 9, 2 | ringidval 19737 |
. . . . . . 7
⊢
(1r‘𝑅) = (0g‘(mulGrp‘𝑅)) |
19 | 16, 17, 18 | mulgnn0z 18728 |
. . . . . 6
⊢
(((mulGrp‘𝑅)
∈ Mnd ∧ 𝑃 ∈
ℕ0) → (𝑃 ↑
(1r‘𝑅)) =
(1r‘𝑅)) |
20 | 11, 15, 19 | syl2anc 584 |
. . . . 5
⊢ (𝜑 → (𝑃 ↑
(1r‘𝑅)) =
(1r‘𝑅)) |
21 | 20 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 = (1r‘𝑅)) → (𝑃 ↑
(1r‘𝑅)) =
(1r‘𝑅)) |
22 | 8, 21 | eqtrd 2780 |
. . 3
⊢ ((𝜑 ∧ 𝑥 = (1r‘𝑅)) → (𝑃 ↑ 𝑥) = (1r‘𝑅)) |
23 | 1, 2 | ringidcl 19805 |
. . . 4
⊢ (𝑅 ∈ Ring →
(1r‘𝑅)
∈ 𝐵) |
24 | 5, 23 | syl 17 |
. . 3
⊢ (𝜑 → (1r‘𝑅) ∈ 𝐵) |
25 | 6, 22, 24, 24 | fvmptd2 6880 |
. 2
⊢ (𝜑 → (𝐹‘(1r‘𝑅)) = (1r‘𝑅)) |
26 | 9 | crngmgp 19789 |
. . . . . 6
⊢ (𝑅 ∈ CRing →
(mulGrp‘𝑅) ∈
CMnd) |
27 | 4, 26 | syl 17 |
. . . . 5
⊢ (𝜑 → (mulGrp‘𝑅) ∈ CMnd) |
28 | 27 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ (𝑖 ∈ 𝐵 ∧ 𝑗 ∈ 𝐵)) → (mulGrp‘𝑅) ∈ CMnd) |
29 | 15 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ (𝑖 ∈ 𝐵 ∧ 𝑗 ∈ 𝐵)) → 𝑃 ∈
ℕ0) |
30 | | simprl 768 |
. . . 4
⊢ ((𝜑 ∧ (𝑖 ∈ 𝐵 ∧ 𝑗 ∈ 𝐵)) → 𝑖 ∈ 𝐵) |
31 | | simprr 770 |
. . . 4
⊢ ((𝜑 ∧ (𝑖 ∈ 𝐵 ∧ 𝑗 ∈ 𝐵)) → 𝑗 ∈ 𝐵) |
32 | 9, 3 | mgpplusg 19722 |
. . . . 5
⊢
(.r‘𝑅) = (+g‘(mulGrp‘𝑅)) |
33 | 16, 17, 32 | mulgnn0di 19425 |
. . . 4
⊢
(((mulGrp‘𝑅)
∈ CMnd ∧ (𝑃 ∈
ℕ0 ∧ 𝑖
∈ 𝐵 ∧ 𝑗 ∈ 𝐵)) → (𝑃 ↑ (𝑖(.r‘𝑅)𝑗)) = ((𝑃 ↑ 𝑖)(.r‘𝑅)(𝑃 ↑ 𝑗))) |
34 | 28, 29, 30, 31, 33 | syl13anc 1371 |
. . 3
⊢ ((𝜑 ∧ (𝑖 ∈ 𝐵 ∧ 𝑗 ∈ 𝐵)) → (𝑃 ↑ (𝑖(.r‘𝑅)𝑗)) = ((𝑃 ↑ 𝑖)(.r‘𝑅)(𝑃 ↑ 𝑗))) |
35 | | simpr 485 |
. . . . 5
⊢ (((𝜑 ∧ (𝑖 ∈ 𝐵 ∧ 𝑗 ∈ 𝐵)) ∧ 𝑥 = (𝑖(.r‘𝑅)𝑗)) → 𝑥 = (𝑖(.r‘𝑅)𝑗)) |
36 | 35 | oveq2d 7287 |
. . . 4
⊢ (((𝜑 ∧ (𝑖 ∈ 𝐵 ∧ 𝑗 ∈ 𝐵)) ∧ 𝑥 = (𝑖(.r‘𝑅)𝑗)) → (𝑃 ↑ 𝑥) = (𝑃 ↑ (𝑖(.r‘𝑅)𝑗))) |
37 | 5 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ (𝑖 ∈ 𝐵 ∧ 𝑗 ∈ 𝐵)) → 𝑅 ∈ Ring) |
38 | 1, 3 | ringcl 19798 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝑖 ∈ 𝐵 ∧ 𝑗 ∈ 𝐵) → (𝑖(.r‘𝑅)𝑗) ∈ 𝐵) |
39 | 37, 30, 31, 38 | syl3anc 1370 |
. . . 4
⊢ ((𝜑 ∧ (𝑖 ∈ 𝐵 ∧ 𝑗 ∈ 𝐵)) → (𝑖(.r‘𝑅)𝑗) ∈ 𝐵) |
40 | | ovexd 7306 |
. . . 4
⊢ ((𝜑 ∧ (𝑖 ∈ 𝐵 ∧ 𝑗 ∈ 𝐵)) → (𝑃 ↑ (𝑖(.r‘𝑅)𝑗)) ∈ V) |
41 | 6, 36, 39, 40 | fvmptd2 6880 |
. . 3
⊢ ((𝜑 ∧ (𝑖 ∈ 𝐵 ∧ 𝑗 ∈ 𝐵)) → (𝐹‘(𝑖(.r‘𝑅)𝑗)) = (𝑃 ↑ (𝑖(.r‘𝑅)𝑗))) |
42 | | simpr 485 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑖 ∈ 𝐵 ∧ 𝑗 ∈ 𝐵)) ∧ 𝑥 = 𝑖) → 𝑥 = 𝑖) |
43 | 42 | oveq2d 7287 |
. . . . 5
⊢ (((𝜑 ∧ (𝑖 ∈ 𝐵 ∧ 𝑗 ∈ 𝐵)) ∧ 𝑥 = 𝑖) → (𝑃 ↑ 𝑥) = (𝑃 ↑ 𝑖)) |
44 | | ovexd 7306 |
. . . . 5
⊢ ((𝜑 ∧ (𝑖 ∈ 𝐵 ∧ 𝑗 ∈ 𝐵)) → (𝑃 ↑ 𝑖) ∈ V) |
45 | 6, 43, 30, 44 | fvmptd2 6880 |
. . . 4
⊢ ((𝜑 ∧ (𝑖 ∈ 𝐵 ∧ 𝑗 ∈ 𝐵)) → (𝐹‘𝑖) = (𝑃 ↑ 𝑖)) |
46 | | simpr 485 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑖 ∈ 𝐵 ∧ 𝑗 ∈ 𝐵)) ∧ 𝑥 = 𝑗) → 𝑥 = 𝑗) |
47 | 46 | oveq2d 7287 |
. . . . 5
⊢ (((𝜑 ∧ (𝑖 ∈ 𝐵 ∧ 𝑗 ∈ 𝐵)) ∧ 𝑥 = 𝑗) → (𝑃 ↑ 𝑥) = (𝑃 ↑ 𝑗)) |
48 | | ovexd 7306 |
. . . . 5
⊢ ((𝜑 ∧ (𝑖 ∈ 𝐵 ∧ 𝑗 ∈ 𝐵)) → (𝑃 ↑ 𝑗) ∈ V) |
49 | 6, 47, 31, 48 | fvmptd2 6880 |
. . . 4
⊢ ((𝜑 ∧ (𝑖 ∈ 𝐵 ∧ 𝑗 ∈ 𝐵)) → (𝐹‘𝑗) = (𝑃 ↑ 𝑗)) |
50 | 45, 49 | oveq12d 7289 |
. . 3
⊢ ((𝜑 ∧ (𝑖 ∈ 𝐵 ∧ 𝑗 ∈ 𝐵)) → ((𝐹‘𝑖)(.r‘𝑅)(𝐹‘𝑗)) = ((𝑃 ↑ 𝑖)(.r‘𝑅)(𝑃 ↑ 𝑗))) |
51 | 34, 41, 50 | 3eqtr4d 2790 |
. 2
⊢ ((𝜑 ∧ (𝑖 ∈ 𝐵 ∧ 𝑗 ∈ 𝐵)) → (𝐹‘(𝑖(.r‘𝑅)𝑗)) = ((𝐹‘𝑖)(.r‘𝑅)(𝐹‘𝑗))) |
52 | | eqid 2740 |
. 2
⊢
(+g‘𝑅) = (+g‘𝑅) |
53 | 11 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (mulGrp‘𝑅) ∈ Mnd) |
54 | 15 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝑃 ∈
ℕ0) |
55 | | simpr 485 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ 𝐵) |
56 | 16, 17 | mulgnn0cl 18718 |
. . . 4
⊢
(((mulGrp‘𝑅)
∈ Mnd ∧ 𝑃 ∈
ℕ0 ∧ 𝑥
∈ 𝐵) → (𝑃 ↑ 𝑥) ∈ 𝐵) |
57 | 53, 54, 55, 56 | syl3anc 1370 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝑃 ↑ 𝑥) ∈ 𝐵) |
58 | 57, 6 | fmptd 6985 |
. 2
⊢ (𝜑 → 𝐹:𝐵⟶𝐵) |
59 | | frobrhm.2 |
. . . 4
⊢ 𝑃 = (chr‘𝑅) |
60 | 4 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ (𝑖 ∈ 𝐵 ∧ 𝑗 ∈ 𝐵)) → 𝑅 ∈ CRing) |
61 | 12 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ (𝑖 ∈ 𝐵 ∧ 𝑗 ∈ 𝐵)) → 𝑃 ∈ ℙ) |
62 | 1, 52, 17, 59, 60, 61, 30, 31 | freshmansdream 31480 |
. . 3
⊢ ((𝜑 ∧ (𝑖 ∈ 𝐵 ∧ 𝑗 ∈ 𝐵)) → (𝑃 ↑ (𝑖(+g‘𝑅)𝑗)) = ((𝑃 ↑ 𝑖)(+g‘𝑅)(𝑃 ↑ 𝑗))) |
63 | | simpr 485 |
. . . . 5
⊢ (((𝜑 ∧ (𝑖 ∈ 𝐵 ∧ 𝑗 ∈ 𝐵)) ∧ 𝑥 = (𝑖(+g‘𝑅)𝑗)) → 𝑥 = (𝑖(+g‘𝑅)𝑗)) |
64 | 63 | oveq2d 7287 |
. . . 4
⊢ (((𝜑 ∧ (𝑖 ∈ 𝐵 ∧ 𝑗 ∈ 𝐵)) ∧ 𝑥 = (𝑖(+g‘𝑅)𝑗)) → (𝑃 ↑ 𝑥) = (𝑃 ↑ (𝑖(+g‘𝑅)𝑗))) |
65 | 1, 52 | ringacl 19815 |
. . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝑖 ∈ 𝐵 ∧ 𝑗 ∈ 𝐵) → (𝑖(+g‘𝑅)𝑗) ∈ 𝐵) |
66 | 37, 30, 31, 65 | syl3anc 1370 |
. . . 4
⊢ ((𝜑 ∧ (𝑖 ∈ 𝐵 ∧ 𝑗 ∈ 𝐵)) → (𝑖(+g‘𝑅)𝑗) ∈ 𝐵) |
67 | | ovexd 7306 |
. . . 4
⊢ ((𝜑 ∧ (𝑖 ∈ 𝐵 ∧ 𝑗 ∈ 𝐵)) → (𝑃 ↑ (𝑖(+g‘𝑅)𝑗)) ∈ V) |
68 | 6, 64, 66, 67 | fvmptd2 6880 |
. . 3
⊢ ((𝜑 ∧ (𝑖 ∈ 𝐵 ∧ 𝑗 ∈ 𝐵)) → (𝐹‘(𝑖(+g‘𝑅)𝑗)) = (𝑃 ↑ (𝑖(+g‘𝑅)𝑗))) |
69 | 45, 49 | oveq12d 7289 |
. . 3
⊢ ((𝜑 ∧ (𝑖 ∈ 𝐵 ∧ 𝑗 ∈ 𝐵)) → ((𝐹‘𝑖)(+g‘𝑅)(𝐹‘𝑗)) = ((𝑃 ↑ 𝑖)(+g‘𝑅)(𝑃 ↑ 𝑗))) |
70 | 62, 68, 69 | 3eqtr4d 2790 |
. 2
⊢ ((𝜑 ∧ (𝑖 ∈ 𝐵 ∧ 𝑗 ∈ 𝐵)) → (𝐹‘(𝑖(+g‘𝑅)𝑗)) = ((𝐹‘𝑖)(+g‘𝑅)(𝐹‘𝑗))) |
71 | 1, 2, 2, 3, 3, 5, 5, 25, 51, 1, 52, 52, 58, 70 | isrhmd 19971 |
1
⊢ (𝜑 → 𝐹 ∈ (𝑅 RingHom 𝑅)) |