Step | Hyp | Ref
| Expression |
1 | | eqid 2736 |
. . 3
⊢
(od‘𝑃) =
(od‘𝑃) |
2 | | eqid 2736 |
. . 3
⊢
(1r‘𝑃) = (1r‘𝑃) |
3 | | eqid 2736 |
. . 3
⊢
(chr‘𝑃) =
(chr‘𝑃) |
4 | 1, 2, 3 | chrval 20928 |
. 2
⊢
((od‘𝑃)‘(1r‘𝑃)) = (chr‘𝑃) |
5 | | eqid 2736 |
. . . . . . . . . 10
⊢
(od‘𝑅) =
(od‘𝑅) |
6 | | eqid 2736 |
. . . . . . . . . 10
⊢
(1r‘𝑅) = (1r‘𝑅) |
7 | | eqid 2736 |
. . . . . . . . . 10
⊢
(chr‘𝑅) =
(chr‘𝑅) |
8 | 5, 6, 7 | chrval 20928 |
. . . . . . . . 9
⊢
((od‘𝑅)‘(1r‘𝑅)) = (chr‘𝑅) |
9 | 8 | eqcomi 2745 |
. . . . . . . 8
⊢
(chr‘𝑅) =
((od‘𝑅)‘(1r‘𝑅)) |
10 | | id 22 |
. . . . . . . . . 10
⊢ (𝑅 ∈ CRing → 𝑅 ∈ CRing) |
11 | 10 | crnggrpd 19978 |
. . . . . . . . 9
⊢ (𝑅 ∈ CRing → 𝑅 ∈ Grp) |
12 | | crngring 19976 |
. . . . . . . . . 10
⊢ (𝑅 ∈ CRing → 𝑅 ∈ Ring) |
13 | | eqid 2736 |
. . . . . . . . . . 11
⊢
(Base‘𝑅) =
(Base‘𝑅) |
14 | 13, 6 | ringidcl 19989 |
. . . . . . . . . 10
⊢ (𝑅 ∈ Ring →
(1r‘𝑅)
∈ (Base‘𝑅)) |
15 | 12, 14 | syl 17 |
. . . . . . . . 9
⊢ (𝑅 ∈ CRing →
(1r‘𝑅)
∈ (Base‘𝑅)) |
16 | 7 | chrcl 20929 |
. . . . . . . . . 10
⊢ (𝑅 ∈ Ring →
(chr‘𝑅) ∈
ℕ0) |
17 | 12, 16 | syl 17 |
. . . . . . . . 9
⊢ (𝑅 ∈ CRing →
(chr‘𝑅) ∈
ℕ0) |
18 | | eqid 2736 |
. . . . . . . . . 10
⊢
(.g‘𝑅) = (.g‘𝑅) |
19 | | eqid 2736 |
. . . . . . . . . 10
⊢
(0g‘𝑅) = (0g‘𝑅) |
20 | 13, 5, 18, 19 | odeq 19332 |
. . . . . . . . 9
⊢ ((𝑅 ∈ Grp ∧
(1r‘𝑅)
∈ (Base‘𝑅) ∧
(chr‘𝑅) ∈
ℕ0) → ((chr‘𝑅) = ((od‘𝑅)‘(1r‘𝑅)) ↔ ∀𝑛 ∈ ℕ0
((chr‘𝑅) ∥
𝑛 ↔ (𝑛(.g‘𝑅)(1r‘𝑅)) = (0g‘𝑅)))) |
21 | 11, 15, 17, 20 | syl3anc 1371 |
. . . . . . . 8
⊢ (𝑅 ∈ CRing →
((chr‘𝑅) =
((od‘𝑅)‘(1r‘𝑅)) ↔ ∀𝑛 ∈ ℕ0
((chr‘𝑅) ∥
𝑛 ↔ (𝑛(.g‘𝑅)(1r‘𝑅)) = (0g‘𝑅)))) |
22 | 9, 21 | mpbii 232 |
. . . . . . 7
⊢ (𝑅 ∈ CRing →
∀𝑛 ∈
ℕ0 ((chr‘𝑅) ∥ 𝑛 ↔ (𝑛(.g‘𝑅)(1r‘𝑅)) = (0g‘𝑅))) |
23 | 22 | r19.21bi 3234 |
. . . . . 6
⊢ ((𝑅 ∈ CRing ∧ 𝑛 ∈ ℕ0)
→ ((chr‘𝑅)
∥ 𝑛 ↔ (𝑛(.g‘𝑅)(1r‘𝑅)) = (0g‘𝑅))) |
24 | | ply1chr.1 |
. . . . . . 7
⊢ 𝑃 = (Poly1‘𝑅) |
25 | | eqid 2736 |
. . . . . . 7
⊢
(algSc‘𝑃) =
(algSc‘𝑃) |
26 | 12 | adantr 481 |
. . . . . . 7
⊢ ((𝑅 ∈ CRing ∧ 𝑛 ∈ ℕ0)
→ 𝑅 ∈
Ring) |
27 | 11 | grpmndd 18760 |
. . . . . . . . 9
⊢ (𝑅 ∈ CRing → 𝑅 ∈ Mnd) |
28 | 27 | adantr 481 |
. . . . . . . 8
⊢ ((𝑅 ∈ CRing ∧ 𝑛 ∈ ℕ0)
→ 𝑅 ∈
Mnd) |
29 | | simpr 485 |
. . . . . . . 8
⊢ ((𝑅 ∈ CRing ∧ 𝑛 ∈ ℕ0)
→ 𝑛 ∈
ℕ0) |
30 | 15 | adantr 481 |
. . . . . . . 8
⊢ ((𝑅 ∈ CRing ∧ 𝑛 ∈ ℕ0)
→ (1r‘𝑅) ∈ (Base‘𝑅)) |
31 | 13, 18, 28, 29, 30 | mulgnn0cld 18897 |
. . . . . . 7
⊢ ((𝑅 ∈ CRing ∧ 𝑛 ∈ ℕ0)
→ (𝑛(.g‘𝑅)(1r‘𝑅)) ∈ (Base‘𝑅)) |
32 | | simpl 483 |
. . . . . . . 8
⊢ ((𝑅 ∈ CRing ∧ 𝑛 ∈ ℕ0)
→ 𝑅 ∈
CRing) |
33 | 13, 19 | ring0cl 19990 |
. . . . . . . 8
⊢ (𝑅 ∈ Ring →
(0g‘𝑅)
∈ (Base‘𝑅)) |
34 | 32, 12, 33 | 3syl 18 |
. . . . . . 7
⊢ ((𝑅 ∈ CRing ∧ 𝑛 ∈ ℕ0)
→ (0g‘𝑅) ∈ (Base‘𝑅)) |
35 | 24, 13, 25, 26, 31, 34 | ply1scleq 32266 |
. . . . . 6
⊢ ((𝑅 ∈ CRing ∧ 𝑛 ∈ ℕ0)
→ (((algSc‘𝑃)‘(𝑛(.g‘𝑅)(1r‘𝑅))) = ((algSc‘𝑃)‘(0g‘𝑅)) ↔ (𝑛(.g‘𝑅)(1r‘𝑅)) = (0g‘𝑅))) |
36 | 24 | ply1sca 21624 |
. . . . . . . . . . . 12
⊢ (𝑅 ∈ CRing → 𝑅 = (Scalar‘𝑃)) |
37 | 36 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ CRing ∧ 𝑛 ∈ ℕ0)
→ 𝑅 =
(Scalar‘𝑃)) |
38 | 37 | fveq2d 6846 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ CRing ∧ 𝑛 ∈ ℕ0)
→ (.g‘𝑅) = (.g‘(Scalar‘𝑃))) |
39 | 38 | oveqd 7374 |
. . . . . . . . 9
⊢ ((𝑅 ∈ CRing ∧ 𝑛 ∈ ℕ0)
→ (𝑛(.g‘𝑅)(1r‘𝑅)) = (𝑛(.g‘(Scalar‘𝑃))(1r‘𝑅))) |
40 | 39 | fveq2d 6846 |
. . . . . . . 8
⊢ ((𝑅 ∈ CRing ∧ 𝑛 ∈ ℕ0)
→ ((algSc‘𝑃)‘(𝑛(.g‘𝑅)(1r‘𝑅))) = ((algSc‘𝑃)‘(𝑛(.g‘(Scalar‘𝑃))(1r‘𝑅)))) |
41 | 24 | ply1assa 21570 |
. . . . . . . . . 10
⊢ (𝑅 ∈ CRing → 𝑃 ∈ AssAlg) |
42 | 41 | adantr 481 |
. . . . . . . . 9
⊢ ((𝑅 ∈ CRing ∧ 𝑛 ∈ ℕ0)
→ 𝑃 ∈
AssAlg) |
43 | 37 | fveq2d 6846 |
. . . . . . . . . 10
⊢ ((𝑅 ∈ CRing ∧ 𝑛 ∈ ℕ0)
→ (Base‘𝑅) =
(Base‘(Scalar‘𝑃))) |
44 | 30, 43 | eleqtrd 2840 |
. . . . . . . . 9
⊢ ((𝑅 ∈ CRing ∧ 𝑛 ∈ ℕ0)
→ (1r‘𝑅) ∈ (Base‘(Scalar‘𝑃))) |
45 | | eqid 2736 |
. . . . . . . . . 10
⊢
(Scalar‘𝑃) =
(Scalar‘𝑃) |
46 | | eqid 2736 |
. . . . . . . . . 10
⊢
(Base‘(Scalar‘𝑃)) = (Base‘(Scalar‘𝑃)) |
47 | | eqid 2736 |
. . . . . . . . . 10
⊢
(.g‘𝑃) = (.g‘𝑃) |
48 | | eqid 2736 |
. . . . . . . . . 10
⊢
(.g‘(Scalar‘𝑃)) =
(.g‘(Scalar‘𝑃)) |
49 | 25, 45, 46, 47, 48 | asclmulg 32263 |
. . . . . . . . 9
⊢ ((𝑃 ∈ AssAlg ∧ 𝑛 ∈ ℕ0
∧ (1r‘𝑅) ∈ (Base‘(Scalar‘𝑃))) → ((algSc‘𝑃)‘(𝑛(.g‘(Scalar‘𝑃))(1r‘𝑅))) = (𝑛(.g‘𝑃)((algSc‘𝑃)‘(1r‘𝑅)))) |
50 | 42, 29, 44, 49 | syl3anc 1371 |
. . . . . . . 8
⊢ ((𝑅 ∈ CRing ∧ 𝑛 ∈ ℕ0)
→ ((algSc‘𝑃)‘(𝑛(.g‘(Scalar‘𝑃))(1r‘𝑅))) = (𝑛(.g‘𝑃)((algSc‘𝑃)‘(1r‘𝑅)))) |
51 | 40, 50 | eqtrd 2776 |
. . . . . . 7
⊢ ((𝑅 ∈ CRing ∧ 𝑛 ∈ ℕ0)
→ ((algSc‘𝑃)‘(𝑛(.g‘𝑅)(1r‘𝑅))) = (𝑛(.g‘𝑃)((algSc‘𝑃)‘(1r‘𝑅)))) |
52 | | eqid 2736 |
. . . . . . . . 9
⊢
(0g‘𝑃) = (0g‘𝑃) |
53 | 24, 25, 19, 52 | ply1scl0 21661 |
. . . . . . . 8
⊢ (𝑅 ∈ Ring →
((algSc‘𝑃)‘(0g‘𝑅)) = (0g‘𝑃)) |
54 | 32, 12, 53 | 3syl 18 |
. . . . . . 7
⊢ ((𝑅 ∈ CRing ∧ 𝑛 ∈ ℕ0)
→ ((algSc‘𝑃)‘(0g‘𝑅)) = (0g‘𝑃)) |
55 | 51, 54 | eqeq12d 2752 |
. . . . . 6
⊢ ((𝑅 ∈ CRing ∧ 𝑛 ∈ ℕ0)
→ (((algSc‘𝑃)‘(𝑛(.g‘𝑅)(1r‘𝑅))) = ((algSc‘𝑃)‘(0g‘𝑅)) ↔ (𝑛(.g‘𝑃)((algSc‘𝑃)‘(1r‘𝑅))) = (0g‘𝑃))) |
56 | 23, 35, 55 | 3bitr2d 306 |
. . . . 5
⊢ ((𝑅 ∈ CRing ∧ 𝑛 ∈ ℕ0)
→ ((chr‘𝑅)
∥ 𝑛 ↔ (𝑛(.g‘𝑃)((algSc‘𝑃)‘(1r‘𝑅))) = (0g‘𝑃))) |
57 | 56 | ralrimiva 3143 |
. . . 4
⊢ (𝑅 ∈ CRing →
∀𝑛 ∈
ℕ0 ((chr‘𝑅) ∥ 𝑛 ↔ (𝑛(.g‘𝑃)((algSc‘𝑃)‘(1r‘𝑅))) = (0g‘𝑃))) |
58 | 24 | ply1crng 21569 |
. . . . . 6
⊢ (𝑅 ∈ CRing → 𝑃 ∈ CRing) |
59 | 58 | crnggrpd 19978 |
. . . . 5
⊢ (𝑅 ∈ CRing → 𝑃 ∈ Grp) |
60 | | eqid 2736 |
. . . . . . 7
⊢
(Base‘𝑃) =
(Base‘𝑃) |
61 | 24, 25, 13, 60 | ply1sclcl 21657 |
. . . . . 6
⊢ ((𝑅 ∈ Ring ∧
(1r‘𝑅)
∈ (Base‘𝑅))
→ ((algSc‘𝑃)‘(1r‘𝑅)) ∈ (Base‘𝑃)) |
62 | 12, 15, 61 | syl2anc 584 |
. . . . 5
⊢ (𝑅 ∈ CRing →
((algSc‘𝑃)‘(1r‘𝑅)) ∈ (Base‘𝑃)) |
63 | 60, 1, 47, 52 | odeq 19332 |
. . . . 5
⊢ ((𝑃 ∈ Grp ∧
((algSc‘𝑃)‘(1r‘𝑅)) ∈ (Base‘𝑃) ∧ (chr‘𝑅) ∈ ℕ0)
→ ((chr‘𝑅) =
((od‘𝑃)‘((algSc‘𝑃)‘(1r‘𝑅))) ↔ ∀𝑛 ∈ ℕ0
((chr‘𝑅) ∥
𝑛 ↔ (𝑛(.g‘𝑃)((algSc‘𝑃)‘(1r‘𝑅))) = (0g‘𝑃)))) |
64 | 59, 62, 17, 63 | syl3anc 1371 |
. . . 4
⊢ (𝑅 ∈ CRing →
((chr‘𝑅) =
((od‘𝑃)‘((algSc‘𝑃)‘(1r‘𝑅))) ↔ ∀𝑛 ∈ ℕ0
((chr‘𝑅) ∥
𝑛 ↔ (𝑛(.g‘𝑃)((algSc‘𝑃)‘(1r‘𝑅))) = (0g‘𝑃)))) |
65 | 57, 64 | mpbird 256 |
. . 3
⊢ (𝑅 ∈ CRing →
(chr‘𝑅) =
((od‘𝑃)‘((algSc‘𝑃)‘(1r‘𝑅)))) |
66 | 24, 25, 6, 2 | ply1scl1 21663 |
. . . . 5
⊢ (𝑅 ∈ Ring →
((algSc‘𝑃)‘(1r‘𝑅)) = (1r‘𝑃)) |
67 | 66 | fveq2d 6846 |
. . . 4
⊢ (𝑅 ∈ Ring →
((od‘𝑃)‘((algSc‘𝑃)‘(1r‘𝑅))) = ((od‘𝑃)‘(1r‘𝑃))) |
68 | 12, 67 | syl 17 |
. . 3
⊢ (𝑅 ∈ CRing →
((od‘𝑃)‘((algSc‘𝑃)‘(1r‘𝑅))) = ((od‘𝑃)‘(1r‘𝑃))) |
69 | 65, 68 | eqtr2d 2777 |
. 2
⊢ (𝑅 ∈ CRing →
((od‘𝑃)‘(1r‘𝑃)) = (chr‘𝑅)) |
70 | 4, 69 | eqtr3id 2790 |
1
⊢ (𝑅 ∈ CRing →
(chr‘𝑃) =
(chr‘𝑅)) |