This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( 𝜑 → ( ( 𝑀 ↑ 𝑋 ) = ( 𝑁 ↑ 𝑋 ) ↔ 𝑀 = 𝑁 ) )