Metamath Proof Explorer

Theorem aks6d1c6isolem1

Description: Lemma to construct the map out of the quotient for AKS. (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 aks6d1c6isolem1 ( 𝜑 → ( ( 𝑅 ↾s 𝑈 ) ↾s ran 𝐹 ) ∈ Grp )

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 eqidd ⊢ ( 𝜑 → ( ( 𝑅 ↾s 𝑈 ) ↾s ran 𝐹 ) = ( ( 𝑅 ↾s 𝑈 ) ↾s ran 𝐹 ) )
7 eqidd ⊢ ( 𝜑 → ( 0g ‘ ( 𝑅 ↾s 𝑈 ) ) = ( 0g ‘ ( 𝑅 ↾s 𝑈 ) ) )
8 eqidd ⊢ ( 𝜑 → ( +g ‘ ( 𝑅 ↾s 𝑈 ) ) = ( +g ‘ ( 𝑅 ↾s 𝑈 ) ) )
9 eqid ⊢ ( Base ‘ ( 𝑅 ↾s 𝑈 ) ) = ( Base ‘ ( 𝑅 ↾s 𝑈 ) )
10 eqid ⊢ ( .g ‘ ( 𝑅 ↾s 𝑈 ) ) = ( .g ‘ ( 𝑅 ↾s 𝑈 ) )
11 1 2 3 primrootsunit ⊢ ( 𝜑 → ( ( 𝑅 PrimRoots 𝐾 ) = ( ( 𝑅 ↾s 𝑈 ) PrimRoots 𝐾 ) ∧ ( 𝑅 ↾s 𝑈 ) ∈ Abel ) )
12 11 simprd ⊢ ( 𝜑 → ( 𝑅 ↾s 𝑈 ) ∈ Abel )
13 12 ablgrpd ⊢ ( 𝜑 → ( 𝑅 ↾s 𝑈 ) ∈ Grp )
14 13 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℤ ) → ( 𝑅 ↾s 𝑈 ) ∈ Grp )
15 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℤ ) → 𝑥 ∈ ℤ )
16 11 simpld ⊢ ( 𝜑 → ( 𝑅 PrimRoots 𝐾 ) = ( ( 𝑅 ↾s 𝑈 ) PrimRoots 𝐾 ) )
17 5 16 eleqtrd ⊢ ( 𝜑 → 𝑀 ∈ ( ( 𝑅 ↾s 𝑈 ) PrimRoots 𝐾 ) )
18 12 ablcmnd ⊢ ( 𝜑 → ( 𝑅 ↾s 𝑈 ) ∈ CMnd )
19 2 nnnn0d ⊢ ( 𝜑 → 𝐾 ∈ ℕ0 )
20 18 19 10 isprimroot ⊢ ( 𝜑 → ( 𝑀 ∈ ( ( 𝑅 ↾s 𝑈 ) PrimRoots 𝐾 ) ↔ ( 𝑀 ∈ ( Base ‘ ( 𝑅 ↾s 𝑈 ) ) ∧ ( 𝐾 ( .g ‘ ( 𝑅 ↾s 𝑈 ) ) 𝑀 ) = ( 0g ‘ ( 𝑅 ↾s 𝑈 ) ) ∧ ∀ 𝑙 ∈ ℕ0 ( ( 𝑙 ( .g ‘ ( 𝑅 ↾s 𝑈 ) ) 𝑀 ) = ( 0g ‘ ( 𝑅 ↾s 𝑈 ) ) → 𝐾 ∥ 𝑙 ) ) ) )
21 20 biimpd ⊢ ( 𝜑 → ( 𝑀 ∈ ( ( 𝑅 ↾s 𝑈 ) PrimRoots 𝐾 ) → ( 𝑀 ∈ ( Base ‘ ( 𝑅 ↾s 𝑈 ) ) ∧ ( 𝐾 ( .g ‘ ( 𝑅 ↾s 𝑈 ) ) 𝑀 ) = ( 0g ‘ ( 𝑅 ↾s 𝑈 ) ) ∧ ∀ 𝑙 ∈ ℕ0 ( ( 𝑙 ( .g ‘ ( 𝑅 ↾s 𝑈 ) ) 𝑀 ) = ( 0g ‘ ( 𝑅 ↾s 𝑈 ) ) → 𝐾 ∥ 𝑙 ) ) ) )
22 17 21 mpd ⊢ ( 𝜑 → ( 𝑀 ∈ ( Base ‘ ( 𝑅 ↾s 𝑈 ) ) ∧ ( 𝐾 ( .g ‘ ( 𝑅 ↾s 𝑈 ) ) 𝑀 ) = ( 0g ‘ ( 𝑅 ↾s 𝑈 ) ) ∧ ∀ 𝑙 ∈ ℕ0 ( ( 𝑙 ( .g ‘ ( 𝑅 ↾s 𝑈 ) ) 𝑀 ) = ( 0g ‘ ( 𝑅 ↾s 𝑈 ) ) → 𝐾 ∥ 𝑙 ) ) )
23 22 simp1d ⊢ ( 𝜑 → 𝑀 ∈ ( Base ‘ ( 𝑅 ↾s 𝑈 ) ) )
24 23 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℤ ) → 𝑀 ∈ ( Base ‘ ( 𝑅 ↾s 𝑈 ) ) )
25 9 10 14 15 24 mulgcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℤ ) → ( 𝑥 ( .g ‘ ( 𝑅 ↾s 𝑈 ) ) 𝑀 ) ∈ ( Base ‘ ( 𝑅 ↾s 𝑈 ) ) )
26 25 4 fmptd ⊢ ( 𝜑 → 𝐹 : ℤ ⟶ ( Base ‘ ( 𝑅 ↾s 𝑈 ) ) )
27 frn ⊢ ( 𝐹 : ℤ ⟶ ( Base ‘ ( 𝑅 ↾s 𝑈 ) ) → ran 𝐹 ⊆ ( Base ‘ ( 𝑅 ↾s 𝑈 ) ) )
28 26 27 syl ⊢ ( 𝜑 → ran 𝐹 ⊆ ( Base ‘ ( 𝑅 ↾s 𝑈 ) ) )
29 0zd ⊢ ( 𝜑 → 0 ∈ ℤ )
30 simpr ⊢ ( ( 𝜑 ∧ 𝑐 = 0 ) → 𝑐 = 0 )
31 30 fveqeq2d ⊢ ( ( 𝜑 ∧ 𝑐 = 0 ) → ( ( 𝐹 ‘ 𝑐 ) = ( 0g ‘ ( 𝑅 ↾s 𝑈 ) ) ↔ ( 𝐹 ‘ 0 ) = ( 0g ‘ ( 𝑅 ↾s 𝑈 ) ) ) )
32 4 a1i ⊢ ( 𝜑 → 𝐹 = ( 𝑥 ∈ ℤ ↦ ( 𝑥 ( .g ‘ ( 𝑅 ↾s 𝑈 ) ) 𝑀 ) ) )
33 simpr ⊢ ( ( 𝜑 ∧ 𝑥 = 0 ) → 𝑥 = 0 )
34 33 oveq1d ⊢ ( ( 𝜑 ∧ 𝑥 = 0 ) → ( 𝑥 ( .g ‘ ( 𝑅 ↾s 𝑈 ) ) 𝑀 ) = ( 0 ( .g ‘ ( 𝑅 ↾s 𝑈 ) ) 𝑀 ) )
35 eqid ⊢ ( 0g ‘ ( 𝑅 ↾s 𝑈 ) ) = ( 0g ‘ ( 𝑅 ↾s 𝑈 ) )
36 9 35 10 mulg0 ⊢ ( 𝑀 ∈ ( Base ‘ ( 𝑅 ↾s 𝑈 ) ) → ( 0 ( .g ‘ ( 𝑅 ↾s 𝑈 ) ) 𝑀 ) = ( 0g ‘ ( 𝑅 ↾s 𝑈 ) ) )
37 23 36 syl ⊢ ( 𝜑 → ( 0 ( .g ‘ ( 𝑅 ↾s 𝑈 ) ) 𝑀 ) = ( 0g ‘ ( 𝑅 ↾s 𝑈 ) ) )
38 37 adantr ⊢ ( ( 𝜑 ∧ 𝑥 = 0 ) → ( 0 ( .g ‘ ( 𝑅 ↾s 𝑈 ) ) 𝑀 ) = ( 0g ‘ ( 𝑅 ↾s 𝑈 ) ) )
39 34 38 eqtrd ⊢ ( ( 𝜑 ∧ 𝑥 = 0 ) → ( 𝑥 ( .g ‘ ( 𝑅 ↾s 𝑈 ) ) 𝑀 ) = ( 0g ‘ ( 𝑅 ↾s 𝑈 ) ) )
40 fvexd ⊢ ( 𝜑 → ( 0g ‘ ( 𝑅 ↾s 𝑈 ) ) ∈ V )
41 32 39 29 40 fvmptd ⊢ ( 𝜑 → ( 𝐹 ‘ 0 ) = ( 0g ‘ ( 𝑅 ↾s 𝑈 ) ) )
42 29 31 41 rspcedvd ⊢ ( 𝜑 → ∃ 𝑐 ∈ ℤ ( 𝐹 ‘ 𝑐 ) = ( 0g ‘ ( 𝑅 ↾s 𝑈 ) ) )
43 26 ffnd ⊢ ( 𝜑 → 𝐹 Fn ℤ )
44 fvelrnb ⊢ ( 𝐹 Fn ℤ → ( ( 0g ‘ ( 𝑅 ↾s 𝑈 ) ) ∈ ran 𝐹 ↔ ∃ 𝑐 ∈ ℤ ( 𝐹 ‘ 𝑐 ) = ( 0g ‘ ( 𝑅 ↾s 𝑈 ) ) ) )
45 43 44 syl ⊢ ( 𝜑 → ( ( 0g ‘ ( 𝑅 ↾s 𝑈 ) ) ∈ ran 𝐹 ↔ ∃ 𝑐 ∈ ℤ ( 𝐹 ‘ 𝑐 ) = ( 0g ‘ ( 𝑅 ↾s 𝑈 ) ) ) )
46 42 45 mpbird ⊢ ( 𝜑 → ( 0g ‘ ( 𝑅 ↾s 𝑈 ) ) ∈ ran 𝐹 )
47 fvelrnb ⊢ ( 𝐹 Fn ℤ → ( 𝑦 ∈ ran 𝐹 ↔ ∃ 𝑑 ∈ ℤ ( 𝐹 ‘ 𝑑 ) = 𝑦 ) )
48 43 47 syl ⊢ ( 𝜑 → ( 𝑦 ∈ ran 𝐹 ↔ ∃ 𝑑 ∈ ℤ ( 𝐹 ‘ 𝑑 ) = 𝑦 ) )
49 48 biimpd ⊢ ( 𝜑 → ( 𝑦 ∈ ran 𝐹 → ∃ 𝑑 ∈ ℤ ( 𝐹 ‘ 𝑑 ) = 𝑦 ) )
50 49 imp ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ran 𝐹 ) → ∃ 𝑑 ∈ ℤ ( 𝐹 ‘ 𝑑 ) = 𝑦 )
51 50 3adant3 ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ran 𝐹 ∧ 𝑧 ∈ ran 𝐹 ) → ∃ 𝑑 ∈ ℤ ( 𝐹 ‘ 𝑑 ) = 𝑦 )
52 simpl1 ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ran 𝐹 ∧ 𝑧 ∈ ran 𝐹 ) ∧ ∃ 𝑑 ∈ ℤ ( 𝐹 ‘ 𝑑 ) = 𝑦 ) → 𝜑 )
53 simpl3 ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ran 𝐹 ∧ 𝑧 ∈ ran 𝐹 ) ∧ ∃ 𝑑 ∈ ℤ ( 𝐹 ‘ 𝑑 ) = 𝑦 ) → 𝑧 ∈ ran 𝐹 )
54 52 53 jca ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ran 𝐹 ∧ 𝑧 ∈ ran 𝐹 ) ∧ ∃ 𝑑 ∈ ℤ ( 𝐹 ‘ 𝑑 ) = 𝑦 ) → ( 𝜑 ∧ 𝑧 ∈ ran 𝐹 ) )
55 fvelrnb ⊢ ( 𝐹 Fn ℤ → ( 𝑧 ∈ ran 𝐹 ↔ ∃ 𝑒 ∈ ℤ ( 𝐹 ‘ 𝑒 ) = 𝑧 ) )
56 43 55 syl ⊢ ( 𝜑 → ( 𝑧 ∈ ran 𝐹 ↔ ∃ 𝑒 ∈ ℤ ( 𝐹 ‘ 𝑒 ) = 𝑧 ) )
57 56 biimpd ⊢ ( 𝜑 → ( 𝑧 ∈ ran 𝐹 → ∃ 𝑒 ∈ ℤ ( 𝐹 ‘ 𝑒 ) = 𝑧 ) )
58 57 imp ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ran 𝐹 ) → ∃ 𝑒 ∈ ℤ ( 𝐹 ‘ 𝑒 ) = 𝑧 )
59 54 58 syl ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ran 𝐹 ∧ 𝑧 ∈ ran 𝐹 ) ∧ ∃ 𝑑 ∈ ℤ ( 𝐹 ‘ 𝑑 ) = 𝑦 ) → ∃ 𝑒 ∈ ℤ ( 𝐹 ‘ 𝑒 ) = 𝑧 )
60 simpll1 ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ran 𝐹 ∧ 𝑧 ∈ ran 𝐹 ) ∧ ∃ 𝑑 ∈ ℤ ( 𝐹 ‘ 𝑑 ) = 𝑦 ) ∧ ∃ 𝑒 ∈ ℤ ( 𝐹 ‘ 𝑒 ) = 𝑧 ) → 𝜑 )
61 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ran 𝐹 ∧ 𝑧 ∈ ran 𝐹 ) ∧ ∃ 𝑑 ∈ ℤ ( 𝐹 ‘ 𝑑 ) = 𝑦 ) ∧ ∃ 𝑒 ∈ ℤ ( 𝐹 ‘ 𝑒 ) = 𝑧 ) → ∃ 𝑑 ∈ ℤ ( 𝐹 ‘ 𝑑 ) = 𝑦 )
62 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ran 𝐹 ∧ 𝑧 ∈ ran 𝐹 ) ∧ ∃ 𝑑 ∈ ℤ ( 𝐹 ‘ 𝑑 ) = 𝑦 ) ∧ ∃ 𝑒 ∈ ℤ ( 𝐹 ‘ 𝑒 ) = 𝑧 ) → ∃ 𝑒 ∈ ℤ ( 𝐹 ‘ 𝑒 ) = 𝑧 )
63 60 61 62 3jca ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ran 𝐹 ∧ 𝑧 ∈ ran 𝐹 ) ∧ ∃ 𝑑 ∈ ℤ ( 𝐹 ‘ 𝑑 ) = 𝑦 ) ∧ ∃ 𝑒 ∈ ℤ ( 𝐹 ‘ 𝑒 ) = 𝑧 ) → ( 𝜑 ∧ ∃ 𝑑 ∈ ℤ ( 𝐹 ‘ 𝑑 ) = 𝑦 ∧ ∃ 𝑒 ∈ ℤ ( 𝐹 ‘ 𝑒 ) = 𝑧 ) )
64 simpr ⊢ ( ( ( ( 𝜑 ∧ ∃ 𝑑 ∈ ℤ ( 𝐹 ‘ 𝑑 ) = 𝑦 ∧ ∃ 𝑒 ∈ ℤ ( 𝐹 ‘ 𝑒 ) = 𝑧 ) ∧ 𝑔 ∈ ℤ ) ∧ ( 𝐹 ‘ 𝑔 ) = 𝑧 ) → ( 𝐹 ‘ 𝑔 ) = 𝑧 )
65 64 eqcomd ⊢ ( ( ( ( 𝜑 ∧ ∃ 𝑑 ∈ ℤ ( 𝐹 ‘ 𝑑 ) = 𝑦 ∧ ∃ 𝑒 ∈ ℤ ( 𝐹 ‘ 𝑒 ) = 𝑧 ) ∧ 𝑔 ∈ ℤ ) ∧ ( 𝐹 ‘ 𝑔 ) = 𝑧 ) → 𝑧 = ( 𝐹 ‘ 𝑔 ) )
66 65 oveq2d ⊢ ( ( ( ( 𝜑 ∧ ∃ 𝑑 ∈ ℤ ( 𝐹 ‘ 𝑑 ) = 𝑦 ∧ ∃ 𝑒 ∈ ℤ ( 𝐹 ‘ 𝑒 ) = 𝑧 ) ∧ 𝑔 ∈ ℤ ) ∧ ( 𝐹 ‘ 𝑔 ) = 𝑧 ) → ( 𝑦 ( +g ‘ ( 𝑅 ↾s 𝑈 ) ) 𝑧 ) = ( 𝑦 ( +g ‘ ( 𝑅 ↾s 𝑈 ) ) ( 𝐹 ‘ 𝑔 ) ) )
67 simpr ⊢ ( ( ( ( ( 𝜑 ∧ ∃ 𝑑 ∈ ℤ ( 𝐹 ‘ 𝑑 ) = 𝑦 ∧ ∃ 𝑒 ∈ ℤ ( 𝐹 ‘ 𝑒 ) = 𝑧 ) ∧ 𝑔 ∈ ℤ ) ∧ 𝑓 ∈ ℤ ) ∧ ( 𝐹 ‘ 𝑓 ) = 𝑦 ) → ( 𝐹 ‘ 𝑓 ) = 𝑦 )
68 67 eqcomd ⊢ ( ( ( ( ( 𝜑 ∧ ∃ 𝑑 ∈ ℤ ( 𝐹 ‘ 𝑑 ) = 𝑦 ∧ ∃ 𝑒 ∈ ℤ ( 𝐹 ‘ 𝑒 ) = 𝑧 ) ∧ 𝑔 ∈ ℤ ) ∧ 𝑓 ∈ ℤ ) ∧ ( 𝐹 ‘ 𝑓 ) = 𝑦 ) → 𝑦 = ( 𝐹 ‘ 𝑓 ) )
69 68 oveq1d ⊢ ( ( ( ( ( 𝜑 ∧ ∃ 𝑑 ∈ ℤ ( 𝐹 ‘ 𝑑 ) = 𝑦 ∧ ∃ 𝑒 ∈ ℤ ( 𝐹 ‘ 𝑒 ) = 𝑧 ) ∧ 𝑔 ∈ ℤ ) ∧ 𝑓 ∈ ℤ ) ∧ ( 𝐹 ‘ 𝑓 ) = 𝑦 ) → ( 𝑦 ( +g ‘ ( 𝑅 ↾s 𝑈 ) ) ( 𝐹 ‘ 𝑔 ) ) = ( ( 𝐹 ‘ 𝑓 ) ( +g ‘ ( 𝑅 ↾s 𝑈 ) ) ( 𝐹 ‘ 𝑔 ) ) )
70 simpll1 ⊢ ( ( ( ( 𝜑 ∧ ∃ 𝑑 ∈ ℤ ( 𝐹 ‘ 𝑑 ) = 𝑦 ∧ ∃ 𝑒 ∈ ℤ ( 𝐹 ‘ 𝑒 ) = 𝑧 ) ∧ 𝑔 ∈ ℤ ) ∧ 𝑓 ∈ ℤ ) → 𝜑 )
71 70 adantr ⊢ ( ( ( ( ( 𝜑 ∧ ∃ 𝑑 ∈ ℤ ( 𝐹 ‘ 𝑑 ) = 𝑦 ∧ ∃ 𝑒 ∈ ℤ ( 𝐹 ‘ 𝑒 ) = 𝑧 ) ∧ 𝑔 ∈ ℤ ) ∧ 𝑓 ∈ ℤ ) ∧ ( 𝐹 ‘ 𝑓 ) = 𝑦 ) → 𝜑 )
72 simpllr ⊢ ( ( ( ( ( 𝜑 ∧ ∃ 𝑑 ∈ ℤ ( 𝐹 ‘ 𝑑 ) = 𝑦 ∧ ∃ 𝑒 ∈ ℤ ( 𝐹 ‘ 𝑒 ) = 𝑧 ) ∧ 𝑔 ∈ ℤ ) ∧ 𝑓 ∈ ℤ ) ∧ ( 𝐹 ‘ 𝑓 ) = 𝑦 ) → 𝑔 ∈ ℤ )
73 simplr ⊢ ( ( ( ( ( 𝜑 ∧ ∃ 𝑑 ∈ ℤ ( 𝐹 ‘ 𝑑 ) = 𝑦 ∧ ∃ 𝑒 ∈ ℤ ( 𝐹 ‘ 𝑒 ) = 𝑧 ) ∧ 𝑔 ∈ ℤ ) ∧ 𝑓 ∈ ℤ ) ∧ ( 𝐹 ‘ 𝑓 ) = 𝑦 ) → 𝑓 ∈ ℤ )
74 71 72 73 3jca ⊢ ( ( ( ( ( 𝜑 ∧ ∃ 𝑑 ∈ ℤ ( 𝐹 ‘ 𝑑 ) = 𝑦 ∧ ∃ 𝑒 ∈ ℤ ( 𝐹 ‘ 𝑒 ) = 𝑧 ) ∧ 𝑔 ∈ ℤ ) ∧ 𝑓 ∈ ℤ ) ∧ ( 𝐹 ‘ 𝑓 ) = 𝑦 ) → ( 𝜑 ∧ 𝑔 ∈ ℤ ∧ 𝑓 ∈ ℤ ) )
75 4 a1i ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ℤ ∧ 𝑓 ∈ ℤ ) → 𝐹 = ( 𝑥 ∈ ℤ ↦ ( 𝑥 ( .g ‘ ( 𝑅 ↾s 𝑈 ) ) 𝑀 ) ) )
76 simpr ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ ℤ ∧ 𝑓 ∈ ℤ ) ∧ 𝑥 = 𝑓 ) → 𝑥 = 𝑓 )
77 76 oveq1d ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ ℤ ∧ 𝑓 ∈ ℤ ) ∧ 𝑥 = 𝑓 ) → ( 𝑥 ( .g ‘ ( 𝑅 ↾s 𝑈 ) ) 𝑀 ) = ( 𝑓 ( .g ‘ ( 𝑅 ↾s 𝑈 ) ) 𝑀 ) )
78 simp3 ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ℤ ∧ 𝑓 ∈ ℤ ) → 𝑓 ∈ ℤ )
79 ovexd ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ℤ ∧ 𝑓 ∈ ℤ ) → ( 𝑓 ( .g ‘ ( 𝑅 ↾s 𝑈 ) ) 𝑀 ) ∈ V )
80 75 77 78 79 fvmptd ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ℤ ∧ 𝑓 ∈ ℤ ) → ( 𝐹 ‘ 𝑓 ) = ( 𝑓 ( .g ‘ ( 𝑅 ↾s 𝑈 ) ) 𝑀 ) )
81 simpr ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ ℤ ∧ 𝑓 ∈ ℤ ) ∧ 𝑥 = 𝑔 ) → 𝑥 = 𝑔 )
82 81 oveq1d ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ ℤ ∧ 𝑓 ∈ ℤ ) ∧ 𝑥 = 𝑔 ) → ( 𝑥 ( .g ‘ ( 𝑅 ↾s 𝑈 ) ) 𝑀 ) = ( 𝑔 ( .g ‘ ( 𝑅 ↾s 𝑈 ) ) 𝑀 ) )
83 simp2 ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ℤ ∧ 𝑓 ∈ ℤ ) → 𝑔 ∈ ℤ )
84 ovexd ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ℤ ∧ 𝑓 ∈ ℤ ) → ( 𝑔 ( .g ‘ ( 𝑅 ↾s 𝑈 ) ) 𝑀 ) ∈ V )
85 75 82 83 84 fvmptd ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ℤ ∧ 𝑓 ∈ ℤ ) → ( 𝐹 ‘ 𝑔 ) = ( 𝑔 ( .g ‘ ( 𝑅 ↾s 𝑈 ) ) 𝑀 ) )
86 80 85 oveq12d ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ℤ ∧ 𝑓 ∈ ℤ ) → ( ( 𝐹 ‘ 𝑓 ) ( +g ‘ ( 𝑅 ↾s 𝑈 ) ) ( 𝐹 ‘ 𝑔 ) ) = ( ( 𝑓 ( .g ‘ ( 𝑅 ↾s 𝑈 ) ) 𝑀 ) ( +g ‘ ( 𝑅 ↾s 𝑈 ) ) ( 𝑔 ( .g ‘ ( 𝑅 ↾s 𝑈 ) ) 𝑀 ) ) )
87 13 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ℤ ∧ 𝑓 ∈ ℤ ) → ( 𝑅 ↾s 𝑈 ) ∈ Grp )
88 23 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ℤ ∧ 𝑓 ∈ ℤ ) → 𝑀 ∈ ( Base ‘ ( 𝑅 ↾s 𝑈 ) ) )
89 78 83 88 3jca ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ℤ ∧ 𝑓 ∈ ℤ ) → ( 𝑓 ∈ ℤ ∧ 𝑔 ∈ ℤ ∧ 𝑀 ∈ ( Base ‘ ( 𝑅 ↾s 𝑈 ) ) ) )
90 eqid ⊢ ( +g ‘ ( 𝑅 ↾s 𝑈 ) ) = ( +g ‘ ( 𝑅 ↾s 𝑈 ) )
91 9 10 90 mulgdir ⊢ ( ( ( 𝑅 ↾s 𝑈 ) ∈ Grp ∧ ( 𝑓 ∈ ℤ ∧ 𝑔 ∈ ℤ ∧ 𝑀 ∈ ( Base ‘ ( 𝑅 ↾s 𝑈 ) ) ) ) → ( ( 𝑓 + 𝑔 ) ( .g ‘ ( 𝑅 ↾s 𝑈 ) ) 𝑀 ) = ( ( 𝑓 ( .g ‘ ( 𝑅 ↾s 𝑈 ) ) 𝑀 ) ( +g ‘ ( 𝑅 ↾s 𝑈 ) ) ( 𝑔 ( .g ‘ ( 𝑅 ↾s 𝑈 ) ) 𝑀 ) ) )
92 87 89 91 syl2anc ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ℤ ∧ 𝑓 ∈ ℤ ) → ( ( 𝑓 + 𝑔 ) ( .g ‘ ( 𝑅 ↾s 𝑈 ) ) 𝑀 ) = ( ( 𝑓 ( .g ‘ ( 𝑅 ↾s 𝑈 ) ) 𝑀 ) ( +g ‘ ( 𝑅 ↾s 𝑈 ) ) ( 𝑔 ( .g ‘ ( 𝑅 ↾s 𝑈 ) ) 𝑀 ) ) )
93 78 83 zaddcld ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ℤ ∧ 𝑓 ∈ ℤ ) → ( 𝑓 + 𝑔 ) ∈ ℤ )
94 simpr ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ ℤ ∧ 𝑓 ∈ ℤ ) ∧ ℎ = ( 𝑓 + 𝑔 ) ) → ℎ = ( 𝑓 + 𝑔 ) )
95 94 fveqeq2d ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ ℤ ∧ 𝑓 ∈ ℤ ) ∧ ℎ = ( 𝑓 + 𝑔 ) ) → ( ( 𝐹 ‘ ℎ ) = ( ( 𝑓 + 𝑔 ) ( .g ‘ ( 𝑅 ↾s 𝑈 ) ) 𝑀 ) ↔ ( 𝐹 ‘ ( 𝑓 + 𝑔 ) ) = ( ( 𝑓 + 𝑔 ) ( .g ‘ ( 𝑅 ↾s 𝑈 ) ) 𝑀 ) ) )
96 simpr ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ ℤ ∧ 𝑓 ∈ ℤ ) ∧ 𝑥 = ( 𝑓 + 𝑔 ) ) → 𝑥 = ( 𝑓 + 𝑔 ) )
97 96 oveq1d ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ ℤ ∧ 𝑓 ∈ ℤ ) ∧ 𝑥 = ( 𝑓 + 𝑔 ) ) → ( 𝑥 ( .g ‘ ( 𝑅 ↾s 𝑈 ) ) 𝑀 ) = ( ( 𝑓 + 𝑔 ) ( .g ‘ ( 𝑅 ↾s 𝑈 ) ) 𝑀 ) )
98 ovexd ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ℤ ∧ 𝑓 ∈ ℤ ) → ( ( 𝑓 + 𝑔 ) ( .g ‘ ( 𝑅 ↾s 𝑈 ) ) 𝑀 ) ∈ V )
99 75 97 93 98 fvmptd ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ℤ ∧ 𝑓 ∈ ℤ ) → ( 𝐹 ‘ ( 𝑓 + 𝑔 ) ) = ( ( 𝑓 + 𝑔 ) ( .g ‘ ( 𝑅 ↾s 𝑈 ) ) 𝑀 ) )
100 93 95 99 rspcedvd ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ℤ ∧ 𝑓 ∈ ℤ ) → ∃ ℎ ∈ ℤ ( 𝐹 ‘ ℎ ) = ( ( 𝑓 + 𝑔 ) ( .g ‘ ( 𝑅 ↾s 𝑈 ) ) 𝑀 ) )
101 fvelrnb ⊢ ( 𝐹 Fn ℤ → ( ( ( 𝑓 + 𝑔 ) ( .g ‘ ( 𝑅 ↾s 𝑈 ) ) 𝑀 ) ∈ ran 𝐹 ↔ ∃ ℎ ∈ ℤ ( 𝐹 ‘ ℎ ) = ( ( 𝑓 + 𝑔 ) ( .g ‘ ( 𝑅 ↾s 𝑈 ) ) 𝑀 ) ) )
102 43 101 syl ⊢ ( 𝜑 → ( ( ( 𝑓 + 𝑔 ) ( .g ‘ ( 𝑅 ↾s 𝑈 ) ) 𝑀 ) ∈ ran 𝐹 ↔ ∃ ℎ ∈ ℤ ( 𝐹 ‘ ℎ ) = ( ( 𝑓 + 𝑔 ) ( .g ‘ ( 𝑅 ↾s 𝑈 ) ) 𝑀 ) ) )
103 102 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ℤ ∧ 𝑓 ∈ ℤ ) → ( ( ( 𝑓 + 𝑔 ) ( .g ‘ ( 𝑅 ↾s 𝑈 ) ) 𝑀 ) ∈ ran 𝐹 ↔ ∃ ℎ ∈ ℤ ( 𝐹 ‘ ℎ ) = ( ( 𝑓 + 𝑔 ) ( .g ‘ ( 𝑅 ↾s 𝑈 ) ) 𝑀 ) ) )
104 100 103 mpbird ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ℤ ∧ 𝑓 ∈ ℤ ) → ( ( 𝑓 + 𝑔 ) ( .g ‘ ( 𝑅 ↾s 𝑈 ) ) 𝑀 ) ∈ ran 𝐹 )
105 92 104 eqeltrrd ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ℤ ∧ 𝑓 ∈ ℤ ) → ( ( 𝑓 ( .g ‘ ( 𝑅 ↾s 𝑈 ) ) 𝑀 ) ( +g ‘ ( 𝑅 ↾s 𝑈 ) ) ( 𝑔 ( .g ‘ ( 𝑅 ↾s 𝑈 ) ) 𝑀 ) ) ∈ ran 𝐹 )
106 86 105 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ℤ ∧ 𝑓 ∈ ℤ ) → ( ( 𝐹 ‘ 𝑓 ) ( +g ‘ ( 𝑅 ↾s 𝑈 ) ) ( 𝐹 ‘ 𝑔 ) ) ∈ ran 𝐹 )
107 74 106 syl ⊢ ( ( ( ( ( 𝜑 ∧ ∃ 𝑑 ∈ ℤ ( 𝐹 ‘ 𝑑 ) = 𝑦 ∧ ∃ 𝑒 ∈ ℤ ( 𝐹 ‘ 𝑒 ) = 𝑧 ) ∧ 𝑔 ∈ ℤ ) ∧ 𝑓 ∈ ℤ ) ∧ ( 𝐹 ‘ 𝑓 ) = 𝑦 ) → ( ( 𝐹 ‘ 𝑓 ) ( +g ‘ ( 𝑅 ↾s 𝑈 ) ) ( 𝐹 ‘ 𝑔 ) ) ∈ ran 𝐹 )
108 69 107 eqeltrd ⊢ ( ( ( ( ( 𝜑 ∧ ∃ 𝑑 ∈ ℤ ( 𝐹 ‘ 𝑑 ) = 𝑦 ∧ ∃ 𝑒 ∈ ℤ ( 𝐹 ‘ 𝑒 ) = 𝑧 ) ∧ 𝑔 ∈ ℤ ) ∧ 𝑓 ∈ ℤ ) ∧ ( 𝐹 ‘ 𝑓 ) = 𝑦 ) → ( 𝑦 ( +g ‘ ( 𝑅 ↾s 𝑈 ) ) ( 𝐹 ‘ 𝑔 ) ) ∈ ran 𝐹 )
109 simpl2 ⊢ ( ( ( 𝜑 ∧ ∃ 𝑑 ∈ ℤ ( 𝐹 ‘ 𝑑 ) = 𝑦 ∧ ∃ 𝑒 ∈ ℤ ( 𝐹 ‘ 𝑒 ) = 𝑧 ) ∧ 𝑔 ∈ ℤ ) → ∃ 𝑑 ∈ ℤ ( 𝐹 ‘ 𝑑 ) = 𝑦 )
110 nfv ⊢ Ⅎ 𝑓 ( 𝐹 ‘ 𝑑 ) = 𝑦
111 nfv ⊢ Ⅎ 𝑑 ( 𝐹 ‘ 𝑓 ) = 𝑦
112 fveqeq2 ⊢ ( 𝑑 = 𝑓 → ( ( 𝐹 ‘ 𝑑 ) = 𝑦 ↔ ( 𝐹 ‘ 𝑓 ) = 𝑦 ) )
113 110 111 112 cbvrexw ⊢ ( ∃ 𝑑 ∈ ℤ ( 𝐹 ‘ 𝑑 ) = 𝑦 ↔ ∃ 𝑓 ∈ ℤ ( 𝐹 ‘ 𝑓 ) = 𝑦 )
114 113 biimpi ⊢ ( ∃ 𝑑 ∈ ℤ ( 𝐹 ‘ 𝑑 ) = 𝑦 → ∃ 𝑓 ∈ ℤ ( 𝐹 ‘ 𝑓 ) = 𝑦 )
115 109 114 syl ⊢ ( ( ( 𝜑 ∧ ∃ 𝑑 ∈ ℤ ( 𝐹 ‘ 𝑑 ) = 𝑦 ∧ ∃ 𝑒 ∈ ℤ ( 𝐹 ‘ 𝑒 ) = 𝑧 ) ∧ 𝑔 ∈ ℤ ) → ∃ 𝑓 ∈ ℤ ( 𝐹 ‘ 𝑓 ) = 𝑦 )
116 108 115 r19.29a ⊢ ( ( ( 𝜑 ∧ ∃ 𝑑 ∈ ℤ ( 𝐹 ‘ 𝑑 ) = 𝑦 ∧ ∃ 𝑒 ∈ ℤ ( 𝐹 ‘ 𝑒 ) = 𝑧 ) ∧ 𝑔 ∈ ℤ ) → ( 𝑦 ( +g ‘ ( 𝑅 ↾s 𝑈 ) ) ( 𝐹 ‘ 𝑔 ) ) ∈ ran 𝐹 )
117 116 adantr ⊢ ( ( ( ( 𝜑 ∧ ∃ 𝑑 ∈ ℤ ( 𝐹 ‘ 𝑑 ) = 𝑦 ∧ ∃ 𝑒 ∈ ℤ ( 𝐹 ‘ 𝑒 ) = 𝑧 ) ∧ 𝑔 ∈ ℤ ) ∧ ( 𝐹 ‘ 𝑔 ) = 𝑧 ) → ( 𝑦 ( +g ‘ ( 𝑅 ↾s 𝑈 ) ) ( 𝐹 ‘ 𝑔 ) ) ∈ ran 𝐹 )
118 66 117 eqeltrd ⊢ ( ( ( ( 𝜑 ∧ ∃ 𝑑 ∈ ℤ ( 𝐹 ‘ 𝑑 ) = 𝑦 ∧ ∃ 𝑒 ∈ ℤ ( 𝐹 ‘ 𝑒 ) = 𝑧 ) ∧ 𝑔 ∈ ℤ ) ∧ ( 𝐹 ‘ 𝑔 ) = 𝑧 ) → ( 𝑦 ( +g ‘ ( 𝑅 ↾s 𝑈 ) ) 𝑧 ) ∈ ran 𝐹 )
119 simp3 ⊢ ( ( 𝜑 ∧ ∃ 𝑑 ∈ ℤ ( 𝐹 ‘ 𝑑 ) = 𝑦 ∧ ∃ 𝑒 ∈ ℤ ( 𝐹 ‘ 𝑒 ) = 𝑧 ) → ∃ 𝑒 ∈ ℤ ( 𝐹 ‘ 𝑒 ) = 𝑧 )
120 nfv ⊢ Ⅎ 𝑔 ( 𝐹 ‘ 𝑒 ) = 𝑧
121 nfv ⊢ Ⅎ 𝑒 ( 𝐹 ‘ 𝑔 ) = 𝑧
122 fveqeq2 ⊢ ( 𝑒 = 𝑔 → ( ( 𝐹 ‘ 𝑒 ) = 𝑧 ↔ ( 𝐹 ‘ 𝑔 ) = 𝑧 ) )
123 120 121 122 cbvrexw ⊢ ( ∃ 𝑒 ∈ ℤ ( 𝐹 ‘ 𝑒 ) = 𝑧 ↔ ∃ 𝑔 ∈ ℤ ( 𝐹 ‘ 𝑔 ) = 𝑧 )
124 123 biimpi ⊢ ( ∃ 𝑒 ∈ ℤ ( 𝐹 ‘ 𝑒 ) = 𝑧 → ∃ 𝑔 ∈ ℤ ( 𝐹 ‘ 𝑔 ) = 𝑧 )
125 119 124 syl ⊢ ( ( 𝜑 ∧ ∃ 𝑑 ∈ ℤ ( 𝐹 ‘ 𝑑 ) = 𝑦 ∧ ∃ 𝑒 ∈ ℤ ( 𝐹 ‘ 𝑒 ) = 𝑧 ) → ∃ 𝑔 ∈ ℤ ( 𝐹 ‘ 𝑔 ) = 𝑧 )
126 118 125 r19.29a ⊢ ( ( 𝜑 ∧ ∃ 𝑑 ∈ ℤ ( 𝐹 ‘ 𝑑 ) = 𝑦 ∧ ∃ 𝑒 ∈ ℤ ( 𝐹 ‘ 𝑒 ) = 𝑧 ) → ( 𝑦 ( +g ‘ ( 𝑅 ↾s 𝑈 ) ) 𝑧 ) ∈ ran 𝐹 )
127 63 126 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ran 𝐹 ∧ 𝑧 ∈ ran 𝐹 ) ∧ ∃ 𝑑 ∈ ℤ ( 𝐹 ‘ 𝑑 ) = 𝑦 ) ∧ ∃ 𝑒 ∈ ℤ ( 𝐹 ‘ 𝑒 ) = 𝑧 ) → ( 𝑦 ( +g ‘ ( 𝑅 ↾s 𝑈 ) ) 𝑧 ) ∈ ran 𝐹 )
128 127 ex ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ran 𝐹 ∧ 𝑧 ∈ ran 𝐹 ) ∧ ∃ 𝑑 ∈ ℤ ( 𝐹 ‘ 𝑑 ) = 𝑦 ) → ( ∃ 𝑒 ∈ ℤ ( 𝐹 ‘ 𝑒 ) = 𝑧 → ( 𝑦 ( +g ‘ ( 𝑅 ↾s 𝑈 ) ) 𝑧 ) ∈ ran 𝐹 ) )
129 59 128 mpd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ran 𝐹 ∧ 𝑧 ∈ ran 𝐹 ) ∧ ∃ 𝑑 ∈ ℤ ( 𝐹 ‘ 𝑑 ) = 𝑦 ) → ( 𝑦 ( +g ‘ ( 𝑅 ↾s 𝑈 ) ) 𝑧 ) ∈ ran 𝐹 )
130 51 129 mpdan ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ran 𝐹 ∧ 𝑧 ∈ ran 𝐹 ) → ( 𝑦 ( +g ‘ ( 𝑅 ↾s 𝑈 ) ) 𝑧 ) ∈ ran 𝐹 )
131 simpr ⊢ ( ( ( ( 𝜑 ∧ ∃ 𝑑 ∈ ℤ ( 𝐹 ‘ 𝑑 ) = 𝑦 ) ∧ 𝑓 ∈ ℤ ) ∧ ( 𝐹 ‘ 𝑓 ) = 𝑦 ) → ( 𝐹 ‘ 𝑓 ) = 𝑦 )
132 131 eqcomd ⊢ ( ( ( ( 𝜑 ∧ ∃ 𝑑 ∈ ℤ ( 𝐹 ‘ 𝑑 ) = 𝑦 ) ∧ 𝑓 ∈ ℤ ) ∧ ( 𝐹 ‘ 𝑓 ) = 𝑦 ) → 𝑦 = ( 𝐹 ‘ 𝑓 ) )
133 132 fveq2d ⊢ ( ( ( ( 𝜑 ∧ ∃ 𝑑 ∈ ℤ ( 𝐹 ‘ 𝑑 ) = 𝑦 ) ∧ 𝑓 ∈ ℤ ) ∧ ( 𝐹 ‘ 𝑓 ) = 𝑦 ) → ( ( invg ‘ ( 𝑅 ↾s 𝑈 ) ) ‘ 𝑦 ) = ( ( invg ‘ ( 𝑅 ↾s 𝑈 ) ) ‘ ( 𝐹 ‘ 𝑓 ) ) )
134 simplll ⊢ ( ( ( ( 𝜑 ∧ ∃ 𝑑 ∈ ℤ ( 𝐹 ‘ 𝑑 ) = 𝑦 ) ∧ 𝑓 ∈ ℤ ) ∧ ( 𝐹 ‘ 𝑓 ) = 𝑦 ) → 𝜑 )
135 simplr ⊢ ( ( ( ( 𝜑 ∧ ∃ 𝑑 ∈ ℤ ( 𝐹 ‘ 𝑑 ) = 𝑦 ) ∧ 𝑓 ∈ ℤ ) ∧ ( 𝐹 ‘ 𝑓 ) = 𝑦 ) → 𝑓 ∈ ℤ )
136 134 135 jca ⊢ ( ( ( ( 𝜑 ∧ ∃ 𝑑 ∈ ℤ ( 𝐹 ‘ 𝑑 ) = 𝑦 ) ∧ 𝑓 ∈ ℤ ) ∧ ( 𝐹 ‘ 𝑓 ) = 𝑦 ) → ( 𝜑 ∧ 𝑓 ∈ ℤ ) )
137 simpr ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ℤ ) → 𝑓 ∈ ℤ )
138 137 znegcld ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ℤ ) → - 𝑓 ∈ ℤ )
139 simpr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ℤ ) ∧ ℎ = - 𝑓 ) → ℎ = - 𝑓 )
140 139 fveqeq2d ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ℤ ) ∧ ℎ = - 𝑓 ) → ( ( 𝐹 ‘ ℎ ) = ( ( invg ‘ ( 𝑅 ↾s 𝑈 ) ) ‘ ( 𝐹 ‘ 𝑓 ) ) ↔ ( 𝐹 ‘ - 𝑓 ) = ( ( invg ‘ ( 𝑅 ↾s 𝑈 ) ) ‘ ( 𝐹 ‘ 𝑓 ) ) ) )
141 4 a1i ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ℤ ) → 𝐹 = ( 𝑥 ∈ ℤ ↦ ( 𝑥 ( .g ‘ ( 𝑅 ↾s 𝑈 ) ) 𝑀 ) ) )
142 simpr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ℤ ) ∧ 𝑥 = - 𝑓 ) → 𝑥 = - 𝑓 )
143 142 oveq1d ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ℤ ) ∧ 𝑥 = - 𝑓 ) → ( 𝑥 ( .g ‘ ( 𝑅 ↾s 𝑈 ) ) 𝑀 ) = ( - 𝑓 ( .g ‘ ( 𝑅 ↾s 𝑈 ) ) 𝑀 ) )
144 ovexd ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ℤ ) → ( - 𝑓 ( .g ‘ ( 𝑅 ↾s 𝑈 ) ) 𝑀 ) ∈ V )
145 141 143 138 144 fvmptd ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ℤ ) → ( 𝐹 ‘ - 𝑓 ) = ( - 𝑓 ( .g ‘ ( 𝑅 ↾s 𝑈 ) ) 𝑀 ) )
146 13 adantr ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ℤ ) → ( 𝑅 ↾s 𝑈 ) ∈ Grp )
147 23 adantr ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ℤ ) → 𝑀 ∈ ( Base ‘ ( 𝑅 ↾s 𝑈 ) ) )
148 eqid ⊢ ( invg ‘ ( 𝑅 ↾s 𝑈 ) ) = ( invg ‘ ( 𝑅 ↾s 𝑈 ) )
149 9 10 148 mulgneg ⊢ ( ( ( 𝑅 ↾s 𝑈 ) ∈ Grp ∧ 𝑓 ∈ ℤ ∧ 𝑀 ∈ ( Base ‘ ( 𝑅 ↾s 𝑈 ) ) ) → ( - 𝑓 ( .g ‘ ( 𝑅 ↾s 𝑈 ) ) 𝑀 ) = ( ( invg ‘ ( 𝑅 ↾s 𝑈 ) ) ‘ ( 𝑓 ( .g ‘ ( 𝑅 ↾s 𝑈 ) ) 𝑀 ) ) )
150 146 137 147 149 syl3anc ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ℤ ) → ( - 𝑓 ( .g ‘ ( 𝑅 ↾s 𝑈 ) ) 𝑀 ) = ( ( invg ‘ ( 𝑅 ↾s 𝑈 ) ) ‘ ( 𝑓 ( .g ‘ ( 𝑅 ↾s 𝑈 ) ) 𝑀 ) ) )
151 simpr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ℤ ) ∧ 𝑥 = 𝑓 ) → 𝑥 = 𝑓 )
152 151 oveq1d ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ℤ ) ∧ 𝑥 = 𝑓 ) → ( 𝑥 ( .g ‘ ( 𝑅 ↾s 𝑈 ) ) 𝑀 ) = ( 𝑓 ( .g ‘ ( 𝑅 ↾s 𝑈 ) ) 𝑀 ) )
153 ovexd ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ℤ ) → ( 𝑓 ( .g ‘ ( 𝑅 ↾s 𝑈 ) ) 𝑀 ) ∈ V )
154 141 152 137 153 fvmptd ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ℤ ) → ( 𝐹 ‘ 𝑓 ) = ( 𝑓 ( .g ‘ ( 𝑅 ↾s 𝑈 ) ) 𝑀 ) )
155 154 eqcomd ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ℤ ) → ( 𝑓 ( .g ‘ ( 𝑅 ↾s 𝑈 ) ) 𝑀 ) = ( 𝐹 ‘ 𝑓 ) )
156 155 fveq2d ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ℤ ) → ( ( invg ‘ ( 𝑅 ↾s 𝑈 ) ) ‘ ( 𝑓 ( .g ‘ ( 𝑅 ↾s 𝑈 ) ) 𝑀 ) ) = ( ( invg ‘ ( 𝑅 ↾s 𝑈 ) ) ‘ ( 𝐹 ‘ 𝑓 ) ) )
157 150 156 eqtrd ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ℤ ) → ( - 𝑓 ( .g ‘ ( 𝑅 ↾s 𝑈 ) ) 𝑀 ) = ( ( invg ‘ ( 𝑅 ↾s 𝑈 ) ) ‘ ( 𝐹 ‘ 𝑓 ) ) )
158 145 157 eqtrd ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ℤ ) → ( 𝐹 ‘ - 𝑓 ) = ( ( invg ‘ ( 𝑅 ↾s 𝑈 ) ) ‘ ( 𝐹 ‘ 𝑓 ) ) )
159 138 140 158 rspcedvd ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ℤ ) → ∃ ℎ ∈ ℤ ( 𝐹 ‘ ℎ ) = ( ( invg ‘ ( 𝑅 ↾s 𝑈 ) ) ‘ ( 𝐹 ‘ 𝑓 ) ) )
160 fvelrnb ⊢ ( 𝐹 Fn ℤ → ( ( ( invg ‘ ( 𝑅 ↾s 𝑈 ) ) ‘ ( 𝐹 ‘ 𝑓 ) ) ∈ ran 𝐹 ↔ ∃ ℎ ∈ ℤ ( 𝐹 ‘ ℎ ) = ( ( invg ‘ ( 𝑅 ↾s 𝑈 ) ) ‘ ( 𝐹 ‘ 𝑓 ) ) ) )
161 43 160 syl ⊢ ( 𝜑 → ( ( ( invg ‘ ( 𝑅 ↾s 𝑈 ) ) ‘ ( 𝐹 ‘ 𝑓 ) ) ∈ ran 𝐹 ↔ ∃ ℎ ∈ ℤ ( 𝐹 ‘ ℎ ) = ( ( invg ‘ ( 𝑅 ↾s 𝑈 ) ) ‘ ( 𝐹 ‘ 𝑓 ) ) ) )
162 161 adantr ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ℤ ) → ( ( ( invg ‘ ( 𝑅 ↾s 𝑈 ) ) ‘ ( 𝐹 ‘ 𝑓 ) ) ∈ ran 𝐹 ↔ ∃ ℎ ∈ ℤ ( 𝐹 ‘ ℎ ) = ( ( invg ‘ ( 𝑅 ↾s 𝑈 ) ) ‘ ( 𝐹 ‘ 𝑓 ) ) ) )
163 159 162 mpbird ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ℤ ) → ( ( invg ‘ ( 𝑅 ↾s 𝑈 ) ) ‘ ( 𝐹 ‘ 𝑓 ) ) ∈ ran 𝐹 )
164 163 a1i ⊢ ( ( ( ( 𝜑 ∧ ∃ 𝑑 ∈ ℤ ( 𝐹 ‘ 𝑑 ) = 𝑦 ) ∧ 𝑓 ∈ ℤ ) ∧ ( 𝐹 ‘ 𝑓 ) = 𝑦 ) → ( ( 𝜑 ∧ 𝑓 ∈ ℤ ) → ( ( invg ‘ ( 𝑅 ↾s 𝑈 ) ) ‘ ( 𝐹 ‘ 𝑓 ) ) ∈ ran 𝐹 ) )
165 136 164 mpd ⊢ ( ( ( ( 𝜑 ∧ ∃ 𝑑 ∈ ℤ ( 𝐹 ‘ 𝑑 ) = 𝑦 ) ∧ 𝑓 ∈ ℤ ) ∧ ( 𝐹 ‘ 𝑓 ) = 𝑦 ) → ( ( invg ‘ ( 𝑅 ↾s 𝑈 ) ) ‘ ( 𝐹 ‘ 𝑓 ) ) ∈ ran 𝐹 )
166 133 165 eqeltrd ⊢ ( ( ( ( 𝜑 ∧ ∃ 𝑑 ∈ ℤ ( 𝐹 ‘ 𝑑 ) = 𝑦 ) ∧ 𝑓 ∈ ℤ ) ∧ ( 𝐹 ‘ 𝑓 ) = 𝑦 ) → ( ( invg ‘ ( 𝑅 ↾s 𝑈 ) ) ‘ 𝑦 ) ∈ ran 𝐹 )
167 113 bilani ⊢ ( ( 𝜑 ∧ ∃ 𝑑 ∈ ℤ ( 𝐹 ‘ 𝑑 ) = 𝑦 ) → ∃ 𝑓 ∈ ℤ ( 𝐹 ‘ 𝑓 ) = 𝑦 )
168 166 167 r19.29a ⊢ ( ( 𝜑 ∧ ∃ 𝑑 ∈ ℤ ( 𝐹 ‘ 𝑑 ) = 𝑦 ) → ( ( invg ‘ ( 𝑅 ↾s 𝑈 ) ) ‘ 𝑦 ) ∈ ran 𝐹 )
169 168 ex ⊢ ( 𝜑 → ( ∃ 𝑑 ∈ ℤ ( 𝐹 ‘ 𝑑 ) = 𝑦 → ( ( invg ‘ ( 𝑅 ↾s 𝑈 ) ) ‘ 𝑦 ) ∈ ran 𝐹 ) )
170 169 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ran 𝐹 ) → ( ∃ 𝑑 ∈ ℤ ( 𝐹 ‘ 𝑑 ) = 𝑦 → ( ( invg ‘ ( 𝑅 ↾s 𝑈 ) ) ‘ 𝑦 ) ∈ ran 𝐹 ) )
171 170 imp ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ran 𝐹 ) ∧ ∃ 𝑑 ∈ ℤ ( 𝐹 ‘ 𝑑 ) = 𝑦 ) → ( ( invg ‘ ( 𝑅 ↾s 𝑈 ) ) ‘ 𝑦 ) ∈ ran 𝐹 )
172 50 171 mpdan ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ran 𝐹 ) → ( ( invg ‘ ( 𝑅 ↾s 𝑈 ) ) ‘ 𝑦 ) ∈ ran 𝐹 )
173 6 7 8 28 46 130 172 13 issubgrpd ⊢ ( 𝜑 → ( ( 𝑅 ↾s 𝑈 ) ↾s ran 𝐹 ) ∈ Grp )