Metamath Proof Explorer

Theorem aks6d1c6isolem2

Description: Lemma to construct the group homomorphism for the AKS Theorem. (Contributed by metakunt, 14-May-2025)

Ref Expression
Hypotheses aks6d1c6isolem1.1 ⊢ ( 𝜑 → 𝑅 ∈ CMnd )
aks6d1c6isolem1.2 ⊢ ( 𝜑 → 𝐾 ∈ ℕ )
aks6d1c6isolem1.3 ⊢ 𝑈 = { 𝑎 ∈ ( Base ‘ 𝑅 ) ∣ ∃ 𝑖 ∈ ( Base ‘ 𝑅 ) ( 𝑖 ( +g ‘ 𝑅 ) 𝑎 ) = ( 0g ‘ 𝑅 ) }
aks6d1c6isolem1.4 ⊢ 𝐹 = ( 𝑥 ∈ ℤ ↦ ( 𝑥 ( .g ‘ ( 𝑅 ↾s 𝑈 ) ) 𝑀 ) )
aks6d1c6isolem1.5 ⊢ ( 𝜑 → 𝑀 ∈ ( 𝑅 PrimRoots 𝐾 ) )
Assertion aks6d1c6isolem2 ( 𝜑 → 𝐹 ∈ ( ℤring GrpHom ( ( 𝑅 ↾s 𝑈 ) ↾s ran 𝐹 ) ) )

Proof

