Theorem primrootsunit

Description: Primitive roots have left inverses. (Contributed by metakunt, 25-Apr-2025)

	Ref	Expression
Hypotheses	primrootsunit.1	⊢ ( 𝜑 → 𝑅 ∈ CMnd )
	primrootsunit.2	⊢ ( 𝜑 → 𝐾 ∈ ℕ )
	primrootsunit.3	⊢ 𝑈 = { 𝑎 ∈ ( Base ‘ 𝑅 ) ∣ ∃ 𝑖 ∈ ( Base ‘ 𝑅 ) ( 𝑖 ( +g ‘ 𝑅 ) 𝑎 ) = ( 0g ‘ 𝑅 ) }
Assertion	primrootsunit	⊢ ( 𝜑 → ( ( 𝑅 PrimRoots 𝐾 ) = ( ( 𝑅 ↾s 𝑈 ) PrimRoots 𝐾 ) ∧ ( 𝑅 ↾s 𝑈 ) ∈ Abel ) )

Proof

Step	Hyp	Ref	Expression
1		primrootsunit.1	⊢ ( 𝜑 → 𝑅 ∈ CMnd )
2		primrootsunit.2	⊢ ( 𝜑 → 𝐾 ∈ ℕ )
3		primrootsunit.3	⊢ 𝑈 = { 𝑎 ∈ ( Base ‘ 𝑅 ) ∣ ∃ 𝑖 ∈ ( Base ‘ 𝑅 ) ( 𝑖 ( +g ‘ 𝑅 ) 𝑎 ) = ( 0g ‘ 𝑅 ) }
4		nfv	⊢ Ⅎ 𝑗 ( 𝑖 ( +g ‘ 𝑅 ) 𝑎 ) = ( 0g ‘ 𝑅 )
5		nfv	⊢ Ⅎ 𝑖 ( 𝑗 ( +g ‘ 𝑅 ) 𝑎 ) = ( 0g ‘ 𝑅 )
6		oveq1	⊢ ( 𝑖 = 𝑗 → ( 𝑖 ( +g ‘ 𝑅 ) 𝑎 ) = ( 𝑗 ( +g ‘ 𝑅 ) 𝑎 ) )
7	6	eqeq1d	⊢ ( 𝑖 = 𝑗 → ( ( 𝑖 ( +g ‘ 𝑅 ) 𝑎 ) = ( 0g ‘ 𝑅 ) ↔ ( 𝑗 ( +g ‘ 𝑅 ) 𝑎 ) = ( 0g ‘ 𝑅 ) ) )
8	4 5 7	cbvrexw	⊢ ( ∃ 𝑖 ∈ ( Base ‘ 𝑅 ) ( 𝑖 ( +g ‘ 𝑅 ) 𝑎 ) = ( 0g ‘ 𝑅 ) ↔ ∃ 𝑗 ∈ ( Base ‘ 𝑅 ) ( 𝑗 ( +g ‘ 𝑅 ) 𝑎 ) = ( 0g ‘ 𝑅 ) )
9	8	rabbii	⊢ { 𝑎 ∈ ( Base ‘ 𝑅 ) ∣ ∃ 𝑖 ∈ ( Base ‘ 𝑅 ) ( 𝑖 ( +g ‘ 𝑅 ) 𝑎 ) = ( 0g ‘ 𝑅 ) } = { 𝑎 ∈ ( Base ‘ 𝑅 ) ∣ ∃ 𝑗 ∈ ( Base ‘ 𝑅 ) ( 𝑗 ( +g ‘ 𝑅 ) 𝑎 ) = ( 0g ‘ 𝑅 ) }
10	3 9	eqtri	⊢ 𝑈 = { 𝑎 ∈ ( Base ‘ 𝑅 ) ∣ ∃ 𝑗 ∈ ( Base ‘ 𝑅 ) ( 𝑗 ( +g ‘ 𝑅 ) 𝑎 ) = ( 0g ‘ 𝑅 ) }
11	1 2 10	primrootsunit1	⊢ ( 𝜑 → ( ( 𝑅 PrimRoots 𝐾 ) = ( ( 𝑅 ↾s 𝑈 ) PrimRoots 𝐾 ) ∧ ( 𝑅 ↾s 𝑈 ) ∈ Abel ) )