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	$⊢ φ \to R \in CMnd$
	aks6d1c6isolem1.2	$⊢ φ \to K \in ℕ$
	aks6d1c6isolem1.3	$⊢ U = \{a \in {Base}_{R} \| \exists i \in {Base}_{R} i +_{R} a = 0_{R}\}$
	aks6d1c6isolem1.4	$⊢ F = (x \in ℤ ⟼ x \cdot_{(R ↾_{𝑠} U)} M)$
	aks6d1c6isolem1.5	$⊢ φ \to M \in (R PrimRoots K)$
	aks6d1c6isolem3.1	$⊢ S = RSpan (ℤ_{ring})$
Assertion	aks6d1c6isolem3	$⊢ φ \to S (\{K\}) = F^{-1} [\{0_{(R ↾_{𝑠} U)}\}]$

Proof

Step	Hyp	Ref	Expression
1		aks6d1c6isolem1.1	$⊢ φ \to R \in CMnd$
2		aks6d1c6isolem1.2	$⊢ φ \to K \in ℕ$
3		aks6d1c6isolem1.3	$⊢ U = \{a \in {Base}_{R} \| \exists i \in {Base}_{R} i +_{R} a = 0_{R}\}$
4		aks6d1c6isolem1.4	$⊢ F = (x \in ℤ ⟼ x \cdot_{(R ↾_{𝑠} U)} M)$
5		aks6d1c6isolem1.5	$⊢ φ \to M \in (R PrimRoots K)$
6		aks6d1c6isolem3.1	$⊢ S = RSpan (ℤ_{ring})$
7		zringring	$⊢ ℤ_{ring} \in Ring$
8	7	a1i	$⊢ φ \to ℤ_{ring} \in Ring$
9	2	nnzd	$⊢ φ \to K \in ℤ$
10		zringbas	$⊢ ℤ = {Base}_{ℤ_{ring}}$
11		dvdsrzring	$⊢ ∥ = ∥_{r} (ℤ_{ring})$
12	10 6 11	rspsn	$⊢ (ℤ_{ring} \in Ring \land K \in ℤ) \to S (\{K\}) = \{z \| K ∥ z\}$
13	8 9 12	syl2anc	$⊢ φ \to S (\{K\}) = \{z \| K ∥ z\}$
14		ovexd	$⊢ (φ \land x \in ℤ) \to x \cdot_{(R ↾_{𝑠} U)} M \in V$
15	14 4	fmptd	$⊢ φ \to F : ℤ ⟶ V$
16	15	ffnd	$⊢ φ \to F Fn ℤ$
17		fniniseg2	$⊢ F Fn ℤ \to F^{-1} [\{0_{(R ↾_{𝑠} U)}\}] = \{z \in ℤ \| F (z) = 0_{(R ↾_{𝑠} U)}\}$
18	16 17	syl	$⊢ φ \to F^{-1} [\{0_{(R ↾_{𝑠} U)}\}] = \{z \in ℤ \| F (z) = 0_{(R ↾_{𝑠} U)}\}$
19	4	a1i	$⊢ (φ \land z \in ℤ) \to F = (x \in ℤ ⟼ x \cdot_{(R ↾_{𝑠} U)} M)$
20		simpr	$⊢ ((φ \land z \in ℤ) \land x = z) \to x = z$
21	20	oveq1d	$⊢ ((φ \land z \in ℤ) \land x = z) \to x \cdot_{(R ↾_{𝑠} U)} M = z \cdot_{(R ↾_{𝑠} U)} M$
22		simpr	$⊢ (φ \land z \in ℤ) \to z \in ℤ$
23		ovexd	$⊢ (φ \land z \in ℤ) \to z \cdot_{(R ↾_{𝑠} U)} M \in V$
24	19 21 22 23	fvmptd	$⊢ (φ \land z \in ℤ) \to F (z) = z \cdot_{(R ↾_{𝑠} U)} M$
25	24	eqeq1d	$⊢ (φ \land z \in ℤ) \to (F (z) = 0_{(R ↾_{𝑠} U)} \leftrightarrow z \cdot_{(R ↾_{𝑠} U)} M = 0_{(R ↾_{𝑠} U)})$
26	1	adantr	$⊢ (φ \land z \in ℤ) \to R \in CMnd$
27	2	adantr	$⊢ (φ \land z \in ℤ) \to K \in ℕ$
28	5	adantr	$⊢ (φ \land z \in ℤ) \to M \in (R PrimRoots K)$
29	26 27 28 3 22	primrootspoweq0	$⊢ (φ \land z \in ℤ) \to (z \cdot_{(R ↾_{𝑠} U)} M = 0_{(R ↾_{𝑠} U)} \leftrightarrow K ∥ z)$
30	25 29	bitrd	$⊢ (φ \land z \in ℤ) \to (F (z) = 0_{(R ↾_{𝑠} U)} \leftrightarrow K ∥ z)$
31	30	rabbidva	$⊢ φ \to \{z \in ℤ \| F (z) = 0_{(R ↾_{𝑠} U)}\} = \{z \in ℤ \| K ∥ z\}$
32		df-rab	$⊢ \{z \in ℤ \| K ∥ z\} = \{z \| (z \in ℤ \land K ∥ z)\}$
33	32	a1i	$⊢ φ \to \{z \in ℤ \| K ∥ z\} = \{z \| (z \in ℤ \land K ∥ z)\}$
34		simpr	$⊢ (z \in ℤ \land K ∥ z) \to K ∥ z$
35		dvdszrcl	$⊢ K ∥ z \to (K \in ℤ \land z \in ℤ)$
36	35	simprd	$⊢ K ∥ z \to z \in ℤ$
37	36	ancri	$⊢ K ∥ z \to (z \in ℤ \land K ∥ z)$
38	34 37	impbii	$⊢ (z \in ℤ \land K ∥ z) \leftrightarrow K ∥ z$
39	38	a1i	$⊢ φ \to ((z \in ℤ \land K ∥ z) \leftrightarrow K ∥ z)$
40	39	abbidv	$⊢ φ \to \{z \| (z \in ℤ \land K ∥ z)\} = \{z \| K ∥ z\}$
41	33 40	eqtrd	$⊢ φ \to \{z \in ℤ \| K ∥ z\} = \{z \| K ∥ z\}$
42	31 41	eqtrd	$⊢ φ \to \{z \in ℤ \| F (z) = 0_{(R ↾_{𝑠} U)}\} = \{z \| K ∥ z\}$
43	18 42	eqtr2d	$⊢ φ \to \{z \| K ∥ z\} = F^{-1} [\{0_{(R ↾_{𝑠} U)}\}]$
44	13 43	eqtrd	$⊢ φ \to S (\{K\}) = F^{-1} [\{0_{(R ↾_{𝑠} U)}\}]$

Metamath Proof Explorer

Theorem aks6d1c6isolem3

Proof