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