Step Hyp Ref Expression
1 aks6d1c6isolem1.1 ⊢ ( 𝜑 → 𝑅 ∈ CMnd )
2 aks6d1c6isolem1.2 ⊢ ( 𝜑 → 𝐾 ∈ ℕ )
3 aks6d1c6isolem1.3 ⊢ 𝑈 = { 𝑎 ∈ ( Base ‘ 𝑅 ) ∣ ∃ 𝑖 ∈ ( Base ‘ 𝑅 ) ( 𝑖 ( +g ‘ 𝑅 ) 𝑎 ) = ( 0g ‘ 𝑅 ) }
4 aks6d1c6isolem1.4 ⊢ 𝐹 = ( 𝑥 ∈ ℤ ↦ ( 𝑥 ( .g ‘ ( 𝑅 ↾s 𝑈 ) ) 𝑀 ) )
5 aks6d1c6isolem1.5 ⊢ ( 𝜑 → 𝑀 ∈ ( 𝑅 PrimRoots 𝐾 ) )
6 zringbas ⊢ ℤ = ( Base ‘ ℤring )
7 eqid ⊢ ( Base ‘ ( ( 𝑅 ↾s 𝑈 ) ↾s ran 𝐹 ) ) = ( Base ‘ ( ( 𝑅 ↾s 𝑈 ) ↾s ran 𝐹 ) )
8 zringplusg ⊢ + = ( +g ‘ ℤring )
9 zex ⊢ ℤ ∈ V
10 9 mptex ⊢ ( 𝑥 ∈ ℤ ↦ ( 𝑥 ( .g ‘ ( 𝑅 ↾s 𝑈 ) ) 𝑀 ) ) ∈ V
11 4 10 eqeltri ⊢ 𝐹 ∈ V
12 11 rnex ⊢ ran 𝐹 ∈ V
13 eqid ⊢ ( ( 𝑅 ↾s 𝑈 ) ↾s ran 𝐹 ) = ( ( 𝑅 ↾s 𝑈 ) ↾s ran 𝐹 )
14 eqid ⊢ ( +g ‘ ( 𝑅 ↾s 𝑈 ) ) = ( +g ‘ ( 𝑅 ↾s 𝑈 ) )
15 13 14 ressplusg ⊢ ( ran 𝐹 ∈ V → ( +g ‘ ( 𝑅 ↾s 𝑈 ) ) = ( +g ‘ ( ( 𝑅 ↾s 𝑈 ) ↾s ran 𝐹 ) ) )
16 12 15 ax-mp ⊢ ( +g ‘ ( 𝑅 ↾s 𝑈 ) ) = ( +g ‘ ( ( 𝑅 ↾s 𝑈 ) ↾s ran 𝐹 ) )
17 zringring ⊢ ℤring ∈ Ring
18 17 a1i ⊢ ( 𝜑 → ℤring ∈ Ring )
19 ringgrp ⊢ ( ℤring ∈ Ring → ℤring ∈ Grp )
20 18 19 syl ⊢ ( 𝜑 → ℤring ∈ Grp )
21 1 2 3 4 5 aks6d1c6isolem1 ⊢ ( 𝜑 → ( ( 𝑅 ↾s 𝑈 ) ↾s ran 𝐹 ) ∈ Grp )
22 ovexd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℤ ) → ( 𝑥 ( .g ‘ ( 𝑅 ↾s 𝑈 ) ) 𝑀 ) ∈ V )
23 22 4 fmptd ⊢ ( 𝜑 → 𝐹 : ℤ ⟶ V )
24 ffn ⊢ ( 𝐹 : ℤ ⟶ V → 𝐹 Fn ℤ )
25 23 24 syl ⊢ ( 𝜑 → 𝐹 Fn ℤ )
26 dffn3 ⊢ ( 𝐹 Fn ℤ ↔ 𝐹 : ℤ ⟶ ran 𝐹 )
27 25 26 sylib ⊢ ( 𝜑 → 𝐹 : ℤ ⟶ ran 𝐹 )
28 fvelrnb ⊢ ( 𝐹 Fn ℤ → ( 𝑤 ∈ ran 𝐹 ↔ ∃ 𝑣 ∈ ℤ ( 𝐹 ‘ 𝑣 ) = 𝑤 ) )
29 25 28 syl ⊢ ( 𝜑 → ( 𝑤 ∈ ran 𝐹 ↔ ∃ 𝑣 ∈ ℤ ( 𝐹 ‘ 𝑣 ) = 𝑤 ) )
30 29 biimpd ⊢ ( 𝜑 → ( 𝑤 ∈ ran 𝐹 → ∃ 𝑣 ∈ ℤ ( 𝐹 ‘ 𝑣 ) = 𝑤 ) )
31 30 imp ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ran 𝐹 ) → ∃ 𝑣 ∈ ℤ ( 𝐹 ‘ 𝑣 ) = 𝑤 )
32 simpr ⊢ ( ( ( ( 𝜑 ∧ ∃ 𝑣 ∈ ℤ ( 𝐹 ‘ 𝑣 ) = 𝑤 ) ∧ 𝑧 ∈ ℤ ) ∧ ( 𝐹 ‘ 𝑧 ) = 𝑤 ) → ( 𝐹 ‘ 𝑧 ) = 𝑤 )
33 32 eqcomd ⊢ ( ( ( ( 𝜑 ∧ ∃ 𝑣 ∈ ℤ ( 𝐹 ‘ 𝑣 ) = 𝑤 ) ∧ 𝑧 ∈ ℤ ) ∧ ( 𝐹 ‘ 𝑧 ) = 𝑤 ) → 𝑤 = ( 𝐹 ‘ 𝑧 ) )
34 simplll ⊢ ( ( ( ( 𝜑 ∧ ∃ 𝑣 ∈ ℤ ( 𝐹 ‘ 𝑣 ) = 𝑤 ) ∧ 𝑧 ∈ ℤ ) ∧ ( 𝐹 ‘ 𝑧 ) = 𝑤 ) → 𝜑 )
35 simplr ⊢ ( ( ( ( 𝜑 ∧ ∃ 𝑣 ∈ ℤ ( 𝐹 ‘ 𝑣 ) = 𝑤 ) ∧ 𝑧 ∈ ℤ ) ∧ ( 𝐹 ‘ 𝑧 ) = 𝑤 ) → 𝑧 ∈ ℤ )
36 34 35 jca ⊢ ( ( ( ( 𝜑 ∧ ∃ 𝑣 ∈ ℤ ( 𝐹 ‘ 𝑣 ) = 𝑤 ) ∧ 𝑧 ∈ ℤ ) ∧ ( 𝐹 ‘ 𝑧 ) = 𝑤 ) → ( 𝜑 ∧ 𝑧 ∈ ℤ ) )
37 4 a1i ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℤ ) → 𝐹 = ( 𝑥 ∈ ℤ ↦ ( 𝑥 ( .g ‘ ( 𝑅 ↾s 𝑈 ) ) 𝑀 ) ) )
38 simpr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℤ ) ∧ 𝑥 = 𝑧 ) → 𝑥 = 𝑧 )
39 38 oveq1d ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℤ ) ∧ 𝑥 = 𝑧 ) → ( 𝑥 ( .g ‘ ( 𝑅 ↾s 𝑈 ) ) 𝑀 ) = ( 𝑧 ( .g ‘ ( 𝑅 ↾s 𝑈 ) ) 𝑀 ) )
40 simpr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℤ ) → 𝑧 ∈ ℤ )
41 ovexd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℤ ) → ( 𝑧 ( .g ‘ ( 𝑅 ↾s 𝑈 ) ) 𝑀 ) ∈ V )
42 37 39 40 41 fvmptd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℤ ) → ( 𝐹 ‘ 𝑧 ) = ( 𝑧 ( .g ‘ ( 𝑅 ↾s 𝑈 ) ) 𝑀 ) )
43 eqid ⊢ ( Base ‘ ( 𝑅 ↾s 𝑈 ) ) = ( Base ‘ ( 𝑅 ↾s 𝑈 ) )
44 eqid ⊢ ( .g ‘ ( 𝑅 ↾s 𝑈 ) ) = ( .g ‘ ( 𝑅 ↾s 𝑈 ) )
45 1 2 3 primrootsunit ⊢ ( 𝜑 → ( ( 𝑅 PrimRoots 𝐾 ) = ( ( 𝑅 ↾s 𝑈 ) PrimRoots 𝐾 ) ∧ ( 𝑅 ↾s 𝑈 ) ∈ Abel ) )
46 45 simprd ⊢ ( 𝜑 → ( 𝑅 ↾s 𝑈 ) ∈ Abel )
47 46 ablgrpd ⊢ ( 𝜑 → ( 𝑅 ↾s 𝑈 ) ∈ Grp )
48 47 adantr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℤ ) → ( 𝑅 ↾s 𝑈 ) ∈ Grp )
49 45 simpld ⊢ ( 𝜑 → ( 𝑅 PrimRoots 𝐾 ) = ( ( 𝑅 ↾s 𝑈 ) PrimRoots 𝐾 ) )
50 5 49 eleqtrd ⊢ ( 𝜑 → 𝑀 ∈ ( ( 𝑅 ↾s 𝑈 ) PrimRoots 𝐾 ) )
51 46 ablcmnd ⊢ ( 𝜑 → ( 𝑅 ↾s 𝑈 ) ∈ CMnd )
52 2 nnnn0d ⊢ ( 𝜑 → 𝐾 ∈ ℕ0 )
53 51 52 44 isprimroot ⊢ ( 𝜑 → ( 𝑀 ∈ ( ( 𝑅 ↾s 𝑈 ) PrimRoots 𝐾 ) ↔ ( 𝑀 ∈ ( Base ‘ ( 𝑅 ↾s 𝑈 ) ) ∧ ( 𝐾 ( .g ‘ ( 𝑅 ↾s 𝑈 ) ) 𝑀 ) = ( 0g ‘ ( 𝑅 ↾s 𝑈 ) ) ∧ ∀ 𝑙 ∈ ℕ0 ( ( 𝑙 ( .g ‘ ( 𝑅 ↾s 𝑈 ) ) 𝑀 ) = ( 0g ‘ ( 𝑅 ↾s 𝑈 ) ) → 𝐾 ∥ 𝑙 ) ) ) )
54 53 biimpd ⊢ ( 𝜑 → ( 𝑀 ∈ ( ( 𝑅 ↾s 𝑈 ) PrimRoots 𝐾 ) → ( 𝑀 ∈ ( Base ‘ ( 𝑅 ↾s 𝑈 ) ) ∧ ( 𝐾 ( .g ‘ ( 𝑅 ↾s 𝑈 ) ) 𝑀 ) = ( 0g ‘ ( 𝑅 ↾s 𝑈 ) ) ∧ ∀ 𝑙 ∈ ℕ0 ( ( 𝑙 ( .g ‘ ( 𝑅 ↾s 𝑈 ) ) 𝑀 ) = ( 0g ‘ ( 𝑅 ↾s 𝑈 ) ) → 𝐾 ∥ 𝑙 ) ) ) )
55 50 54 mpd ⊢ ( 𝜑 → ( 𝑀 ∈ ( Base ‘ ( 𝑅 ↾s 𝑈 ) ) ∧ ( 𝐾 ( .g ‘ ( 𝑅 ↾s 𝑈 ) ) 𝑀 ) = ( 0g ‘ ( 𝑅 ↾s 𝑈 ) ) ∧ ∀ 𝑙 ∈ ℕ0 ( ( 𝑙 ( .g ‘ ( 𝑅 ↾s 𝑈 ) ) 𝑀 ) = ( 0g ‘ ( 𝑅 ↾s 𝑈 ) ) → 𝐾 ∥ 𝑙 ) ) )
56 55 simp1d ⊢ ( 𝜑 → 𝑀 ∈ ( Base ‘ ( 𝑅 ↾s 𝑈 ) ) )
57 56 adantr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℤ ) → 𝑀 ∈ ( Base ‘ ( 𝑅 ↾s 𝑈 ) ) )
58 43 44 48 40 57 mulgcld ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℤ ) → ( 𝑧 ( .g ‘ ( 𝑅 ↾s 𝑈 ) ) 𝑀 ) ∈ ( Base ‘ ( 𝑅 ↾s 𝑈 ) ) )
59 42 58 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℤ ) → ( 𝐹 ‘ 𝑧 ) ∈ ( Base ‘ ( 𝑅 ↾s 𝑈 ) ) )
60 36 59 syl ⊢ ( ( ( ( 𝜑 ∧ ∃ 𝑣 ∈ ℤ ( 𝐹 ‘ 𝑣 ) = 𝑤 ) ∧ 𝑧 ∈ ℤ ) ∧ ( 𝐹 ‘ 𝑧 ) = 𝑤 ) → ( 𝐹 ‘ 𝑧 ) ∈ ( Base ‘ ( 𝑅 ↾s 𝑈 ) ) )
61 33 60 eqeltrd ⊢ ( ( ( ( 𝜑 ∧ ∃ 𝑣 ∈ ℤ ( 𝐹 ‘ 𝑣 ) = 𝑤 ) ∧ 𝑧 ∈ ℤ ) ∧ ( 𝐹 ‘ 𝑧 ) = 𝑤 ) → 𝑤 ∈ ( Base ‘ ( 𝑅 ↾s 𝑈 ) ) )
62 nfv ⊢ Ⅎ 𝑧 ( 𝐹 ‘ 𝑣 ) = 𝑤
63 nfv ⊢ Ⅎ 𝑣 ( 𝐹 ‘ 𝑧 ) = 𝑤
64 fveqeq2 ⊢ ( 𝑣 = 𝑧 → ( ( 𝐹 ‘ 𝑣 ) = 𝑤 ↔ ( 𝐹 ‘ 𝑧 ) = 𝑤 ) )
65 62 63 64 cbvrexw ⊢ ( ∃ 𝑣 ∈ ℤ ( 𝐹 ‘ 𝑣 ) = 𝑤 ↔ ∃ 𝑧 ∈ ℤ ( 𝐹 ‘ 𝑧 ) = 𝑤 )
66 65 biimpi ⊢ ( ∃ 𝑣 ∈ ℤ ( 𝐹 ‘ 𝑣 ) = 𝑤 → ∃ 𝑧 ∈ ℤ ( 𝐹 ‘ 𝑧 ) = 𝑤 )
67 66 adantl ⊢ ( ( 𝜑 ∧ ∃ 𝑣 ∈ ℤ ( 𝐹 ‘ 𝑣 ) = 𝑤 ) → ∃ 𝑧 ∈ ℤ ( 𝐹 ‘ 𝑧 ) = 𝑤 )
68 61 67 r19.29a ⊢ ( ( 𝜑 ∧ ∃ 𝑣 ∈ ℤ ( 𝐹 ‘ 𝑣 ) = 𝑤 ) → 𝑤 ∈ ( Base ‘ ( 𝑅 ↾s 𝑈 ) ) )
69 68 ex ⊢ ( 𝜑 → ( ∃ 𝑣 ∈ ℤ ( 𝐹 ‘ 𝑣 ) = 𝑤 → 𝑤 ∈ ( Base ‘ ( 𝑅 ↾s 𝑈 ) ) ) )
70 69 adantr ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ran 𝐹 ) → ( ∃ 𝑣 ∈ ℤ ( 𝐹 ‘ 𝑣 ) = 𝑤 → 𝑤 ∈ ( Base ‘ ( 𝑅 ↾s 𝑈 ) ) ) )
71 70 imp ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ran 𝐹 ) ∧ ∃ 𝑣 ∈ ℤ ( 𝐹 ‘ 𝑣 ) = 𝑤 ) → 𝑤 ∈ ( Base ‘ ( 𝑅 ↾s 𝑈 ) ) )
72 31 71 mpdan ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ran 𝐹 ) → 𝑤 ∈ ( Base ‘ ( 𝑅 ↾s 𝑈 ) ) )
73 72 ex ⊢ ( 𝜑 → ( 𝑤 ∈ ran 𝐹 → 𝑤 ∈ ( Base ‘ ( 𝑅 ↾s 𝑈 ) ) ) )
74 73 ssrdv ⊢ ( 𝜑 → ran 𝐹 ⊆ ( Base ‘ ( 𝑅 ↾s 𝑈 ) ) )
75 13 43 ressbas2 ⊢ ( ran 𝐹 ⊆ ( Base ‘ ( 𝑅 ↾s 𝑈 ) ) → ran 𝐹 = ( Base ‘ ( ( 𝑅 ↾s 𝑈 ) ↾s ran 𝐹 ) ) )
76 74 75 syl ⊢ ( 𝜑 → ran 𝐹 = ( Base ‘ ( ( 𝑅 ↾s 𝑈 ) ↾s ran 𝐹 ) ) )
77 76 feq3d ⊢ ( 𝜑 → ( 𝐹 : ℤ ⟶ ran 𝐹 ↔ 𝐹 : ℤ ⟶ ( Base ‘ ( ( 𝑅 ↾s 𝑈 ) ↾s ran 𝐹 ) ) ) )
78 27 77 mpbid ⊢ ( 𝜑 → 𝐹 : ℤ ⟶ ( Base ‘ ( ( 𝑅 ↾s 𝑈 ) ↾s ran 𝐹 ) ) )
79 4 a1i ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) → 𝐹 = ( 𝑥 ∈ ℤ ↦ ( 𝑥 ( .g ‘ ( 𝑅 ↾s 𝑈 ) ) 𝑀 ) ) )
80 simpr ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ 𝑥 = ( 𝑦 + 𝑧 ) ) → 𝑥 = ( 𝑦 + 𝑧 ) )
81 80 oveq1d ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ 𝑥 = ( 𝑦 + 𝑧 ) ) → ( 𝑥 ( .g ‘ ( 𝑅 ↾s 𝑈 ) ) 𝑀 ) = ( ( 𝑦 + 𝑧 ) ( .g ‘ ( 𝑅 ↾s 𝑈 ) ) 𝑀 ) )
82 simprl ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) → 𝑦 ∈ ℤ )
83 simprr ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) → 𝑧 ∈ ℤ )
84 82 83 zaddcld ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) → ( 𝑦 + 𝑧 ) ∈ ℤ )
85 ovexd ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) → ( ( 𝑦 + 𝑧 ) ( .g ‘ ( 𝑅 ↾s 𝑈 ) ) 𝑀 ) ∈ V )
86 79 81 84 85 fvmptd ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) → ( 𝐹 ‘ ( 𝑦 + 𝑧 ) ) = ( ( 𝑦 + 𝑧 ) ( .g ‘ ( 𝑅 ↾s 𝑈 ) ) 𝑀 ) )
87 47 adantr ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) → ( 𝑅 ↾s 𝑈 ) ∈ Grp )
88 56 adantr ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) → 𝑀 ∈ ( Base ‘ ( 𝑅 ↾s 𝑈 ) ) )
89 82 83 88 3jca ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) → ( 𝑦 ∈ ℤ ∧ 𝑧 ∈ ℤ ∧ 𝑀 ∈ ( Base ‘ ( 𝑅 ↾s 𝑈 ) ) ) )
90 43 44 14 mulgdir ⊢ ( ( ( 𝑅 ↾s 𝑈 ) ∈ Grp ∧ ( 𝑦 ∈ ℤ ∧ 𝑧 ∈ ℤ ∧ 𝑀 ∈ ( Base ‘ ( 𝑅 ↾s 𝑈 ) ) ) ) → ( ( 𝑦 + 𝑧 ) ( .g ‘ ( 𝑅 ↾s 𝑈 ) ) 𝑀 ) = ( ( 𝑦 ( .g ‘ ( 𝑅 ↾s 𝑈 ) ) 𝑀 ) ( +g ‘ ( 𝑅 ↾s 𝑈 ) ) ( 𝑧 ( .g ‘ ( 𝑅 ↾s 𝑈 ) ) 𝑀 ) ) )
91 87 89 90 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) → ( ( 𝑦 + 𝑧 ) ( .g ‘ ( 𝑅 ↾s 𝑈 ) ) 𝑀 ) = ( ( 𝑦 ( .g ‘ ( 𝑅 ↾s 𝑈 ) ) 𝑀 ) ( +g ‘ ( 𝑅 ↾s 𝑈 ) ) ( 𝑧 ( .g ‘ ( 𝑅 ↾s 𝑈 ) ) 𝑀 ) ) )
92 simpr ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ 𝑥 = 𝑦 ) → 𝑥 = 𝑦 )
93 92 oveq1d ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ 𝑥 = 𝑦 ) → ( 𝑥 ( .g ‘ ( 𝑅 ↾s 𝑈 ) ) 𝑀 ) = ( 𝑦 ( .g ‘ ( 𝑅 ↾s 𝑈 ) ) 𝑀 ) )
94 ovexd ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) → ( 𝑦 ( .g ‘ ( 𝑅 ↾s 𝑈 ) ) 𝑀 ) ∈ V )
95 79 93 82 94 fvmptd ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) → ( 𝐹 ‘ 𝑦 ) = ( 𝑦 ( .g ‘ ( 𝑅 ↾s 𝑈 ) ) 𝑀 ) )
96 simpr ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ 𝑥 = 𝑧 ) → 𝑥 = 𝑧 )
97 96 oveq1d ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) ∧ 𝑥 = 𝑧 ) → ( 𝑥 ( .g ‘ ( 𝑅 ↾s 𝑈 ) ) 𝑀 ) = ( 𝑧 ( .g ‘ ( 𝑅 ↾s 𝑈 ) ) 𝑀 ) )
98 ovexd ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) → ( 𝑧 ( .g ‘ ( 𝑅 ↾s 𝑈 ) ) 𝑀 ) ∈ V )
99 79 97 83 98 fvmptd ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) → ( 𝐹 ‘ 𝑧 ) = ( 𝑧 ( .g ‘ ( 𝑅 ↾s 𝑈 ) ) 𝑀 ) )
100 95 99 oveq12d ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) → ( ( 𝐹 ‘ 𝑦 ) ( +g ‘ ( 𝑅 ↾s 𝑈 ) ) ( 𝐹 ‘ 𝑧 ) ) = ( ( 𝑦 ( .g ‘ ( 𝑅 ↾s 𝑈 ) ) 𝑀 ) ( +g ‘ ( 𝑅 ↾s 𝑈 ) ) ( 𝑧 ( .g ‘ ( 𝑅 ↾s 𝑈 ) ) 𝑀 ) ) )
101 100 eqcomd ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) → ( ( 𝑦 ( .g ‘ ( 𝑅 ↾s 𝑈 ) ) 𝑀 ) ( +g ‘ ( 𝑅 ↾s 𝑈 ) ) ( 𝑧 ( .g ‘ ( 𝑅 ↾s 𝑈 ) ) 𝑀 ) ) = ( ( 𝐹 ‘ 𝑦 ) ( +g ‘ ( 𝑅 ↾s 𝑈 ) ) ( 𝐹 ‘ 𝑧 ) ) )
102 91 101 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) → ( ( 𝑦 + 𝑧 ) ( .g ‘ ( 𝑅 ↾s 𝑈 ) ) 𝑀 ) = ( ( 𝐹 ‘ 𝑦 ) ( +g ‘ ( 𝑅 ↾s 𝑈 ) ) ( 𝐹 ‘ 𝑧 ) ) )
103 86 102 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ℤ ∧ 𝑧 ∈ ℤ ) ) → ( 𝐹 ‘ ( 𝑦 + 𝑧 ) ) = ( ( 𝐹 ‘ 𝑦 ) ( +g ‘ ( 𝑅 ↾s 𝑈 ) ) ( 𝐹 ‘ 𝑧 ) ) )
104 6 7 8 16 20 21 78 103 isghmd ⊢ ( 𝜑 → 𝐹 ∈ ( ℤring GrpHom ( ( 𝑅 ↾s 𝑈 ) ↾s ran 𝐹 ) ) )