Theorem ply1moneq

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

	Ref	Expression
Hypotheses	ply1moneq.p	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
	ply1moneq.x	$$⊢X={\mathrm{var}}_1\left(R\right)$$
	ply1moneq.e	$$⊢\underset{\dot{}}{\times }={\cdot }_{{\mathrm{mulGrp}}_P}$$
	ply1moneq.r	$$⊢\phi \to R\in \mathrm{NzRing}$$
	ply1moneq.m	$$⊢\phi \to M\in {\mathbb{N}}_0$$
	ply1moneq.n	$$⊢\phi \to N\in {\mathbb{N}}_0$$
Assertion	ply1moneq	$$⊢\phi \to \left(M\underset{\dot{}}{\times }X=N\underset{\dot{}}{\times }X\leftrightarrow M=N\right)$$

Proof

Step	Hyp	Ref	Expression
1		ply1moneq.p	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
2		ply1moneq.x	$$⊢X={\mathrm{var}}_1\left(R\right)$$
3		ply1moneq.e	$$⊢\underset{\dot{}}{\times }={\cdot }_{{\mathrm{mulGrp}}_P}$$
4		ply1moneq.r	$$⊢\phi \to R\in \mathrm{NzRing}$$
5		ply1moneq.m	$$⊢\phi \to M\in {\mathbb{N}}_0$$
6		ply1moneq.n	$$⊢\phi \to N\in {\mathbb{N}}_0$$
7		nzrring	$$⊢R\in \mathrm{NzRing}\to R\in \mathrm{Ring}$$
8	4 7	syl	$$⊢\phi \to R\in \mathrm{Ring}$$
9		eqid	$$⊢0_R=0_R$$
10		eqid	$$⊢1_R=1_R$$
11	1 2 3 8 5 9 10	coe1mon	$$⊢\phi \to {\mathrm{coe}}_1\left(M\underset{\dot{}}{\times }X\right)=\left(k\in {\mathbb{N}}_0⟼if\left(k=M,1_R,0_R\right)\right)$$
12		fvexd	$$⊢\left(\phi \wedge k\in {\mathbb{N}}_0\right)\to 1_R\in \mathrm{V}$$
13		fvexd	$$⊢\left(\phi \wedge k\in {\mathbb{N}}_0\right)\to 0_R\in \mathrm{V}$$
14	12 13	ifcld	$$⊢\left(\phi \wedge k\in {\mathbb{N}}_0\right)\to if\left(k=M,1_R,0_R\right)\in \mathrm{V}$$
15	11 14	fvmpt2d	$$⊢\left(\phi \wedge k\in {\mathbb{N}}_0\right)\to {\mathrm{coe}}_1\left(M\underset{\dot{}}{\times }X\right)\left(k\right)=if\left(k=M,1_R,0_R\right)$$
16	1 2 3 8 6 9 10	coe1mon	$$⊢\phi \to {\mathrm{coe}}_1\left(N\underset{\dot{}}{\times }X\right)=\left(k\in {\mathbb{N}}_0⟼if\left(k=N,1_R,0_R\right)\right)$$
17	12 13	ifcld	$$⊢\left(\phi \wedge k\in {\mathbb{N}}_0\right)\to if\left(k=N,1_R,0_R\right)\in \mathrm{V}$$
18	16 17	fvmpt2d	$$⊢\left(\phi \wedge k\in {\mathbb{N}}_0\right)\to {\mathrm{coe}}_1\left(N\underset{\dot{}}{\times }X\right)\left(k\right)=if\left(k=N,1_R,0_R\right)$$
19	15 18	eqeq12d	$$⊢\left(\phi \wedge k\in {\mathbb{N}}_0\right)\to \left({\mathrm{coe}}_1\left(M\underset{\dot{}}{\times }X\right)\left(k\right)={\mathrm{coe}}_1\left(N\underset{\dot{}}{\times }X\right)\left(k\right)\leftrightarrow if\left(k=M,1_R,0_R\right)=if\left(k=N,1_R,0_R\right)\right)$$
20	10 9	nzrnz	$$⊢R\in \mathrm{NzRing}\to 1_R\ne 0_R$$
21	4 20	syl	$$⊢\phi \to 1_R\ne 0_R$$
22	21	adantr	$$⊢\left(\phi \wedge k\in {\mathbb{N}}_0\right)\to 1_R\ne 0_R$$
23		ifnebib	$$⊢1_R\ne 0_R\to \left(if\left(k=M,1_R,0_R\right)=if\left(k=N,1_R,0_R\right)\leftrightarrow \left(k=M\leftrightarrow k=N\right)\right)$$
24	22 23	syl	$$⊢\left(\phi \wedge k\in {\mathbb{N}}_0\right)\to \left(if\left(k=M,1_R,0_R\right)=if\left(k=N,1_R,0_R\right)\leftrightarrow \left(k=M\leftrightarrow k=N\right)\right)$$
25	19 24	bitrd	$$⊢\left(\phi \wedge k\in {\mathbb{N}}_0\right)\to \left({\mathrm{coe}}_1\left(M\underset{\dot{}}{\times }X\right)\left(k\right)={\mathrm{coe}}_1\left(N\underset{\dot{}}{\times }X\right)\left(k\right)\leftrightarrow \left(k=M\leftrightarrow k=N\right)\right)$$
26	25	ralbidva	$$⊢\phi \to \left(\forall k\in {\mathbb{N}}_0{\mathrm{coe}}_1\left(M\underset{\dot{}}{\times }X\right)\left(k\right)={\mathrm{coe}}_1\left(N\underset{\dot{}}{\times }X\right)\left(k\right)\leftrightarrow \forall k\in {\mathbb{N}}_0\left(k=M\leftrightarrow k=N\right)\right)$$
27		eqid	$$⊢{\mathrm{mulGrp}}_P={\mathrm{mulGrp}}_P$$
28		eqid	$$⊢{\mathrm{Base}}_P={\mathrm{Base}}_P$$
29	1 2 27 3 28	ply1moncl	$$⊢\left(R\in \mathrm{Ring}\wedge M\in {\mathbb{N}}_0\right)\to M\underset{\dot{}}{\times }X\in {\mathrm{Base}}_P$$
30	8 5 29	syl2anc	$$⊢\phi \to M\underset{\dot{}}{\times }X\in {\mathrm{Base}}_P$$
31	1 2 27 3 28	ply1moncl	$$⊢\left(R\in \mathrm{Ring}\wedge N\in {\mathbb{N}}_0\right)\to N\underset{\dot{}}{\times }X\in {\mathrm{Base}}_P$$
32	8 6 31	syl2anc	$$⊢\phi \to N\underset{\dot{}}{\times }X\in {\mathrm{Base}}_P$$
33		eqid	$$⊢{\mathrm{coe}}_1\left(M\underset{\dot{}}{\times }X\right)={\mathrm{coe}}_1\left(M\underset{\dot{}}{\times }X\right)$$
34		eqid	$$⊢{\mathrm{coe}}_1\left(N\underset{\dot{}}{\times }X\right)={\mathrm{coe}}_1\left(N\underset{\dot{}}{\times }X\right)$$
35	1 28 33 34	ply1coe1eq	$$⊢\left(R\in \mathrm{Ring}\wedge M\underset{\dot{}}{\times }X\in {\mathrm{Base}}_P\wedge N\underset{\dot{}}{\times }X\in {\mathrm{Base}}_P\right)\to \left(\forall k\in {\mathbb{N}}_0{\mathrm{coe}}_1\left(M\underset{\dot{}}{\times }X\right)\left(k\right)={\mathrm{coe}}_1\left(N\underset{\dot{}}{\times }X\right)\left(k\right)\leftrightarrow M\underset{\dot{}}{\times }X=N\underset{\dot{}}{\times }X\right)$$
36	8 30 32 35	syl3anc	$$⊢\phi \to \left(\forall k\in {\mathbb{N}}_0{\mathrm{coe}}_1\left(M\underset{\dot{}}{\times }X\right)\left(k\right)={\mathrm{coe}}_1\left(N\underset{\dot{}}{\times }X\right)\left(k\right)\leftrightarrow M\underset{\dot{}}{\times }X=N\underset{\dot{}}{\times }X\right)$$
37	5 6	eqelbid	$$⊢\phi \to \left(\forall k\in {\mathbb{N}}_0\left(k=M\leftrightarrow k=N\right)\leftrightarrow M=N\right)$$
38	26 36 37	3bitr3d	$$⊢\phi \to \left(M\underset{\dot{}}{\times }X=N\underset{\dot{}}{\times }X\leftrightarrow M=N\right)$$