Metamath Proof Explorer

Theorem aks5lem3a

Description: Lemma for AKS section 5. (Contributed by metakunt, 17-Jun-2025)

Ref Expression
Hypotheses aks5lema.1 ⊢ ( 𝜑 → 𝐾 ∈ Field )
aks5lema.2 ⊢ 𝑃 = ( chr ‘ 𝐾 )
aks5lema.3 ⊢ ( 𝜑 → ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ ∧ 𝑃 ∥ 𝑁 ) )
aks5lema.9 ⊢ 𝐵 = ( 𝑆 /s ( 𝑆 ~QG 𝐿 ) )
aks5lema.10 ⊢ 𝐿 = ( ( RSpan ‘ 𝑆 ) ‘ { ( ( 𝑅 ( .g ‘ ( mulGrp ‘ 𝑆 ) ) ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( -g ‘ 𝑆 ) ( 1r ‘ 𝑆 ) ) } )
aks5lema.11 ⊢ ( 𝜑 → 𝑅 ∈ ℕ )
aks5lema.14 ⊢ ∼ = { ⟨ 𝑒 , 𝑓 ⟩ ∣ ( 𝑒 ∈ ℕ ∧ 𝑓 ∈ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) ∧ ∀ 𝑦 ∈ ( ( mulGrp ‘ 𝐾 ) PrimRoots 𝑅 ) ( 𝑒 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) ( ( ( eval1 ‘ 𝐾 ) ‘ 𝑓 ) ‘ 𝑦 ) ) = ( ( ( eval1 ‘ 𝐾 ) ‘ 𝑓 ) ‘ ( 𝑒 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑦 ) ) ) }
aks5lema.15 ⊢ 𝑆 = ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) )
aks5lem3a.4 ⊢ 𝐹 = ( 𝑝 ∈ ( Base ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ↦ ( 𝐺 ∘ 𝑝 ) )
aks5lem3a.5 ⊢ 𝐺 = ( 𝑞 ∈ ( Base ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ↦ ∪ ( ( ℤRHom ‘ 𝐾 ) “ 𝑞 ) )
aks5lem3a.6 ⊢ 𝐻 = ( 𝑟 ∈ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) ↦ ( ( ( eval1 ‘ 𝐾 ) ‘ 𝑟 ) ‘ 𝑀 ) )
aks5lem3a.7 ⊢ ( 𝜑 → 𝑀 ∈ ( ( mulGrp ‘ 𝐾 ) PrimRoots 𝑅 ) )
aks5lem3a.8 ⊢ 𝐼 = ( 𝑠 ∈ ( Base ‘ 𝐵 ) ↦ ∪ ( ( 𝐻 ∘ 𝐹 ) “ 𝑠 ) )
aks5lem3a.12 ⊢ ( 𝜑 → 𝐴 ∈ ℤ )
aks5lem3a.13 ⊢ ( 𝜑 → [ ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝑆 ) ) ( ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ( +g ‘ 𝑆 ) ( ( algSc ‘ 𝑆 ) ‘ ( ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ‘ 𝐴 ) ) ) ) ] ( 𝑆 ~QG 𝐿 ) = [ ( ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝑆 ) ) ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( +g ‘ 𝑆 ) ( ( algSc ‘ 𝑆 ) ‘ ( ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ‘ 𝐴 ) ) ) ] ( 𝑆 ~QG 𝐿 ) )
Assertion aks5lem3a ( 𝜑 → ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) ( ( ( eval1 ‘ 𝐾 ) ‘ ( ( var1 ‘ 𝐾 ) ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ) ) ‘ 𝑀 ) ) = ( ( ( eval1 ‘ 𝐾 ) ‘ ( ( var1 ‘ 𝐾 ) ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ) ) ‘ ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑀 ) ) )

Proof

