Theorem 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	⊢ 𝐾 = ( Base ‘ 𝑅 )
	cply1coe0.0	⊢ 0 = ( 0g ‘ 𝑅 )
	cply1coe0.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
	cply1coe0.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
	cply1coe0.a	⊢ 𝐴 = ( algSc ‘ 𝑃 )
Assertion	cply1coe0	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ 𝐾 ) → ∀ 𝑛 ∈ ℕ ( ( coe1 ‘ ( 𝐴 ‘ 𝑆 ) ) ‘ 𝑛 ) = 0 )

Proof

Step	Hyp	Ref	Expression
1		cply1coe0.k	⊢ 𝐾 = ( Base ‘ 𝑅 )
2		cply1coe0.0	⊢ 0 = ( 0g ‘ 𝑅 )
3		cply1coe0.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
4		cply1coe0.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
5		cply1coe0.a	⊢ 𝐴 = ( algSc ‘ 𝑃 )
6	3 5 1 2	coe1scl	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ 𝐾 ) → ( coe1 ‘ ( 𝐴 ‘ 𝑆 ) ) = ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 = 0 , 𝑆 , 0 ) ) )
7	6	adantr	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ 𝐾 ) ∧ 𝑛 ∈ ℕ ) → ( coe1 ‘ ( 𝐴 ‘ 𝑆 ) ) = ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 = 0 , 𝑆 , 0 ) ) )
8		nnne0	⊢ ( 𝑛 ∈ ℕ → 𝑛 ≠ 0 )
9	8	neneqd	⊢ ( 𝑛 ∈ ℕ → ¬ 𝑛 = 0 )
10	9	adantl	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ 𝐾 ) ∧ 𝑛 ∈ ℕ ) → ¬ 𝑛 = 0 )
11	10	adantr	⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ 𝐾 ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 = 𝑛 ) → ¬ 𝑛 = 0 )
12		eqeq1	⊢ ( 𝑘 = 𝑛 → ( 𝑘 = 0 ↔ 𝑛 = 0 ) )
13	12	notbid	⊢ ( 𝑘 = 𝑛 → ( ¬ 𝑘 = 0 ↔ ¬ 𝑛 = 0 ) )
14	13	adantl	⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ 𝐾 ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 = 𝑛 ) → ( ¬ 𝑘 = 0 ↔ ¬ 𝑛 = 0 ) )
15	11 14	mpbird	⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ 𝐾 ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 = 𝑛 ) → ¬ 𝑘 = 0 )
16	15	iffalsed	⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ 𝐾 ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑘 = 𝑛 ) → if ( 𝑘 = 0 , 𝑆 , 0 ) = 0 )
17		nnnn0	⊢ ( 𝑛 ∈ ℕ → 𝑛 ∈ ℕ0 )
18	17	adantl	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ 𝐾 ) ∧ 𝑛 ∈ ℕ ) → 𝑛 ∈ ℕ0 )
19	2	fvexi	⊢ 0 ∈ V
20	19	a1i	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ 𝐾 ) ∧ 𝑛 ∈ ℕ ) → 0 ∈ V )
21	7 16 18 20	fvmptd	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ 𝐾 ) ∧ 𝑛 ∈ ℕ ) → ( ( coe1 ‘ ( 𝐴 ‘ 𝑆 ) ) ‘ 𝑛 ) = 0 )
22	21	ralrimiva	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ 𝐾 ) → ∀ 𝑛 ∈ ℕ ( ( coe1 ‘ ( 𝐴 ‘ 𝑆 ) ) ‘ 𝑛 ) = 0 )