Theorem deg1ldg

Description: A nonzero univariate polynomial always has a nonzero leading coefficient. (Contributed by Stefan O'Rear, 23-Mar-2015)

	Ref	Expression
Hypotheses	deg1z.d	⊢ 𝐷 = ( deg1 ‘ 𝑅 )
	deg1z.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
	deg1z.z	⊢ 0 = ( 0g ‘ 𝑃 )
	deg1nn0cl.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
	deg1ldg.y	⊢ 𝑌 = ( 0g ‘ 𝑅 )
	deg1ldg.a	⊢ 𝐴 = ( coe1 ‘ 𝐹 )
Assertion	deg1ldg	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 0 ) → ( 𝐴 ‘ ( 𝐷 ‘ 𝐹 ) ) ≠ 𝑌 )

Proof

Step	Hyp	Ref	Expression
1		deg1z.d	⊢ 𝐷 = ( deg1 ‘ 𝑅 )
2		deg1z.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
3		deg1z.z	⊢ 0 = ( 0g ‘ 𝑃 )
4		deg1nn0cl.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
5		deg1ldg.y	⊢ 𝑌 = ( 0g ‘ 𝑅 )
6		deg1ldg.a	⊢ 𝐴 = ( coe1 ‘ 𝐹 )
7	1	deg1fval	⊢ 𝐷 = ( 1o mDeg 𝑅 )
8		eqid	⊢ ( 1o mPoly 𝑅 ) = ( 1o mPoly 𝑅 )
9		eqid	⊢ ( PwSer1 ‘ 𝑅 ) = ( PwSer1 ‘ 𝑅 )
10	2 9 4	ply1bas	⊢ 𝐵 = ( Base ‘ ( 1o mPoly 𝑅 ) )
11		psr1baslem	⊢ ( ℕ0 ↑m 1o ) = { 𝑐 ∈ ( ℕ0 ↑m 1o ) ∣ ( ◡ 𝑐 “ ℕ ) ∈ Fin }
12		tdeglem2	⊢ ( 𝑎 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑎 ‘ ∅ ) ) = ( 𝑎 ∈ ( ℕ0 ↑m 1o ) ↦ ( ℂfld Σg 𝑎 ) )
13	8 2 3	ply1mpl0	⊢ 0 = ( 0g ‘ ( 1o mPoly 𝑅 ) )
14	7 8 10 5 11 12 13	mdegldg	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 0 ) → ∃ 𝑏 ∈ ( ℕ0 ↑m 1o ) ( ( 𝐹 ‘ 𝑏 ) ≠ 𝑌 ∧ ( ( 𝑎 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑎 ‘ ∅ ) ) ‘ 𝑏 ) = ( 𝐷 ‘ 𝐹 ) ) )
15	6	fvcoe1	⊢ ( ( 𝐹 ∈ 𝐵 ∧ 𝑏 ∈ ( ℕ0 ↑m 1o ) ) → ( 𝐹 ‘ 𝑏 ) = ( 𝐴 ‘ ( 𝑏 ‘ ∅ ) ) )
16	15	3ad2antl2	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 0 ) ∧ 𝑏 ∈ ( ℕ0 ↑m 1o ) ) → ( 𝐹 ‘ 𝑏 ) = ( 𝐴 ‘ ( 𝑏 ‘ ∅ ) ) )
17		fveq1	⊢ ( 𝑎 = 𝑏 → ( 𝑎 ‘ ∅ ) = ( 𝑏 ‘ ∅ ) )
18		eqid	⊢ ( 𝑎 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑎 ‘ ∅ ) ) = ( 𝑎 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑎 ‘ ∅ ) )
19		fvex	⊢ ( 𝑏 ‘ ∅ ) ∈ V
20	17 18 19	fvmpt	⊢ ( 𝑏 ∈ ( ℕ0 ↑m 1o ) → ( ( 𝑎 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑎 ‘ ∅ ) ) ‘ 𝑏 ) = ( 𝑏 ‘ ∅ ) )
21	20	fveq2d	⊢ ( 𝑏 ∈ ( ℕ0 ↑m 1o ) → ( 𝐴 ‘ ( ( 𝑎 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑎 ‘ ∅ ) ) ‘ 𝑏 ) ) = ( 𝐴 ‘ ( 𝑏 ‘ ∅ ) ) )
22	21	adantl	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 0 ) ∧ 𝑏 ∈ ( ℕ0 ↑m 1o ) ) → ( 𝐴 ‘ ( ( 𝑎 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑎 ‘ ∅ ) ) ‘ 𝑏 ) ) = ( 𝐴 ‘ ( 𝑏 ‘ ∅ ) ) )
23	16 22	eqtr4d	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 0 ) ∧ 𝑏 ∈ ( ℕ0 ↑m 1o ) ) → ( 𝐹 ‘ 𝑏 ) = ( 𝐴 ‘ ( ( 𝑎 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑎 ‘ ∅ ) ) ‘ 𝑏 ) ) )
24	23	neeq1d	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 0 ) ∧ 𝑏 ∈ ( ℕ0 ↑m 1o ) ) → ( ( 𝐹 ‘ 𝑏 ) ≠ 𝑌 ↔ ( 𝐴 ‘ ( ( 𝑎 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑎 ‘ ∅ ) ) ‘ 𝑏 ) ) ≠ 𝑌 ) )
25	24	anbi1d	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 0 ) ∧ 𝑏 ∈ ( ℕ0 ↑m 1o ) ) → ( ( ( 𝐹 ‘ 𝑏 ) ≠ 𝑌 ∧ ( ( 𝑎 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑎 ‘ ∅ ) ) ‘ 𝑏 ) = ( 𝐷 ‘ 𝐹 ) ) ↔ ( ( 𝐴 ‘ ( ( 𝑎 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑎 ‘ ∅ ) ) ‘ 𝑏 ) ) ≠ 𝑌 ∧ ( ( 𝑎 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑎 ‘ ∅ ) ) ‘ 𝑏 ) = ( 𝐷 ‘ 𝐹 ) ) ) )
26	25	biancomd	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 0 ) ∧ 𝑏 ∈ ( ℕ0 ↑m 1o ) ) → ( ( ( 𝐹 ‘ 𝑏 ) ≠ 𝑌 ∧ ( ( 𝑎 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑎 ‘ ∅ ) ) ‘ 𝑏 ) = ( 𝐷 ‘ 𝐹 ) ) ↔ ( ( ( 𝑎 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑎 ‘ ∅ ) ) ‘ 𝑏 ) = ( 𝐷 ‘ 𝐹 ) ∧ ( 𝐴 ‘ ( ( 𝑎 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑎 ‘ ∅ ) ) ‘ 𝑏 ) ) ≠ 𝑌 ) ) )
27	26	rexbidva	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 0 ) → ( ∃ 𝑏 ∈ ( ℕ0 ↑m 1o ) ( ( 𝐹 ‘ 𝑏 ) ≠ 𝑌 ∧ ( ( 𝑎 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑎 ‘ ∅ ) ) ‘ 𝑏 ) = ( 𝐷 ‘ 𝐹 ) ) ↔ ∃ 𝑏 ∈ ( ℕ0 ↑m 1o ) ( ( ( 𝑎 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑎 ‘ ∅ ) ) ‘ 𝑏 ) = ( 𝐷 ‘ 𝐹 ) ∧ ( 𝐴 ‘ ( ( 𝑎 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑎 ‘ ∅ ) ) ‘ 𝑏 ) ) ≠ 𝑌 ) ) )
28		df1o2	⊢ 1o = { ∅ }
29		nn0ex	⊢ ℕ0 ∈ V
30		0ex	⊢ ∅ ∈ V
31	28 29 30 18	mapsnf1o2	⊢ ( 𝑎 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑎 ‘ ∅ ) ) : ( ℕ0 ↑m 1o ) –1-1-onto→ ℕ0
32		f1ofo	⊢ ( ( 𝑎 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑎 ‘ ∅ ) ) : ( ℕ0 ↑m 1o ) –1-1-onto→ ℕ0 → ( 𝑎 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑎 ‘ ∅ ) ) : ( ℕ0 ↑m 1o ) –onto→ ℕ0 )
33		eqeq1	⊢ ( ( ( 𝑎 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑎 ‘ ∅ ) ) ‘ 𝑏 ) = 𝑑 → ( ( ( 𝑎 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑎 ‘ ∅ ) ) ‘ 𝑏 ) = ( 𝐷 ‘ 𝐹 ) ↔ 𝑑 = ( 𝐷 ‘ 𝐹 ) ) )
34		fveq2	⊢ ( ( ( 𝑎 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑎 ‘ ∅ ) ) ‘ 𝑏 ) = 𝑑 → ( 𝐴 ‘ ( ( 𝑎 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑎 ‘ ∅ ) ) ‘ 𝑏 ) ) = ( 𝐴 ‘ 𝑑 ) )
35	34	neeq1d	⊢ ( ( ( 𝑎 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑎 ‘ ∅ ) ) ‘ 𝑏 ) = 𝑑 → ( ( 𝐴 ‘ ( ( 𝑎 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑎 ‘ ∅ ) ) ‘ 𝑏 ) ) ≠ 𝑌 ↔ ( 𝐴 ‘ 𝑑 ) ≠ 𝑌 ) )
36	33 35	anbi12d	⊢ ( ( ( 𝑎 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑎 ‘ ∅ ) ) ‘ 𝑏 ) = 𝑑 → ( ( ( ( 𝑎 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑎 ‘ ∅ ) ) ‘ 𝑏 ) = ( 𝐷 ‘ 𝐹 ) ∧ ( 𝐴 ‘ ( ( 𝑎 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑎 ‘ ∅ ) ) ‘ 𝑏 ) ) ≠ 𝑌 ) ↔ ( 𝑑 = ( 𝐷 ‘ 𝐹 ) ∧ ( 𝐴 ‘ 𝑑 ) ≠ 𝑌 ) ) )
37	36	cbvexfo	⊢ ( ( 𝑎 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑎 ‘ ∅ ) ) : ( ℕ0 ↑m 1o ) –onto→ ℕ0 → ( ∃ 𝑏 ∈ ( ℕ0 ↑m 1o ) ( ( ( 𝑎 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑎 ‘ ∅ ) ) ‘ 𝑏 ) = ( 𝐷 ‘ 𝐹 ) ∧ ( 𝐴 ‘ ( ( 𝑎 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑎 ‘ ∅ ) ) ‘ 𝑏 ) ) ≠ 𝑌 ) ↔ ∃ 𝑑 ∈ ℕ0 ( 𝑑 = ( 𝐷 ‘ 𝐹 ) ∧ ( 𝐴 ‘ 𝑑 ) ≠ 𝑌 ) ) )
38	31 32 37	mp2b	⊢ ( ∃ 𝑏 ∈ ( ℕ0 ↑m 1o ) ( ( ( 𝑎 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑎 ‘ ∅ ) ) ‘ 𝑏 ) = ( 𝐷 ‘ 𝐹 ) ∧ ( 𝐴 ‘ ( ( 𝑎 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑎 ‘ ∅ ) ) ‘ 𝑏 ) ) ≠ 𝑌 ) ↔ ∃ 𝑑 ∈ ℕ0 ( 𝑑 = ( 𝐷 ‘ 𝐹 ) ∧ ( 𝐴 ‘ 𝑑 ) ≠ 𝑌 ) )
39	27 38	bitrdi	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 0 ) → ( ∃ 𝑏 ∈ ( ℕ0 ↑m 1o ) ( ( 𝐹 ‘ 𝑏 ) ≠ 𝑌 ∧ ( ( 𝑎 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑎 ‘ ∅ ) ) ‘ 𝑏 ) = ( 𝐷 ‘ 𝐹 ) ) ↔ ∃ 𝑑 ∈ ℕ0 ( 𝑑 = ( 𝐷 ‘ 𝐹 ) ∧ ( 𝐴 ‘ 𝑑 ) ≠ 𝑌 ) ) )
40	1 2 3 4	deg1nn0cl	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 0 ) → ( 𝐷 ‘ 𝐹 ) ∈ ℕ0 )
41		fveq2	⊢ ( 𝑑 = ( 𝐷 ‘ 𝐹 ) → ( 𝐴 ‘ 𝑑 ) = ( 𝐴 ‘ ( 𝐷 ‘ 𝐹 ) ) )
42	41	neeq1d	⊢ ( 𝑑 = ( 𝐷 ‘ 𝐹 ) → ( ( 𝐴 ‘ 𝑑 ) ≠ 𝑌 ↔ ( 𝐴 ‘ ( 𝐷 ‘ 𝐹 ) ) ≠ 𝑌 ) )
43	42	ceqsrexv	⊢ ( ( 𝐷 ‘ 𝐹 ) ∈ ℕ0 → ( ∃ 𝑑 ∈ ℕ0 ( 𝑑 = ( 𝐷 ‘ 𝐹 ) ∧ ( 𝐴 ‘ 𝑑 ) ≠ 𝑌 ) ↔ ( 𝐴 ‘ ( 𝐷 ‘ 𝐹 ) ) ≠ 𝑌 ) )
44	40 43	syl	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 0 ) → ( ∃ 𝑑 ∈ ℕ0 ( 𝑑 = ( 𝐷 ‘ 𝐹 ) ∧ ( 𝐴 ‘ 𝑑 ) ≠ 𝑌 ) ↔ ( 𝐴 ‘ ( 𝐷 ‘ 𝐹 ) ) ≠ 𝑌 ) )
45	39 44	bitrd	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 0 ) → ( ∃ 𝑏 ∈ ( ℕ0 ↑m 1o ) ( ( 𝐹 ‘ 𝑏 ) ≠ 𝑌 ∧ ( ( 𝑎 ∈ ( ℕ0 ↑m 1o ) ↦ ( 𝑎 ‘ ∅ ) ) ‘ 𝑏 ) = ( 𝐷 ‘ 𝐹 ) ) ↔ ( 𝐴 ‘ ( 𝐷 ‘ 𝐹 ) ) ≠ 𝑌 ) )
46	14 45	mpbid	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐹 ≠ 0 ) → ( 𝐴 ‘ ( 𝐷 ‘ 𝐹 ) ) ≠ 𝑌 )