Theorem coe1mon

Description: Coefficient vector of a monomial. (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}$$
	coe1mon.r	$$⊢\phi \to R\in \mathrm{Ring}$$
	coe1mon.n	$$⊢\phi \to N\in {\mathbb{N}}_0$$
	coe1mon.0	$$⊢\underset{\dot{}}{0}=0_R$$
	coe1mon.1	$$⊢\underset{\dot{}}{1}=1_R$$
Assertion	coe1mon	$$⊢\phi \to {\mathrm{coe}}_1\left(N\underset{\dot{}}{\times }X\right)=\left(k\in {\mathbb{N}}_0⟼if\left(k=N,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\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		coe1mon.r	$$⊢\phi \to R\in \mathrm{Ring}$$
5		coe1mon.n	$$⊢\phi \to N\in {\mathbb{N}}_0$$
6		coe1mon.0	$$⊢\underset{\dot{}}{0}=0_R$$
7		coe1mon.1	$$⊢\underset{\dot{}}{1}=1_R$$
8	1	ply1sca	$$⊢R\in \mathrm{Ring}\to R=\mathrm{Scalar}\left(P\right)$$
9	4 8	syl	$$⊢\phi \to R=\mathrm{Scalar}\left(P\right)$$
10	9	fveq2d	$$⊢\phi \to 1_R=1_{\mathrm{Scalar}\left(P\right)}$$
11	7 10	eqtrid	$$⊢\phi \to \underset{\dot{}}{1}=1_{\mathrm{Scalar}\left(P\right)}$$
12	11	oveq1d	$$⊢\phi \to \underset{\dot{}}{1}{\cdot }_P\left(N\underset{\dot{}}{\times }X\right)=1_{\mathrm{Scalar}\left(P\right)}{\cdot }_P\left(N\underset{\dot{}}{\times }X\right)$$
13	1	ply1lmod	$$⊢R\in \mathrm{Ring}\to P\in \mathrm{LMod}$$
14	4 13	syl	$$⊢\phi \to P\in \mathrm{LMod}$$
15		eqid	$$⊢{\mathrm{mulGrp}}_P={\mathrm{mulGrp}}_P$$
16		eqid	$$⊢{\mathrm{Base}}_P={\mathrm{Base}}_P$$
17	1 2 15 3 16	ply1moncl	$$⊢\left(R\in \mathrm{Ring}\wedge N\in {\mathbb{N}}_0\right)\to N\underset{\dot{}}{\times }X\in {\mathrm{Base}}_P$$
18	4 5 17	syl2anc	$$⊢\phi \to N\underset{\dot{}}{\times }X\in {\mathrm{Base}}_P$$
19		eqid	$$⊢\mathrm{Scalar}\left(P\right)=\mathrm{Scalar}\left(P\right)$$
20		eqid	$$⊢{\cdot }_P={\cdot }_P$$
21		eqid	$$⊢1_{\mathrm{Scalar}\left(P\right)}=1_{\mathrm{Scalar}\left(P\right)}$$
22	16 19 20 21	lmodvs1	$$⊢\left(P\in \mathrm{LMod}\wedge N\underset{\dot{}}{\times }X\in {\mathrm{Base}}_P\right)\to 1_{\mathrm{Scalar}\left(P\right)}{\cdot }_P\left(N\underset{\dot{}}{\times }X\right)=N\underset{\dot{}}{\times }X$$
23	14 18 22	syl2anc	$$⊢\phi \to 1_{\mathrm{Scalar}\left(P\right)}{\cdot }_P\left(N\underset{\dot{}}{\times }X\right)=N\underset{\dot{}}{\times }X$$
24	12 23	eqtrd	$$⊢\phi \to \underset{\dot{}}{1}{\cdot }_P\left(N\underset{\dot{}}{\times }X\right)=N\underset{\dot{}}{\times }X$$
25	24	fveq2d	$$⊢\phi \to {\mathrm{coe}}_1\left(\underset{\dot{}}{1}{\cdot }_P\left(N\underset{\dot{}}{\times }X\right)\right)={\mathrm{coe}}_1\left(N\underset{\dot{}}{\times }X\right)$$
26		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
27	26 7	ringidcl	$$⊢R\in \mathrm{Ring}\to \underset{\dot{}}{1}\in {\mathrm{Base}}_R$$
28	4 27	syl	$$⊢\phi \to \underset{\dot{}}{1}\in {\mathrm{Base}}_R$$
29	6 26 1 2 20 15 3	coe1tm	$$⊢\left(R\in \mathrm{Ring}\wedge \underset{\dot{}}{1}\in {\mathrm{Base}}_R\wedge N\in {\mathbb{N}}_0\right)\to {\mathrm{coe}}_1\left(\underset{\dot{}}{1}{\cdot }_P\left(N\underset{\dot{}}{\times }X\right)\right)=\left(k\in {\mathbb{N}}_0⟼if\left(k=N,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)$$
30	4 28 5 29	syl3anc	$$⊢\phi \to {\mathrm{coe}}_1\left(\underset{\dot{}}{1}{\cdot }_P\left(N\underset{\dot{}}{\times }X\right)\right)=\left(k\in {\mathbb{N}}_0⟼if\left(k=N,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)$$
31	25 30	eqtr3d	$$⊢\phi \to {\mathrm{coe}}_1\left(N\underset{\dot{}}{\times }X\right)=\left(k\in {\mathbb{N}}_0⟼if\left(k=N,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)$$