| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | eqid 2736 | . 2
⊢
(0g‘𝐾) = (0g‘𝐾) | 
| 2 |  | aks5lem1.1 | . . 3
⊢ (𝜑 → 𝐾 ∈ Field) | 
| 3 |  | aks5lem1.2 | . . 3
⊢ 𝑃 = (chr‘𝐾) | 
| 4 |  | aks5lem1.3 | . . 3
⊢ (𝜑 → (𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ ∧ 𝑃 ∥ 𝑁)) | 
| 5 |  | aks5lem1.4 | . . 3
⊢ 𝐹 = (𝑝 ∈
(Base‘(Poly1‘(ℤ/nℤ‘𝑁))) ↦ (𝐺 ∘ 𝑝)) | 
| 6 |  | aks5lem1.5 | . . 3
⊢ 𝐺 = (𝑞 ∈
(Base‘(ℤ/nℤ‘𝑁)) ↦ ∪
((ℤRHom‘𝐾)
“ 𝑞)) | 
| 7 |  | aks5lem1.6 | . . 3
⊢ 𝐻 = (𝑟 ∈
(Base‘(Poly1‘𝐾)) ↦ (((eval1‘𝐾)‘𝑟)‘𝑀)) | 
| 8 |  | aks5lem2.1 | . . . . . 6
⊢ (𝜑 → 𝑀 ∈ ((mulGrp‘𝐾) PrimRoots 𝑅)) | 
| 9 | 2 | fldcrngd 20743 | . . . . . . . 8
⊢ (𝜑 → 𝐾 ∈ CRing) | 
| 10 |  | eqid 2736 | . . . . . . . . 9
⊢
(mulGrp‘𝐾) =
(mulGrp‘𝐾) | 
| 11 | 10 | crngmgp 20239 | . . . . . . . 8
⊢ (𝐾 ∈ CRing →
(mulGrp‘𝐾) ∈
CMnd) | 
| 12 | 9, 11 | syl 17 | . . . . . . 7
⊢ (𝜑 → (mulGrp‘𝐾) ∈ CMnd) | 
| 13 |  | aks5lem2.5 | . . . . . . . 8
⊢ (𝜑 → 𝑅 ∈ ℕ) | 
| 14 | 13 | nnnn0d 12589 | . . . . . . 7
⊢ (𝜑 → 𝑅 ∈
ℕ0) | 
| 15 |  | eqid 2736 | . . . . . . 7
⊢
(.g‘(mulGrp‘𝐾)) =
(.g‘(mulGrp‘𝐾)) | 
| 16 | 12, 14, 15 | isprimroot 42095 | . . . . . 6
⊢ (𝜑 → (𝑀 ∈ ((mulGrp‘𝐾) PrimRoots 𝑅) ↔ (𝑀 ∈ (Base‘(mulGrp‘𝐾)) ∧ (𝑅(.g‘(mulGrp‘𝐾))𝑀) = (0g‘(mulGrp‘𝐾)) ∧ ∀𝑙 ∈ ℕ0
((𝑙(.g‘(mulGrp‘𝐾))𝑀) = (0g‘(mulGrp‘𝐾)) → 𝑅 ∥ 𝑙)))) | 
| 17 | 8, 16 | mpbid 232 | . . . . 5
⊢ (𝜑 → (𝑀 ∈ (Base‘(mulGrp‘𝐾)) ∧ (𝑅(.g‘(mulGrp‘𝐾))𝑀) = (0g‘(mulGrp‘𝐾)) ∧ ∀𝑙 ∈ ℕ0
((𝑙(.g‘(mulGrp‘𝐾))𝑀) = (0g‘(mulGrp‘𝐾)) → 𝑅 ∥ 𝑙))) | 
| 18 | 17 | simp1d 1142 | . . . 4
⊢ (𝜑 → 𝑀 ∈ (Base‘(mulGrp‘𝐾))) | 
| 19 |  | eqid 2736 | . . . . . 6
⊢
(Base‘𝐾) =
(Base‘𝐾) | 
| 20 | 10, 19 | mgpbas 20143 | . . . . 5
⊢
(Base‘𝐾) =
(Base‘(mulGrp‘𝐾)) | 
| 21 | 20 | eqcomi 2745 | . . . 4
⊢
(Base‘(mulGrp‘𝐾)) = (Base‘𝐾) | 
| 22 | 18, 21 | eleqtrdi 2850 | . . 3
⊢ (𝜑 → 𝑀 ∈ (Base‘𝐾)) | 
| 23 | 2, 3, 4, 5, 6, 7, 22 | aks5lem1 42188 | . 2
⊢ (𝜑 → (𝐻 ∘ 𝐹) ∈
((Poly1‘(ℤ/nℤ‘𝑁)) RingHom 𝐾)) | 
| 24 |  | eqid 2736 | . 2
⊢ (◡(𝐻 ∘ 𝐹) “ {(0g‘𝐾)}) = (◡(𝐻 ∘ 𝐹) “ {(0g‘𝐾)}) | 
| 25 |  | aks5lem2.3 | . 2
⊢ 𝐴 =
((Poly1‘(ℤ/nℤ‘𝑁)) /s
((Poly1‘(ℤ/nℤ‘𝑁)) ~QG 𝐿)) | 
| 26 |  | aks5lem2.2 | . 2
⊢ 𝐼 = (𝑠 ∈ (Base‘𝐴) ↦ ∪
((𝐻 ∘ 𝐹) “ 𝑠)) | 
| 27 | 4 | simp2d 1143 | . . . . 5
⊢ (𝜑 → 𝑁 ∈ ℕ) | 
| 28 | 27 | nnnn0d 12589 | . . . 4
⊢ (𝜑 → 𝑁 ∈
ℕ0) | 
| 29 |  | eqid 2736 | . . . . 5
⊢
(ℤ/nℤ‘𝑁) = (ℤ/nℤ‘𝑁) | 
| 30 | 29 | zncrng 21564 | . . . 4
⊢ (𝑁 ∈ ℕ0
→ (ℤ/nℤ‘𝑁) ∈ CRing) | 
| 31 | 28, 30 | syl 17 | . . 3
⊢ (𝜑 →
(ℤ/nℤ‘𝑁) ∈ CRing) | 
| 32 |  | eqid 2736 | . . . 4
⊢
(Poly1‘(ℤ/nℤ‘𝑁)) =
(Poly1‘(ℤ/nℤ‘𝑁)) | 
| 33 | 32 | ply1crng 22201 | . . 3
⊢
((ℤ/nℤ‘𝑁) ∈ CRing →
(Poly1‘(ℤ/nℤ‘𝑁)) ∈ CRing) | 
| 34 | 31, 33 | syl 17 | . 2
⊢ (𝜑 →
(Poly1‘(ℤ/nℤ‘𝑁)) ∈ CRing) | 
| 35 |  | aks5lem2.4 | . 2
⊢ 𝐿 =
((RSpan‘(Poly1‘(ℤ/nℤ‘𝑁)))‘{((𝑅(.g‘(mulGrp‘(Poly1‘(ℤ/nℤ‘𝑁))))(var1‘(ℤ/nℤ‘𝑁)))(-g‘(Poly1‘(ℤ/nℤ‘𝑁)))(1r‘(Poly1‘(ℤ/nℤ‘𝑁))))}) | 
| 36 | 34 | crnggrpd 20245 | . . 3
⊢ (𝜑 →
(Poly1‘(ℤ/nℤ‘𝑁)) ∈ Grp) | 
| 37 |  | eqid 2736 | . . . . 5
⊢
(mulGrp‘(Poly1‘(ℤ/nℤ‘𝑁))) =
(mulGrp‘(Poly1‘(ℤ/nℤ‘𝑁))) | 
| 38 |  | eqid 2736 | . . . . 5
⊢
(Base‘(Poly1‘(ℤ/nℤ‘𝑁))) =
(Base‘(Poly1‘(ℤ/nℤ‘𝑁))) | 
| 39 | 37, 38 | mgpbas 20143 | . . . 4
⊢
(Base‘(Poly1‘(ℤ/nℤ‘𝑁))) =
(Base‘(mulGrp‘(Poly1‘(ℤ/nℤ‘𝑁)))) | 
| 40 |  | eqid 2736 | . . . 4
⊢
(.g‘(mulGrp‘(Poly1‘(ℤ/nℤ‘𝑁)))) =
(.g‘(mulGrp‘(Poly1‘(ℤ/nℤ‘𝑁)))) | 
| 41 | 34 | crngringd 20244 | . . . . 5
⊢ (𝜑 →
(Poly1‘(ℤ/nℤ‘𝑁)) ∈ Ring) | 
| 42 | 37 | ringmgp 20237 | . . . . 5
⊢
((Poly1‘(ℤ/nℤ‘𝑁)) ∈ Ring →
(mulGrp‘(Poly1‘(ℤ/nℤ‘𝑁))) ∈ Mnd) | 
| 43 | 41, 42 | syl 17 | . . . 4
⊢ (𝜑 →
(mulGrp‘(Poly1‘(ℤ/nℤ‘𝑁))) ∈ Mnd) | 
| 44 | 31 | crngringd 20244 | . . . . 5
⊢ (𝜑 →
(ℤ/nℤ‘𝑁) ∈ Ring) | 
| 45 |  | eqid 2736 | . . . . . 6
⊢
(var1‘(ℤ/nℤ‘𝑁)) =
(var1‘(ℤ/nℤ‘𝑁)) | 
| 46 | 45, 32, 38 | vr1cl 22220 | . . . . 5
⊢
((ℤ/nℤ‘𝑁) ∈ Ring →
(var1‘(ℤ/nℤ‘𝑁)) ∈
(Base‘(Poly1‘(ℤ/nℤ‘𝑁)))) | 
| 47 | 44, 46 | syl 17 | . . . 4
⊢ (𝜑 →
(var1‘(ℤ/nℤ‘𝑁)) ∈
(Base‘(Poly1‘(ℤ/nℤ‘𝑁)))) | 
| 48 | 39, 40, 43, 14, 47 | mulgnn0cld 19114 | . . 3
⊢ (𝜑 → (𝑅(.g‘(mulGrp‘(Poly1‘(ℤ/nℤ‘𝑁))))(var1‘(ℤ/nℤ‘𝑁))) ∈ (Base‘(Poly1‘(ℤ/nℤ‘𝑁)))) | 
| 49 |  | eqid 2736 | . . . . 5
⊢
(1r‘(Poly1‘(ℤ/nℤ‘𝑁))) =
(1r‘(Poly1‘(ℤ/nℤ‘𝑁))) | 
| 50 | 38, 49 | ringidcl 20263 | . . . 4
⊢
((Poly1‘(ℤ/nℤ‘𝑁)) ∈ Ring →
(1r‘(Poly1‘(ℤ/nℤ‘𝑁))) ∈
(Base‘(Poly1‘(ℤ/nℤ‘𝑁)))) | 
| 51 | 41, 50 | syl 17 | . . 3
⊢ (𝜑 →
(1r‘(Poly1‘(ℤ/nℤ‘𝑁))) ∈
(Base‘(Poly1‘(ℤ/nℤ‘𝑁)))) | 
| 52 |  | eqid 2736 | . . . 4
⊢
(-g‘(Poly1‘(ℤ/nℤ‘𝑁))) =
(-g‘(Poly1‘(ℤ/nℤ‘𝑁))) | 
| 53 | 38, 52 | grpsubcl 19039 | . . 3
⊢
(((Poly1‘(ℤ/nℤ‘𝑁)) ∈ Grp ∧ (𝑅(.g‘(mulGrp‘(Poly1‘(ℤ/nℤ‘𝑁))))(var1‘(ℤ/nℤ‘𝑁))) ∈ (Base‘(Poly1‘(ℤ/nℤ‘𝑁))) ∧ (1r‘(Poly1‘(ℤ/nℤ‘𝑁))) ∈ (Base‘(Poly1‘(ℤ/nℤ‘𝑁)))) → ((𝑅(.g‘(mulGrp‘(Poly1‘(ℤ/nℤ‘𝑁))))(var1‘(ℤ/nℤ‘𝑁)))(-g‘(Poly1‘(ℤ/nℤ‘𝑁)))(1r‘(Poly1‘(ℤ/nℤ‘𝑁)))) ∈
(Base‘(Poly1‘(ℤ/nℤ‘𝑁)))) | 
| 54 | 36, 48, 51, 53 | syl3anc 1372 | . 2
⊢ (𝜑 → ((𝑅(.g‘(mulGrp‘(Poly1‘(ℤ/nℤ‘𝑁))))(var1‘(ℤ/nℤ‘𝑁)))(-g‘(Poly1‘(ℤ/nℤ‘𝑁)))(1r‘(Poly1‘(ℤ/nℤ‘𝑁)))) ∈
(Base‘(Poly1‘(ℤ/nℤ‘𝑁)))) | 
| 55 |  | fvexd 6920 | . . . . . . . . . 10
⊢ (𝜑 →
(Base‘(ℤ/nℤ‘𝑁)) ∈ V) | 
| 56 | 55 | mptexd 7245 | . . . . . . . . 9
⊢ (𝜑 → (𝑞 ∈
(Base‘(ℤ/nℤ‘𝑁)) ↦ ∪
((ℤRHom‘𝐾)
“ 𝑞)) ∈
V) | 
| 57 | 6, 56 | eqeltrid 2844 | . . . . . . . 8
⊢ (𝜑 → 𝐺 ∈ V) | 
| 58 | 57 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑝 ∈
(Base‘(Poly1‘(ℤ/nℤ‘𝑁)))) → 𝐺 ∈ V) | 
| 59 |  | vex 3483 | . . . . . . . 8
⊢ 𝑝 ∈ V | 
| 60 | 59 | a1i 11 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑝 ∈
(Base‘(Poly1‘(ℤ/nℤ‘𝑁)))) → 𝑝 ∈ V) | 
| 61 | 58, 60 | coexd 7954 | . . . . . 6
⊢ ((𝜑 ∧ 𝑝 ∈
(Base‘(Poly1‘(ℤ/nℤ‘𝑁)))) → (𝐺 ∘ 𝑝) ∈ V) | 
| 62 | 61, 5 | fmptd 7133 | . . . . 5
⊢ (𝜑 → 𝐹:(Base‘(Poly1‘(ℤ/nℤ‘𝑁)))⟶V) | 
| 63 | 62 | ffund 6739 | . . . 4
⊢ (𝜑 → Fun 𝐹) | 
| 64 | 62 | fdmd 6745 | . . . . 5
⊢ (𝜑 → dom 𝐹 =
(Base‘(Poly1‘(ℤ/nℤ‘𝑁)))) | 
| 65 | 54, 64 | eleqtrrd 2843 | . . . 4
⊢ (𝜑 → ((𝑅(.g‘(mulGrp‘(Poly1‘(ℤ/nℤ‘𝑁))))(var1‘(ℤ/nℤ‘𝑁)))(-g‘(Poly1‘(ℤ/nℤ‘𝑁)))(1r‘(Poly1‘(ℤ/nℤ‘𝑁)))) ∈ dom 𝐹) | 
| 66 |  | fvco 7006 | . . . 4
⊢ ((Fun
𝐹 ∧ ((𝑅(.g‘(mulGrp‘(Poly1‘(ℤ/nℤ‘𝑁))))(var1‘(ℤ/nℤ‘𝑁)))(-g‘(Poly1‘(ℤ/nℤ‘𝑁)))(1r‘(Poly1‘(ℤ/nℤ‘𝑁)))) ∈ dom 𝐹) →
((𝐻 ∘ 𝐹)‘((𝑅(.g‘(mulGrp‘(Poly1‘(ℤ/nℤ‘𝑁))))(var1‘(ℤ/nℤ‘𝑁)))(-g‘(Poly1‘(ℤ/nℤ‘𝑁)))(1r‘(Poly1‘(ℤ/nℤ‘𝑁))))) = (𝐻‘(𝐹‘((𝑅(.g‘(mulGrp‘(Poly1‘(ℤ/nℤ‘𝑁))))(var1‘(ℤ/nℤ‘𝑁)))(-g‘(Poly1‘(ℤ/nℤ‘𝑁)))(1r‘(Poly1‘(ℤ/nℤ‘𝑁))))))) | 
| 67 | 63, 65, 66 | syl2anc 584 | . . 3
⊢ (𝜑 → ((𝐻 ∘ 𝐹)‘((𝑅(.g‘(mulGrp‘(Poly1‘(ℤ/nℤ‘𝑁))))(var1‘(ℤ/nℤ‘𝑁)))(-g‘(Poly1‘(ℤ/nℤ‘𝑁)))(1r‘(Poly1‘(ℤ/nℤ‘𝑁))))) = (𝐻‘(𝐹‘((𝑅(.g‘(mulGrp‘(Poly1‘(ℤ/nℤ‘𝑁))))(var1‘(ℤ/nℤ‘𝑁)))(-g‘(Poly1‘(ℤ/nℤ‘𝑁)))(1r‘(Poly1‘(ℤ/nℤ‘𝑁))))))) | 
| 68 |  | eqid 2736 | . . . . . . . 8
⊢
(Poly1‘𝐾) = (Poly1‘𝐾) | 
| 69 | 9 | crngringd 20244 | . . . . . . . . 9
⊢ (𝜑 → 𝐾 ∈ Ring) | 
| 70 | 4 | simp1d 1142 | . . . . . . . . . . . 12
⊢ (𝜑 → 𝑃 ∈ ℙ) | 
| 71 |  | prmnn 16712 | . . . . . . . . . . . 12
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℕ) | 
| 72 | 70, 71 | syl 17 | . . . . . . . . . . 11
⊢ (𝜑 → 𝑃 ∈ ℕ) | 
| 73 | 3, 72 | eqeltrrid 2845 | . . . . . . . . . 10
⊢ (𝜑 → (chr‘𝐾) ∈
ℕ) | 
| 74 | 73 | nnzd 12642 | . . . . . . . . 9
⊢ (𝜑 → (chr‘𝐾) ∈
ℤ) | 
| 75 | 4 | simp3d 1144 | . . . . . . . . . 10
⊢ (𝜑 → 𝑃 ∥ 𝑁) | 
| 76 | 3, 75 | eqbrtrrid 5178 | . . . . . . . . 9
⊢ (𝜑 → (chr‘𝐾) ∥ 𝑁) | 
| 77 | 69, 27, 74, 76, 29, 6 | zndvdchrrhm 41973 | . . . . . . . 8
⊢ (𝜑 → 𝐺 ∈
((ℤ/nℤ‘𝑁) RingHom 𝐾)) | 
| 78 | 32, 68, 38, 5, 77 | rhmply1 22391 | . . . . . . 7
⊢ (𝜑 → 𝐹 ∈
((Poly1‘(ℤ/nℤ‘𝑁)) RingHom (Poly1‘𝐾))) | 
| 79 |  | rhmghm 20485 | . . . . . . 7
⊢ (𝐹 ∈
((Poly1‘(ℤ/nℤ‘𝑁)) RingHom (Poly1‘𝐾)) → 𝐹 ∈
((Poly1‘(ℤ/nℤ‘𝑁)) GrpHom (Poly1‘𝐾))) | 
| 80 | 78, 79 | syl 17 | . . . . . 6
⊢ (𝜑 → 𝐹 ∈
((Poly1‘(ℤ/nℤ‘𝑁)) GrpHom (Poly1‘𝐾))) | 
| 81 |  | eqid 2736 | . . . . . . 7
⊢
(-g‘(Poly1‘𝐾)) =
(-g‘(Poly1‘𝐾)) | 
| 82 | 38, 52, 81 | ghmsub 19243 | . . . . . 6
⊢ ((𝐹 ∈
((Poly1‘(ℤ/nℤ‘𝑁)) GrpHom (Poly1‘𝐾)) ∧ (𝑅(.g‘(mulGrp‘(Poly1‘(ℤ/nℤ‘𝑁))))(var1‘(ℤ/nℤ‘𝑁))) ∈ (Base‘(Poly1‘(ℤ/nℤ‘𝑁))) ∧ (1r‘(Poly1‘(ℤ/nℤ‘𝑁))) ∈ (Base‘(Poly1‘(ℤ/nℤ‘𝑁)))) → (𝐹‘((𝑅(.g‘(mulGrp‘(Poly1‘(ℤ/nℤ‘𝑁))))(var1‘(ℤ/nℤ‘𝑁)))(-g‘(Poly1‘(ℤ/nℤ‘𝑁)))(1r‘(Poly1‘(ℤ/nℤ‘𝑁))))) = ((𝐹‘(𝑅(.g‘(mulGrp‘(Poly1‘(ℤ/nℤ‘𝑁))))(var1‘(ℤ/nℤ‘𝑁))))(-g‘(Poly1‘𝐾))(𝐹‘(1r‘(Poly1‘(ℤ/nℤ‘𝑁)))))) | 
| 83 | 80, 48, 51, 82 | syl3anc 1372 | . . . . 5
⊢ (𝜑 → (𝐹‘((𝑅(.g‘(mulGrp‘(Poly1‘(ℤ/nℤ‘𝑁))))(var1‘(ℤ/nℤ‘𝑁)))(-g‘(Poly1‘(ℤ/nℤ‘𝑁)))(1r‘(Poly1‘(ℤ/nℤ‘𝑁))))) = ((𝐹‘(𝑅(.g‘(mulGrp‘(Poly1‘(ℤ/nℤ‘𝑁))))(var1‘(ℤ/nℤ‘𝑁))))(-g‘(Poly1‘𝐾))(𝐹‘(1r‘(Poly1‘(ℤ/nℤ‘𝑁)))))) | 
| 84 | 83 | fveq2d 6909 | . . . 4
⊢ (𝜑 → (𝐻‘(𝐹‘((𝑅(.g‘(mulGrp‘(Poly1‘(ℤ/nℤ‘𝑁))))(var1‘(ℤ/nℤ‘𝑁)))(-g‘(Poly1‘(ℤ/nℤ‘𝑁)))(1r‘(Poly1‘(ℤ/nℤ‘𝑁)))))) = (𝐻‘((𝐹‘(𝑅(.g‘(mulGrp‘(Poly1‘(ℤ/nℤ‘𝑁))))(var1‘(ℤ/nℤ‘𝑁))))(-g‘(Poly1‘𝐾))(𝐹‘(1r‘(Poly1‘(ℤ/nℤ‘𝑁))))))) | 
| 85 |  | eqid 2736 | . . . . . . . 8
⊢
(eval1‘𝐾) = (eval1‘𝐾) | 
| 86 |  | eqid 2736 | . . . . . . . 8
⊢
(Base‘(Poly1‘𝐾)) =
(Base‘(Poly1‘𝐾)) | 
| 87 | 85, 68, 19, 86, 9, 22, 7 | evl1maprhm 22384 | . . . . . . 7
⊢ (𝜑 → 𝐻 ∈ ((Poly1‘𝐾) RingHom 𝐾)) | 
| 88 |  | rhmghm 20485 | . . . . . . 7
⊢ (𝐻 ∈
((Poly1‘𝐾)
RingHom 𝐾) → 𝐻 ∈
((Poly1‘𝐾)
GrpHom 𝐾)) | 
| 89 | 87, 88 | syl 17 | . . . . . 6
⊢ (𝜑 → 𝐻 ∈ ((Poly1‘𝐾) GrpHom 𝐾)) | 
| 90 | 38, 86 | rhmf 20486 | . . . . . . . 8
⊢ (𝐹 ∈
((Poly1‘(ℤ/nℤ‘𝑁)) RingHom (Poly1‘𝐾)) → 𝐹:(Base‘(Poly1‘(ℤ/nℤ‘𝑁)))⟶(Base‘(Poly1‘𝐾))) | 
| 91 | 78, 90 | syl 17 | . . . . . . 7
⊢ (𝜑 → 𝐹:(Base‘(Poly1‘(ℤ/nℤ‘𝑁)))⟶(Base‘(Poly1‘𝐾))) | 
| 92 | 91, 48 | ffvelcdmd 7104 | . . . . . 6
⊢ (𝜑 → (𝐹‘(𝑅(.g‘(mulGrp‘(Poly1‘(ℤ/nℤ‘𝑁))))(var1‘(ℤ/nℤ‘𝑁)))) ∈ (Base‘(Poly1‘𝐾))) | 
| 93 | 91, 51 | ffvelcdmd 7104 | . . . . . 6
⊢ (𝜑 → (𝐹‘(1r‘(Poly1‘(ℤ/nℤ‘𝑁)))) ∈ (Base‘(Poly1‘𝐾))) | 
| 94 |  | eqid 2736 | . . . . . . 7
⊢
(-g‘𝐾) = (-g‘𝐾) | 
| 95 | 86, 81, 94 | ghmsub 19243 | . . . . . 6
⊢ ((𝐻 ∈
((Poly1‘𝐾)
GrpHom 𝐾) ∧ (𝐹‘(𝑅(.g‘(mulGrp‘(Poly1‘(ℤ/nℤ‘𝑁))))(var1‘(ℤ/nℤ‘𝑁)))) ∈ (Base‘(Poly1‘𝐾)) ∧ (𝐹‘(1r‘(Poly1‘(ℤ/nℤ‘𝑁)))) ∈ (Base‘(Poly1‘𝐾))) → (𝐻‘((𝐹‘(𝑅(.g‘(mulGrp‘(Poly1‘(ℤ/nℤ‘𝑁))))(var1‘(ℤ/nℤ‘𝑁))))(-g‘(Poly1‘𝐾))(𝐹‘(1r‘(Poly1‘(ℤ/nℤ‘𝑁)))))) = ((𝐻‘(𝐹‘(𝑅(.g‘(mulGrp‘(Poly1‘(ℤ/nℤ‘𝑁))))(var1‘(ℤ/nℤ‘𝑁)))))(-g‘𝐾)(𝐻‘(𝐹‘(1r‘(Poly1‘(ℤ/nℤ‘𝑁))))))) | 
| 96 | 89, 92, 93, 95 | syl3anc 1372 | . . . . 5
⊢ (𝜑 → (𝐻‘((𝐹‘(𝑅(.g‘(mulGrp‘(Poly1‘(ℤ/nℤ‘𝑁))))(var1‘(ℤ/nℤ‘𝑁))))(-g‘(Poly1‘𝐾))(𝐹‘(1r‘(Poly1‘(ℤ/nℤ‘𝑁)))))) = ((𝐻‘(𝐹‘(𝑅(.g‘(mulGrp‘(Poly1‘(ℤ/nℤ‘𝑁))))(var1‘(ℤ/nℤ‘𝑁)))))(-g‘𝐾)(𝐻‘(𝐹‘(1r‘(Poly1‘(ℤ/nℤ‘𝑁))))))) | 
| 97 |  | eqid 2736 | . . . . . . . . . . . . . . . . 17
⊢
(.r‘(Poly1‘(ℤ/nℤ‘𝑁))) =
(.r‘(Poly1‘(ℤ/nℤ‘𝑁))) | 
| 98 | 38, 97, 49, 41, 48 | ringlidmd 20270 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 →
((1r‘(Poly1‘(ℤ/nℤ‘𝑁)))(.r‘(Poly1‘(ℤ/nℤ‘𝑁)))(𝑅(.g‘(mulGrp‘(Poly1‘(ℤ/nℤ‘𝑁))))(var1‘(ℤ/nℤ‘𝑁)))) = (𝑅(.g‘(mulGrp‘(Poly1‘(ℤ/nℤ‘𝑁))))(var1‘(ℤ/nℤ‘𝑁)))) | 
| 99 | 98 | eqcomd 2742 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑅(.g‘(mulGrp‘(Poly1‘(ℤ/nℤ‘𝑁))))(var1‘(ℤ/nℤ‘𝑁))) = ((1r‘(Poly1‘(ℤ/nℤ‘𝑁)))(.r‘(Poly1‘(ℤ/nℤ‘𝑁)))(𝑅(.g‘(mulGrp‘(Poly1‘(ℤ/nℤ‘𝑁))))(var1‘(ℤ/nℤ‘𝑁))))) | 
| 100 | 31 | elexd 3503 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 →
(ℤ/nℤ‘𝑁) ∈ V) | 
| 101 | 32 | ply1sca 22255 | . . . . . . . . . . . . . . . . . . . . 21
⊢
((ℤ/nℤ‘𝑁) ∈ V →
(ℤ/nℤ‘𝑁) =
(Scalar‘(Poly1‘(ℤ/nℤ‘𝑁)))) | 
| 102 | 100, 101 | syl 17 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 →
(ℤ/nℤ‘𝑁) =
(Scalar‘(Poly1‘(ℤ/nℤ‘𝑁)))) | 
| 103 | 102 | fveq2d 6909 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 →
(1r‘(ℤ/nℤ‘𝑁)) =
(1r‘(Scalar‘(Poly1‘(ℤ/nℤ‘𝑁))))) | 
| 104 | 103 | fveq2d 6909 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 →
((algSc‘(Poly1‘(ℤ/nℤ‘𝑁)))‘(1r‘(ℤ/nℤ‘𝑁))) =
((algSc‘(Poly1‘(ℤ/nℤ‘𝑁)))‘(1r‘(Scalar‘(Poly1‘(ℤ/nℤ‘𝑁)))))) | 
| 105 |  | eqid 2736 | . . . . . . . . . . . . . . . . . . 19
⊢
(algSc‘(Poly1‘(ℤ/nℤ‘𝑁))) =
(algSc‘(Poly1‘(ℤ/nℤ‘𝑁))) | 
| 106 |  | eqid 2736 | . . . . . . . . . . . . . . . . . . 19
⊢
(Scalar‘(Poly1‘(ℤ/nℤ‘𝑁))) =
(Scalar‘(Poly1‘(ℤ/nℤ‘𝑁))) | 
| 107 | 32 | ply1lmod 22254 | . . . . . . . . . . . . . . . . . . . 20
⊢
((ℤ/nℤ‘𝑁) ∈ Ring →
(Poly1‘(ℤ/nℤ‘𝑁)) ∈ LMod) | 
| 108 | 44, 107 | syl 17 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 →
(Poly1‘(ℤ/nℤ‘𝑁)) ∈ LMod) | 
| 109 | 105, 106,
108, 41 | ascl1 21906 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 →
((algSc‘(Poly1‘(ℤ/nℤ‘𝑁)))‘(1r‘(Scalar‘(Poly1‘(ℤ/nℤ‘𝑁))))) = (1r‘(Poly1‘(ℤ/nℤ‘𝑁)))) | 
| 110 | 104, 109 | eqtrd 2776 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 →
((algSc‘(Poly1‘(ℤ/nℤ‘𝑁)))‘(1r‘(ℤ/nℤ‘𝑁))) =
(1r‘(Poly1‘(ℤ/nℤ‘𝑁)))) | 
| 111 | 110 | eqcomd 2742 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 →
(1r‘(Poly1‘(ℤ/nℤ‘𝑁))) =
((algSc‘(Poly1‘(ℤ/nℤ‘𝑁)))‘(1r‘(ℤ/nℤ‘𝑁)))) | 
| 112 | 111 | oveq1d 7447 | . . . . . . . . . . . . . . 15
⊢ (𝜑 →
((1r‘(Poly1‘(ℤ/nℤ‘𝑁)))(.r‘(Poly1‘(ℤ/nℤ‘𝑁)))(𝑅(.g‘(mulGrp‘(Poly1‘(ℤ/nℤ‘𝑁))))(var1‘(ℤ/nℤ‘𝑁)))) = (((algSc‘(Poly1‘(ℤ/nℤ‘𝑁)))‘(1r‘(ℤ/nℤ‘𝑁)))(.r‘(Poly1‘(ℤ/nℤ‘𝑁)))(𝑅(.g‘(mulGrp‘(Poly1‘(ℤ/nℤ‘𝑁))))(var1‘(ℤ/nℤ‘𝑁))))) | 
| 113 | 99, 112 | eqtrd 2776 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑅(.g‘(mulGrp‘(Poly1‘(ℤ/nℤ‘𝑁))))(var1‘(ℤ/nℤ‘𝑁))) = (((algSc‘(Poly1‘(ℤ/nℤ‘𝑁)))‘(1r‘(ℤ/nℤ‘𝑁)))(.r‘(Poly1‘(ℤ/nℤ‘𝑁)))(𝑅(.g‘(mulGrp‘(Poly1‘(ℤ/nℤ‘𝑁))))(var1‘(ℤ/nℤ‘𝑁))))) | 
| 114 | 32 | ply1assa 22202 | . . . . . . . . . . . . . . . 16
⊢
((ℤ/nℤ‘𝑁) ∈ CRing →
(Poly1‘(ℤ/nℤ‘𝑁)) ∈ AssAlg) | 
| 115 | 31, 114 | syl 17 | . . . . . . . . . . . . . . 15
⊢ (𝜑 →
(Poly1‘(ℤ/nℤ‘𝑁)) ∈ AssAlg) | 
| 116 |  | eqid 2736 | . . . . . . . . . . . . . . . . . 18
⊢
(Base‘(ℤ/nℤ‘𝑁)) =
(Base‘(ℤ/nℤ‘𝑁)) | 
| 117 |  | eqid 2736 | . . . . . . . . . . . . . . . . . 18
⊢
(1r‘(ℤ/nℤ‘𝑁)) =
(1r‘(ℤ/nℤ‘𝑁)) | 
| 118 | 116, 117 | ringidcl 20263 | . . . . . . . . . . . . . . . . 17
⊢
((ℤ/nℤ‘𝑁) ∈ Ring →
(1r‘(ℤ/nℤ‘𝑁)) ∈
(Base‘(ℤ/nℤ‘𝑁))) | 
| 119 | 44, 118 | syl 17 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 →
(1r‘(ℤ/nℤ‘𝑁)) ∈
(Base‘(ℤ/nℤ‘𝑁))) | 
| 120 | 102 | fveq2d 6909 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 →
(Base‘(ℤ/nℤ‘𝑁)) =
(Base‘(Scalar‘(Poly1‘(ℤ/nℤ‘𝑁))))) | 
| 121 | 119, 120 | eleqtrd 2842 | . . . . . . . . . . . . . . 15
⊢ (𝜑 →
(1r‘(ℤ/nℤ‘𝑁)) ∈
(Base‘(Scalar‘(Poly1‘(ℤ/nℤ‘𝑁))))) | 
| 122 |  | eqid 2736 | . . . . . . . . . . . . . . . 16
⊢
(Base‘(Scalar‘(Poly1‘(ℤ/nℤ‘𝑁)))) =
(Base‘(Scalar‘(Poly1‘(ℤ/nℤ‘𝑁)))) | 
| 123 |  | eqid 2736 | . . . . . . . . . . . . . . . 16
⊢ (
·𝑠
‘(Poly1‘(ℤ/nℤ‘𝑁))) = ( ·𝑠
‘(Poly1‘(ℤ/nℤ‘𝑁))) | 
| 124 | 105, 106,
122, 38, 97, 123 | asclmul1 21907 | . . . . . . . . . . . . . . 15
⊢
(((Poly1‘(ℤ/nℤ‘𝑁)) ∈ AssAlg ∧
(1r‘(ℤ/nℤ‘𝑁)) ∈
(Base‘(Scalar‘(Poly1‘(ℤ/nℤ‘𝑁)))) ∧ (𝑅(.g‘(mulGrp‘(Poly1‘(ℤ/nℤ‘𝑁))))(var1‘(ℤ/nℤ‘𝑁))) ∈ (Base‘(Poly1‘(ℤ/nℤ‘𝑁)))) → (((algSc‘(Poly1‘(ℤ/nℤ‘𝑁)))‘(1r‘(ℤ/nℤ‘𝑁)))(.r‘(Poly1‘(ℤ/nℤ‘𝑁)))(𝑅(.g‘(mulGrp‘(Poly1‘(ℤ/nℤ‘𝑁))))(var1‘(ℤ/nℤ‘𝑁)))) = ((1r‘(ℤ/nℤ‘𝑁))( ·𝑠
‘(Poly1‘(ℤ/nℤ‘𝑁)))(𝑅(.g‘(mulGrp‘(Poly1‘(ℤ/nℤ‘𝑁))))(var1‘(ℤ/nℤ‘𝑁))))) | 
| 125 | 115, 121,
48, 124 | syl3anc 1372 | . . . . . . . . . . . . . 14
⊢ (𝜑 →
(((algSc‘(Poly1‘(ℤ/nℤ‘𝑁)))‘(1r‘(ℤ/nℤ‘𝑁)))(.r‘(Poly1‘(ℤ/nℤ‘𝑁)))(𝑅(.g‘(mulGrp‘(Poly1‘(ℤ/nℤ‘𝑁))))(var1‘(ℤ/nℤ‘𝑁)))) = ((1r‘(ℤ/nℤ‘𝑁))( ·𝑠
‘(Poly1‘(ℤ/nℤ‘𝑁)))(𝑅(.g‘(mulGrp‘(Poly1‘(ℤ/nℤ‘𝑁))))(var1‘(ℤ/nℤ‘𝑁))))) | 
| 126 | 113, 125 | eqtrd 2776 | . . . . . . . . . . . . 13
⊢ (𝜑 → (𝑅(.g‘(mulGrp‘(Poly1‘(ℤ/nℤ‘𝑁))))(var1‘(ℤ/nℤ‘𝑁))) = ((1r‘(ℤ/nℤ‘𝑁))( ·𝑠
‘(Poly1‘(ℤ/nℤ‘𝑁)))(𝑅(.g‘(mulGrp‘(Poly1‘(ℤ/nℤ‘𝑁))))(var1‘(ℤ/nℤ‘𝑁))))) | 
| 127 | 126 | fveq2d 6909 | . . . . . . . . . . . 12
⊢ (𝜑 → (𝐹‘(𝑅(.g‘(mulGrp‘(Poly1‘(ℤ/nℤ‘𝑁))))(var1‘(ℤ/nℤ‘𝑁)))) = (𝐹‘((1r‘(ℤ/nℤ‘𝑁))( ·𝑠
‘(Poly1‘(ℤ/nℤ‘𝑁)))(𝑅(.g‘(mulGrp‘(Poly1‘(ℤ/nℤ‘𝑁))))(var1‘(ℤ/nℤ‘𝑁)))))) | 
| 128 |  | eqid 2736 | . . . . . . . . . . . . 13
⊢
(var1‘𝐾) = (var1‘𝐾) | 
| 129 |  | eqid 2736 | . . . . . . . . . . . . 13
⊢ (
·𝑠 ‘(Poly1‘𝐾)) = (
·𝑠 ‘(Poly1‘𝐾)) | 
| 130 |  | eqid 2736 | . . . . . . . . . . . . 13
⊢
(mulGrp‘(Poly1‘𝐾)) =
(mulGrp‘(Poly1‘𝐾)) | 
| 131 |  | eqid 2736 | . . . . . . . . . . . . 13
⊢
(.g‘(mulGrp‘(Poly1‘𝐾))) =
(.g‘(mulGrp‘(Poly1‘𝐾))) | 
| 132 | 32, 68, 38, 116, 5, 45, 128, 123, 129, 37, 130, 40, 131, 77, 119, 14 | rhmply1mon 22394 | . . . . . . . . . . . 12
⊢ (𝜑 → (𝐹‘((1r‘(ℤ/nℤ‘𝑁))( ·𝑠
‘(Poly1‘(ℤ/nℤ‘𝑁)))(𝑅(.g‘(mulGrp‘(Poly1‘(ℤ/nℤ‘𝑁))))(var1‘(ℤ/nℤ‘𝑁))))) = ((𝐺‘(1r‘(ℤ/nℤ‘𝑁)))( ·𝑠 ‘(Poly1‘𝐾))(𝑅(.g‘(mulGrp‘(Poly1‘𝐾)))(var1‘𝐾)))) | 
| 133 | 127, 132 | eqtrd 2776 | . . . . . . . . . . 11
⊢ (𝜑 → (𝐹‘(𝑅(.g‘(mulGrp‘(Poly1‘(ℤ/nℤ‘𝑁))))(var1‘(ℤ/nℤ‘𝑁)))) = ((𝐺‘(1r‘(ℤ/nℤ‘𝑁)))( ·𝑠 ‘(Poly1‘𝐾))(𝑅(.g‘(mulGrp‘(Poly1‘𝐾)))(var1‘𝐾)))) | 
| 134 | 133 | fveq2d 6909 | . . . . . . . . . 10
⊢ (𝜑 → (𝐻‘(𝐹‘(𝑅(.g‘(mulGrp‘(Poly1‘(ℤ/nℤ‘𝑁))))(var1‘(ℤ/nℤ‘𝑁))))) = (𝐻‘((𝐺‘(1r‘(ℤ/nℤ‘𝑁)))( ·𝑠 ‘(Poly1‘𝐾))(𝑅(.g‘(mulGrp‘(Poly1‘𝐾)))(var1‘𝐾))))) | 
| 135 |  | eqid 2736 | . . . . . . . . . . . . . . 15
⊢
(1r‘𝐾) = (1r‘𝐾) | 
| 136 | 117, 135 | rhm1 20490 | . . . . . . . . . . . . . 14
⊢ (𝐺 ∈
((ℤ/nℤ‘𝑁) RingHom 𝐾) → (𝐺‘(1r‘(ℤ/nℤ‘𝑁))) = (1r‘𝐾)) | 
| 137 | 77, 136 | syl 17 | . . . . . . . . . . . . 13
⊢ (𝜑 → (𝐺‘(1r‘(ℤ/nℤ‘𝑁))) = (1r‘𝐾)) | 
| 138 | 137 | oveq1d 7447 | . . . . . . . . . . . 12
⊢ (𝜑 → ((𝐺‘(1r‘(ℤ/nℤ‘𝑁)))( ·𝑠
‘(Poly1‘𝐾))(𝑅(.g‘(mulGrp‘(Poly1‘𝐾)))(var1‘𝐾))) = ((1r‘𝐾)( ·𝑠
‘(Poly1‘𝐾))(𝑅(.g‘(mulGrp‘(Poly1‘𝐾)))(var1‘𝐾)))) | 
| 139 | 138 | fveq2d 6909 | . . . . . . . . . . 11
⊢ (𝜑 → (𝐻‘((𝐺‘(1r‘(ℤ/nℤ‘𝑁)))( ·𝑠
‘(Poly1‘𝐾))(𝑅(.g‘(mulGrp‘(Poly1‘𝐾)))(var1‘𝐾)))) = (𝐻‘((1r‘𝐾)( ·𝑠
‘(Poly1‘𝐾))(𝑅(.g‘(mulGrp‘(Poly1‘𝐾)))(var1‘𝐾))))) | 
| 140 | 68 | ply1assa 22202 | . . . . . . . . . . . . . . . 16
⊢ (𝐾 ∈ CRing →
(Poly1‘𝐾)
∈ AssAlg) | 
| 141 | 9, 140 | syl 17 | . . . . . . . . . . . . . . 15
⊢ (𝜑 →
(Poly1‘𝐾)
∈ AssAlg) | 
| 142 | 19, 135 | ringidcl 20263 | . . . . . . . . . . . . . . . . 17
⊢ (𝐾 ∈ Ring →
(1r‘𝐾)
∈ (Base‘𝐾)) | 
| 143 | 69, 142 | syl 17 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → (1r‘𝐾) ∈ (Base‘𝐾)) | 
| 144 | 68 | ply1sca 22255 | . . . . . . . . . . . . . . . . . 18
⊢ (𝐾 ∈ Field → 𝐾 =
(Scalar‘(Poly1‘𝐾))) | 
| 145 | 2, 144 | syl 17 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐾 =
(Scalar‘(Poly1‘𝐾))) | 
| 146 | 145 | fveq2d 6909 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → (Base‘𝐾) =
(Base‘(Scalar‘(Poly1‘𝐾)))) | 
| 147 | 143, 146 | eleqtrd 2842 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → (1r‘𝐾) ∈
(Base‘(Scalar‘(Poly1‘𝐾)))) | 
| 148 | 130, 86 | mgpbas 20143 | . . . . . . . . . . . . . . . 16
⊢
(Base‘(Poly1‘𝐾)) =
(Base‘(mulGrp‘(Poly1‘𝐾))) | 
| 149 | 68 | ply1crng 22201 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝐾 ∈ CRing →
(Poly1‘𝐾)
∈ CRing) | 
| 150 | 9, 149 | syl 17 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 →
(Poly1‘𝐾)
∈ CRing) | 
| 151 |  | crngring 20243 | . . . . . . . . . . . . . . . . . 18
⊢
((Poly1‘𝐾) ∈ CRing →
(Poly1‘𝐾)
∈ Ring) | 
| 152 | 150, 151 | syl 17 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 →
(Poly1‘𝐾)
∈ Ring) | 
| 153 | 130 | ringmgp 20237 | . . . . . . . . . . . . . . . . 17
⊢
((Poly1‘𝐾) ∈ Ring →
(mulGrp‘(Poly1‘𝐾)) ∈ Mnd) | 
| 154 | 152, 153 | syl 17 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 →
(mulGrp‘(Poly1‘𝐾)) ∈ Mnd) | 
| 155 | 128, 68, 86 | vr1cl 22220 | . . . . . . . . . . . . . . . . 17
⊢ (𝐾 ∈ Ring →
(var1‘𝐾)
∈ (Base‘(Poly1‘𝐾))) | 
| 156 | 69, 155 | syl 17 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 →
(var1‘𝐾)
∈ (Base‘(Poly1‘𝐾))) | 
| 157 | 148, 131,
154, 14, 156 | mulgnn0cld 19114 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑅(.g‘(mulGrp‘(Poly1‘𝐾)))(var1‘𝐾)) ∈ (Base‘(Poly1‘𝐾))) | 
| 158 |  | eqid 2736 | . . . . . . . . . . . . . . . 16
⊢
(algSc‘(Poly1‘𝐾)) =
(algSc‘(Poly1‘𝐾)) | 
| 159 |  | eqid 2736 | . . . . . . . . . . . . . . . 16
⊢
(Scalar‘(Poly1‘𝐾)) =
(Scalar‘(Poly1‘𝐾)) | 
| 160 |  | eqid 2736 | . . . . . . . . . . . . . . . 16
⊢
(Base‘(Scalar‘(Poly1‘𝐾))) =
(Base‘(Scalar‘(Poly1‘𝐾))) | 
| 161 |  | eqid 2736 | . . . . . . . . . . . . . . . 16
⊢
(.r‘(Poly1‘𝐾)) =
(.r‘(Poly1‘𝐾)) | 
| 162 | 158, 159,
160, 86, 161, 129 | asclmul1 21907 | . . . . . . . . . . . . . . 15
⊢
(((Poly1‘𝐾) ∈ AssAlg ∧
(1r‘𝐾)
∈ (Base‘(Scalar‘(Poly1‘𝐾))) ∧ (𝑅(.g‘(mulGrp‘(Poly1‘𝐾)))(var1‘𝐾)) ∈ (Base‘(Poly1‘𝐾))) → (((algSc‘(Poly1‘𝐾))‘(1r‘𝐾))(.r‘(Poly1‘𝐾))(𝑅(.g‘(mulGrp‘(Poly1‘𝐾)))(var1‘𝐾))) = ((1r‘𝐾)( ·𝑠
‘(Poly1‘𝐾))(𝑅(.g‘(mulGrp‘(Poly1‘𝐾)))(var1‘𝐾)))) | 
| 163 | 141, 147,
157, 162 | syl3anc 1372 | . . . . . . . . . . . . . 14
⊢ (𝜑 →
(((algSc‘(Poly1‘𝐾))‘(1r‘𝐾))(.r‘(Poly1‘𝐾))(𝑅(.g‘(mulGrp‘(Poly1‘𝐾)))(var1‘𝐾))) = ((1r‘𝐾)( ·𝑠
‘(Poly1‘𝐾))(𝑅(.g‘(mulGrp‘(Poly1‘𝐾)))(var1‘𝐾)))) | 
| 164 | 163 | eqcomd 2742 | . . . . . . . . . . . . 13
⊢ (𝜑 →
((1r‘𝐾)(
·𝑠 ‘(Poly1‘𝐾))(𝑅(.g‘(mulGrp‘(Poly1‘𝐾)))(var1‘𝐾))) = (((algSc‘(Poly1‘𝐾))‘(1r‘𝐾))(.r‘(Poly1‘𝐾))(𝑅(.g‘(mulGrp‘(Poly1‘𝐾)))(var1‘𝐾)))) | 
| 165 | 164 | fveq2d 6909 | . . . . . . . . . . . 12
⊢ (𝜑 → (𝐻‘((1r‘𝐾)(
·𝑠 ‘(Poly1‘𝐾))(𝑅(.g‘(mulGrp‘(Poly1‘𝐾)))(var1‘𝐾)))) = (𝐻‘(((algSc‘(Poly1‘𝐾))‘(1r‘𝐾))(.r‘(Poly1‘𝐾))(𝑅(.g‘(mulGrp‘(Poly1‘𝐾)))(var1‘𝐾))))) | 
| 166 |  | eqid 2736 | . . . . . . . . . . . . . . . 16
⊢
(1r‘(Poly1‘𝐾)) =
(1r‘(Poly1‘𝐾)) | 
| 167 | 68, 158, 135, 166, 69 | ply1ascl1 22258 | . . . . . . . . . . . . . . 15
⊢ (𝜑 →
((algSc‘(Poly1‘𝐾))‘(1r‘𝐾)) =
(1r‘(Poly1‘𝐾))) | 
| 168 | 167 | oveq1d 7447 | . . . . . . . . . . . . . 14
⊢ (𝜑 →
(((algSc‘(Poly1‘𝐾))‘(1r‘𝐾))(.r‘(Poly1‘𝐾))(𝑅(.g‘(mulGrp‘(Poly1‘𝐾)))(var1‘𝐾))) = ((1r‘(Poly1‘𝐾))(.r‘(Poly1‘𝐾))(𝑅(.g‘(mulGrp‘(Poly1‘𝐾)))(var1‘𝐾)))) | 
| 169 | 168 | fveq2d 6909 | . . . . . . . . . . . . 13
⊢ (𝜑 → (𝐻‘(((algSc‘(Poly1‘𝐾))‘(1r‘𝐾))(.r‘(Poly1‘𝐾))(𝑅(.g‘(mulGrp‘(Poly1‘𝐾)))(var1‘𝐾)))) = (𝐻‘((1r‘(Poly1‘𝐾))(.r‘(Poly1‘𝐾))(𝑅(.g‘(mulGrp‘(Poly1‘𝐾)))(var1‘𝐾))))) | 
| 170 | 86, 161, 166, 152, 157 | ringlidmd 20270 | . . . . . . . . . . . . . . 15
⊢ (𝜑 →
((1r‘(Poly1‘𝐾))(.r‘(Poly1‘𝐾))(𝑅(.g‘(mulGrp‘(Poly1‘𝐾)))(var1‘𝐾))) = (𝑅(.g‘(mulGrp‘(Poly1‘𝐾)))(var1‘𝐾))) | 
| 171 | 170 | fveq2d 6909 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐻‘((1r‘(Poly1‘𝐾))(.r‘(Poly1‘𝐾))(𝑅(.g‘(mulGrp‘(Poly1‘𝐾)))(var1‘𝐾)))) = (𝐻‘(𝑅(.g‘(mulGrp‘(Poly1‘𝐾)))(var1‘𝐾)))) | 
| 172 | 7 | a1i 11 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐻 = (𝑟 ∈
(Base‘(Poly1‘𝐾)) ↦ (((eval1‘𝐾)‘𝑟)‘𝑀))) | 
| 173 |  | simpr 484 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑟 = (𝑅(.g‘(mulGrp‘(Poly1‘𝐾)))(var1‘𝐾))) → 𝑟
= (𝑅(.g‘(mulGrp‘(Poly1‘𝐾)))(var1‘𝐾))) | 
| 174 | 173 | fveq2d 6909 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑟 = (𝑅(.g‘(mulGrp‘(Poly1‘𝐾)))(var1‘𝐾))) → ((eval1‘𝐾)‘𝑟) =
((eval1‘𝐾)‘(𝑅(.g‘(mulGrp‘(Poly1‘𝐾)))(var1‘𝐾)))) | 
| 175 | 174 | fveq1d 6907 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑟 = (𝑅(.g‘(mulGrp‘(Poly1‘𝐾)))(var1‘𝐾))) → (((eval1‘𝐾)‘𝑟)‘𝑀) =
(((eval1‘𝐾)‘(𝑅(.g‘(mulGrp‘(Poly1‘𝐾)))(var1‘𝐾)))‘𝑀)) | 
| 176 |  | fvexd 6920 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 →
(((eval1‘𝐾)‘(𝑅(.g‘(mulGrp‘(Poly1‘𝐾)))(var1‘𝐾)))‘𝑀)
∈ V) | 
| 177 | 172, 175,
157, 176 | fvmptd 7022 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐻‘(𝑅(.g‘(mulGrp‘(Poly1‘𝐾)))(var1‘𝐾))) = (((eval1‘𝐾)‘(𝑅(.g‘(mulGrp‘(Poly1‘𝐾)))(var1‘𝐾)))‘𝑀)) | 
| 178 | 85, 128, 19, 68, 86, 9, 22 | evl1vard 22342 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 →
((var1‘𝐾)
∈ (Base‘(Poly1‘𝐾)) ∧ (((eval1‘𝐾)‘(var1‘𝐾))‘𝑀) = 𝑀)) | 
| 179 | 85, 68, 19, 86, 9, 22, 178, 131, 15, 14 | evl1expd 22350 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((𝑅(.g‘(mulGrp‘(Poly1‘𝐾)))(var1‘𝐾)) ∈ (Base‘(Poly1‘𝐾)) ∧ (((eval1‘𝐾)‘(𝑅(.g‘(mulGrp‘(Poly1‘𝐾)))(var1‘𝐾)))‘𝑀)
= (𝑅(.g‘(mulGrp‘𝐾))𝑀))) | 
| 180 | 179 | simprd 495 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 →
(((eval1‘𝐾)‘(𝑅(.g‘(mulGrp‘(Poly1‘𝐾)))(var1‘𝐾)))‘𝑀)
= (𝑅(.g‘(mulGrp‘𝐾))𝑀)) | 
| 181 | 17 | simp2d 1143 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝑅(.g‘(mulGrp‘𝐾))𝑀) = (0g‘(mulGrp‘𝐾))) | 
| 182 | 10, 135 | ringidval 20181 | . . . . . . . . . . . . . . . . . . 19
⊢
(1r‘𝐾) = (0g‘(mulGrp‘𝐾)) | 
| 183 | 182 | eqcomi 2745 | . . . . . . . . . . . . . . . . . 18
⊢
(0g‘(mulGrp‘𝐾)) = (1r‘𝐾) | 
| 184 | 183 | a1i 11 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 →
(0g‘(mulGrp‘𝐾)) = (1r‘𝐾)) | 
| 185 | 181, 184 | eqtrd 2776 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑅(.g‘(mulGrp‘𝐾))𝑀) = (1r‘𝐾)) | 
| 186 | 180, 185 | eqtrd 2776 | . . . . . . . . . . . . . . 15
⊢ (𝜑 →
(((eval1‘𝐾)‘(𝑅(.g‘(mulGrp‘(Poly1‘𝐾)))(var1‘𝐾)))‘𝑀)
= (1r‘𝐾)) | 
| 187 | 177, 186 | eqtrd 2776 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐻‘(𝑅(.g‘(mulGrp‘(Poly1‘𝐾)))(var1‘𝐾))) = (1r‘𝐾)) | 
| 188 | 171, 187 | eqtrd 2776 | . . . . . . . . . . . . 13
⊢ (𝜑 → (𝐻‘((1r‘(Poly1‘𝐾))(.r‘(Poly1‘𝐾))(𝑅(.g‘(mulGrp‘(Poly1‘𝐾)))(var1‘𝐾)))) = (1r‘𝐾)) | 
| 189 | 169, 188 | eqtrd 2776 | . . . . . . . . . . . 12
⊢ (𝜑 → (𝐻‘(((algSc‘(Poly1‘𝐾))‘(1r‘𝐾))(.r‘(Poly1‘𝐾))(𝑅(.g‘(mulGrp‘(Poly1‘𝐾)))(var1‘𝐾)))) = (1r‘𝐾)) | 
| 190 | 165, 189 | eqtrd 2776 | . . . . . . . . . . 11
⊢ (𝜑 → (𝐻‘((1r‘𝐾)(
·𝑠 ‘(Poly1‘𝐾))(𝑅(.g‘(mulGrp‘(Poly1‘𝐾)))(var1‘𝐾)))) = (1r‘𝐾)) | 
| 191 | 139, 190 | eqtrd 2776 | . . . . . . . . . 10
⊢ (𝜑 → (𝐻‘((𝐺‘(1r‘(ℤ/nℤ‘𝑁)))( ·𝑠
‘(Poly1‘𝐾))(𝑅(.g‘(mulGrp‘(Poly1‘𝐾)))(var1‘𝐾)))) = (1r‘𝐾)) | 
| 192 | 134, 191 | eqtrd 2776 | . . . . . . . . 9
⊢ (𝜑 → (𝐻‘(𝐹‘(𝑅(.g‘(mulGrp‘(Poly1‘(ℤ/nℤ‘𝑁))))(var1‘(ℤ/nℤ‘𝑁))))) = (1r‘𝐾)) | 
| 193 | 166, 135 | rhm1 20490 | . . . . . . . . . . 11
⊢ (𝐻 ∈
((Poly1‘𝐾)
RingHom 𝐾) → (𝐻‘(1r‘(Poly1‘𝐾))) = (1r‘𝐾)) | 
| 194 | 87, 193 | syl 17 | . . . . . . . . . 10
⊢ (𝜑 → (𝐻‘(1r‘(Poly1‘𝐾))) = (1r‘𝐾)) | 
| 195 | 194 | eqcomd 2742 | . . . . . . . . 9
⊢ (𝜑 → (1r‘𝐾) = (𝐻‘(1r‘(Poly1‘𝐾)))) | 
| 196 | 192, 195 | eqtrd 2776 | . . . . . . . 8
⊢ (𝜑 → (𝐻‘(𝐹‘(𝑅(.g‘(mulGrp‘(Poly1‘(ℤ/nℤ‘𝑁))))(var1‘(ℤ/nℤ‘𝑁))))) = (𝐻‘(1r‘(Poly1‘𝐾)))) | 
| 197 | 196, 194 | eqtrd 2776 | . . . . . . 7
⊢ (𝜑 → (𝐻‘(𝐹‘(𝑅(.g‘(mulGrp‘(Poly1‘(ℤ/nℤ‘𝑁))))(var1‘(ℤ/nℤ‘𝑁))))) = (1r‘𝐾)) | 
| 198 | 49, 166 | rhm1 20490 | . . . . . . . . . 10
⊢ (𝐹 ∈
((Poly1‘(ℤ/nℤ‘𝑁)) RingHom (Poly1‘𝐾)) → (𝐹‘(1r‘(Poly1‘(ℤ/nℤ‘𝑁)))) = (1r‘(Poly1‘𝐾))) | 
| 199 | 78, 198 | syl 17 | . . . . . . . . 9
⊢ (𝜑 → (𝐹‘(1r‘(Poly1‘(ℤ/nℤ‘𝑁)))) = (1r‘(Poly1‘𝐾))) | 
| 200 | 199 | fveq2d 6909 | . . . . . . . 8
⊢ (𝜑 → (𝐻‘(𝐹‘(1r‘(Poly1‘(ℤ/nℤ‘𝑁))))) = (𝐻‘(1r‘(Poly1‘𝐾)))) | 
| 201 | 200, 194 | eqtrd 2776 | . . . . . . 7
⊢ (𝜑 → (𝐻‘(𝐹‘(1r‘(Poly1‘(ℤ/nℤ‘𝑁))))) = (1r‘𝐾)) | 
| 202 | 197, 201 | oveq12d 7450 | . . . . . 6
⊢ (𝜑 → ((𝐻‘(𝐹‘(𝑅(.g‘(mulGrp‘(Poly1‘(ℤ/nℤ‘𝑁))))(var1‘(ℤ/nℤ‘𝑁)))))(-g‘𝐾)(𝐻‘(𝐹‘(1r‘(Poly1‘(ℤ/nℤ‘𝑁)))))) = ((1r‘𝐾)(-g‘𝐾)(1r‘𝐾))) | 
| 203 | 69 | ringgrpd 20240 | . . . . . . 7
⊢ (𝜑 → 𝐾 ∈ Grp) | 
| 204 | 19, 1, 94 | grpsubid 19043 | . . . . . . 7
⊢ ((𝐾 ∈ Grp ∧
(1r‘𝐾)
∈ (Base‘𝐾))
→ ((1r‘𝐾)(-g‘𝐾)(1r‘𝐾)) = (0g‘𝐾)) | 
| 205 | 203, 143,
204 | syl2anc 584 | . . . . . 6
⊢ (𝜑 →
((1r‘𝐾)(-g‘𝐾)(1r‘𝐾)) = (0g‘𝐾)) | 
| 206 | 202, 205 | eqtrd 2776 | . . . . 5
⊢ (𝜑 → ((𝐻‘(𝐹‘(𝑅(.g‘(mulGrp‘(Poly1‘(ℤ/nℤ‘𝑁))))(var1‘(ℤ/nℤ‘𝑁)))))(-g‘𝐾)(𝐻‘(𝐹‘(1r‘(Poly1‘(ℤ/nℤ‘𝑁)))))) = (0g‘𝐾)) | 
| 207 | 96, 206 | eqtrd 2776 | . . . 4
⊢ (𝜑 → (𝐻‘((𝐹‘(𝑅(.g‘(mulGrp‘(Poly1‘(ℤ/nℤ‘𝑁))))(var1‘(ℤ/nℤ‘𝑁))))(-g‘(Poly1‘𝐾))(𝐹‘(1r‘(Poly1‘(ℤ/nℤ‘𝑁)))))) = (0g‘𝐾)) | 
| 208 | 84, 207 | eqtrd 2776 | . . 3
⊢ (𝜑 → (𝐻‘(𝐹‘((𝑅(.g‘(mulGrp‘(Poly1‘(ℤ/nℤ‘𝑁))))(var1‘(ℤ/nℤ‘𝑁)))(-g‘(Poly1‘(ℤ/nℤ‘𝑁)))(1r‘(Poly1‘(ℤ/nℤ‘𝑁)))))) = (0g‘𝐾)) | 
| 209 | 67, 208 | eqtrd 2776 | . 2
⊢ (𝜑 → ((𝐻 ∘ 𝐹)‘((𝑅(.g‘(mulGrp‘(Poly1‘(ℤ/nℤ‘𝑁))))(var1‘(ℤ/nℤ‘𝑁)))(-g‘(Poly1‘(ℤ/nℤ‘𝑁)))(1r‘(Poly1‘(ℤ/nℤ‘𝑁))))) = (0g‘𝐾)) | 
| 210 | 1, 23, 24, 25, 26, 34, 35, 54, 209 | rhmqusspan 42187 | 1
⊢ (𝜑 → (𝐼 ∈ (𝐴 RingHom 𝐾) ∧ ∀𝑔 ∈
(Base‘(Poly1‘(ℤ/nℤ‘𝑁)))(𝐼‘[𝑔]((Poly1‘(ℤ/nℤ‘𝑁)) ~QG 𝐿)) = ((𝐻
∘ 𝐹)‘𝑔))) |