Theorem ply1moneq

Description: Two monomials are equal iff their powers are equal. (Contributed by Thierry Arnoux, 20-Feb-2025)

	Ref	Expression
Hypotheses	ply1moneq.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
	ply1moneq.x	⊢ 𝑋 = ( var1 ‘ 𝑅 )
	ply1moneq.e	⊢ ↑ = ( .g ‘ ( mulGrp ‘ 𝑃 ) )
	ply1moneq.r	⊢ ( 𝜑 → 𝑅 ∈ NzRing )
	ply1moneq.m	⊢ ( 𝜑 → 𝑀 ∈ ℕ0 )
	ply1moneq.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
Assertion	ply1moneq	⊢ ( 𝜑 → ( ( 𝑀 ↑ 𝑋 ) = ( 𝑁 ↑ 𝑋 ) ↔ 𝑀 = 𝑁 ) )

Proof

Step	Hyp	Ref	Expression
1		ply1moneq.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
2		ply1moneq.x	⊢ 𝑋 = ( var1 ‘ 𝑅 )
3		ply1moneq.e	⊢ ↑ = ( .g ‘ ( mulGrp ‘ 𝑃 ) )
4		ply1moneq.r	⊢ ( 𝜑 → 𝑅 ∈ NzRing )
5		ply1moneq.m	⊢ ( 𝜑 → 𝑀 ∈ ℕ0 )
6		ply1moneq.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
7		nzrring	⊢ ( 𝑅 ∈ NzRing → 𝑅 ∈ Ring )
8	4 7	syl	⊢ ( 𝜑 → 𝑅 ∈ Ring )
9		eqid	⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
10		eqid	⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
11	1 2 3 8 5 9 10	coe1mon	⊢ ( 𝜑 → ( coe1 ‘ ( 𝑀 ↑ 𝑋 ) ) = ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 = 𝑀 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) )
12		fvexd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 1r ‘ 𝑅 ) ∈ V )
13		fvexd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 0g ‘ 𝑅 ) ∈ V )
14	12 13	ifcld	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → if ( 𝑘 = 𝑀 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ∈ V )
15	11 14	fvmpt2d	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ( coe1 ‘ ( 𝑀 ↑ 𝑋 ) ) ‘ 𝑘 ) = if ( 𝑘 = 𝑀 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) )
16	1 2 3 8 6 9 10	coe1mon	⊢ ( 𝜑 → ( coe1 ‘ ( 𝑁 ↑ 𝑋 ) ) = ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 = 𝑁 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) )
17	12 13	ifcld	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → if ( 𝑘 = 𝑁 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ∈ V )
18	16 17	fvmpt2d	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ( coe1 ‘ ( 𝑁 ↑ 𝑋 ) ) ‘ 𝑘 ) = if ( 𝑘 = 𝑁 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) )
19	15 18	eqeq12d	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ( ( coe1 ‘ ( 𝑀 ↑ 𝑋 ) ) ‘ 𝑘 ) = ( ( coe1 ‘ ( 𝑁 ↑ 𝑋 ) ) ‘ 𝑘 ) ↔ if ( 𝑘 = 𝑀 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) = if ( 𝑘 = 𝑁 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) )
20	10 9	nzrnz	⊢ ( 𝑅 ∈ NzRing → ( 1r ‘ 𝑅 ) ≠ ( 0g ‘ 𝑅 ) )
21	4 20	syl	⊢ ( 𝜑 → ( 1r ‘ 𝑅 ) ≠ ( 0g ‘ 𝑅 ) )
22	21	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 1r ‘ 𝑅 ) ≠ ( 0g ‘ 𝑅 ) )
23		ifnebib	⊢ ( ( 1r ‘ 𝑅 ) ≠ ( 0g ‘ 𝑅 ) → ( if ( 𝑘 = 𝑀 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) = if ( 𝑘 = 𝑁 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ↔ ( 𝑘 = 𝑀 ↔ 𝑘 = 𝑁 ) ) )
24	22 23	syl	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( if ( 𝑘 = 𝑀 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) = if ( 𝑘 = 𝑁 , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ↔ ( 𝑘 = 𝑀 ↔ 𝑘 = 𝑁 ) ) )
25	19 24	bitrd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ( ( coe1 ‘ ( 𝑀 ↑ 𝑋 ) ) ‘ 𝑘 ) = ( ( coe1 ‘ ( 𝑁 ↑ 𝑋 ) ) ‘ 𝑘 ) ↔ ( 𝑘 = 𝑀 ↔ 𝑘 = 𝑁 ) ) )
26	25	ralbidva	⊢ ( 𝜑 → ( ∀ 𝑘 ∈ ℕ0 ( ( coe1 ‘ ( 𝑀 ↑ 𝑋 ) ) ‘ 𝑘 ) = ( ( coe1 ‘ ( 𝑁 ↑ 𝑋 ) ) ‘ 𝑘 ) ↔ ∀ 𝑘 ∈ ℕ0 ( 𝑘 = 𝑀 ↔ 𝑘 = 𝑁 ) ) )
27		eqid	⊢ ( mulGrp ‘ 𝑃 ) = ( mulGrp ‘ 𝑃 )
28		eqid	⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
29	1 2 27 3 28	ply1moncl	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ ℕ0 ) → ( 𝑀 ↑ 𝑋 ) ∈ ( Base ‘ 𝑃 ) )
30	8 5 29	syl2anc	⊢ ( 𝜑 → ( 𝑀 ↑ 𝑋 ) ∈ ( Base ‘ 𝑃 ) )
31	1 2 27 3 28	ply1moncl	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ ℕ0 ) → ( 𝑁 ↑ 𝑋 ) ∈ ( Base ‘ 𝑃 ) )
32	8 6 31	syl2anc	⊢ ( 𝜑 → ( 𝑁 ↑ 𝑋 ) ∈ ( Base ‘ 𝑃 ) )
33		eqid	⊢ ( coe1 ‘ ( 𝑀 ↑ 𝑋 ) ) = ( coe1 ‘ ( 𝑀 ↑ 𝑋 ) )
34		eqid	⊢ ( coe1 ‘ ( 𝑁 ↑ 𝑋 ) ) = ( coe1 ‘ ( 𝑁 ↑ 𝑋 ) )
35	1 28 33 34	ply1coe1eq	⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑀 ↑ 𝑋 ) ∈ ( Base ‘ 𝑃 ) ∧ ( 𝑁 ↑ 𝑋 ) ∈ ( Base ‘ 𝑃 ) ) → ( ∀ 𝑘 ∈ ℕ0 ( ( coe1 ‘ ( 𝑀 ↑ 𝑋 ) ) ‘ 𝑘 ) = ( ( coe1 ‘ ( 𝑁 ↑ 𝑋 ) ) ‘ 𝑘 ) ↔ ( 𝑀 ↑ 𝑋 ) = ( 𝑁 ↑ 𝑋 ) ) )
36	8 30 32 35	syl3anc	⊢ ( 𝜑 → ( ∀ 𝑘 ∈ ℕ0 ( ( coe1 ‘ ( 𝑀 ↑ 𝑋 ) ) ‘ 𝑘 ) = ( ( coe1 ‘ ( 𝑁 ↑ 𝑋 ) ) ‘ 𝑘 ) ↔ ( 𝑀 ↑ 𝑋 ) = ( 𝑁 ↑ 𝑋 ) ) )
37	5 6	eqelbid	⊢ ( 𝜑 → ( ∀ 𝑘 ∈ ℕ0 ( 𝑘 = 𝑀 ↔ 𝑘 = 𝑁 ) ↔ 𝑀 = 𝑁 ) )
38	26 36 37	3bitr3d	⊢ ( 𝜑 → ( ( 𝑀 ↑ 𝑋 ) = ( 𝑁 ↑ 𝑋 ) ↔ 𝑀 = 𝑁 ) )