Metamath Proof Explorer

Theorem aks6d1c6lem5

Description: Eliminate the size hypothesis. Claim 6. (Contributed by metakunt, 15-May-2025)

Ref Expression
Hypotheses aks6d1c6lem5.1 ⊢ ∼ = { ⟨ 𝑒 , 𝑓 ⟩ ∣ ( 𝑒 ∈ ℕ ∧ 𝑓 ∈ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) ∧ ∀ 𝑦 ∈ ( ( mulGrp ‘ 𝐾 ) PrimRoots 𝑅 ) ( 𝑒 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) ( ( ( eval1 ‘ 𝐾 ) ‘ 𝑓 ) ‘ 𝑦 ) ) = ( ( ( eval1 ‘ 𝐾 ) ‘ 𝑓 ) ‘ ( 𝑒 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑦 ) ) ) }
aks6d1c6lem5.2 ⊢ 𝑃 = ( chr ‘ 𝐾 )
aks6d1c6lem5.3 ⊢ ( 𝜑 → 𝐾 ∈ Field )
aks6d1c6lem5.4 ⊢ ( 𝜑 → 𝑃 ∈ ℙ )
aks6d1c6lem5.5 ⊢ ( 𝜑 → 𝑅 ∈ ℕ )
aks6d1c6lem5.6 ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
aks6d1c6lem5.7 ⊢ ( 𝜑 → 𝑃 ∥ 𝑁 )
aks6d1c6lem5.8 ⊢ ( 𝜑 → ( 𝑁 gcd 𝑅 ) = 1 )
aks6d1c6lem5.9 ⊢ ( 𝜑 → ∀ 𝑏 ∈ ( 1 ... 𝐴 ) ( 𝑏 gcd 𝑁 ) = 1 )
aks6d1c6lem5.10 ⊢ 𝐺 = ( 𝑔 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ↦ ( ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) Σg ( 𝑖 ∈ ( 0 ... 𝐴 ) ↦ ( ( 𝑔 ‘ 𝑖 ) ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) ) ( ( var1 ‘ 𝐾 ) ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ) ) )
aks6d1c6lem5.11 ⊢ 𝐴 = ( ⌊ ‘ ( ( √ ‘ ( ϕ ‘ 𝑅 ) ) · ( 2 logb 𝑁 ) ) )
aksaks6dlem5.12 ⊢ 𝐸 = ( 𝑘 ∈ ℕ0 , 𝑙 ∈ ℕ0 ↦ ( ( 𝑃 ↑ 𝑘 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑙 ) ) )
aks6d1c6lem5.13 ⊢ 𝐿 = ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑅 ) )
aks6d1c6lem5.14 ⊢ ( 𝜑 → ∀ 𝑎 ∈ ( 1 ... 𝐴 ) 𝑁 ∼ ( ( var1 ‘ 𝐾 ) ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑎 ) ) ) )
aks6d1c6lem5.15 ⊢ ( 𝜑 → ( 𝑥 ∈ ( Base ‘ 𝐾 ) ↦ ( 𝑃 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑥 ) ) ∈ ( 𝐾 RingIso 𝐾 ) )
aks6d1c6lem5.16 ⊢ ( 𝜑 → 𝑀 ∈ ( ( mulGrp ‘ 𝐾 ) PrimRoots 𝑅 ) )
aks6d1c6lem5.17 ⊢ 𝐻 = ( ℎ ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ↦ ( ( ( eval1 ‘ 𝐾 ) ‘ ( 𝐺 ‘ ℎ ) ) ‘ 𝑀 ) )
aks6d1c6lem5.18 ⊢ 𝐷 = ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) )
aks6d1c6lem5.19 ⊢ 𝑆 = { 𝑠 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ∣ Σ 𝑡 ∈ ( 0 ... 𝐴 ) ( 𝑠 ‘ 𝑡 ) ≤ ( 𝐷 − 1 ) }
aks6d1c6lem5.20 ⊢ 𝐽 = ( 𝑗 ∈ ℤ ↦ ( 𝑗 ( .g ‘ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ) 𝑀 ) )
aks6d1c6lem5.22 ⊢ 𝑈 = { 𝑚 ∈ ( Base ‘ ( mulGrp ‘ 𝐾 ) ) ∣ ∃ 𝑛 ∈ ( Base ‘ ( mulGrp ‘ 𝐾 ) ) ( 𝑛 ( +g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑚 ) = ( 0g ‘ ( mulGrp ‘ 𝐾 ) ) }
aks6d1c6lem5.23 ⊢ 𝑋 = ( 𝑏 ∈ ( Base ‘ ( ℤring /s ( ℤring ~QG ( ◡ 𝐽 “ { ( 0g ‘ ( ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ↾s ran 𝐽 ) ) } ) ) ) ) ↦ ∪ ( 𝐽 “ 𝑏 ) )
Assertion aks6d1c6lem5 ( 𝜑 → ( ( 𝐷 + 𝐴 ) C ( 𝐷 − 1 ) ) ≤ ( ♯ ‘ ( 𝐻 “ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 aks6d1c6lem5.1 ⊢ ∼ = { ⟨ 𝑒 , 𝑓 ⟩ ∣ ( 𝑒 ∈ ℕ ∧ 𝑓 ∈ ( Base ‘ ( Poly1 ‘ 𝐾 ) ) ∧ ∀ 𝑦 ∈ ( ( mulGrp ‘ 𝐾 ) PrimRoots 𝑅 ) ( 𝑒 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) ( ( ( eval1 ‘ 𝐾 ) ‘ 𝑓 ) ‘ 𝑦 ) ) = ( ( ( eval1 ‘ 𝐾 ) ‘ 𝑓 ) ‘ ( 𝑒 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑦 ) ) ) }
2 aks6d1c6lem5.2 ⊢ 𝑃 = ( chr ‘ 𝐾 )
3 aks6d1c6lem5.3 ⊢ ( 𝜑 → 𝐾 ∈ Field )
4 aks6d1c6lem5.4 ⊢ ( 𝜑 → 𝑃 ∈ ℙ )
5 aks6d1c6lem5.5 ⊢ ( 𝜑 → 𝑅 ∈ ℕ )
6 aks6d1c6lem5.6 ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
7 aks6d1c6lem5.7 ⊢ ( 𝜑 → 𝑃 ∥ 𝑁 )
8 aks6d1c6lem5.8 ⊢ ( 𝜑 → ( 𝑁 gcd 𝑅 ) = 1 )
9 aks6d1c6lem5.9 ⊢ ( 𝜑 → ∀ 𝑏 ∈ ( 1 ... 𝐴 ) ( 𝑏 gcd 𝑁 ) = 1 )
10 aks6d1c6lem5.10 ⊢ 𝐺 = ( 𝑔 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ↦ ( ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) Σg ( 𝑖 ∈ ( 0 ... 𝐴 ) ↦ ( ( 𝑔 ‘ 𝑖 ) ( .g ‘ ( mulGrp ‘ ( Poly1 ‘ 𝐾 ) ) ) ( ( var1 ‘ 𝐾 ) ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑖 ) ) ) ) ) ) )
11 aks6d1c6lem5.11 ⊢ 𝐴 = ( ⌊ ‘ ( ( √ ‘ ( ϕ ‘ 𝑅 ) ) · ( 2 logb 𝑁 ) ) )
12 aksaks6dlem5.12 ⊢ 𝐸 = ( 𝑘 ∈ ℕ0 , 𝑙 ∈ ℕ0 ↦ ( ( 𝑃 ↑ 𝑘 ) · ( ( 𝑁 / 𝑃 ) ↑ 𝑙 ) ) )
13 aks6d1c6lem5.13 ⊢ 𝐿 = ( ℤRHom ‘ ( ℤ/nℤ ‘ 𝑅 ) )
14 aks6d1c6lem5.14 ⊢ ( 𝜑 → ∀ 𝑎 ∈ ( 1 ... 𝐴 ) 𝑁 ∼ ( ( var1 ‘ 𝐾 ) ( +g ‘ ( Poly1 ‘ 𝐾 ) ) ( ( algSc ‘ ( Poly1 ‘ 𝐾 ) ) ‘ ( ( ℤRHom ‘ 𝐾 ) ‘ 𝑎 ) ) ) )
15 aks6d1c6lem5.15 ⊢ ( 𝜑 → ( 𝑥 ∈ ( Base ‘ 𝐾 ) ↦ ( 𝑃 ( .g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑥 ) ) ∈ ( 𝐾 RingIso 𝐾 ) )
16 aks6d1c6lem5.16 ⊢ ( 𝜑 → 𝑀 ∈ ( ( mulGrp ‘ 𝐾 ) PrimRoots 𝑅 ) )
17 aks6d1c6lem5.17 ⊢ 𝐻 = ( ℎ ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ↦ ( ( ( eval1 ‘ 𝐾 ) ‘ ( 𝐺 ‘ ℎ ) ) ‘ 𝑀 ) )
18 aks6d1c6lem5.18 ⊢ 𝐷 = ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) )
19 aks6d1c6lem5.19 ⊢ 𝑆 = { 𝑠 ∈ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ∣ Σ 𝑡 ∈ ( 0 ... 𝐴 ) ( 𝑠 ‘ 𝑡 ) ≤ ( 𝐷 − 1 ) }
20 aks6d1c6lem5.20 ⊢ 𝐽 = ( 𝑗 ∈ ℤ ↦ ( 𝑗 ( .g ‘ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ) 𝑀 ) )
21 aks6d1c6lem5.22 ⊢ 𝑈 = { 𝑚 ∈ ( Base ‘ ( mulGrp ‘ 𝐾 ) ) ∣ ∃ 𝑛 ∈ ( Base ‘ ( mulGrp ‘ 𝐾 ) ) ( 𝑛 ( +g ‘ ( mulGrp ‘ 𝐾 ) ) 𝑚 ) = ( 0g ‘ ( mulGrp ‘ 𝐾 ) ) }
22 aks6d1c6lem5.23 ⊢ 𝑋 = ( 𝑏 ∈ ( Base ‘ ( ℤring /s ( ℤring ~QG ( ◡ 𝐽 “ { ( 0g ‘ ( ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ↾s ran 𝐽 ) ) } ) ) ) ) ↦ ∪ ( 𝐽 “ 𝑏 ) )
23 eqid ⊢ ( 0g ‘ ( ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ↾s ran 𝐽 ) ) = ( 0g ‘ ( ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ↾s ran 𝐽 ) )
24 3 fldcrngd ⊢ ( 𝜑 → 𝐾 ∈ CRing )
25 eqid ⊢ ( mulGrp ‘ 𝐾 ) = ( mulGrp ‘ 𝐾 )
26 25 crngmgp ⊢ ( 𝐾 ∈ CRing → ( mulGrp ‘ 𝐾 ) ∈ CMnd )
27 24 26 syl ⊢ ( 𝜑 → ( mulGrp ‘ 𝐾 ) ∈ CMnd )
28 27 5 21 20 16 aks6d1c6isolem2 ⊢ ( 𝜑 → 𝐽 ∈ ( ℤring GrpHom ( ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ↾s ran 𝐽 ) ) )
29 eqid ⊢ ( ◡ 𝐽 “ { ( 0g ‘ ( ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ↾s ran 𝐽 ) ) } ) = ( ◡ 𝐽 “ { ( 0g ‘ ( ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ↾s ran 𝐽 ) ) } )
30 eqid ⊢ ( ℤring /s ( ℤring ~QG ( ◡ 𝐽 “ { ( 0g ‘ ( ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ↾s ran 𝐽 ) ) } ) ) ) = ( ℤring /s ( ℤring ~QG ( ◡ 𝐽 “ { ( 0g ‘ ( ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ↾s ran 𝐽 ) ) } ) ) )
31 zringbas ⊢ ℤ = ( Base ‘ ℤring )
32 nfcv ⊢ Ⅎ 𝑐 [ 𝑑 ] ( ℤring ~QG ( ◡ 𝐽 “ { ( 0g ‘ ( ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ↾s ran 𝐽 ) ) } ) )
33 nfcv ⊢ Ⅎ 𝑑 [ 𝑐 ] ( ℤring ~QG ( ◡ 𝐽 “ { ( 0g ‘ ( ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ↾s ran 𝐽 ) ) } ) )
34 eceq1 ⊢ ( 𝑑 = 𝑐 → [ 𝑑 ] ( ℤring ~QG ( ◡ 𝐽 “ { ( 0g ‘ ( ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ↾s ran 𝐽 ) ) } ) ) = [ 𝑐 ] ( ℤring ~QG ( ◡ 𝐽 “ { ( 0g ‘ ( ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ↾s ran 𝐽 ) ) } ) ) )
35 32 33 34 cbvmpt ⊢ ( 𝑑 ∈ ℤ ↦ [ 𝑑 ] ( ℤring ~QG ( ◡ 𝐽 “ { ( 0g ‘ ( ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ↾s ran 𝐽 ) ) } ) ) ) = ( 𝑐 ∈ ℤ ↦ [ 𝑐 ] ( ℤring ~QG ( ◡ 𝐽 “ { ( 0g ‘ ( ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ↾s ran 𝐽 ) ) } ) ) )
36 23 28 29 30 22 31 35 ghmquskerco ⊢ ( 𝜑 → 𝐽 = ( 𝑋 ∘ ( 𝑑 ∈ ℤ ↦ [ 𝑑 ] ( ℤring ~QG ( ◡ 𝐽 “ { ( 0g ‘ ( ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ↾s ran 𝐽 ) ) } ) ) ) ) )
37 eqid ⊢ ( RSpan ‘ ℤring ) = ( RSpan ‘ ℤring )
38 27 5 21 20 16 37 aks6d1c6isolem3 ⊢ ( 𝜑 → ( ( RSpan ‘ ℤring ) ‘ { 𝑅 } ) = ( ◡ 𝐽 “ { ( 0g ‘ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ) } ) )
39 27 5 21 primrootsunit ⊢ ( 𝜑 → ( ( ( mulGrp ‘ 𝐾 ) PrimRoots 𝑅 ) = ( ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) PrimRoots 𝑅 ) ∧ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ∈ Abel ) )
40 39 simprd ⊢ ( 𝜑 → ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ∈ Abel )
41 40 ablgrpd ⊢ ( 𝜑 → ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ∈ Grp )
42 41 grpmndd ⊢ ( 𝜑 → ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ∈ Mnd )
43 0zd ⊢ ( 𝜑 → 0 ∈ ℤ )
44 simpr ⊢ ( ( 𝜑 ∧ 𝑤 = 0 ) → 𝑤 = 0 )
45 44 fveqeq2d ⊢ ( ( 𝜑 ∧ 𝑤 = 0 ) → ( ( 𝐽 ‘ 𝑤 ) = ( 0g ‘ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ) ↔ ( 𝐽 ‘ 0 ) = ( 0g ‘ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ) ) )
46 20 a1i ⊢ ( 𝜑 → 𝐽 = ( 𝑗 ∈ ℤ ↦ ( 𝑗 ( .g ‘ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ) 𝑀 ) ) )
47 simpr ⊢ ( ( 𝜑 ∧ 𝑗 = 0 ) → 𝑗 = 0 )
48 47 oveq1d ⊢ ( ( 𝜑 ∧ 𝑗 = 0 ) → ( 𝑗 ( .g ‘ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ) 𝑀 ) = ( 0 ( .g ‘ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ) 𝑀 ) )
49 39 simpld ⊢ ( 𝜑 → ( ( mulGrp ‘ 𝐾 ) PrimRoots 𝑅 ) = ( ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) PrimRoots 𝑅 ) )
50 16 49 eleqtrd ⊢ ( 𝜑 → 𝑀 ∈ ( ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) PrimRoots 𝑅 ) )
51 40 ablcmnd ⊢ ( 𝜑 → ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ∈ CMnd )
52 5 nnnn0d ⊢ ( 𝜑 → 𝑅 ∈ ℕ0 )
53 eqid ⊢ ( .g ‘ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ) = ( .g ‘ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) )
54 51 52 53 isprimroot ⊢ ( 𝜑 → ( 𝑀 ∈ ( ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) PrimRoots 𝑅 ) ↔ ( 𝑀 ∈ ( Base ‘ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ) ∧ ( 𝑅 ( .g ‘ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ) 𝑀 ) = ( 0g ‘ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ) ∧ ∀ 𝑙 ∈ ℕ0 ( ( 𝑙 ( .g ‘ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ) 𝑀 ) = ( 0g ‘ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ) → 𝑅 ∥ 𝑙 ) ) ) )
55 54 biimpd ⊢ ( 𝜑 → ( 𝑀 ∈ ( ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) PrimRoots 𝑅 ) → ( 𝑀 ∈ ( Base ‘ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ) ∧ ( 𝑅 ( .g ‘ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ) 𝑀 ) = ( 0g ‘ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ) ∧ ∀ 𝑙 ∈ ℕ0 ( ( 𝑙 ( .g ‘ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ) 𝑀 ) = ( 0g ‘ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ) → 𝑅 ∥ 𝑙 ) ) ) )
56 50 55 mpd ⊢ ( 𝜑 → ( 𝑀 ∈ ( Base ‘ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ) ∧ ( 𝑅 ( .g ‘ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ) 𝑀 ) = ( 0g ‘ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ) ∧ ∀ 𝑙 ∈ ℕ0 ( ( 𝑙 ( .g ‘ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ) 𝑀 ) = ( 0g ‘ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ) → 𝑅 ∥ 𝑙 ) ) )
57 56 simp1d ⊢ ( 𝜑 → 𝑀 ∈ ( Base ‘ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ) )
58 eqid ⊢ ( Base ‘ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ) = ( Base ‘ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) )
59 eqid ⊢ ( 0g ‘ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ) = ( 0g ‘ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) )
60 58 59 53 mulg0 ⊢ ( 𝑀 ∈ ( Base ‘ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ) → ( 0 ( .g ‘ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ) 𝑀 ) = ( 0g ‘ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ) )
61 57 60 syl ⊢ ( 𝜑 → ( 0 ( .g ‘ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ) 𝑀 ) = ( 0g ‘ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ) )
62 61 adantr ⊢ ( ( 𝜑 ∧ 𝑗 = 0 ) → ( 0 ( .g ‘ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ) 𝑀 ) = ( 0g ‘ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ) )
63 48 62 eqtrd ⊢ ( ( 𝜑 ∧ 𝑗 = 0 ) → ( 𝑗 ( .g ‘ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ) 𝑀 ) = ( 0g ‘ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ) )
64 fvexd ⊢ ( 𝜑 → ( 0g ‘ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ) ∈ V )
65 46 63 43 64 fvmptd ⊢ ( 𝜑 → ( 𝐽 ‘ 0 ) = ( 0g ‘ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ) )
66 43 45 65 rspcedvd ⊢ ( 𝜑 → ∃ 𝑤 ∈ ℤ ( 𝐽 ‘ 𝑤 ) = ( 0g ‘ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ) )
67 41 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℤ ) → ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ∈ Grp )
68 simpr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℤ ) → 𝑗 ∈ ℤ )
69 57 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℤ ) → 𝑀 ∈ ( Base ‘ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ) )
70 58 53 67 68 69 mulgcld ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℤ ) → ( 𝑗 ( .g ‘ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ) 𝑀 ) ∈ ( Base ‘ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ) )
71 70 20 fmptd ⊢ ( 𝜑 → 𝐽 : ℤ ⟶ ( Base ‘ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ) )
72 71 ffnd ⊢ ( 𝜑 → 𝐽 Fn ℤ )
73 fvelrnb ⊢ ( 𝐽 Fn ℤ → ( ( 0g ‘ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ) ∈ ran 𝐽 ↔ ∃ 𝑤 ∈ ℤ ( 𝐽 ‘ 𝑤 ) = ( 0g ‘ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ) ) )
74 72 73 syl ⊢ ( 𝜑 → ( ( 0g ‘ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ) ∈ ran 𝐽 ↔ ∃ 𝑤 ∈ ℤ ( 𝐽 ‘ 𝑤 ) = ( 0g ‘ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ) ) )
75 66 74 mpbird ⊢ ( 𝜑 → ( 0g ‘ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ) ∈ ran 𝐽 )
76 71 frnd ⊢ ( 𝜑 → ran 𝐽 ⊆ ( Base ‘ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ) )
77 eqid ⊢ ( ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ↾s ran 𝐽 ) = ( ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ↾s ran 𝐽 )
78 77 58 59 ress0g ⊢ ( ( ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ∈ Mnd ∧ ( 0g ‘ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ) ∈ ran 𝐽 ∧ ran 𝐽 ⊆ ( Base ‘ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ) ) → ( 0g ‘ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ) = ( 0g ‘ ( ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ↾s ran 𝐽 ) ) )
79 42 75 76 78 syl3anc ⊢ ( 𝜑 → ( 0g ‘ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ) = ( 0g ‘ ( ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ↾s ran 𝐽 ) ) )
80 79 sneqd ⊢ ( 𝜑 → { ( 0g ‘ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ) } = { ( 0g ‘ ( ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ↾s ran 𝐽 ) ) } )
81 80 imaeq2d ⊢ ( 𝜑 → ( ◡ 𝐽 “ { ( 0g ‘ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ) } ) = ( ◡ 𝐽 “ { ( 0g ‘ ( ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ↾s ran 𝐽 ) ) } ) )
82 38 81 eqtr2d ⊢ ( 𝜑 → ( ◡ 𝐽 “ { ( 0g ‘ ( ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ↾s ran 𝐽 ) ) } ) = ( ( RSpan ‘ ℤring ) ‘ { 𝑅 } ) )
83 82 oveq2d ⊢ ( 𝜑 → ( ℤring ~QG ( ◡ 𝐽 “ { ( 0g ‘ ( ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ↾s ran 𝐽 ) ) } ) ) = ( ℤring ~QG ( ( RSpan ‘ ℤring ) ‘ { 𝑅 } ) ) )
84 83 eceq2d ⊢ ( 𝜑 → [ 𝑑 ] ( ℤring ~QG ( ◡ 𝐽 “ { ( 0g ‘ ( ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ↾s ran 𝐽 ) ) } ) ) = [ 𝑑 ] ( ℤring ~QG ( ( RSpan ‘ ℤring ) ‘ { 𝑅 } ) ) )
85 84 mpteq2dv ⊢ ( 𝜑 → ( 𝑑 ∈ ℤ ↦ [ 𝑑 ] ( ℤring ~QG ( ◡ 𝐽 “ { ( 0g ‘ ( ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ↾s ran 𝐽 ) ) } ) ) ) = ( 𝑑 ∈ ℤ ↦ [ 𝑑 ] ( ℤring ~QG ( ( RSpan ‘ ℤring ) ‘ { 𝑅 } ) ) ) )
86 eqid ⊢ ( ℤring ~QG ( ( RSpan ‘ ℤring ) ‘ { 𝑅 } ) ) = ( ℤring ~QG ( ( RSpan ‘ ℤring ) ‘ { 𝑅 } ) )
87 eqid ⊢ ( ℤ/nℤ ‘ 𝑅 ) = ( ℤ/nℤ ‘ 𝑅 )
88 37 86 87 13 znzrh2 ⊢ ( 𝑅 ∈ ℕ0 → 𝐿 = ( 𝑑 ∈ ℤ ↦ [ 𝑑 ] ( ℤring ~QG ( ( RSpan ‘ ℤring ) ‘ { 𝑅 } ) ) ) )
89 52 88 syl ⊢ ( 𝜑 → 𝐿 = ( 𝑑 ∈ ℤ ↦ [ 𝑑 ] ( ℤring ~QG ( ( RSpan ‘ ℤring ) ‘ { 𝑅 } ) ) ) )
90 89 eqcomd ⊢ ( 𝜑 → ( 𝑑 ∈ ℤ ↦ [ 𝑑 ] ( ℤring ~QG ( ( RSpan ‘ ℤring ) ‘ { 𝑅 } ) ) ) = 𝐿 )
91 85 90 eqtrd ⊢ ( 𝜑 → ( 𝑑 ∈ ℤ ↦ [ 𝑑 ] ( ℤring ~QG ( ◡ 𝐽 “ { ( 0g ‘ ( ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ↾s ran 𝐽 ) ) } ) ) ) = 𝐿 )
92 91 coeq2d ⊢ ( 𝜑 → ( 𝑋 ∘ ( 𝑑 ∈ ℤ ↦ [ 𝑑 ] ( ℤring ~QG ( ◡ 𝐽 “ { ( 0g ‘ ( ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ↾s ran 𝐽 ) ) } ) ) ) ) = ( 𝑋 ∘ 𝐿 ) )
93 36 92 eqtrd ⊢ ( 𝜑 → 𝐽 = ( 𝑋 ∘ 𝐿 ) )
94 93 coeq2d ⊢ ( 𝜑 → ( ◡ 𝑋 ∘ 𝐽 ) = ( ◡ 𝑋 ∘ ( 𝑋 ∘ 𝐿 ) ) )
95 coass ⊢ ( ( ◡ 𝑋 ∘ 𝑋 ) ∘ 𝐿 ) = ( ◡ 𝑋 ∘ ( 𝑋 ∘ 𝐿 ) )
96 95 eqcomi ⊢ ( ◡ 𝑋 ∘ ( 𝑋 ∘ 𝐿 ) ) = ( ( ◡ 𝑋 ∘ 𝑋 ) ∘ 𝐿 )
97 94 96 eqtrdi ⊢ ( 𝜑 → ( ◡ 𝑋 ∘ 𝐽 ) = ( ( ◡ 𝑋 ∘ 𝑋 ) ∘ 𝐿 ) )
98 77 58 ressbas2 ⊢ ( ran 𝐽 ⊆ ( Base ‘ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ) → ran 𝐽 = ( Base ‘ ( ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ↾s ran 𝐽 ) ) )
99 76 98 syl ⊢ ( 𝜑 → ran 𝐽 = ( Base ‘ ( ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ↾s ran 𝐽 ) ) )
100 23 28 29 30 22 99 ghmqusker ⊢ ( 𝜑 → 𝑋 ∈ ( ( ℤring /s ( ℤring ~QG ( ◡ 𝐽 “ { ( 0g ‘ ( ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ↾s ran 𝐽 ) ) } ) ) ) GrpIso ( ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ↾s ran 𝐽 ) ) )
101 eqid ⊢ ( Base ‘ ( ℤring /s ( ℤring ~QG ( ◡ 𝐽 “ { ( 0g ‘ ( ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ↾s ran 𝐽 ) ) } ) ) ) ) = ( Base ‘ ( ℤring /s ( ℤring ~QG ( ◡ 𝐽 “ { ( 0g ‘ ( ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ↾s ran 𝐽 ) ) } ) ) ) )
102 eqid ⊢ ( Base ‘ ( ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ↾s ran 𝐽 ) ) = ( Base ‘ ( ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ↾s ran 𝐽 ) )
103 101 102 gimf1o ⊢ ( 𝑋 ∈ ( ( ℤring /s ( ℤring ~QG ( ◡ 𝐽 “ { ( 0g ‘ ( ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ↾s ran 𝐽 ) ) } ) ) ) GrpIso ( ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ↾s ran 𝐽 ) ) → 𝑋 : ( Base ‘ ( ℤring /s ( ℤring ~QG ( ◡ 𝐽 “ { ( 0g ‘ ( ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ↾s ran 𝐽 ) ) } ) ) ) ) –1-1-onto→ ( Base ‘ ( ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ↾s ran 𝐽 ) ) )
104 100 103 syl ⊢ ( 𝜑 → 𝑋 : ( Base ‘ ( ℤring /s ( ℤring ~QG ( ◡ 𝐽 “ { ( 0g ‘ ( ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ↾s ran 𝐽 ) ) } ) ) ) ) –1-1-onto→ ( Base ‘ ( ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ↾s ran 𝐽 ) ) )
105 f1ococnv1 ⊢ ( 𝑋 : ( Base ‘ ( ℤring /s ( ℤring ~QG ( ◡ 𝐽 “ { ( 0g ‘ ( ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ↾s ran 𝐽 ) ) } ) ) ) ) –1-1-onto→ ( Base ‘ ( ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ↾s ran 𝐽 ) ) → ( ◡ 𝑋 ∘ 𝑋 ) = ( I ↾ ( Base ‘ ( ℤring /s ( ℤring ~QG ( ◡ 𝐽 “ { ( 0g ‘ ( ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ↾s ran 𝐽 ) ) } ) ) ) ) ) )
106 104 105 syl ⊢ ( 𝜑 → ( ◡ 𝑋 ∘ 𝑋 ) = ( I ↾ ( Base ‘ ( ℤring /s ( ℤring ~QG ( ◡ 𝐽 “ { ( 0g ‘ ( ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ↾s ran 𝐽 ) ) } ) ) ) ) ) )
107 106 coeq1d ⊢ ( 𝜑 → ( ( ◡ 𝑋 ∘ 𝑋 ) ∘ 𝐿 ) = ( ( I ↾ ( Base ‘ ( ℤring /s ( ℤring ~QG ( ◡ 𝐽 “ { ( 0g ‘ ( ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ↾s ran 𝐽 ) ) } ) ) ) ) ) ∘ 𝐿 ) )
108 87 zncrng ⊢ ( 𝑅 ∈ ℕ0 → ( ℤ/nℤ ‘ 𝑅 ) ∈ CRing )
109 52 108 syl ⊢ ( 𝜑 → ( ℤ/nℤ ‘ 𝑅 ) ∈ CRing )
110 crngring ⊢ ( ( ℤ/nℤ ‘ 𝑅 ) ∈ CRing → ( ℤ/nℤ ‘ 𝑅 ) ∈ Ring )
111 13 zrhrhm ⊢ ( ( ℤ/nℤ ‘ 𝑅 ) ∈ Ring → 𝐿 ∈ ( ℤring RingHom ( ℤ/nℤ ‘ 𝑅 ) ) )
112 eqid ⊢ ( Base ‘ ( ℤ/nℤ ‘ 𝑅 ) ) = ( Base ‘ ( ℤ/nℤ ‘ 𝑅 ) )
113 31 112 rhmf ⊢ ( 𝐿 ∈ ( ℤring RingHom ( ℤ/nℤ ‘ 𝑅 ) ) → 𝐿 : ℤ ⟶ ( Base ‘ ( ℤ/nℤ ‘ 𝑅 ) ) )
114 109 110 111 113 4syl ⊢ ( 𝜑 → 𝐿 : ℤ ⟶ ( Base ‘ ( ℤ/nℤ ‘ 𝑅 ) ) )
115 eqid ⊢ ( ℤring /s ( ℤring ~QG ( ( RSpan ‘ ℤring ) ‘ { 𝑅 } ) ) ) = ( ℤring /s ( ℤring ~QG ( ( RSpan ‘ ℤring ) ‘ { 𝑅 } ) ) )
116 37 115 87 znbas2 ⊢ ( 𝑅 ∈ ℕ0 → ( Base ‘ ( ℤring /s ( ℤring ~QG ( ( RSpan ‘ ℤring ) ‘ { 𝑅 } ) ) ) ) = ( Base ‘ ( ℤ/nℤ ‘ 𝑅 ) ) )
117 52 116 syl ⊢ ( 𝜑 → ( Base ‘ ( ℤring /s ( ℤring ~QG ( ( RSpan ‘ ℤring ) ‘ { 𝑅 } ) ) ) ) = ( Base ‘ ( ℤ/nℤ ‘ 𝑅 ) ) )
118 117 feq3d ⊢ ( 𝜑 → ( 𝐿 : ℤ ⟶ ( Base ‘ ( ℤring /s ( ℤring ~QG ( ( RSpan ‘ ℤring ) ‘ { 𝑅 } ) ) ) ) ↔ 𝐿 : ℤ ⟶ ( Base ‘ ( ℤ/nℤ ‘ 𝑅 ) ) ) )
119 114 118 mpbird ⊢ ( 𝜑 → 𝐿 : ℤ ⟶ ( Base ‘ ( ℤring /s ( ℤring ~QG ( ( RSpan ‘ ℤring ) ‘ { 𝑅 } ) ) ) ) )
120 82 eqcomd ⊢ ( 𝜑 → ( ( RSpan ‘ ℤring ) ‘ { 𝑅 } ) = ( ◡ 𝐽 “ { ( 0g ‘ ( ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ↾s ran 𝐽 ) ) } ) )
121 120 oveq2d ⊢ ( 𝜑 → ( ℤring ~QG ( ( RSpan ‘ ℤring ) ‘ { 𝑅 } ) ) = ( ℤring ~QG ( ◡ 𝐽 “ { ( 0g ‘ ( ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ↾s ran 𝐽 ) ) } ) ) )
122 121 oveq2d ⊢ ( 𝜑 → ( ℤring /s ( ℤring ~QG ( ( RSpan ‘ ℤring ) ‘ { 𝑅 } ) ) ) = ( ℤring /s ( ℤring ~QG ( ◡ 𝐽 “ { ( 0g ‘ ( ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ↾s ran 𝐽 ) ) } ) ) ) )
123 122 fveq2d ⊢ ( 𝜑 → ( Base ‘ ( ℤring /s ( ℤring ~QG ( ( RSpan ‘ ℤring ) ‘ { 𝑅 } ) ) ) ) = ( Base ‘ ( ℤring /s ( ℤring ~QG ( ◡ 𝐽 “ { ( 0g ‘ ( ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ↾s ran 𝐽 ) ) } ) ) ) ) )
124 123 feq3d ⊢ ( 𝜑 → ( 𝐿 : ℤ ⟶ ( Base ‘ ( ℤring /s ( ℤring ~QG ( ( RSpan ‘ ℤring ) ‘ { 𝑅 } ) ) ) ) ↔ 𝐿 : ℤ ⟶ ( Base ‘ ( ℤring /s ( ℤring ~QG ( ◡ 𝐽 “ { ( 0g ‘ ( ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ↾s ran 𝐽 ) ) } ) ) ) ) ) )
125 119 124 mpbid ⊢ ( 𝜑 → 𝐿 : ℤ ⟶ ( Base ‘ ( ℤring /s ( ℤring ~QG ( ◡ 𝐽 “ { ( 0g ‘ ( ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ↾s ran 𝐽 ) ) } ) ) ) ) )
126 fcoi2 ⊢ ( 𝐿 : ℤ ⟶ ( Base ‘ ( ℤring /s ( ℤring ~QG ( ◡ 𝐽 “ { ( 0g ‘ ( ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ↾s ran 𝐽 ) ) } ) ) ) ) → ( ( I ↾ ( Base ‘ ( ℤring /s ( ℤring ~QG ( ◡ 𝐽 “ { ( 0g ‘ ( ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ↾s ran 𝐽 ) ) } ) ) ) ) ) ∘ 𝐿 ) = 𝐿 )
127 125 126 syl ⊢ ( 𝜑 → ( ( I ↾ ( Base ‘ ( ℤring /s ( ℤring ~QG ( ◡ 𝐽 “ { ( 0g ‘ ( ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ↾s ran 𝐽 ) ) } ) ) ) ) ) ∘ 𝐿 ) = 𝐿 )
128 107 127 eqtrd ⊢ ( 𝜑 → ( ( ◡ 𝑋 ∘ 𝑋 ) ∘ 𝐿 ) = 𝐿 )
129 97 128 eqtr2d ⊢ ( 𝜑 → 𝐿 = ( ◡ 𝑋 ∘ 𝐽 ) )
130 129 imaeq1d ⊢ ( 𝜑 → ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) = ( ( ◡ 𝑋 ∘ 𝐽 ) “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) )
131 imaco ⊢ ( ( ◡ 𝑋 ∘ 𝐽 ) “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) = ( ◡ 𝑋 “ ( 𝐽 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) )
132 131 a1i ⊢ ( 𝜑 → ( ( ◡ 𝑋 ∘ 𝐽 ) “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) = ( ◡ 𝑋 “ ( 𝐽 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) )
133 130 132 eqtrd ⊢ ( 𝜑 → ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) = ( ◡ 𝑋 “ ( 𝐽 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) )
134 133 fveq2d ⊢ ( 𝜑 → ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) = ( ♯ ‘ ( ◡ 𝑋 “ ( 𝐽 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) )
135 simplll ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝐽 “ ℤ ) ) ∧ 𝑢 ∈ ℤ ) ∧ ( 𝐽 ‘ 𝑢 ) = 𝑤 ) → 𝜑 )
136 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝐽 “ ℤ ) ) ∧ 𝑢 ∈ ℤ ) ∧ ( 𝐽 ‘ 𝑢 ) = 𝑤 ) → 𝑢 ∈ ℤ )
137 135 136 jca ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝐽 “ ℤ ) ) ∧ 𝑢 ∈ ℤ ) ∧ ( 𝐽 ‘ 𝑢 ) = 𝑤 ) → ( 𝜑 ∧ 𝑢 ∈ ℤ ) )
138 simplr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ℤ ) ∧ 𝑦 ∈ ℤ ) ∧ 𝑧 ∈ ( 0 ... ( 𝑅 − 1 ) ) ) ∧ 𝑢 = ( ( 𝑦 · 𝑅 ) + 𝑧 ) ) → 𝑧 ∈ ( 0 ... ( 𝑅 − 1 ) ) )
139 simpr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ℤ ) ∧ 𝑦 ∈ ℤ ) ∧ 𝑧 ∈ ( 0 ... ( 𝑅 − 1 ) ) ) ∧ 𝑢 = ( ( 𝑦 · 𝑅 ) + 𝑧 ) ) ∧ 𝑣 = 𝑧 ) → 𝑣 = 𝑧 )
140 139 fveqeq2d ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ℤ ) ∧ 𝑦 ∈ ℤ ) ∧ 𝑧 ∈ ( 0 ... ( 𝑅 − 1 ) ) ) ∧ 𝑢 = ( ( 𝑦 · 𝑅 ) + 𝑧 ) ) ∧ 𝑣 = 𝑧 ) → ( ( 𝐽 ‘ 𝑣 ) = ( 𝐽 ‘ 𝑢 ) ↔ ( 𝐽 ‘ 𝑧 ) = ( 𝐽 ‘ 𝑢 ) ) )
141 20 a1i ⊢ ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ℤ ) ∧ 𝑦 ∈ ℤ ) ∧ 𝑧 ∈ ( 0 ... ( 𝑅 − 1 ) ) ) ∧ 𝑢 = ( ( 𝑦 · 𝑅 ) + 𝑧 ) ) → 𝐽 = ( 𝑗 ∈ ℤ ↦ ( 𝑗 ( .g ‘ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ) 𝑀 ) ) )
142 simpr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ℤ ) ∧ 𝑦 ∈ ℤ ) ∧ 𝑧 ∈ ( 0 ... ( 𝑅 − 1 ) ) ) ∧ 𝑢 = ( ( 𝑦 · 𝑅 ) + 𝑧 ) ) ∧ 𝑗 = 𝑧 ) → 𝑗 = 𝑧 )
143 142 oveq1d ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ℤ ) ∧ 𝑦 ∈ ℤ ) ∧ 𝑧 ∈ ( 0 ... ( 𝑅 − 1 ) ) ) ∧ 𝑢 = ( ( 𝑦 · 𝑅 ) + 𝑧 ) ) ∧ 𝑗 = 𝑧 ) → ( 𝑗 ( .g ‘ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ) 𝑀 ) = ( 𝑧 ( .g ‘ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ) 𝑀 ) )
144 fzssz ⊢ ( 0 ... ( 𝑅 − 1 ) ) ⊆ ℤ
145 144 138 sselid ⊢ ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ℤ ) ∧ 𝑦 ∈ ℤ ) ∧ 𝑧 ∈ ( 0 ... ( 𝑅 − 1 ) ) ) ∧ 𝑢 = ( ( 𝑦 · 𝑅 ) + 𝑧 ) ) → 𝑧 ∈ ℤ )
146 ovexd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ℤ ) ∧ 𝑦 ∈ ℤ ) ∧ 𝑧 ∈ ( 0 ... ( 𝑅 − 1 ) ) ) ∧ 𝑢 = ( ( 𝑦 · 𝑅 ) + 𝑧 ) ) → ( 𝑧 ( .g ‘ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ) 𝑀 ) ∈ V )
147 141 143 145 146 fvmptd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ℤ ) ∧ 𝑦 ∈ ℤ ) ∧ 𝑧 ∈ ( 0 ... ( 𝑅 − 1 ) ) ) ∧ 𝑢 = ( ( 𝑦 · 𝑅 ) + 𝑧 ) ) → ( 𝐽 ‘ 𝑧 ) = ( 𝑧 ( .g ‘ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ) 𝑀 ) )
148 simpr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ℤ ) ∧ 𝑦 ∈ ℤ ) ∧ 𝑧 ∈ ( 0 ... ( 𝑅 − 1 ) ) ) ∧ 𝑢 = ( ( 𝑦 · 𝑅 ) + 𝑧 ) ) ∧ 𝑗 = 𝑢 ) → 𝑗 = 𝑢 )
149 148 oveq1d ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ℤ ) ∧ 𝑦 ∈ ℤ ) ∧ 𝑧 ∈ ( 0 ... ( 𝑅 − 1 ) ) ) ∧ 𝑢 = ( ( 𝑦 · 𝑅 ) + 𝑧 ) ) ∧ 𝑗 = 𝑢 ) → ( 𝑗 ( .g ‘ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ) 𝑀 ) = ( 𝑢 ( .g ‘ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ) 𝑀 ) )
150 simpr ⊢ ( ( 𝜑 ∧ 𝑢 ∈ ℤ ) → 𝑢 ∈ ℤ )
151 150 ad3antrrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ℤ ) ∧ 𝑦 ∈ ℤ ) ∧ 𝑧 ∈ ( 0 ... ( 𝑅 − 1 ) ) ) ∧ 𝑢 = ( ( 𝑦 · 𝑅 ) + 𝑧 ) ) → 𝑢 ∈ ℤ )
152 ovexd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ℤ ) ∧ 𝑦 ∈ ℤ ) ∧ 𝑧 ∈ ( 0 ... ( 𝑅 − 1 ) ) ) ∧ 𝑢 = ( ( 𝑦 · 𝑅 ) + 𝑧 ) ) → ( 𝑢 ( .g ‘ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ) 𝑀 ) ∈ V )
153 141 149 151 152 fvmptd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ℤ ) ∧ 𝑦 ∈ ℤ ) ∧ 𝑧 ∈ ( 0 ... ( 𝑅 − 1 ) ) ) ∧ 𝑢 = ( ( 𝑦 · 𝑅 ) + 𝑧 ) ) → ( 𝐽 ‘ 𝑢 ) = ( 𝑢 ( .g ‘ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ) 𝑀 ) )
154 simpr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ℤ ) ∧ 𝑦 ∈ ℤ ) ∧ 𝑧 ∈ ( 0 ... ( 𝑅 − 1 ) ) ) ∧ 𝑢 = ( ( 𝑦 · 𝑅 ) + 𝑧 ) ) → 𝑢 = ( ( 𝑦 · 𝑅 ) + 𝑧 ) )
155 154 oveq1d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ℤ ) ∧ 𝑦 ∈ ℤ ) ∧ 𝑧 ∈ ( 0 ... ( 𝑅 − 1 ) ) ) ∧ 𝑢 = ( ( 𝑦 · 𝑅 ) + 𝑧 ) ) → ( 𝑢 ( .g ‘ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ) 𝑀 ) = ( ( ( 𝑦 · 𝑅 ) + 𝑧 ) ( .g ‘ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ) 𝑀 ) )
156 41 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ℤ ) ∧ 𝑦 ∈ ℤ ) ∧ 𝑧 ∈ ( 0 ... ( 𝑅 − 1 ) ) ) → ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ∈ Grp )
157 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ℤ ) ∧ 𝑦 ∈ ℤ ) ∧ 𝑧 ∈ ( 0 ... ( 𝑅 − 1 ) ) ) → 𝑦 ∈ ℤ )
158 5 adantr ⊢ ( ( 𝜑 ∧ 𝑢 ∈ ℤ ) → 𝑅 ∈ ℕ )
159 158 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ℤ ) ∧ 𝑦 ∈ ℤ ) ∧ 𝑧 ∈ ( 0 ... ( 𝑅 − 1 ) ) ) → 𝑅 ∈ ℕ )
160 159 nnzd ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ℤ ) ∧ 𝑦 ∈ ℤ ) ∧ 𝑧 ∈ ( 0 ... ( 𝑅 − 1 ) ) ) → 𝑅 ∈ ℤ )
161 157 160 zmulcld ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ℤ ) ∧ 𝑦 ∈ ℤ ) ∧ 𝑧 ∈ ( 0 ... ( 𝑅 − 1 ) ) ) → ( 𝑦 · 𝑅 ) ∈ ℤ )
162 144 sseli ⊢ ( 𝑧 ∈ ( 0 ... ( 𝑅 − 1 ) ) → 𝑧 ∈ ℤ )
163 162 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ℤ ) ∧ 𝑦 ∈ ℤ ) ∧ 𝑧 ∈ ( 0 ... ( 𝑅 − 1 ) ) ) → 𝑧 ∈ ℤ )
164 57 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ℤ ) ∧ 𝑦 ∈ ℤ ) ∧ 𝑧 ∈ ( 0 ... ( 𝑅 − 1 ) ) ) → 𝑀 ∈ ( Base ‘ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ) )
165 161 163 164 3jca ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ℤ ) ∧ 𝑦 ∈ ℤ ) ∧ 𝑧 ∈ ( 0 ... ( 𝑅 − 1 ) ) ) → ( ( 𝑦 · 𝑅 ) ∈ ℤ ∧ 𝑧 ∈ ℤ ∧ 𝑀 ∈ ( Base ‘ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ) ) )
166 eqid ⊢ ( +g ‘ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ) = ( +g ‘ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) )
167 58 53 166 mulgdir ⊢ ( ( ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ∈ Grp ∧ ( ( 𝑦 · 𝑅 ) ∈ ℤ ∧ 𝑧 ∈ ℤ ∧ 𝑀 ∈ ( Base ‘ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ) ) ) → ( ( ( 𝑦 · 𝑅 ) + 𝑧 ) ( .g ‘ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ) 𝑀 ) = ( ( ( 𝑦 · 𝑅 ) ( .g ‘ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ) 𝑀 ) ( +g ‘ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ) ( 𝑧 ( .g ‘ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ) 𝑀 ) ) )
168 156 165 167 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ℤ ) ∧ 𝑦 ∈ ℤ ) ∧ 𝑧 ∈ ( 0 ... ( 𝑅 − 1 ) ) ) → ( ( ( 𝑦 · 𝑅 ) + 𝑧 ) ( .g ‘ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ) 𝑀 ) = ( ( ( 𝑦 · 𝑅 ) ( .g ‘ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ) 𝑀 ) ( +g ‘ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ) ( 𝑧 ( .g ‘ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ) 𝑀 ) ) )
169 157 160 164 3jca ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ℤ ) ∧ 𝑦 ∈ ℤ ) ∧ 𝑧 ∈ ( 0 ... ( 𝑅 − 1 ) ) ) → ( 𝑦 ∈ ℤ ∧ 𝑅 ∈ ℤ ∧ 𝑀 ∈ ( Base ‘ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ) ) )
170 58 53 mulgass ⊢ ( ( ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ∈ Grp ∧ ( 𝑦 ∈ ℤ ∧ 𝑅 ∈ ℤ ∧ 𝑀 ∈ ( Base ‘ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ) ) ) → ( ( 𝑦 · 𝑅 ) ( .g ‘ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ) 𝑀 ) = ( 𝑦 ( .g ‘ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ) ( 𝑅 ( .g ‘ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ) 𝑀 ) ) )
171 156 169 170 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ℤ ) ∧ 𝑦 ∈ ℤ ) ∧ 𝑧 ∈ ( 0 ... ( 𝑅 − 1 ) ) ) → ( ( 𝑦 · 𝑅 ) ( .g ‘ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ) 𝑀 ) = ( 𝑦 ( .g ‘ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ) ( 𝑅 ( .g ‘ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ) 𝑀 ) ) )
172 56 simp2d ⊢ ( 𝜑 → ( 𝑅 ( .g ‘ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ) 𝑀 ) = ( 0g ‘ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ) )
173 172 adantr ⊢ ( ( 𝜑 ∧ 𝑢 ∈ ℤ ) → ( 𝑅 ( .g ‘ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ) 𝑀 ) = ( 0g ‘ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ) )
174 173 adantr ⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ℤ ) ∧ 𝑦 ∈ ℤ ) → ( 𝑅 ( .g ‘ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ) 𝑀 ) = ( 0g ‘ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ) )
175 174 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ℤ ) ∧ 𝑦 ∈ ℤ ) ∧ 𝑧 ∈ ( 0 ... ( 𝑅 − 1 ) ) ) → ( 𝑅 ( .g ‘ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ) 𝑀 ) = ( 0g ‘ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ) )
176 175 oveq2d ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ℤ ) ∧ 𝑦 ∈ ℤ ) ∧ 𝑧 ∈ ( 0 ... ( 𝑅 − 1 ) ) ) → ( 𝑦 ( .g ‘ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ) ( 𝑅 ( .g ‘ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ) 𝑀 ) ) = ( 𝑦 ( .g ‘ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ) ( 0g ‘ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ) ) )
177 58 53 59 mulgz ⊢ ( ( ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ∈ Grp ∧ 𝑦 ∈ ℤ ) → ( 𝑦 ( .g ‘ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ) ( 0g ‘ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ) ) = ( 0g ‘ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ) )
178 156 157 177 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ℤ ) ∧ 𝑦 ∈ ℤ ) ∧ 𝑧 ∈ ( 0 ... ( 𝑅 − 1 ) ) ) → ( 𝑦 ( .g ‘ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ) ( 0g ‘ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ) ) = ( 0g ‘ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ) )
179 176 178 eqtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ℤ ) ∧ 𝑦 ∈ ℤ ) ∧ 𝑧 ∈ ( 0 ... ( 𝑅 − 1 ) ) ) → ( 𝑦 ( .g ‘ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ) ( 𝑅 ( .g ‘ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ) 𝑀 ) ) = ( 0g ‘ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ) )
180 171 179 eqtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ℤ ) ∧ 𝑦 ∈ ℤ ) ∧ 𝑧 ∈ ( 0 ... ( 𝑅 − 1 ) ) ) → ( ( 𝑦 · 𝑅 ) ( .g ‘ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ) 𝑀 ) = ( 0g ‘ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ) )
181 180 oveq1d ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ℤ ) ∧ 𝑦 ∈ ℤ ) ∧ 𝑧 ∈ ( 0 ... ( 𝑅 − 1 ) ) ) → ( ( ( 𝑦 · 𝑅 ) ( .g ‘ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ) 𝑀 ) ( +g ‘ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ) ( 𝑧 ( .g ‘ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ) 𝑀 ) ) = ( ( 0g ‘ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ) ( +g ‘ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ) ( 𝑧 ( .g ‘ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ) 𝑀 ) ) )
182 58 53 156 163 164 mulgcld ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ℤ ) ∧ 𝑦 ∈ ℤ ) ∧ 𝑧 ∈ ( 0 ... ( 𝑅 − 1 ) ) ) → ( 𝑧 ( .g ‘ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ) 𝑀 ) ∈ ( Base ‘ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ) )
183 58 166 59 156 182 grplidd ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ℤ ) ∧ 𝑦 ∈ ℤ ) ∧ 𝑧 ∈ ( 0 ... ( 𝑅 − 1 ) ) ) → ( ( 0g ‘ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ) ( +g ‘ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ) ( 𝑧 ( .g ‘ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ) 𝑀 ) ) = ( 𝑧 ( .g ‘ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ) 𝑀 ) )
184 181 183 eqtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ℤ ) ∧ 𝑦 ∈ ℤ ) ∧ 𝑧 ∈ ( 0 ... ( 𝑅 − 1 ) ) ) → ( ( ( 𝑦 · 𝑅 ) ( .g ‘ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ) 𝑀 ) ( +g ‘ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ) ( 𝑧 ( .g ‘ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ) 𝑀 ) ) = ( 𝑧 ( .g ‘ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ) 𝑀 ) )
185 168 184 eqtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑢 ∈ ℤ ) ∧ 𝑦 ∈ ℤ ) ∧ 𝑧 ∈ ( 0 ... ( 𝑅 − 1 ) ) ) → ( ( ( 𝑦 · 𝑅 ) + 𝑧 ) ( .g ‘ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ) 𝑀 ) = ( 𝑧 ( .g ‘ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ) 𝑀 ) )
186 185 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ℤ ) ∧ 𝑦 ∈ ℤ ) ∧ 𝑧 ∈ ( 0 ... ( 𝑅 − 1 ) ) ) ∧ 𝑢 = ( ( 𝑦 · 𝑅 ) + 𝑧 ) ) → ( ( ( 𝑦 · 𝑅 ) + 𝑧 ) ( .g ‘ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ) 𝑀 ) = ( 𝑧 ( .g ‘ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ) 𝑀 ) )
187 155 186 eqtrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ℤ ) ∧ 𝑦 ∈ ℤ ) ∧ 𝑧 ∈ ( 0 ... ( 𝑅 − 1 ) ) ) ∧ 𝑢 = ( ( 𝑦 · 𝑅 ) + 𝑧 ) ) → ( 𝑢 ( .g ‘ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ) 𝑀 ) = ( 𝑧 ( .g ‘ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ) 𝑀 ) )
188 153 187 eqtr2d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ℤ ) ∧ 𝑦 ∈ ℤ ) ∧ 𝑧 ∈ ( 0 ... ( 𝑅 − 1 ) ) ) ∧ 𝑢 = ( ( 𝑦 · 𝑅 ) + 𝑧 ) ) → ( 𝑧 ( .g ‘ ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ) 𝑀 ) = ( 𝐽 ‘ 𝑢 ) )
189 147 188 eqtrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ℤ ) ∧ 𝑦 ∈ ℤ ) ∧ 𝑧 ∈ ( 0 ... ( 𝑅 − 1 ) ) ) ∧ 𝑢 = ( ( 𝑦 · 𝑅 ) + 𝑧 ) ) → ( 𝐽 ‘ 𝑧 ) = ( 𝐽 ‘ 𝑢 ) )
190 138 140 189 rspcedvd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑢 ∈ ℤ ) ∧ 𝑦 ∈ ℤ ) ∧ 𝑧 ∈ ( 0 ... ( 𝑅 − 1 ) ) ) ∧ 𝑢 = ( ( 𝑦 · 𝑅 ) + 𝑧 ) ) → ∃ 𝑣 ∈ ( 0 ... ( 𝑅 − 1 ) ) ( 𝐽 ‘ 𝑣 ) = ( 𝐽 ‘ 𝑢 ) )
191 150 158 remexz ⊢ ( ( 𝜑 ∧ 𝑢 ∈ ℤ ) → ∃ 𝑦 ∈ ℤ ∃ 𝑧 ∈ ( 0 ... ( 𝑅 − 1 ) ) 𝑢 = ( ( 𝑦 · 𝑅 ) + 𝑧 ) )
192 190 191 r19.29vva ⊢ ( ( 𝜑 ∧ 𝑢 ∈ ℤ ) → ∃ 𝑣 ∈ ( 0 ... ( 𝑅 − 1 ) ) ( 𝐽 ‘ 𝑣 ) = ( 𝐽 ‘ 𝑢 ) )
193 137 192 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝐽 “ ℤ ) ) ∧ 𝑢 ∈ ℤ ) ∧ ( 𝐽 ‘ 𝑢 ) = 𝑤 ) → ∃ 𝑣 ∈ ( 0 ... ( 𝑅 − 1 ) ) ( 𝐽 ‘ 𝑣 ) = ( 𝐽 ‘ 𝑢 ) )
194 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝐽 “ ℤ ) ) ∧ 𝑢 ∈ ℤ ) ∧ ( 𝐽 ‘ 𝑢 ) = 𝑤 ) → ( 𝐽 ‘ 𝑢 ) = 𝑤 )
195 194 eqcomd ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝐽 “ ℤ ) ) ∧ 𝑢 ∈ ℤ ) ∧ ( 𝐽 ‘ 𝑢 ) = 𝑤 ) → 𝑤 = ( 𝐽 ‘ 𝑢 ) )
196 195 eqeq2d ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝐽 “ ℤ ) ) ∧ 𝑢 ∈ ℤ ) ∧ ( 𝐽 ‘ 𝑢 ) = 𝑤 ) → ( ( 𝐽 ‘ 𝑣 ) = 𝑤 ↔ ( 𝐽 ‘ 𝑣 ) = ( 𝐽 ‘ 𝑢 ) ) )
197 196 rexbidv ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝐽 “ ℤ ) ) ∧ 𝑢 ∈ ℤ ) ∧ ( 𝐽 ‘ 𝑢 ) = 𝑤 ) → ( ∃ 𝑣 ∈ ( 0 ... ( 𝑅 − 1 ) ) ( 𝐽 ‘ 𝑣 ) = 𝑤 ↔ ∃ 𝑣 ∈ ( 0 ... ( 𝑅 − 1 ) ) ( 𝐽 ‘ 𝑣 ) = ( 𝐽 ‘ 𝑢 ) ) )
198 193 197 mpbird ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝐽 “ ℤ ) ) ∧ 𝑢 ∈ ℤ ) ∧ ( 𝐽 ‘ 𝑢 ) = 𝑤 ) → ∃ 𝑣 ∈ ( 0 ... ( 𝑅 − 1 ) ) ( 𝐽 ‘ 𝑣 ) = 𝑤 )
199 ssidd ⊢ ( 𝜑 → ℤ ⊆ ℤ )
200 fvelimab ⊢ ( ( 𝐽 Fn ℤ ∧ ℤ ⊆ ℤ ) → ( 𝑤 ∈ ( 𝐽 “ ℤ ) ↔ ∃ 𝑢 ∈ ℤ ( 𝐽 ‘ 𝑢 ) = 𝑤 ) )
201 72 199 200 syl2anc ⊢ ( 𝜑 → ( 𝑤 ∈ ( 𝐽 “ ℤ ) ↔ ∃ 𝑢 ∈ ℤ ( 𝐽 ‘ 𝑢 ) = 𝑤 ) )
202 201 biimpd ⊢ ( 𝜑 → ( 𝑤 ∈ ( 𝐽 “ ℤ ) → ∃ 𝑢 ∈ ℤ ( 𝐽 ‘ 𝑢 ) = 𝑤 ) )
203 202 imp ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 𝐽 “ ℤ ) ) → ∃ 𝑢 ∈ ℤ ( 𝐽 ‘ 𝑢 ) = 𝑤 )
204 198 203 r19.29a ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 𝐽 “ ℤ ) ) → ∃ 𝑣 ∈ ( 0 ... ( 𝑅 − 1 ) ) ( 𝐽 ‘ 𝑣 ) = 𝑤 )
205 144 a1i ⊢ ( 𝜑 → ( 0 ... ( 𝑅 − 1 ) ) ⊆ ℤ )
206 fvelimab ⊢ ( ( 𝐽 Fn ℤ ∧ ( 0 ... ( 𝑅 − 1 ) ) ⊆ ℤ ) → ( 𝑤 ∈ ( 𝐽 “ ( 0 ... ( 𝑅 − 1 ) ) ) ↔ ∃ 𝑣 ∈ ( 0 ... ( 𝑅 − 1 ) ) ( 𝐽 ‘ 𝑣 ) = 𝑤 ) )
207 72 205 206 syl2anc ⊢ ( 𝜑 → ( 𝑤 ∈ ( 𝐽 “ ( 0 ... ( 𝑅 − 1 ) ) ) ↔ ∃ 𝑣 ∈ ( 0 ... ( 𝑅 − 1 ) ) ( 𝐽 ‘ 𝑣 ) = 𝑤 ) )
208 207 adantr ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 𝐽 “ ℤ ) ) → ( 𝑤 ∈ ( 𝐽 “ ( 0 ... ( 𝑅 − 1 ) ) ) ↔ ∃ 𝑣 ∈ ( 0 ... ( 𝑅 − 1 ) ) ( 𝐽 ‘ 𝑣 ) = 𝑤 ) )
209 204 208 mpbird ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 𝐽 “ ℤ ) ) → 𝑤 ∈ ( 𝐽 “ ( 0 ... ( 𝑅 − 1 ) ) ) )
210 209 ex ⊢ ( 𝜑 → ( 𝑤 ∈ ( 𝐽 “ ℤ ) → 𝑤 ∈ ( 𝐽 “ ( 0 ... ( 𝑅 − 1 ) ) ) ) )
211 210 ssrdv ⊢ ( 𝜑 → ( 𝐽 “ ℤ ) ⊆ ( 𝐽 “ ( 0 ... ( 𝑅 − 1 ) ) ) )
212 207 biimpd ⊢ ( 𝜑 → ( 𝑤 ∈ ( 𝐽 “ ( 0 ... ( 𝑅 − 1 ) ) ) → ∃ 𝑣 ∈ ( 0 ... ( 𝑅 − 1 ) ) ( 𝐽 ‘ 𝑣 ) = 𝑤 ) )
213 212 imp ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 𝐽 “ ( 0 ... ( 𝑅 − 1 ) ) ) ) → ∃ 𝑣 ∈ ( 0 ... ( 𝑅 − 1 ) ) ( 𝐽 ‘ 𝑣 ) = 𝑤 )
214 144 sseli ⊢ ( 𝑣 ∈ ( 0 ... ( 𝑅 − 1 ) ) → 𝑣 ∈ ℤ )
215 214 adantr ⊢ ( ( 𝑣 ∈ ( 0 ... ( 𝑅 − 1 ) ) ∧ ( 𝐽 ‘ 𝑣 ) = 𝑤 ) → 𝑣 ∈ ℤ )
216 215 adantl ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝐽 “ ( 0 ... ( 𝑅 − 1 ) ) ) ) ∧ ( 𝑣 ∈ ( 0 ... ( 𝑅 − 1 ) ) ∧ ( 𝐽 ‘ 𝑣 ) = 𝑤 ) ) → 𝑣 ∈ ℤ )
217 simprr ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ( 𝐽 “ ( 0 ... ( 𝑅 − 1 ) ) ) ) ∧ ( 𝑣 ∈ ( 0 ... ( 𝑅 − 1 ) ) ∧ ( 𝐽 ‘ 𝑣 ) = 𝑤 ) ) → ( 𝐽 ‘ 𝑣 ) = 𝑤 )
218 213 216 217 reximssdv ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 𝐽 “ ( 0 ... ( 𝑅 − 1 ) ) ) ) → ∃ 𝑣 ∈ ℤ ( 𝐽 ‘ 𝑣 ) = 𝑤 )
219 72 adantr ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 𝐽 “ ( 0 ... ( 𝑅 − 1 ) ) ) ) → 𝐽 Fn ℤ )
220 ssidd ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 𝐽 “ ( 0 ... ( 𝑅 − 1 ) ) ) ) → ℤ ⊆ ℤ )
221 fvelimab ⊢ ( ( 𝐽 Fn ℤ ∧ ℤ ⊆ ℤ ) → ( 𝑤 ∈ ( 𝐽 “ ℤ ) ↔ ∃ 𝑣 ∈ ℤ ( 𝐽 ‘ 𝑣 ) = 𝑤 ) )
222 219 220 221 syl2anc ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 𝐽 “ ( 0 ... ( 𝑅 − 1 ) ) ) ) → ( 𝑤 ∈ ( 𝐽 “ ℤ ) ↔ ∃ 𝑣 ∈ ℤ ( 𝐽 ‘ 𝑣 ) = 𝑤 ) )
223 218 222 mpbird ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ( 𝐽 “ ( 0 ... ( 𝑅 − 1 ) ) ) ) → 𝑤 ∈ ( 𝐽 “ ℤ ) )
224 223 ex ⊢ ( 𝜑 → ( 𝑤 ∈ ( 𝐽 “ ( 0 ... ( 𝑅 − 1 ) ) ) → 𝑤 ∈ ( 𝐽 “ ℤ ) ) )
225 224 ssrdv ⊢ ( 𝜑 → ( 𝐽 “ ( 0 ... ( 𝑅 − 1 ) ) ) ⊆ ( 𝐽 “ ℤ ) )
226 211 225 eqssd ⊢ ( 𝜑 → ( 𝐽 “ ℤ ) = ( 𝐽 “ ( 0 ... ( 𝑅 − 1 ) ) ) )
227 72 fnfund ⊢ ( 𝜑 → Fun 𝐽 )
228 fzfid ⊢ ( 𝜑 → ( 0 ... ( 𝑅 − 1 ) ) ∈ Fin )
229 imafi ⊢ ( ( Fun 𝐽 ∧ ( 0 ... ( 𝑅 − 1 ) ) ∈ Fin ) → ( 𝐽 “ ( 0 ... ( 𝑅 − 1 ) ) ) ∈ Fin )
230 227 228 229 syl2anc ⊢ ( 𝜑 → ( 𝐽 “ ( 0 ... ( 𝑅 − 1 ) ) ) ∈ Fin )
231 226 230 eqeltrd ⊢ ( 𝜑 → ( 𝐽 “ ℤ ) ∈ Fin )
232 6 4 7 12 aks6d1c2p1 ⊢ ( 𝜑 → 𝐸 : ( ℕ0 × ℕ0 ) ⟶ ℕ )
233 nnssz ⊢ ℕ ⊆ ℤ
234 233 a1i ⊢ ( 𝜑 → ℕ ⊆ ℤ )
235 232 234 jca ⊢ ( 𝜑 → ( 𝐸 : ( ℕ0 × ℕ0 ) ⟶ ℕ ∧ ℕ ⊆ ℤ ) )
236 fss ⊢ ( ( 𝐸 : ( ℕ0 × ℕ0 ) ⟶ ℕ ∧ ℕ ⊆ ℤ ) → 𝐸 : ( ℕ0 × ℕ0 ) ⟶ ℤ )
237 235 236 syl ⊢ ( 𝜑 → 𝐸 : ( ℕ0 × ℕ0 ) ⟶ ℤ )
238 237 frnd ⊢ ( 𝜑 → ran 𝐸 ⊆ ℤ )
239 232 ffnd ⊢ ( 𝜑 → 𝐸 Fn ( ℕ0 × ℕ0 ) )
240 fnima ⊢ ( 𝐸 Fn ( ℕ0 × ℕ0 ) → ( 𝐸 “ ( ℕ0 × ℕ0 ) ) = ran 𝐸 )
241 239 240 syl ⊢ ( 𝜑 → ( 𝐸 “ ( ℕ0 × ℕ0 ) ) = ran 𝐸 )
242 241 sseq1d ⊢ ( 𝜑 → ( ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ⊆ ℤ ↔ ran 𝐸 ⊆ ℤ ) )
243 238 242 mpbird ⊢ ( 𝜑 → ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ⊆ ℤ )
244 imass2 ⊢ ( ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ⊆ ℤ → ( 𝐽 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ⊆ ( 𝐽 “ ℤ ) )
245 243 244 syl ⊢ ( 𝜑 → ( 𝐽 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ⊆ ( 𝐽 “ ℤ ) )
246 231 245 ssfid ⊢ ( 𝜑 → ( 𝐽 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ∈ Fin )
247 dff1o2 ⊢ ( 𝑋 : ( Base ‘ ( ℤring /s ( ℤring ~QG ( ◡ 𝐽 “ { ( 0g ‘ ( ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ↾s ran 𝐽 ) ) } ) ) ) ) –1-1-onto→ ( Base ‘ ( ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ↾s ran 𝐽 ) ) ↔ ( 𝑋 Fn ( Base ‘ ( ℤring /s ( ℤring ~QG ( ◡ 𝐽 “ { ( 0g ‘ ( ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ↾s ran 𝐽 ) ) } ) ) ) ) ∧ Fun ◡ 𝑋 ∧ ran 𝑋 = ( Base ‘ ( ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ↾s ran 𝐽 ) ) ) )
248 247 biimpi ⊢ ( 𝑋 : ( Base ‘ ( ℤring /s ( ℤring ~QG ( ◡ 𝐽 “ { ( 0g ‘ ( ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ↾s ran 𝐽 ) ) } ) ) ) ) –1-1-onto→ ( Base ‘ ( ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ↾s ran 𝐽 ) ) → ( 𝑋 Fn ( Base ‘ ( ℤring /s ( ℤring ~QG ( ◡ 𝐽 “ { ( 0g ‘ ( ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ↾s ran 𝐽 ) ) } ) ) ) ) ∧ Fun ◡ 𝑋 ∧ ran 𝑋 = ( Base ‘ ( ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ↾s ran 𝐽 ) ) ) )
249 248 simp2d ⊢ ( 𝑋 : ( Base ‘ ( ℤring /s ( ℤring ~QG ( ◡ 𝐽 “ { ( 0g ‘ ( ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ↾s ran 𝐽 ) ) } ) ) ) ) –1-1-onto→ ( Base ‘ ( ( ( mulGrp ‘ 𝐾 ) ↾s 𝑈 ) ↾s ran 𝐽 ) ) → Fun ◡ 𝑋 )
250 104 249 syl ⊢ ( 𝜑 → Fun ◡ 𝑋 )
251 imadomfi ⊢ ( ( ( 𝐽 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ∈ Fin ∧ Fun ◡ 𝑋 ) → ( ◡ 𝑋 “ ( 𝐽 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ≼ ( 𝐽 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) )
252 246 250 251 syl2anc ⊢ ( 𝜑 → ( ◡ 𝑋 “ ( 𝐽 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ≼ ( 𝐽 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) )
253 hashdomi ⊢ ( ( ◡ 𝑋 “ ( 𝐽 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ≼ ( 𝐽 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) → ( ♯ ‘ ( ◡ 𝑋 “ ( 𝐽 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ≤ ( ♯ ‘ ( 𝐽 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) )
254 252 253 syl ⊢ ( 𝜑 → ( ♯ ‘ ( ◡ 𝑋 “ ( 𝐽 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ) ≤ ( ♯ ‘ ( 𝐽 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) )
255 134 254 eqbrtrd ⊢ ( 𝜑 → ( ♯ ‘ ( 𝐿 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) ≤ ( ♯ ‘ ( 𝐽 “ ( 𝐸 “ ( ℕ0 × ℕ0 ) ) ) ) )
256 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 255 21 aks6d1c6lem4 ⊢ ( 𝜑 → ( ( 𝐷 + 𝐴 ) C ( 𝐷 − 1 ) ) ≤ ( ♯ ‘ ( 𝐻 “ ( ℕ0 ↑m ( 0 ... 𝐴 ) ) ) ) )