Theorem deg1scl

Description: A nonzero scalar polynomial has zero degree. (Contributed by Stefan O'Rear, 29-Mar-2015)

	Ref	Expression
Hypotheses	deg1sclle.d	⊢ 𝐷 = ( deg1 ‘ 𝑅 )
	deg1sclle.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
	deg1sclle.k	⊢ 𝐾 = ( Base ‘ 𝑅 )
	deg1sclle.a	⊢ 𝐴 = ( algSc ‘ 𝑃 )
	deg1scl.z	⊢ 0 = ( 0g ‘ 𝑅 )
Assertion	deg1scl	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾 ∧ 𝐹 ≠ 0 ) → ( 𝐷 ‘ ( 𝐴 ‘ 𝐹 ) ) = 0 )

Proof

Step	Hyp	Ref	Expression
1		deg1sclle.d	⊢ 𝐷 = ( deg1 ‘ 𝑅 )
2		deg1sclle.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
3		deg1sclle.k	⊢ 𝐾 = ( Base ‘ 𝑅 )
4		deg1sclle.a	⊢ 𝐴 = ( algSc ‘ 𝑃 )
5		deg1scl.z	⊢ 0 = ( 0g ‘ 𝑅 )
6	1 2 3 4	deg1sclle	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾 ) → ( 𝐷 ‘ ( 𝐴 ‘ 𝐹 ) ) ≤ 0 )
7	6	3adant3	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾 ∧ 𝐹 ≠ 0 ) → ( 𝐷 ‘ ( 𝐴 ‘ 𝐹 ) ) ≤ 0 )
8		simp1	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾 ∧ 𝐹 ≠ 0 ) → 𝑅 ∈ Ring )
9		eqid	⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
10	2 4 3 9	ply1sclcl	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾 ) → ( 𝐴 ‘ 𝐹 ) ∈ ( Base ‘ 𝑃 ) )
11	10	3adant3	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾 ∧ 𝐹 ≠ 0 ) → ( 𝐴 ‘ 𝐹 ) ∈ ( Base ‘ 𝑃 ) )
12		eqid	⊢ ( 0g ‘ 𝑃 ) = ( 0g ‘ 𝑃 )
13	2 4 5 12 3	ply1scln0	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾 ∧ 𝐹 ≠ 0 ) → ( 𝐴 ‘ 𝐹 ) ≠ ( 0g ‘ 𝑃 ) )
14	1 2 12 9	deg1nn0cl	⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝐴 ‘ 𝐹 ) ∈ ( Base ‘ 𝑃 ) ∧ ( 𝐴 ‘ 𝐹 ) ≠ ( 0g ‘ 𝑃 ) ) → ( 𝐷 ‘ ( 𝐴 ‘ 𝐹 ) ) ∈ ℕ0 )
15	8 11 13 14	syl3anc	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾 ∧ 𝐹 ≠ 0 ) → ( 𝐷 ‘ ( 𝐴 ‘ 𝐹 ) ) ∈ ℕ0 )
16		nn0le0eq0	⊢ ( ( 𝐷 ‘ ( 𝐴 ‘ 𝐹 ) ) ∈ ℕ0 → ( ( 𝐷 ‘ ( 𝐴 ‘ 𝐹 ) ) ≤ 0 ↔ ( 𝐷 ‘ ( 𝐴 ‘ 𝐹 ) ) = 0 ) )
17	15 16	syl	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾 ∧ 𝐹 ≠ 0 ) → ( ( 𝐷 ‘ ( 𝐴 ‘ 𝐹 ) ) ≤ 0 ↔ ( 𝐷 ‘ ( 𝐴 ‘ 𝐹 ) ) = 0 ) )
18	7 17	mpbid	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐾 ∧ 𝐹 ≠ 0 ) → ( 𝐷 ‘ ( 𝐴 ‘ 𝐹 ) ) = 0 )