coe1vr1

Description: Polynomial coefficient of the variable. (Contributed by Thierry Arnoux, 22-Jun-2025)

	Ref	Expression
Hypotheses	coe1vr1.1	$⊢ P = {Poly}_{1} (R)$
	coe1vr1.2	$⊢ X = {var}_{1} (R)$
	coe1vr1.3	$⊢ φ \to R \in Ring$
	coe1vr1.4	$⊢ \underset{˙}{0} = 0_{R}$
	coe1vr1.5	$⊢ \underset{˙}{1} = 1_{R}$
Assertion	coe1vr1	$⊢ φ \to {coe}_{1} (X) = (k \in ℕ_{0} ⟼ if (k = 1, \underset{˙}{1}, \underset{˙}{0}))$

Step	Hyp	Ref	Expression
1		coe1vr1.1	$⊢ P = {Poly}_{1} (R)$
2		coe1vr1.2	$⊢ X = {var}_{1} (R)$
3		coe1vr1.3	$⊢ φ \to R \in Ring$
4		coe1vr1.4	$⊢ \underset{˙}{0} = 0_{R}$
5		coe1vr1.5	$⊢ \underset{˙}{1} = 1_{R}$
6		eqid	$⊢ {Base}_{P} = {Base}_{P}$
7	2 1 6	vr1cl	$⊢ R \in Ring \to X \in {Base}_{P}$
8		eqid	$⊢ {mulGrp}_{P} = {mulGrp}_{P}$
9	8 6	mgpbas	$⊢ {Base}_{P} = {Base}_{{mulGrp}_{P}}$
10		eqid	$⊢ \cdot_{{mulGrp}_{P}} = \cdot_{{mulGrp}_{P}}$
11	9 10	mulg1	$⊢ X \in {Base}_{P} \to 1 \cdot_{{mulGrp}_{P}} X = X$
12	3 7 11	3syl	$⊢ φ \to 1 \cdot_{{mulGrp}_{P}} X = X$
13	12	fveq2d	$⊢ φ \to {coe}_{1} (1 \cdot_{{mulGrp}_{P}} X) = {coe}_{1} (X)$
14		1nn0	$⊢ 1 \in ℕ_{0}$
15	14	a1i	$⊢ φ \to 1 \in ℕ_{0}$
16	1 2 10 3 15 4 5	coe1mon	$⊢ φ \to {coe}_{1} (1 \cdot_{{mulGrp}_{P}} X) = (k \in ℕ_{0} ⟼ if (k = 1, \underset{˙}{1}, \underset{˙}{0}))$
17	13 16	eqtr3d	$⊢ φ \to {coe}_{1} (X) = (k \in ℕ_{0} ⟼ if (k = 1, \underset{˙}{1}, \underset{˙}{0}))$

Metamath Proof Explorer