cply1coe0

Description: All but the first coefficient of a constant polynomial ( i.e. a "lifted scalar") are zero. (Contributed by AV, 16-Nov-2019)

	Ref	Expression
Hypotheses	cply1coe0.k	$⊢ K = {Base}_{R}$
	cply1coe0.0	$⊢ \underset{˙}{0} = 0_{R}$
	cply1coe0.p	$⊢ P = {Poly}_{1} (R)$
	cply1coe0.b	$⊢ B = {Base}_{P}$
	cply1coe0.a	$⊢ A = algSc (P)$
Assertion	cply1coe0	$⊢ (R \in Ring \land S \in K) \to \forall n \in ℕ {coe}_{1} (A (S)) (n) = \underset{˙}{0}$

Proof

Step	Hyp	Ref	Expression
1		cply1coe0.k	$⊢ K = {Base}_{R}$
2		cply1coe0.0	$⊢ \underset{˙}{0} = 0_{R}$
3		cply1coe0.p	$⊢ P = {Poly}_{1} (R)$
4		cply1coe0.b	$⊢ B = {Base}_{P}$
5		cply1coe0.a	$⊢ A = algSc (P)$
6	3 5 1 2	coe1scl	$⊢ (R \in Ring \land S \in K) \to {coe}_{1} (A (S)) = (k \in ℕ_{0} ⟼ if (k = 0, S, \underset{˙}{0}))$
7	6	adantr	$⊢ ((R \in Ring \land S \in K) \land n \in ℕ) \to {coe}_{1} (A (S)) = (k \in ℕ_{0} ⟼ if (k = 0, S, \underset{˙}{0}))$
8		nnne0	$⊢ n \in ℕ \to n \neq 0$
9	8	neneqd	$⊢ n \in ℕ \to \neg n = 0$
10	9	adantl	$⊢ ((R \in Ring \land S \in K) \land n \in ℕ) \to \neg n = 0$
11	10	adantr	$⊢ (((R \in Ring \land S \in K) \land n \in ℕ) \land k = n) \to \neg n = 0$
12		eqeq1	$⊢ k = n \to (k = 0 \leftrightarrow n = 0)$
13	12	notbid	$⊢ k = n \to (\neg k = 0 \leftrightarrow \neg n = 0)$
14	13	adantl	$⊢ (((R \in Ring \land S \in K) \land n \in ℕ) \land k = n) \to (\neg k = 0 \leftrightarrow \neg n = 0)$
15	11 14	mpbird	$⊢ (((R \in Ring \land S \in K) \land n \in ℕ) \land k = n) \to \neg k = 0$
16	15	iffalsed	$⊢ (((R \in Ring \land S \in K) \land n \in ℕ) \land k = n) \to if (k = 0, S, \underset{˙}{0}) = \underset{˙}{0}$
17		nnnn0	$⊢ n \in ℕ \to n \in ℕ_{0}$
18	17	adantl	$⊢ ((R \in Ring \land S \in K) \land n \in ℕ) \to n \in ℕ_{0}$
19	2	fvexi	$⊢ \underset{˙}{0} \in V$
20	19	a1i	$⊢ ((R \in Ring \land S \in K) \land n \in ℕ) \to \underset{˙}{0} \in V$
21	7 16 18 20	fvmptd	$⊢ ((R \in Ring \land S \in K) \land n \in ℕ) \to {coe}_{1} (A (S)) (n) = \underset{˙}{0}$
22	21	ralrimiva	$⊢ (R \in Ring \land S \in K) \to \forall n \in ℕ {coe}_{1} (A (S)) (n) = \underset{˙}{0}$

Metamath Proof Explorer

Theorem cply1coe0

Proof