Step Hyp Ref Expression
1 aks5lema.1 ⊢ ( 𝜑 → 𝐾 ∈ Field )
2 aks5lema.2 ⊢ 𝑃 = ( chr ‘ 𝐾 )
3 aks5lema.3 ⊢ ( 𝜑 → ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ ∧ 𝑃 ∥ 𝑁 ) )
4 aks5lema.9 ⊢ 𝐵 = ( 𝑆 /s ( 𝑆 ~QG 𝐿 ) )
5 aks5lema.10 ⊢ 𝐿 = ( ( RSpan ‘ 𝑆 ) ‘ { ( ( 𝑅 ( .g ‘ ( mulGrp ‘ 𝑆 ) ) ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( -g ‘ 𝑆 ) ( 1r ‘ 𝑆 ) ) } )
6 aks5lema.11 ⊢ ( 𝜑 → 𝑅 ∈ ℕ )
7 aks5lema.14 ⊢ ∼ = { ⟨ 𝑒 , 𝑓 ⟩ ∣ ( 𝑒 ∈ ℕ ∧ 𝑓 ∈ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) ∧ ∀ 𝑦 ∈ ( ( mulGrp ‘ 𝐾 ) PrimRoots 𝑅 ) ( 𝑒 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) ( ( ( eval1 ‘ 𝐾 ) ‘ 𝑓 ) ‘ 𝑦 ) ) = ( ( ( eval1 ‘ 𝐾 ) ‘ 𝑓 ) ‘ ( 𝑒 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑦 ) ) ) }
8 aks5lema.15 ⊢ 𝑆 = ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) )
9 aks5lem3a.4 ⊢ 𝐹 = ( 𝑝 ∈ ( Base ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ↦ ( 𝐺 ∘ 𝑝 ) )
10 aks5lem3a.5 ⊢ 𝐺 = ( 𝑞 ∈ ( Base ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ↦ ∪ ( ( ℤRHom ‘ 𝐾 ) “ 𝑞 ) )
11 aks5lem3a.6 ⊢ 𝐻 = ( 𝑟 ∈ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) ↦ ( ( ( eval1 ‘ 𝐾 ) ‘ 𝑟 ) ‘ 𝑀 ) )
12 aks5lem3a.7 ⊢ ( 𝜑 → 𝑀 ∈ ( ( mulGrp ‘ 𝐾 ) PrimRoots 𝑅 ) )
13 aks5lem3a.8 ⊢ 𝐼 = ( 𝑠 ∈ ( Base ‘ 𝐵 ) ↦ ∪ ( ( 𝐻 ∘ 𝐹 ) “ 𝑠 ) )
14 aks5lem3a.12 ⊢ ( 𝜑 → 𝐴 ∈ ℤ )
15 aks5lem3a.13 ⊢ ( 𝜑 → [ ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝑆 ) ) ( ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ( +g ‘ 𝑆 ) ( ( algSc ‘ 𝑆 ) ‘ ( ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ‘ 𝐴 ) ) ) ) ] ( 𝑆 ~QG 𝐿 ) = [ ( ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝑆 ) ) ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( +g ‘ 𝑆 ) ( ( algSc ‘ 𝑆 ) ‘ ( ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ‘ 𝐴 ) ) ) ] ( 𝑆 ~QG 𝐿 ) )
16 1 fldcrngd ⊢ ( 𝜑 → 𝐾 ∈ CRing )
17 eqid ⊢ ( mulGrp ‘ 𝐾 ) = ( mulGrp ‘ 𝐾 )
18 17 crngmgp ⊢ ( 𝐾 ∈ CRing → ( mulGrp ‘ 𝐾 ) ∈ CMnd )
19 16 18 syl ⊢ ( 𝜑 → ( mulGrp ‘ 𝐾 ) ∈ CMnd )
20 6 nnnn0d ⊢ ( 𝜑 → 𝑅 ∈ ℕ0 )
21 eqid ⊢ ( .g ‘ ( mulGrp ‘ 𝐾 ) ) = ( .g ‘ ( mulGrp ‘ 𝐾 ) )
22 19 20 21 isprimroot ⊢ ( 𝜑 → ( 𝑀 ∈ ( ( mulGrp ‘ 𝐾 ) PrimRoots 𝑅 ) ↔ ( 𝑀 ∈ ( Base ‘ ( mulGrp ‘ 𝐾 ) ) ∧ ( 𝑅 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑀 ) = ( 0g ‘ ( mulGrp ‘ 𝐾 ) ) ∧ ∀ 𝑑 ∈ ℕ0 ( ( 𝑑 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑀 ) = ( 0g ‘ ( mulGrp ‘ 𝐾 ) ) → 𝑅 ∥ 𝑑 ) ) ) )
23 12 22 mpbid ⊢ ( 𝜑 → ( 𝑀 ∈ ( Base ‘ ( mulGrp ‘ 𝐾 ) ) ∧ ( 𝑅 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑀 ) = ( 0g ‘ ( mulGrp ‘ 𝐾 ) ) ∧ ∀ 𝑑 ∈ ℕ0 ( ( 𝑑 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑀 ) = ( 0g ‘ ( mulGrp ‘ 𝐾 ) ) → 𝑅 ∥ 𝑑 ) ) )
24 23 simp1d ⊢ ( 𝜑 → 𝑀 ∈ ( Base ‘ ( mulGrp ‘ 𝐾 ) ) )
25 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
26 17 25 mgpbas ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ ( mulGrp ‘ 𝐾 ) )
27 26 eqcomi ⊢ ( Base ‘ ( mulGrp ‘ 𝐾 ) ) = ( Base ‘ 𝐾 )
28 24 27 eleqtrdi ⊢ ( 𝜑 → 𝑀 ∈ ( Base ‘ 𝐾 ) )
29 1 2 3 9 10 11 28 aks5lem1 ⊢ ( 𝜑 → ( 𝐻 ∘ 𝐹 ) ∈ ( ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) RingHom 𝐾 ) )
30 eqid ⊢ ( mulGrp ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) = ( mulGrp ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) )
31 30 17 rhmmhm ⊢ ( ( 𝐻 ∘ 𝐹 ) ∈ ( ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) RingHom 𝐾 ) → ( 𝐻 ∘ 𝐹 ) ∈ ( ( mulGrp ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) MndHom ( mulGrp ‘ 𝐾 ) ) )
32 29 31 syl ⊢ ( 𝜑 → ( 𝐻 ∘ 𝐹 ) ∈ ( ( mulGrp ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) MndHom ( mulGrp ‘ 𝐾 ) ) )
33 3 simp2d ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
34 33 nnnn0d ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
35 eqid ⊢ ( Base ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) = ( Base ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) )
36 eqid ⊢ ( +g ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) = ( +g ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) )
37 eqid ⊢ ( ℤ/nℤ ‘ 𝑁 ) = ( ℤ/nℤ ‘ 𝑁 )
38 37 zncrng ⊢ ( 𝑁 ∈ ℕ0 → ( ℤ/nℤ ‘ 𝑁 ) ∈ CRing )
39 34 38 syl ⊢ ( 𝜑 → ( ℤ/nℤ ‘ 𝑁 ) ∈ CRing )
40 eqid ⊢ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) = ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) )
41 40 ply1crng ⊢ ( ( ℤ/nℤ ‘ 𝑁 ) ∈ CRing → ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ∈ CRing )
42 39 41 syl ⊢ ( 𝜑 → ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ∈ CRing )
43 42 crngringd ⊢ ( 𝜑 → ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ∈ Ring )
44 ringgrp ⊢ ( ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ∈ Ring → ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ∈ Grp )
45 43 44 syl ⊢ ( 𝜑 → ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ∈ Grp )
46 39 crngringd ⊢ ( 𝜑 → ( ℤ/nℤ ‘ 𝑁 ) ∈ Ring )
47 eqid ⊢ ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) = ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) )
48 47 40 35 vr1cl ⊢ ( ( ℤ/nℤ ‘ 𝑁 ) ∈ Ring → ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ∈ ( Base ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) )
49 46 48 syl ⊢ ( 𝜑 → ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ∈ ( Base ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) )
50 eqid ⊢ ( algSc ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) = ( algSc ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) )
51 eqid ⊢ ( ℤRHom ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) = ( ℤRHom ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) )
52 eqid ⊢ ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑁 ) ) = ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑁 ) )
53 40 50 51 52 39 14 ply1asclzrhval ⊢ ( 𝜑 → ( ( algSc ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ‘ ( ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ‘ 𝐴 ) ) = ( ( ℤRHom ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ‘ 𝐴 ) )
54 51 zrhrhm ⊢ ( ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ∈ Ring → ( ℤRHom ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ∈ ( ℤring RingHom ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) )
55 zringbas ⊢ ℤ = ( Base ‘ ℤring )
56 55 35 rhmf ⊢ ( ( ℤRHom ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ∈ ( ℤring RingHom ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) → ( ℤRHom ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) : ℤ ⟶ ( Base ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) )
57 54 56 syl ⊢ ( ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ∈ Ring → ( ℤRHom ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) : ℤ ⟶ ( Base ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) )
58 43 57 syl ⊢ ( 𝜑 → ( ℤRHom ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) : ℤ ⟶ ( Base ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) )
59 58 14 ffvelcdmd ⊢ ( 𝜑 → ( ( ℤRHom ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ‘ 𝐴 ) ∈ ( Base ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) )
60 53 59 eqeltrd ⊢ ( 𝜑 → ( ( algSc ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ‘ ( ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ‘ 𝐴 ) ) ∈ ( Base ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) )
61 35 36 45 49 60 grpcld ⊢ ( 𝜑 → ( ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ( +g ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( ( algSc ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ‘ ( ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ‘ 𝐴 ) ) ) ∈ ( Base ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) )
62 30 35 mgpbas ⊢ ( Base ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) = ( Base ‘ ( mulGrp ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) )
63 eqid ⊢ ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ) = ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) )
64 62 63 21 mhmmulg ⊢ ( ( ( 𝐻 ∘ 𝐹 ) ∈ ( ( mulGrp ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) MndHom ( mulGrp ‘ 𝐾 ) ) ∧ 𝑁 ∈ ℕ0 ∧ ( ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ( +g ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( ( algSc ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ‘ ( ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ‘ 𝐴 ) ) ) ∈ ( Base ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ) → ( ( 𝐻 ∘ 𝐹 ) ‘ ( 𝑁 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ) ( ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ( +g ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( ( algSc ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ‘ ( ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ‘ 𝐴 ) ) ) ) ) = ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) ( ( 𝐻 ∘ 𝐹 ) ‘ ( ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ( +g ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( ( algSc ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ‘ ( ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ‘ 𝐴 ) ) ) ) ) )
65 32 34 61 64 syl3anc ⊢ ( 𝜑 → ( ( 𝐻 ∘ 𝐹 ) ‘ ( 𝑁 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ) ( ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ( +g ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( ( algSc ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ‘ ( ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ‘ 𝐴 ) ) ) ) ) = ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) ( ( 𝐻 ∘ 𝐹 ) ‘ ( ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ( +g ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( ( algSc ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ‘ ( ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ‘ 𝐴 ) ) ) ) ) )
66 eqid ⊢ ( Poly1 ‘ 𝐾 ) = ( Poly1 ‘ 𝐾 )
67 16 crngringd ⊢ ( 𝜑 → 𝐾 ∈ Ring )
68 2 eqcomi ⊢ ( chr ‘ 𝐾 ) = 𝑃
69 3 simp1d ⊢ ( 𝜑 → 𝑃 ∈ ℙ )
70 prmnn ⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℕ )
71 69 70 syl ⊢ ( 𝜑 → 𝑃 ∈ ℕ )
72 71 nnzd ⊢ ( 𝜑 → 𝑃 ∈ ℤ )
73 68 72 eqeltrid ⊢ ( 𝜑 → ( chr ‘ 𝐾 ) ∈ ℤ )
74 68 a1i ⊢ ( 𝜑 → ( chr ‘ 𝐾 ) = 𝑃 )
75 3 simp3d ⊢ ( 𝜑 → 𝑃 ∥ 𝑁 )
76 74 75 eqbrtrd ⊢ ( 𝜑 → ( chr ‘ 𝐾 ) ∥ 𝑁 )
77 67 33 73 76 37 10 zndvdchrrhm ⊢ ( 𝜑 → 𝐺 ∈ ( ( ℤ/nℤ ‘ 𝑁 ) RingHom 𝐾 ) )
78 40 66 35 9 77 rhmply1 ⊢ ( 𝜑 → 𝐹 ∈ ( ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) RingHom ( Poly1 ‘ 𝐾 ) ) )
79 eqid ⊢ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) = ( Base ‘ ( Poly1 ‘ 𝐾 ) )
80 35 79 rhmf ⊢ ( 𝐹 ∈ ( ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) RingHom ( Poly1 ‘ 𝐾 ) ) → 𝐹 : ( Base ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ⟶ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) )
81 78 80 syl ⊢ ( 𝜑 → 𝐹 : ( Base ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ⟶ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) )
82 81 61 fvco3d ⊢ ( 𝜑 → ( ( 𝐻 ∘ 𝐹 ) ‘ ( ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ( +g ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( ( algSc ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ‘ ( ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ‘ 𝐴 ) ) ) ) = ( 𝐻 ‘ ( 𝐹 ‘ ( ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ( +g ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( ( algSc ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ‘ ( ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ‘ 𝐴 ) ) ) ) ) )
83 11 a1i ⊢ ( 𝜑 → 𝐻 = ( 𝑟 ∈ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) ↦ ( ( ( eval1 ‘ 𝐾 ) ‘ 𝑟 ) ‘ 𝑀 ) ) )
84 simpr ⊢ ( ( 𝜑 ∧ 𝑟 = ( 𝐹 ‘ ( ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ( +g ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( ( algSc ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ‘ ( ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ‘ 𝐴 ) ) ) ) ) → 𝑟 = ( 𝐹 ‘ ( ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ( +g ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( ( algSc ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ‘ ( ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ‘ 𝐴 ) ) ) ) )
85 84 fveq2d ⊢ ( ( 𝜑 ∧ 𝑟 = ( 𝐹 ‘ ( ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ( +g ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( ( algSc ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ‘ ( ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ‘ 𝐴 ) ) ) ) ) → ( ( eval1 ‘ 𝐾 ) ‘ 𝑟 ) = ( ( eval1 ‘ 𝐾 ) ‘ ( 𝐹 ‘ ( ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ( +g ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( ( algSc ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ‘ ( ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ‘ 𝐴 ) ) ) ) ) )
86 85 fveq1d ⊢ ( ( 𝜑 ∧ 𝑟 = ( 𝐹 ‘ ( ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ( +g ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( ( algSc ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ‘ ( ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ‘ 𝐴 ) ) ) ) ) → ( ( ( eval1 ‘ 𝐾 ) ‘ 𝑟 ) ‘ 𝑀 ) = ( ( ( eval1 ‘ 𝐾 ) ‘ ( 𝐹 ‘ ( ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ( +g ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( ( algSc ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ‘ ( ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ‘ 𝐴 ) ) ) ) ) ‘ 𝑀 ) )
87 81 61 ffvelcdmd ⊢ ( 𝜑 → ( 𝐹 ‘ ( ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ( +g ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( ( algSc ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ‘ ( ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ‘ 𝐴 ) ) ) ) ∈ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) )
88 fvexd ⊢ ( 𝜑 → ( ( ( eval1 ‘ 𝐾 ) ‘ ( 𝐹 ‘ ( ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ( +g ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( ( algSc ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ‘ ( ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ‘ 𝐴 ) ) ) ) ) ‘ 𝑀 ) ∈ V )
89 83 86 87 88 fvmptd ⊢ ( 𝜑 → ( 𝐻 ‘ ( 𝐹 ‘ ( ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ( +g ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( ( algSc ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ‘ ( ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ‘ 𝐴 ) ) ) ) ) = ( ( ( eval1 ‘ 𝐾 ) ‘ ( 𝐹 ‘ ( ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ( +g ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( ( algSc ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ‘ ( ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ‘ 𝐴 ) ) ) ) ) ‘ 𝑀 ) )
90 rhmghm ⊢ ( 𝐹 ∈ ( ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) RingHom ( Poly1 ‘ 𝐾 ) ) → 𝐹 ∈ ( ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) GrpHom ( Poly1 ‘ 𝐾 ) ) )
91 78 90 syl ⊢ ( 𝜑 → 𝐹 ∈ ( ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) GrpHom ( Poly1 ‘ 𝐾 ) ) )
92 eqid ⊢ ( +g ‘ ( Poly1 ‘ 𝐾 ) ) = ( +g ‘ ( Poly1 ‘ 𝐾 ) )
93 35 36 92 ghmlin ⊢ ( ( 𝐹 ∈ ( ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) GrpHom ( Poly1 ‘ 𝐾 ) ) ∧ ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ∈ ( Base ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ∧ ( ( algSc ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ‘ ( ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ‘ 𝐴 ) ) ∈ ( Base ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ) → ( 𝐹 ‘ ( ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ( +g ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( ( algSc ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ‘ ( ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ‘ 𝐴 ) ) ) ) = ( ( 𝐹 ‘ ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝐹 ‘ ( ( algSc ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ‘ ( ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ‘ 𝐴 ) ) ) ) )
94 91 49 60 93 syl3anc ⊢ ( 𝜑 → ( 𝐹 ‘ ( ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ( +g ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( ( algSc ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ‘ ( ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ‘ 𝐴 ) ) ) ) = ( ( 𝐹 ‘ ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝐹 ‘ ( ( algSc ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ‘ ( ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ‘ 𝐴 ) ) ) ) )
95 eqid ⊢ ( var1 ‘ 𝐾 ) = ( var1 ‘ 𝐾 )
96 40 66 35 9 47 95 77 rhmply1vr1 ⊢ ( 𝜑 → ( 𝐹 ‘ ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) = ( var1 ‘ 𝐾 ) )
97 53 fveq2d ⊢ ( 𝜑 → ( 𝐹 ‘ ( ( algSc ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ‘ ( ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ‘ 𝐴 ) ) ) = ( 𝐹 ‘ ( ( ℤRHom ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ‘ 𝐴 ) ) )
98 eqid ⊢ ( ℤRHom ‘ ( Poly1 ‘ 𝐾 ) ) = ( ℤRHom ‘ ( Poly1 ‘ 𝐾 ) )
99 78 14 51 98 rhmzrhval ⊢ ( 𝜑 → ( 𝐹 ‘ ( ( ℤRHom ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ‘ 𝐴 ) ) = ( ( ℤRHom ‘ ( Poly1 ‘ 𝐾 ) ) ‘ 𝐴 ) )
100 97 99 eqtrd ⊢ ( 𝜑 → ( 𝐹 ‘ ( ( algSc ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ‘ ( ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ‘ 𝐴 ) ) ) = ( ( ℤRHom ‘ ( Poly1 ‘ 𝐾 ) ) ‘ 𝐴 ) )
101 eqid ⊢ ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) = ( algSc ‘ ( Poly1 ‘ 𝐾 ) )
102 eqid ⊢ ( ℤRHom ‘ 𝐾 ) = ( ℤRHom ‘ 𝐾 )
103 66 101 98 102 16 14 ply1asclzrhval ⊢ ( 𝜑 → ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) = ( ( ℤRHom ‘ ( Poly1 ‘ 𝐾 ) ) ‘ 𝐴 ) )
104 100 103 eqtr4d ⊢ ( 𝜑 → ( 𝐹 ‘ ( ( algSc ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ‘ ( ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ‘ 𝐴 ) ) ) = ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) )
105 96 104 oveq12d ⊢ ( 𝜑 → ( ( 𝐹 ‘ ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝐹 ‘ ( ( algSc ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ‘ ( ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ‘ 𝐴 ) ) ) ) = ( ( var1 ‘ 𝐾 ) ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ) )
106 94 105 eqtrd ⊢ ( 𝜑 → ( 𝐹 ‘ ( ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ( +g ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( ( algSc ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ‘ ( ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ‘ 𝐴 ) ) ) ) = ( ( var1 ‘ 𝐾 ) ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ) )
107 106 fveq2d ⊢ ( 𝜑 → ( ( eval1 ‘ 𝐾 ) ‘ ( 𝐹 ‘ ( ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ( +g ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( ( algSc ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ‘ ( ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ‘ 𝐴 ) ) ) ) ) = ( ( eval1 ‘ 𝐾 ) ‘ ( ( var1 ‘ 𝐾 ) ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ) ) )
108 107 fveq1d ⊢ ( 𝜑 → ( ( ( eval1 ‘ 𝐾 ) ‘ ( 𝐹 ‘ ( ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ( +g ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( ( algSc ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ‘ ( ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ‘ 𝐴 ) ) ) ) ) ‘ 𝑀 ) = ( ( ( eval1 ‘ 𝐾 ) ‘ ( ( var1 ‘ 𝐾 ) ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ) ) ‘ 𝑀 ) )
109 89 108 eqtrd ⊢ ( 𝜑 → ( 𝐻 ‘ ( 𝐹 ‘ ( ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ( +g ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( ( algSc ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ‘ ( ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ‘ 𝐴 ) ) ) ) ) = ( ( ( eval1 ‘ 𝐾 ) ‘ ( ( var1 ‘ 𝐾 ) ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ) ) ‘ 𝑀 ) )
110 82 109 eqtrd ⊢ ( 𝜑 → ( ( 𝐻 ∘ 𝐹 ) ‘ ( ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ( +g ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( ( algSc ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ‘ ( ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ‘ 𝐴 ) ) ) ) = ( ( ( eval1 ‘ 𝐾 ) ‘ ( ( var1 ‘ 𝐾 ) ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ) ) ‘ 𝑀 ) )
111 110 oveq2d ⊢ ( 𝜑 → ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) ( ( 𝐻 ∘ 𝐹 ) ‘ ( ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ( +g ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( ( algSc ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ‘ ( ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ‘ 𝐴 ) ) ) ) ) = ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) ( ( ( eval1 ‘ 𝐾 ) ‘ ( ( var1 ‘ 𝐾 ) ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ) ) ‘ 𝑀 ) ) )
112 65 111 eqtr2d ⊢ ( 𝜑 → ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) ( ( ( eval1 ‘ 𝐾 ) ‘ ( ( var1 ‘ 𝐾 ) ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ) ) ‘ 𝑀 ) ) = ( ( 𝐻 ∘ 𝐹 ) ‘ ( 𝑁 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ) ( ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ( +g ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( ( algSc ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ‘ ( ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ‘ 𝐴 ) ) ) ) ) )
113 eceq1 ⊢ ( 𝑢 = ( 𝑁 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ) ( ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ( +g ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( ( algSc ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ‘ ( ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ‘ 𝐴 ) ) ) ) → [ 𝑢 ] ( ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ~QG 𝐿 ) = [ ( 𝑁 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ) ( ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ( +g ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( ( algSc ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ‘ ( ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ‘ 𝐴 ) ) ) ) ] ( ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ~QG 𝐿 ) )
114 113 fveq2d ⊢ ( 𝑢 = ( 𝑁 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ) ( ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ( +g ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( ( algSc ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ‘ ( ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ‘ 𝐴 ) ) ) ) → ( 𝐼 ‘ [ 𝑢 ] ( ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ~QG 𝐿 ) ) = ( 𝐼 ‘ [ ( 𝑁 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ) ( ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ( +g ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( ( algSc ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ‘ ( ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ‘ 𝐴 ) ) ) ) ] ( ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ~QG 𝐿 ) ) )
115 fveq2 ⊢ ( 𝑢 = ( 𝑁 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ) ( ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ( +g ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( ( algSc ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ‘ ( ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ‘ 𝐴 ) ) ) ) → ( ( 𝐻 ∘ 𝐹 ) ‘ 𝑢 ) = ( ( 𝐻 ∘ 𝐹 ) ‘ ( 𝑁 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ) ( ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ( +g ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( ( algSc ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ‘ ( ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ‘ 𝐴 ) ) ) ) ) )
116 114 115 eqeq12d ⊢ ( 𝑢 = ( 𝑁 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ) ( ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ( +g ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( ( algSc ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ‘ ( ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ‘ 𝐴 ) ) ) ) → ( ( 𝐼 ‘ [ 𝑢 ] ( ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ~QG 𝐿 ) ) = ( ( 𝐻 ∘ 𝐹 ) ‘ 𝑢 ) ↔ ( 𝐼 ‘ [ ( 𝑁 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ) ( ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ( +g ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( ( algSc ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ‘ ( ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ‘ 𝐴 ) ) ) ) ] ( ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ~QG 𝐿 ) ) = ( ( 𝐻 ∘ 𝐹 ) ‘ ( 𝑁 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ) ( ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ( +g ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( ( algSc ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ‘ ( ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ‘ 𝐴 ) ) ) ) ) ) )
117 8 oveq1i ⊢ ( 𝑆 ~QG 𝐿 ) = ( ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ~QG 𝐿 )
118 8 117 oveq12i ⊢ ( 𝑆 /s ( 𝑆 ~QG 𝐿 ) ) = ( ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) /s ( ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ~QG 𝐿 ) )
119 4 118 eqtri ⊢ 𝐵 = ( ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) /s ( ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ~QG 𝐿 ) )
120 8 fveq2i ⊢ ( RSpan ‘ 𝑆 ) = ( RSpan ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) )
121 8 fveq2i ⊢ ( mulGrp ‘ 𝑆 ) = ( mulGrp ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) )
122 121 fveq2i ⊢ ( .g ‘ ( mulGrp ‘ 𝑆 ) ) = ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) )
123 122 oveqi ⊢ ( 𝑅 ( .g ‘ ( mulGrp ‘ 𝑆 ) ) ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) = ( 𝑅 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ) ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) )
124 8 fveq2i ⊢ ( 1r ‘ 𝑆 ) = ( 1r ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) )
125 8 fveq2i ⊢ ( -g ‘ 𝑆 ) = ( -g ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) )
126 123 124 125 oveq123i ⊢ ( ( 𝑅 ( .g ‘ ( mulGrp ‘ 𝑆 ) ) ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( -g ‘ 𝑆 ) ( 1r ‘ 𝑆 ) ) = ( ( 𝑅 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ) ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( -g ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( 1r ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) )
127 126 sneqi ⊢ { ( ( 𝑅 ( .g ‘ ( mulGrp ‘ 𝑆 ) ) ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( -g ‘ 𝑆 ) ( 1r ‘ 𝑆 ) ) } = { ( ( 𝑅 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ) ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( -g ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( 1r ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ) }
128 120 127 fveq12i ⊢ ( ( RSpan ‘ 𝑆 ) ‘ { ( ( 𝑅 ( .g ‘ ( mulGrp ‘ 𝑆 ) ) ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( -g ‘ 𝑆 ) ( 1r ‘ 𝑆 ) ) } ) = ( ( RSpan ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ‘ { ( ( 𝑅 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ) ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( -g ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( 1r ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ) } )
129 5 128 eqtri ⊢ 𝐿 = ( ( RSpan ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ‘ { ( ( 𝑅 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ) ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( -g ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( 1r ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ) } )
130 1 2 3 9 10 11 12 13 119 129 6 aks5lem2 ⊢ ( 𝜑 → ( 𝐼 ∈ ( 𝐵 RingHom 𝐾 ) ∧ ∀ 𝑢 ∈ ( Base ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( 𝐼 ‘ [ 𝑢 ] ( ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ~QG 𝐿 ) ) = ( ( 𝐻 ∘ 𝐹 ) ‘ 𝑢 ) ) )
131 130 simprd ⊢ ( 𝜑 → ∀ 𝑢 ∈ ( Base ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( 𝐼 ‘ [ 𝑢 ] ( ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ~QG 𝐿 ) ) = ( ( 𝐻 ∘ 𝐹 ) ‘ 𝑢 ) )
132 30 ringmgp ⊢ ( ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ∈ Ring → ( mulGrp ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ∈ Mnd )
133 43 132 syl ⊢ ( 𝜑 → ( mulGrp ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ∈ Mnd )
134 62 63 133 34 61 mulgnn0cld ⊢ ( 𝜑 → ( 𝑁 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ) ( ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ( +g ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( ( algSc ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ‘ ( ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ‘ 𝐴 ) ) ) ) ∈ ( Base ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) )
135 116 131 134 rspcdva ⊢ ( 𝜑 → ( 𝐼 ‘ [ ( 𝑁 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ) ( ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ( +g ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( ( algSc ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ‘ ( ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ‘ 𝐴 ) ) ) ) ] ( ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ~QG 𝐿 ) ) = ( ( 𝐻 ∘ 𝐹 ) ‘ ( 𝑁 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ) ( ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ( +g ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( ( algSc ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ‘ ( ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ‘ 𝐴 ) ) ) ) ) )
136 135 eqcomd ⊢ ( 𝜑 → ( ( 𝐻 ∘ 𝐹 ) ‘ ( 𝑁 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ) ( ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ( +g ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( ( algSc ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ‘ ( ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ‘ 𝐴 ) ) ) ) ) = ( 𝐼 ‘ [ ( 𝑁 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ) ( ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ( +g ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( ( algSc ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ‘ ( ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ‘ 𝐴 ) ) ) ) ] ( ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ~QG 𝐿 ) ) )
137 8 eqcomi ⊢ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) = 𝑆
138 137 a1i ⊢ ( 𝜑 → ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) = 𝑆 )
139 138 fveq2d ⊢ ( 𝜑 → ( mulGrp ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) = ( mulGrp ‘ 𝑆 ) )
140 139 fveq2d ⊢ ( 𝜑 → ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ) = ( .g ‘ ( mulGrp ‘ 𝑆 ) ) )
141 eqidd ⊢ ( 𝜑 → 𝑁 = 𝑁 )
142 138 fveq2d ⊢ ( 𝜑 → ( +g ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) = ( +g ‘ 𝑆 ) )
143 eqidd ⊢ ( 𝜑 → ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) = ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) )
144 138 fveq2d ⊢ ( 𝜑 → ( algSc ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) = ( algSc ‘ 𝑆 ) )
145 144 fveq1d ⊢ ( 𝜑 → ( ( algSc ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ‘ ( ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ‘ 𝐴 ) ) = ( ( algSc ‘ 𝑆 ) ‘ ( ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ‘ 𝐴 ) ) )
146 142 143 145 oveq123d ⊢ ( 𝜑 → ( ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ( +g ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( ( algSc ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ‘ ( ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ‘ 𝐴 ) ) ) = ( ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ( +g ‘ 𝑆 ) ( ( algSc ‘ 𝑆 ) ‘ ( ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ‘ 𝐴 ) ) ) )
147 140 141 146 oveq123d ⊢ ( 𝜑 → ( 𝑁 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ) ( ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ( +g ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( ( algSc ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ‘ ( ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ‘ 𝐴 ) ) ) ) = ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝑆 ) ) ( ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ( +g ‘ 𝑆 ) ( ( algSc ‘ 𝑆 ) ‘ ( ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ‘ 𝐴 ) ) ) ) )
148 147 eceq1d ⊢ ( 𝜑 → [ ( 𝑁 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ) ( ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ( +g ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( ( algSc ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ‘ ( ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ‘ 𝐴 ) ) ) ) ] ( ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ~QG 𝐿 ) = [ ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝑆 ) ) ( ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ( +g ‘ 𝑆 ) ( ( algSc ‘ 𝑆 ) ‘ ( ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ‘ 𝐴 ) ) ) ) ] ( ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ~QG 𝐿 ) )
149 138 oveq1d ⊢ ( 𝜑 → ( ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ~QG 𝐿 ) = ( 𝑆 ~QG 𝐿 ) )
150 149 eceq2d ⊢ ( 𝜑 → [ ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝑆 ) ) ( ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ( +g ‘ 𝑆 ) ( ( algSc ‘ 𝑆 ) ‘ ( ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ‘ 𝐴 ) ) ) ) ] ( ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ~QG 𝐿 ) = [ ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝑆 ) ) ( ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ( +g ‘ 𝑆 ) ( ( algSc ‘ 𝑆 ) ‘ ( ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ‘ 𝐴 ) ) ) ) ] ( 𝑆 ~QG 𝐿 ) )
151 148 150 eqtrd ⊢ ( 𝜑 → [ ( 𝑁 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ) ( ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ( +g ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( ( algSc ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ‘ ( ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ‘ 𝐴 ) ) ) ) ] ( ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ~QG 𝐿 ) = [ ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝑆 ) ) ( ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ( +g ‘ 𝑆 ) ( ( algSc ‘ 𝑆 ) ‘ ( ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ‘ 𝐴 ) ) ) ) ] ( 𝑆 ~QG 𝐿 ) )
152 eqcom ⊢ ( ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) = 𝑆 ↔ 𝑆 = ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) )
153 152 imbi2i ⊢ ( ( 𝜑 → ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) = 𝑆 ) ↔ ( 𝜑 → 𝑆 = ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) )
154 138 153 mpbi ⊢ ( 𝜑 → 𝑆 = ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) )
155 154 fveq2d ⊢ ( 𝜑 → ( +g ‘ 𝑆 ) = ( +g ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) )
156 154 fveq2d ⊢ ( 𝜑 → ( mulGrp ‘ 𝑆 ) = ( mulGrp ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) )
157 156 fveq2d ⊢ ( 𝜑 → ( .g ‘ ( mulGrp ‘ 𝑆 ) ) = ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ) )
158 157 oveqd ⊢ ( 𝜑 → ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝑆 ) ) ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) = ( 𝑁 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ) ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) )
159 154 fveq2d ⊢ ( 𝜑 → ( algSc ‘ 𝑆 ) = ( algSc ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) )
160 159 fveq1d ⊢ ( 𝜑 → ( ( algSc ‘ 𝑆 ) ‘ ( ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ‘ 𝐴 ) ) = ( ( algSc ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ‘ ( ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ‘ 𝐴 ) ) )
161 155 158 160 oveq123d ⊢ ( 𝜑 → ( ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝑆 ) ) ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( +g ‘ 𝑆 ) ( ( algSc ‘ 𝑆 ) ‘ ( ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ‘ 𝐴 ) ) ) = ( ( 𝑁 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ) ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( +g ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( ( algSc ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ‘ ( ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ‘ 𝐴 ) ) ) )
162 161 eceq1d ⊢ ( 𝜑 → [ ( ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝑆 ) ) ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( +g ‘ 𝑆 ) ( ( algSc ‘ 𝑆 ) ‘ ( ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ‘ 𝐴 ) ) ) ] ( 𝑆 ~QG 𝐿 ) = [ ( ( 𝑁 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ) ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( +g ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( ( algSc ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ‘ ( ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ‘ 𝐴 ) ) ) ] ( 𝑆 ~QG 𝐿 ) )
163 149 eqcomd ⊢ ( 𝜑 → ( 𝑆 ~QG 𝐿 ) = ( ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ~QG 𝐿 ) )
164 163 eceq2d ⊢ ( 𝜑 → [ ( ( 𝑁 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ) ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( +g ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( ( algSc ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ‘ ( ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ‘ 𝐴 ) ) ) ] ( 𝑆 ~QG 𝐿 ) = [ ( ( 𝑁 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ) ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( +g ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( ( algSc ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ‘ ( ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ‘ 𝐴 ) ) ) ] ( ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ~QG 𝐿 ) )
165 162 164 eqtrd ⊢ ( 𝜑 → [ ( ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝑆 ) ) ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( +g ‘ 𝑆 ) ( ( algSc ‘ 𝑆 ) ‘ ( ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ‘ 𝐴 ) ) ) ] ( 𝑆 ~QG 𝐿 ) = [ ( ( 𝑁 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ) ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( +g ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( ( algSc ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ‘ ( ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ‘ 𝐴 ) ) ) ] ( ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ~QG 𝐿 ) )
166 151 15 165 3eqtrd ⊢ ( 𝜑 → [ ( 𝑁 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ) ( ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ( +g ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( ( algSc ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ‘ ( ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ‘ 𝐴 ) ) ) ) ] ( ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ~QG 𝐿 ) = [ ( ( 𝑁 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ) ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( +g ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( ( algSc ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ‘ ( ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ‘ 𝐴 ) ) ) ] ( ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ~QG 𝐿 ) )
167 166 fveq2d ⊢ ( 𝜑 → ( 𝐼 ‘ [ ( 𝑁 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ) ( ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ( +g ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( ( algSc ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ‘ ( ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ‘ 𝐴 ) ) ) ) ] ( ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ~QG 𝐿 ) ) = ( 𝐼 ‘ [ ( ( 𝑁 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ) ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( +g ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( ( algSc ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ‘ ( ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ‘ 𝐴 ) ) ) ] ( ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ~QG 𝐿 ) ) )
168 eceq1 ⊢ ( 𝑢 = ( ( 𝑁 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ) ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( +g ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( ( algSc ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ‘ ( ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ‘ 𝐴 ) ) ) → [ 𝑢 ] ( ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ~QG 𝐿 ) = [ ( ( 𝑁 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ) ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( +g ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( ( algSc ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ‘ ( ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ‘ 𝐴 ) ) ) ] ( ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ~QG 𝐿 ) )
169 168 fveq2d ⊢ ( 𝑢 = ( ( 𝑁 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ) ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( +g ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( ( algSc ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ‘ ( ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ‘ 𝐴 ) ) ) → ( 𝐼 ‘ [ 𝑢 ] ( ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ~QG 𝐿 ) ) = ( 𝐼 ‘ [ ( ( 𝑁 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ) ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( +g ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( ( algSc ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ‘ ( ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ‘ 𝐴 ) ) ) ] ( ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ~QG 𝐿 ) ) )
170 fveq2 ⊢ ( 𝑢 = ( ( 𝑁 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ) ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( +g ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( ( algSc ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ‘ ( ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ‘ 𝐴 ) ) ) → ( ( 𝐻 ∘ 𝐹 ) ‘ 𝑢 ) = ( ( 𝐻 ∘ 𝐹 ) ‘ ( ( 𝑁 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ) ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( +g ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( ( algSc ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ‘ ( ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ‘ 𝐴 ) ) ) ) )
171 169 170 eqeq12d ⊢ ( 𝑢 = ( ( 𝑁 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ) ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( +g ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( ( algSc ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ‘ ( ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ‘ 𝐴 ) ) ) → ( ( 𝐼 ‘ [ 𝑢 ] ( ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ~QG 𝐿 ) ) = ( ( 𝐻 ∘ 𝐹 ) ‘ 𝑢 ) ↔ ( 𝐼 ‘ [ ( ( 𝑁 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ) ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( +g ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( ( algSc ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ‘ ( ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ‘ 𝐴 ) ) ) ] ( ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ~QG 𝐿 ) ) = ( ( 𝐻 ∘ 𝐹 ) ‘ ( ( 𝑁 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ) ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( +g ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( ( algSc ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ‘ ( ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ‘ 𝐴 ) ) ) ) ) )
172 62 63 133 34 49 mulgnn0cld ⊢ ( 𝜑 → ( 𝑁 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ) ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ∈ ( Base ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) )
173 35 36 45 172 60 grpcld ⊢ ( 𝜑 → ( ( 𝑁 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ) ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( +g ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( ( algSc ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ‘ ( ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ‘ 𝐴 ) ) ) ∈ ( Base ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) )
174 171 131 173 rspcdva ⊢ ( 𝜑 → ( 𝐼 ‘ [ ( ( 𝑁 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ) ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( +g ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( ( algSc ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ‘ ( ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ‘ 𝐴 ) ) ) ] ( ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ~QG 𝐿 ) ) = ( ( 𝐻 ∘ 𝐹 ) ‘ ( ( 𝑁 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ) ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( +g ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( ( algSc ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ‘ ( ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ‘ 𝐴 ) ) ) ) )
175 136 167 174 3eqtrd ⊢ ( 𝜑 → ( ( 𝐻 ∘ 𝐹 ) ‘ ( 𝑁 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ) ( ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ( +g ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( ( algSc ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ‘ ( ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ‘ 𝐴 ) ) ) ) ) = ( ( 𝐻 ∘ 𝐹 ) ‘ ( ( 𝑁 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ) ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( +g ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( ( algSc ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ‘ ( ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ‘ 𝐴 ) ) ) ) )
176 81 173 fvco3d ⊢ ( 𝜑 → ( ( 𝐻 ∘ 𝐹 ) ‘ ( ( 𝑁 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ) ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( +g ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( ( algSc ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ‘ ( ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ‘ 𝐴 ) ) ) ) = ( 𝐻 ‘ ( 𝐹 ‘ ( ( 𝑁 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ) ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( +g ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( ( algSc ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ‘ ( ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ‘ 𝐴 ) ) ) ) ) )
177 simpr ⊢ ( ( 𝜑 ∧ 𝑟 = ( 𝐹 ‘ ( ( 𝑁 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ) ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( +g ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( ( algSc ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ‘ ( ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ‘ 𝐴 ) ) ) ) ) → 𝑟 = ( 𝐹 ‘ ( ( 𝑁 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ) ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( +g ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( ( algSc ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ‘ ( ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ‘ 𝐴 ) ) ) ) )
178 177 fveq2d ⊢ ( ( 𝜑 ∧ 𝑟 = ( 𝐹 ‘ ( ( 𝑁 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ) ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( +g ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( ( algSc ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ‘ ( ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ‘ 𝐴 ) ) ) ) ) → ( ( eval1 ‘ 𝐾 ) ‘ 𝑟 ) = ( ( eval1 ‘ 𝐾 ) ‘ ( 𝐹 ‘ ( ( 𝑁 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ) ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( +g ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( ( algSc ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ‘ ( ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ‘ 𝐴 ) ) ) ) ) )
179 178 fveq1d ⊢ ( ( 𝜑 ∧ 𝑟 = ( 𝐹 ‘ ( ( 𝑁 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ) ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( +g ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( ( algSc ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ‘ ( ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ‘ 𝐴 ) ) ) ) ) → ( ( ( eval1 ‘ 𝐾 ) ‘ 𝑟 ) ‘ 𝑀 ) = ( ( ( eval1 ‘ 𝐾 ) ‘ ( 𝐹 ‘ ( ( 𝑁 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ) ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( +g ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( ( algSc ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ‘ ( ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ‘ 𝐴 ) ) ) ) ) ‘ 𝑀 ) )
180 81 173 ffvelcdmd ⊢ ( 𝜑 → ( 𝐹 ‘ ( ( 𝑁 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ) ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( +g ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( ( algSc ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ‘ ( ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ‘ 𝐴 ) ) ) ) ∈ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) )
181 fvexd ⊢ ( 𝜑 → ( ( ( eval1 ‘ 𝐾 ) ‘ ( 𝐹 ‘ ( ( 𝑁 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ) ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( +g ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( ( algSc ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ‘ ( ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ‘ 𝐴 ) ) ) ) ) ‘ 𝑀 ) ∈ V )
182 83 179 180 181 fvmptd ⊢ ( 𝜑 → ( 𝐻 ‘ ( 𝐹 ‘ ( ( 𝑁 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ) ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( +g ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( ( algSc ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ‘ ( ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ‘ 𝐴 ) ) ) ) ) = ( ( ( eval1 ‘ 𝐾 ) ‘ ( 𝐹 ‘ ( ( 𝑁 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ) ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( +g ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( ( algSc ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ‘ ( ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ‘ 𝐴 ) ) ) ) ) ‘ 𝑀 ) )
183 35 36 92 ghmlin ⊢ ( ( 𝐹 ∈ ( ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) GrpHom ( Poly1 ‘ 𝐾 ) ) ∧ ( 𝑁 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ) ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ∈ ( Base ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ∧ ( ( algSc ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ‘ ( ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ‘ 𝐴 ) ) ∈ ( Base ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ) → ( 𝐹 ‘ ( ( 𝑁 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ) ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( +g ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( ( algSc ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ‘ ( ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ‘ 𝐴 ) ) ) ) = ( ( 𝐹 ‘ ( 𝑁 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ) ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ) ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝐹 ‘ ( ( algSc ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ‘ ( ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ‘ 𝐴 ) ) ) ) )
184 91 172 60 183 syl3anc ⊢ ( 𝜑 → ( 𝐹 ‘ ( ( 𝑁 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ) ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( +g ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( ( algSc ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ‘ ( ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ‘ 𝐴 ) ) ) ) = ( ( 𝐹 ‘ ( 𝑁 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ) ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ) ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝐹 ‘ ( ( algSc ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ‘ ( ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ‘ 𝐴 ) ) ) ) )
185 184 fveq2d ⊢ ( 𝜑 → ( ( eval1 ‘ 𝐾 ) ‘ ( 𝐹 ‘ ( ( 𝑁 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ) ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( +g ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( ( algSc ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ‘ ( ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ‘ 𝐴 ) ) ) ) ) = ( ( eval1 ‘ 𝐾 ) ‘ ( ( 𝐹 ‘ ( 𝑁 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ) ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ) ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝐹 ‘ ( ( algSc ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ‘ ( ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ‘ 𝐴 ) ) ) ) ) )
186 185 fveq1d ⊢ ( 𝜑 → ( ( ( eval1 ‘ 𝐾 ) ‘ ( 𝐹 ‘ ( ( 𝑁 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ) ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( +g ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( ( algSc ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ‘ ( ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ‘ 𝐴 ) ) ) ) ) ‘ 𝑀 ) = ( ( ( eval1 ‘ 𝐾 ) ‘ ( ( 𝐹 ‘ ( 𝑁 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ) ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ) ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝐹 ‘ ( ( algSc ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ‘ ( ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ‘ 𝐴 ) ) ) ) ) ‘ 𝑀 ) )
187 eqid ⊢ ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) = ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) )
188 30 187 rhmmhm ⊢ ( 𝐹 ∈ ( ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) RingHom ( Poly1 ‘ 𝐾 ) ) → 𝐹 ∈ ( ( mulGrp ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) MndHom ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) ) )
189 78 188 syl ⊢ ( 𝜑 → 𝐹 ∈ ( ( mulGrp ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) MndHom ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) ) )
190 eqid ⊢ ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) ) = ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) )
191 62 63 190 mhmmulg ⊢ ( ( 𝐹 ∈ ( ( mulGrp ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) MndHom ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) ) ∧ 𝑁 ∈ ℕ0 ∧ ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ∈ ( Base ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ) → ( 𝐹 ‘ ( 𝑁 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ) ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ) = ( 𝑁 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) ) ( 𝐹 ‘ ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ) )
192 189 34 49 191 syl3anc ⊢ ( 𝜑 → ( 𝐹 ‘ ( 𝑁 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ) ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ) = ( 𝑁 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) ) ( 𝐹 ‘ ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ) )
193 192 97 oveq12d ⊢ ( 𝜑 → ( ( 𝐹 ‘ ( 𝑁 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ) ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ) ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝐹 ‘ ( ( algSc ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ‘ ( ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ‘ 𝐴 ) ) ) ) = ( ( 𝑁 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) ) ( 𝐹 ‘ ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ) ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝐹 ‘ ( ( ℤRHom ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ‘ 𝐴 ) ) ) )
194 193 fveq2d ⊢ ( 𝜑 → ( ( eval1 ‘ 𝐾 ) ‘ ( ( 𝐹 ‘ ( 𝑁 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ) ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ) ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝐹 ‘ ( ( algSc ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ‘ ( ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ‘ 𝐴 ) ) ) ) ) = ( ( eval1 ‘ 𝐾 ) ‘ ( ( 𝑁 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) ) ( 𝐹 ‘ ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ) ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝐹 ‘ ( ( ℤRHom ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ‘ 𝐴 ) ) ) ) )
195 194 fveq1d ⊢ ( 𝜑 → ( ( ( eval1 ‘ 𝐾 ) ‘ ( ( 𝐹 ‘ ( 𝑁 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ) ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ) ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝐹 ‘ ( ( algSc ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ‘ ( ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ‘ 𝐴 ) ) ) ) ) ‘ 𝑀 ) = ( ( ( eval1 ‘ 𝐾 ) ‘ ( ( 𝑁 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) ) ( 𝐹 ‘ ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ) ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝐹 ‘ ( ( ℤRHom ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ‘ 𝐴 ) ) ) ) ‘ 𝑀 ) )
196 96 oveq2d ⊢ ( 𝜑 → ( 𝑁 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) ) ( 𝐹 ‘ ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ) = ( 𝑁 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) ) ( var1 ‘ 𝐾 ) ) )
197 196 99 oveq12d ⊢ ( 𝜑 → ( ( 𝑁 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) ) ( 𝐹 ‘ ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ) ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝐹 ‘ ( ( ℤRHom ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ‘ 𝐴 ) ) ) = ( ( 𝑁 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) ) ( var1 ‘ 𝐾 ) ) ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( ℤRHom ‘ ( Poly1 ‘ 𝐾 ) ) ‘ 𝐴 ) ) )
198 197 fveq2d ⊢ ( 𝜑 → ( ( eval1 ‘ 𝐾 ) ‘ ( ( 𝑁 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) ) ( 𝐹 ‘ ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ) ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝐹 ‘ ( ( ℤRHom ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ‘ 𝐴 ) ) ) ) = ( ( eval1 ‘ 𝐾 ) ‘ ( ( 𝑁 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) ) ( var1 ‘ 𝐾 ) ) ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( ℤRHom ‘ ( Poly1 ‘ 𝐾 ) ) ‘ 𝐴 ) ) ) )
199 198 fveq1d ⊢ ( 𝜑 → ( ( ( eval1 ‘ 𝐾 ) ‘ ( ( 𝑁 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) ) ( 𝐹 ‘ ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ) ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝐹 ‘ ( ( ℤRHom ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ‘ 𝐴 ) ) ) ) ‘ 𝑀 ) = ( ( ( eval1 ‘ 𝐾 ) ‘ ( ( 𝑁 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) ) ( var1 ‘ 𝐾 ) ) ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( ℤRHom ‘ ( Poly1 ‘ 𝐾 ) ) ‘ 𝐴 ) ) ) ‘ 𝑀 ) )
200 eqid ⊢ ( eval1 ‘ 𝐾 ) = ( eval1 ‘ 𝐾 )
201 200 95 25 66 79 16 28 evl1vard ⊢ ( 𝜑 → ( ( var1 ‘ 𝐾 ) ∈ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) ∧ ( ( ( eval1 ‘ 𝐾 ) ‘ ( var1 ‘ 𝐾 ) ) ‘ 𝑀 ) = 𝑀 ) )
202 200 66 25 79 16 28 201 190 21 34 evl1expd ⊢ ( 𝜑 → ( ( 𝑁 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) ) ( var1 ‘ 𝐾 ) ) ∈ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) ∧ ( ( ( eval1 ‘ 𝐾 ) ‘ ( 𝑁 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) ) ( var1 ‘ 𝐾 ) ) ) ‘ 𝑀 ) = ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑀 ) ) )
203 66 ply1crng ⊢ ( 𝐾 ∈ CRing → ( Poly1 ‘ 𝐾 ) ∈ CRing )
204 16 203 syl ⊢ ( 𝜑 → ( Poly1 ‘ 𝐾 ) ∈ CRing )
205 204 crngringd ⊢ ( 𝜑 → ( Poly1 ‘ 𝐾 ) ∈ Ring )
206 98 zrhrhm ⊢ ( ( Poly1 ‘ 𝐾 ) ∈ Ring → ( ℤRHom ‘ ( Poly1 ‘ 𝐾 ) ) ∈ ( ℤring RingHom ( Poly1 ‘ 𝐾 ) ) )
207 55 79 rhmf ⊢ ( ( ℤRHom ‘ ( Poly1 ‘ 𝐾 ) ) ∈ ( ℤring RingHom ( Poly1 ‘ 𝐾 ) ) → ( ℤRHom ‘ ( Poly1 ‘ 𝐾 ) ) : ℤ ⟶ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) )
208 206 207 syl ⊢ ( ( Poly1 ‘ 𝐾 ) ∈ Ring → ( ℤRHom ‘ ( Poly1 ‘ 𝐾 ) ) : ℤ ⟶ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) )
209 205 208 syl ⊢ ( 𝜑 → ( ℤRHom ‘ ( Poly1 ‘ 𝐾 ) ) : ℤ ⟶ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) )
210 209 14 ffvelcdmd ⊢ ( 𝜑 → ( ( ℤRHom ‘ ( Poly1 ‘ 𝐾 ) ) ‘ 𝐴 ) ∈ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) )
211 eqidd ⊢ ( 𝜑 → ( ( ( eval1 ‘ 𝐾 ) ‘ ( ( ℤRHom ‘ ( Poly1 ‘ 𝐾 ) ) ‘ 𝐴 ) ) ‘ 𝑀 ) = ( ( ( eval1 ‘ 𝐾 ) ‘ ( ( ℤRHom ‘ ( Poly1 ‘ 𝐾 ) ) ‘ 𝐴 ) ) ‘ 𝑀 ) )
212 210 211 jca ⊢ ( 𝜑 → ( ( ( ℤRHom ‘ ( Poly1 ‘ 𝐾 ) ) ‘ 𝐴 ) ∈ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) ∧ ( ( ( eval1 ‘ 𝐾 ) ‘ ( ( ℤRHom ‘ ( Poly1 ‘ 𝐾 ) ) ‘ 𝐴 ) ) ‘ 𝑀 ) = ( ( ( eval1 ‘ 𝐾 ) ‘ ( ( ℤRHom ‘ ( Poly1 ‘ 𝐾 ) ) ‘ 𝐴 ) ) ‘ 𝑀 ) ) )
213 eqid ⊢ ( +g ‘ 𝐾 ) = ( +g ‘ 𝐾 )
214 200 66 25 79 16 28 202 212 92 213 evl1addd ⊢ ( 𝜑 → ( ( ( 𝑁 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) ) ( var1 ‘ 𝐾 ) ) ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( ℤRHom ‘ ( Poly1 ‘ 𝐾 ) ) ‘ 𝐴 ) ) ∈ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) ∧ ( ( ( eval1 ‘ 𝐾 ) ‘ ( ( 𝑁 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) ) ( var1 ‘ 𝐾 ) ) ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( ℤRHom ‘ ( Poly1 ‘ 𝐾 ) ) ‘ 𝐴 ) ) ) ‘ 𝑀 ) = ( ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑀 ) ( +g ‘ 𝐾 ) ( ( ( eval1 ‘ 𝐾 ) ‘ ( ( ℤRHom ‘ ( Poly1 ‘ 𝐾 ) ) ‘ 𝐴 ) ) ‘ 𝑀 ) ) ) )
215 214 simprd ⊢ ( 𝜑 → ( ( ( eval1 ‘ 𝐾 ) ‘ ( ( 𝑁 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) ) ( var1 ‘ 𝐾 ) ) ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( ℤRHom ‘ ( Poly1 ‘ 𝐾 ) ) ‘ 𝐴 ) ) ) ‘ 𝑀 ) = ( ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑀 ) ( +g ‘ 𝐾 ) ( ( ( eval1 ‘ 𝐾 ) ‘ ( ( ℤRHom ‘ ( Poly1 ‘ 𝐾 ) ) ‘ 𝐴 ) ) ‘ 𝑀 ) ) )
216 102 zrhrhm ⊢ ( 𝐾 ∈ Ring → ( ℤRHom ‘ 𝐾 ) ∈ ( ℤring RingHom 𝐾 ) )
217 55 25 rhmf ⊢ ( ( ℤRHom ‘ 𝐾 ) ∈ ( ℤring RingHom 𝐾 ) → ( ℤRHom ‘ 𝐾 ) : ℤ ⟶ ( Base ‘ 𝐾 ) )
218 216 217 syl ⊢ ( 𝐾 ∈ Ring → ( ℤRHom ‘ 𝐾 ) : ℤ ⟶ ( Base ‘ 𝐾 ) )
219 67 218 syl ⊢ ( 𝜑 → ( ℤRHom ‘ 𝐾 ) : ℤ ⟶ ( Base ‘ 𝐾 ) )
220 219 14 ffvelcdmd ⊢ ( 𝜑 → ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ∈ ( Base ‘ 𝐾 ) )
221 200 66 25 101 79 16 220 28 evl1scad ⊢ ( 𝜑 → ( ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ∈ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) ∧ ( ( ( eval1 ‘ 𝐾 ) ‘ ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ) ‘ 𝑀 ) = ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) )
222 221 simprd ⊢ ( 𝜑 → ( ( ( eval1 ‘ 𝐾 ) ‘ ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ) ‘ 𝑀 ) = ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) )
223 222 eqcomd ⊢ ( 𝜑 → ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) = ( ( ( eval1 ‘ 𝐾 ) ‘ ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ) ‘ 𝑀 ) )
224 103 fveq2d ⊢ ( 𝜑 → ( ( eval1 ‘ 𝐾 ) ‘ ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ) = ( ( eval1 ‘ 𝐾 ) ‘ ( ( ℤRHom ‘ ( Poly1 ‘ 𝐾 ) ) ‘ 𝐴 ) ) )
225 224 fveq1d ⊢ ( 𝜑 → ( ( ( eval1 ‘ 𝐾 ) ‘ ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ) ‘ 𝑀 ) = ( ( ( eval1 ‘ 𝐾 ) ‘ ( ( ℤRHom ‘ ( Poly1 ‘ 𝐾 ) ) ‘ 𝐴 ) ) ‘ 𝑀 ) )
226 223 225 eqtr2d ⊢ ( 𝜑 → ( ( ( eval1 ‘ 𝐾 ) ‘ ( ( ℤRHom ‘ ( Poly1 ‘ 𝐾 ) ) ‘ 𝐴 ) ) ‘ 𝑀 ) = ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) )
227 226 oveq2d ⊢ ( 𝜑 → ( ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑀 ) ( +g ‘ 𝐾 ) ( ( ( eval1 ‘ 𝐾 ) ‘ ( ( ℤRHom ‘ ( Poly1 ‘ 𝐾 ) ) ‘ 𝐴 ) ) ‘ 𝑀 ) ) = ( ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑀 ) ( +g ‘ 𝐾 ) ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) )
228 215 227 eqtrd ⊢ ( 𝜑 → ( ( ( eval1 ‘ 𝐾 ) ‘ ( ( 𝑁 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) ) ( var1 ‘ 𝐾 ) ) ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( ℤRHom ‘ ( Poly1 ‘ 𝐾 ) ) ‘ 𝐴 ) ) ) ‘ 𝑀 ) = ( ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑀 ) ( +g ‘ 𝐾 ) ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) )
229 199 228 eqtrd ⊢ ( 𝜑 → ( ( ( eval1 ‘ 𝐾 ) ‘ ( ( 𝑁 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) ) ( 𝐹 ‘ ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ) ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝐹 ‘ ( ( ℤRHom ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ‘ 𝐴 ) ) ) ) ‘ 𝑀 ) = ( ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑀 ) ( +g ‘ 𝐾 ) ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) )
230 19 cmnmndd ⊢ ( 𝜑 → ( mulGrp ‘ 𝐾 ) ∈ Mnd )
231 26 21 230 34 28 mulgnn0cld ⊢ ( 𝜑 → ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑀 ) ∈ ( Base ‘ 𝐾 ) )
232 200 95 25 66 79 16 231 evl1vard ⊢ ( 𝜑 → ( ( var1 ‘ 𝐾 ) ∈ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) ∧ ( ( ( eval1 ‘ 𝐾 ) ‘ ( var1 ‘ 𝐾 ) ) ‘ ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑀 ) ) = ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑀 ) ) )
233 200 66 25 101 79 16 220 231 evl1scad ⊢ ( 𝜑 → ( ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ∈ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) ∧ ( ( ( eval1 ‘ 𝐾 ) ‘ ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ) ‘ ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑀 ) ) = ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) )
234 200 66 25 79 16 231 232 233 92 213 evl1addd ⊢ ( 𝜑 → ( ( ( var1 ‘ 𝐾 ) ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ) ∈ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) ∧ ( ( ( eval1 ‘ 𝐾 ) ‘ ( ( var1 ‘ 𝐾 ) ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ) ) ‘ ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑀 ) ) = ( ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑀 ) ( +g ‘ 𝐾 ) ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ) )
235 234 simprd ⊢ ( 𝜑 → ( ( ( eval1 ‘ 𝐾 ) ‘ ( ( var1 ‘ 𝐾 ) ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ) ) ‘ ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑀 ) ) = ( ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑀 ) ( +g ‘ 𝐾 ) ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) )
236 229 235 eqtr4d ⊢ ( 𝜑 → ( ( ( eval1 ‘ 𝐾 ) ‘ ( ( 𝑁 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) ) ( 𝐹 ‘ ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ) ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝐹 ‘ ( ( ℤRHom ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ‘ 𝐴 ) ) ) ) ‘ 𝑀 ) = ( ( ( eval1 ‘ 𝐾 ) ‘ ( ( var1 ‘ 𝐾 ) ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ) ) ‘ ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑀 ) ) )
237 195 236 eqtrd ⊢ ( 𝜑 → ( ( ( eval1 ‘ 𝐾 ) ‘ ( ( 𝐹 ‘ ( 𝑁 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ) ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ) ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( 𝐹 ‘ ( ( algSc ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ‘ ( ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ‘ 𝐴 ) ) ) ) ) ‘ 𝑀 ) = ( ( ( eval1 ‘ 𝐾 ) ‘ ( ( var1 ‘ 𝐾 ) ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ) ) ‘ ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑀 ) ) )
238 186 237 eqtrd ⊢ ( 𝜑 → ( ( ( eval1 ‘ 𝐾 ) ‘ ( 𝐹 ‘ ( ( 𝑁 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ) ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( +g ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( ( algSc ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ‘ ( ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ‘ 𝐴 ) ) ) ) ) ‘ 𝑀 ) = ( ( ( eval1 ‘ 𝐾 ) ‘ ( ( var1 ‘ 𝐾 ) ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ) ) ‘ ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑀 ) ) )
239 182 238 eqtrd ⊢ ( 𝜑 → ( 𝐻 ‘ ( 𝐹 ‘ ( ( 𝑁 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ) ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( +g ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( ( algSc ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ‘ ( ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ‘ 𝐴 ) ) ) ) ) = ( ( ( eval1 ‘ 𝐾 ) ‘ ( ( var1 ‘ 𝐾 ) ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ) ) ‘ ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑀 ) ) )
240 176 239 eqtrd ⊢ ( 𝜑 → ( ( 𝐻 ∘ 𝐹 ) ‘ ( ( 𝑁 ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ) ( var1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( +g ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ( ( algSc ‘ ( Poly1 ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ) ‘ ( ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑁 ) ) ‘ 𝐴 ) ) ) ) = ( ( ( eval1 ‘ 𝐾 ) ‘ ( ( var1 ‘ 𝐾 ) ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ) ) ‘ ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑀 ) ) )
241 112 175 240 3eqtrd ⊢ ( 𝜑 → ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) ( ( ( eval1 ‘ 𝐾 ) ‘ ( ( var1 ‘ 𝐾 ) ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ) ) ‘ 𝑀 ) ) = ( ( ( eval1 ‘ 𝐾 ) ‘ ( ( var1 ‘ 𝐾 ) ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝐴 ) ) ) ) ‘ ( 𝑁 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑀 ) ) )