Theorem aks6d1c6isolem3

Description: The preimage of a map sending a primitive root to its powers of zero is equal to the set of integers that divide R . (Contributed by metakunt, 15-May-2025)

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

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		aks6d1c6isolem3.1	⊢ 𝑆 = ( RSpan ‘ ℤring )
7		zringring	⊢ ℤring ∈ Ring
8	7	a1i	⊢ ( 𝜑 → ℤring ∈ Ring )
9	2	nnzd	⊢ ( 𝜑 → 𝐾 ∈ ℤ )
10		zringbas	⊢ ℤ = ( Base ‘ ℤring )
11		dvdsrzring	⊢ ∥ = ( ∥r ‘ ℤring )
12	10 6 11	rspsn	⊢ ( ( ℤring ∈ Ring ∧ 𝐾 ∈ ℤ ) → ( 𝑆 ‘ { 𝐾 } ) = { 𝑧 ∣ 𝐾 ∥ 𝑧 } )
13	8 9 12	syl2anc	⊢ ( 𝜑 → ( 𝑆 ‘ { 𝐾 } ) = { 𝑧 ∣ 𝐾 ∥ 𝑧 } )
14		ovexd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℤ ) → ( 𝑥 ( .g ‘ ( 𝑅 ↾s 𝑈 ) ) 𝑀 ) ∈ V )
15	14 4	fmptd	⊢ ( 𝜑 → 𝐹 : ℤ ⟶ V )
16	15	ffnd	⊢ ( 𝜑 → 𝐹 Fn ℤ )
17		fniniseg2	⊢ ( 𝐹 Fn ℤ → ( ◡ 𝐹 “ { ( 0g ‘ ( 𝑅 ↾s 𝑈 ) ) } ) = { 𝑧 ∈ ℤ ∣ ( 𝐹 ‘ 𝑧 ) = ( 0g ‘ ( 𝑅 ↾s 𝑈 ) ) } )
18	16 17	syl	⊢ ( 𝜑 → ( ◡ 𝐹 “ { ( 0g ‘ ( 𝑅 ↾s 𝑈 ) ) } ) = { 𝑧 ∈ ℤ ∣ ( 𝐹 ‘ 𝑧 ) = ( 0g ‘ ( 𝑅 ↾s 𝑈 ) ) } )
19	4	a1i	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℤ ) → 𝐹 = ( 𝑥 ∈ ℤ ↦ ( 𝑥 ( .g ‘ ( 𝑅 ↾s 𝑈 ) ) 𝑀 ) ) )
20		simpr	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℤ ) ∧ 𝑥 = 𝑧 ) → 𝑥 = 𝑧 )
21	20	oveq1d	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℤ ) ∧ 𝑥 = 𝑧 ) → ( 𝑥 ( .g ‘ ( 𝑅 ↾s 𝑈 ) ) 𝑀 ) = ( 𝑧 ( .g ‘ ( 𝑅 ↾s 𝑈 ) ) 𝑀 ) )
22		simpr	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℤ ) → 𝑧 ∈ ℤ )
23		ovexd	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℤ ) → ( 𝑧 ( .g ‘ ( 𝑅 ↾s 𝑈 ) ) 𝑀 ) ∈ V )
24	19 21 22 23	fvmptd	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℤ ) → ( 𝐹 ‘ 𝑧 ) = ( 𝑧 ( .g ‘ ( 𝑅 ↾s 𝑈 ) ) 𝑀 ) )
25	24	eqeq1d	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℤ ) → ( ( 𝐹 ‘ 𝑧 ) = ( 0g ‘ ( 𝑅 ↾s 𝑈 ) ) ↔ ( 𝑧 ( .g ‘ ( 𝑅 ↾s 𝑈 ) ) 𝑀 ) = ( 0g ‘ ( 𝑅 ↾s 𝑈 ) ) ) )
26	1	adantr	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℤ ) → 𝑅 ∈ CMnd )
27	2	adantr	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℤ ) → 𝐾 ∈ ℕ )
28	5	adantr	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℤ ) → 𝑀 ∈ ( 𝑅 PrimRoots 𝐾 ) )
29	26 27 28 3 22	primrootspoweq0	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℤ ) → ( ( 𝑧 ( .g ‘ ( 𝑅 ↾s 𝑈 ) ) 𝑀 ) = ( 0g ‘ ( 𝑅 ↾s 𝑈 ) ) ↔ 𝐾 ∥ 𝑧 ) )
30	25 29	bitrd	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℤ ) → ( ( 𝐹 ‘ 𝑧 ) = ( 0g ‘ ( 𝑅 ↾s 𝑈 ) ) ↔ 𝐾 ∥ 𝑧 ) )
31	30	rabbidva	⊢ ( 𝜑 → { 𝑧 ∈ ℤ ∣ ( 𝐹 ‘ 𝑧 ) = ( 0g ‘ ( 𝑅 ↾s 𝑈 ) ) } = { 𝑧 ∈ ℤ ∣ 𝐾 ∥ 𝑧 } )
32		df-rab	⊢ { 𝑧 ∈ ℤ ∣ 𝐾 ∥ 𝑧 } = { 𝑧 ∣ ( 𝑧 ∈ ℤ ∧ 𝐾 ∥ 𝑧 ) }
33	32	a1i	⊢ ( 𝜑 → { 𝑧 ∈ ℤ ∣ 𝐾 ∥ 𝑧 } = { 𝑧 ∣ ( 𝑧 ∈ ℤ ∧ 𝐾 ∥ 𝑧 ) } )
34		simpr	⊢ ( ( 𝑧 ∈ ℤ ∧ 𝐾 ∥ 𝑧 ) → 𝐾 ∥ 𝑧 )
35		dvdszrcl	⊢ ( 𝐾 ∥ 𝑧 → ( 𝐾 ∈ ℤ ∧ 𝑧 ∈ ℤ ) )
36	35	simprd	⊢ ( 𝐾 ∥ 𝑧 → 𝑧 ∈ ℤ )
37	36	ancri	⊢ ( 𝐾 ∥ 𝑧 → ( 𝑧 ∈ ℤ ∧ 𝐾 ∥ 𝑧 ) )
38	34 37	impbii	⊢ ( ( 𝑧 ∈ ℤ ∧ 𝐾 ∥ 𝑧 ) ↔ 𝐾 ∥ 𝑧 )
39	38	a1i	⊢ ( 𝜑 → ( ( 𝑧 ∈ ℤ ∧ 𝐾 ∥ 𝑧 ) ↔ 𝐾 ∥ 𝑧 ) )
40	39	abbidv	⊢ ( 𝜑 → { 𝑧 ∣ ( 𝑧 ∈ ℤ ∧ 𝐾 ∥ 𝑧 ) } = { 𝑧 ∣ 𝐾 ∥ 𝑧 } )
41	33 40	eqtrd	⊢ ( 𝜑 → { 𝑧 ∈ ℤ ∣ 𝐾 ∥ 𝑧 } = { 𝑧 ∣ 𝐾 ∥ 𝑧 } )
42	31 41	eqtrd	⊢ ( 𝜑 → { 𝑧 ∈ ℤ ∣ ( 𝐹 ‘ 𝑧 ) = ( 0g ‘ ( 𝑅 ↾s 𝑈 ) ) } = { 𝑧 ∣ 𝐾 ∥ 𝑧 } )
43	18 42	eqtr2d	⊢ ( 𝜑 → { 𝑧 ∣ 𝐾 ∥ 𝑧 } = ( ◡ 𝐹 “ { ( 0g ‘ ( 𝑅 ↾s 𝑈 ) ) } ) )
44	13 43	eqtrd	⊢ ( 𝜑 → ( 𝑆 ‘ { 𝐾 } ) = ( ◡ 𝐹 “ { ( 0g ‘ ( 𝑅 ↾s 𝑈 ) ) } ) )