ply1unit

Description: In a field F , a polynomial C is a unit iff it has degree 0. This corresponds to the nonzero scalars, see ply1asclunit . (Contributed by Thierry Arnoux, 25-Apr-2025)

	Ref	Expression
Hypotheses	ply1asclunit.1	$⊢ P = {Poly}_{1} (F)$
	ply1asclunit.2	$⊢ A = algSc (P)$
	ply1asclunit.3	$⊢ B = {Base}_{F}$
	ply1asclunit.4	$⊢ \underset{˙}{0} = 0_{F}$
	ply1asclunit.5	$⊢ φ \to F \in Field$
	ply1unit.d	$⊢ D = \deg_{1} (F)$
	ply1unit.f	$⊢ φ \to C \in {Base}_{P}$
Assertion	ply1unit	$⊢ φ \to (C \in Unit (P) \leftrightarrow D (C) = 0)$

Proof

Step	Hyp	Ref	Expression
1		ply1asclunit.1	$⊢ P = {Poly}_{1} (F)$
2		ply1asclunit.2	$⊢ A = algSc (P)$
3		ply1asclunit.3	$⊢ B = {Base}_{F}$
4		ply1asclunit.4	$⊢ \underset{˙}{0} = 0_{F}$
5		ply1asclunit.5	$⊢ φ \to F \in Field$
6		ply1unit.d	$⊢ D = \deg_{1} (F)$
7		ply1unit.f	$⊢ φ \to C \in {Base}_{P}$
8	5	fldcrngd	$⊢ φ \to F \in CRing$
9	8	crngringd	$⊢ φ \to F \in Ring$
10	9	adantr	$⊢ (φ \land C \in Unit (P)) \to F \in Ring$
11	1	ply1ring	$⊢ F \in Ring \to P \in Ring$
12	9 11	syl	$⊢ φ \to P \in Ring$
13		eqid	$⊢ Unit (P) = Unit (P)$
14		eqid	$⊢ {inv}_{r} (P) = {inv}_{r} (P)$
15	13 14	unitinvcl	$⊢ (P \in Ring \land C \in Unit (P)) \to {inv}_{r} (P) (C) \in Unit (P)$
16	12 15	sylan	$⊢ (φ \land C \in Unit (P)) \to {inv}_{r} (P) (C) \in Unit (P)$
17		eqid	$⊢ {Base}_{P} = {Base}_{P}$
18	17 13	unitcl	$⊢ {inv}_{r} (P) (C) \in Unit (P) \to {inv}_{r} (P) (C) \in {Base}_{P}$
19	16 18	syl	$⊢ (φ \land C \in Unit (P)) \to {inv}_{r} (P) (C) \in {Base}_{P}$
20		eqid	$⊢ 0_{P} = 0_{P}$
21	5	flddrngd	$⊢ φ \to F \in DivRing$
22		drngnzr	$⊢ F \in DivRing \to F \in NzRing$
23	1	ply1nz	$⊢ F \in NzRing \to P \in NzRing$
24	21 22 23	3syl	$⊢ φ \to P \in NzRing$
25	24	adantr	$⊢ (φ \land C \in Unit (P)) \to P \in NzRing$
26	13 20 25 16	unitnz	$⊢ (φ \land C \in Unit (P)) \to {inv}_{r} (P) (C) \neq 0_{P}$
27	6 1 20 17	deg1nn0cl	$⊢ (F \in Ring \land {inv}_{r} (P) (C) \in {Base}_{P} \land {inv}_{r} (P) (C) \neq 0_{P}) \to D ({inv}_{r} (P) (C)) \in ℕ_{0}$
28	10 19 26 27	syl3anc	$⊢ (φ \land C \in Unit (P)) \to D ({inv}_{r} (P) (C)) \in ℕ_{0}$
29	28	nn0red	$⊢ (φ \land C \in Unit (P)) \to D ({inv}_{r} (P) (C)) \in ℝ$
30	28	nn0ge0d	$⊢ (φ \land C \in Unit (P)) \to 0 \leq D ({inv}_{r} (P) (C))$
31	29 30	jca	$⊢ (φ \land C \in Unit (P)) \to (D ({inv}_{r} (P) (C)) \in ℝ \land 0 \leq D ({inv}_{r} (P) (C)))$
32	7	adantr	$⊢ (φ \land C \in Unit (P)) \to C \in {Base}_{P}$
33		simpr	$⊢ (φ \land C \in Unit (P)) \to C \in Unit (P)$
34	13 20 25 33	unitnz	$⊢ (φ \land C \in Unit (P)) \to C \neq 0_{P}$
35	6 1 20 17	deg1nn0cl	$⊢ (F \in Ring \land C \in {Base}_{P} \land C \neq 0_{P}) \to D (C) \in ℕ_{0}$
36	10 32 34 35	syl3anc	$⊢ (φ \land C \in Unit (P)) \to D (C) \in ℕ_{0}$
37	36	nn0red	$⊢ (φ \land C \in Unit (P)) \to D (C) \in ℝ$
38	36	nn0ge0d	$⊢ (φ \land C \in Unit (P)) \to 0 \leq D (C)$
39		eqid	$⊢ \cdot_{P} = \cdot_{P}$
40		eqid	$⊢ 1_{P} = 1_{P}$
41	13 14 39 40	unitlinv	$⊢ (P \in Ring \land C \in Unit (P)) \to {inv}_{r} (P) (C) \cdot_{P} C = 1_{P}$
42	12 41	sylan	$⊢ (φ \land C \in Unit (P)) \to {inv}_{r} (P) (C) \cdot_{P} C = 1_{P}$
43	42	fveq2d	$⊢ (φ \land C \in Unit (P)) \to D ({inv}_{r} (P) (C) \cdot_{P} C) = D (1_{P})$
44		eqid	$⊢ RLReg (F) = RLReg (F)$
45		drngdomn	$⊢ F \in DivRing \to F \in Domn$
46	21 45	syl	$⊢ φ \to F \in Domn$
47	46	adantr	$⊢ (φ \land C \in Unit (P)) \to F \in Domn$
48		eqid	$⊢ {coe}_{1} ({inv}_{r} (P) (C)) = {coe}_{1} ({inv}_{r} (P) (C))$
49	48 17 1 3	coe1fvalcl	$⊢ ({inv}_{r} (P) (C) \in {Base}_{P} \land D ({inv}_{r} (P) (C)) \in ℕ_{0}) \to {coe}_{1} ({inv}_{r} (P) (C)) (D ({inv}_{r} (P) (C))) \in B$
50	19 28 49	syl2anc	$⊢ (φ \land C \in Unit (P)) \to {coe}_{1} ({inv}_{r} (P) (C)) (D ({inv}_{r} (P) (C))) \in B$
51	6 1 20 17 4 48	deg1ldg	$⊢ (F \in Ring \land {inv}_{r} (P) (C) \in {Base}_{P} \land {inv}_{r} (P) (C) \neq 0_{P}) \to {coe}_{1} ({inv}_{r} (P) (C)) (D ({inv}_{r} (P) (C))) \neq \underset{˙}{0}$
52	10 19 26 51	syl3anc	$⊢ (φ \land C \in Unit (P)) \to {coe}_{1} ({inv}_{r} (P) (C)) (D ({inv}_{r} (P) (C))) \neq \underset{˙}{0}$
53	3 44 4	domnrrg	$⊢ (F \in Domn \land {coe}_{1} ({inv}_{r} (P) (C)) (D ({inv}_{r} (P) (C))) \in B \land {coe}_{1} ({inv}_{r} (P) (C)) (D ({inv}_{r} (P) (C))) \neq \underset{˙}{0}) \to {coe}_{1} ({inv}_{r} (P) (C)) (D ({inv}_{r} (P) (C))) \in RLReg (F)$
54	47 50 52 53	syl3anc	$⊢ (φ \land C \in Unit (P)) \to {coe}_{1} ({inv}_{r} (P) (C)) (D ({inv}_{r} (P) (C))) \in RLReg (F)$
55	6 1 44 17 39 20 10 19 26 54 32 34	deg1mul2	$⊢ (φ \land C \in Unit (P)) \to D ({inv}_{r} (P) (C) \cdot_{P} C) = D ({inv}_{r} (P) (C)) + D (C)$
56		eqid	$⊢ {Monic}_{1p} (F) = {Monic}_{1p} (F)$
57	1 40 56 6	mon1pid	$⊢ F \in NzRing \to (1_{P} \in {Monic}_{1p} (F) \land D (1_{P}) = 0)$
58	57	simprd	$⊢ F \in NzRing \to D (1_{P}) = 0$
59	21 22 58	3syl	$⊢ φ \to D (1_{P}) = 0$
60	59	adantr	$⊢ (φ \land C \in Unit (P)) \to D (1_{P}) = 0$
61	43 55 60	3eqtr3d	$⊢ (φ \land C \in Unit (P)) \to D ({inv}_{r} (P) (C)) + D (C) = 0$
62		add20	$⊢ ((D ({inv}_{r} (P) (C)) \in ℝ \land 0 \leq D ({inv}_{r} (P) (C))) \land (D (C) \in ℝ \land 0 \leq D (C))) \to (D ({inv}_{r} (P) (C)) + D (C) = 0 \leftrightarrow (D ({inv}_{r} (P) (C)) = 0 \land D (C) = 0))$
63	62	anassrs	$⊢ (((D ({inv}_{r} (P) (C)) \in ℝ \land 0 \leq D ({inv}_{r} (P) (C))) \land D (C) \in ℝ) \land 0 \leq D (C)) \to (D ({inv}_{r} (P) (C)) + D (C) = 0 \leftrightarrow (D ({inv}_{r} (P) (C)) = 0 \land D (C) = 0))$
64	63	simplbda	$⊢ ((((D ({inv}_{r} (P) (C)) \in ℝ \land 0 \leq D ({inv}_{r} (P) (C))) \land D (C) \in ℝ) \land 0 \leq D (C)) \land D ({inv}_{r} (P) (C)) + D (C) = 0) \to D (C) = 0$
65	31 37 38 61 64	syl1111anc	$⊢ (φ \land C \in Unit (P)) \to D (C) = 0$
66	9	adantr	$⊢ (φ \land D (C) = 0) \to F \in Ring$
67	7	adantr	$⊢ (φ \land D (C) = 0) \to C \in {Base}_{P}$
68	6 1 17	deg1xrcl	$⊢ C \in {Base}_{P} \to D (C) \in ℝ^{*}$
69	7 68	syl	$⊢ φ \to D (C) \in ℝ^{*}$
70		0xr	$⊢ 0 \in ℝ^{*}$
71		xeqlelt	$⊢ (D (C) \in ℝ^{} \land 0 \in ℝ^{}) \to (D (C) = 0 \leftrightarrow (D (C) \leq 0 \land \neg D (C) < 0))$
72	69 70 71	sylancl	$⊢ φ \to (D (C) = 0 \leftrightarrow (D (C) \leq 0 \land \neg D (C) < 0))$
73	72	simprbda	$⊢ (φ \land D (C) = 0) \to D (C) \leq 0$
74	6 1 17 2	deg1le0	$⊢ (F \in Ring \land C \in {Base}_{P}) \to (D (C) \leq 0 \leftrightarrow C = A ({coe}_{1} (C) (0)))$
75	74	biimpa	$⊢ ((F \in Ring \land C \in {Base}_{P}) \land D (C) \leq 0) \to C = A ({coe}_{1} (C) (0))$
76	66 67 73 75	syl21anc	$⊢ (φ \land D (C) = 0) \to C = A ({coe}_{1} (C) (0))$
77	5	adantr	$⊢ (φ \land D (C) = 0) \to F \in Field$
78		0nn0	$⊢ 0 \in ℕ_{0}$
79		eqid	$⊢ {coe}_{1} (C) = {coe}_{1} (C)$
80	79 17 1 3	coe1fvalcl	$⊢ (C \in {Base}_{P} \land 0 \in ℕ_{0}) \to {coe}_{1} (C) (0) \in B$
81	67 78 80	sylancl	$⊢ (φ \land D (C) = 0) \to {coe}_{1} (C) (0) \in B$
82		simpl	$⊢ (φ \land D (C) = 0) \to φ$
83	72	simplbda	$⊢ (φ \land D (C) = 0) \to \neg D (C) < 0$
84	6 1 20 17	deg1lt0	$⊢ (F \in Ring \land C \in {Base}_{P}) \to (D (C) < 0 \leftrightarrow C = 0_{P})$
85	84	necon3bbid	$⊢ (F \in Ring \land C \in {Base}_{P}) \to (\neg D (C) < 0 \leftrightarrow C \neq 0_{P})$
86	85	biimpa	$⊢ ((F \in Ring \land C \in {Base}_{P}) \land \neg D (C) < 0) \to C \neq 0_{P}$
87	66 67 83 86	syl21anc	$⊢ (φ \land D (C) = 0) \to C \neq 0_{P}$
88	9	adantr	$⊢ (φ \land D (C) \leq 0) \to F \in Ring$
89	7	adantr	$⊢ (φ \land D (C) \leq 0) \to C \in {Base}_{P}$
90		simpr	$⊢ (φ \land D (C) \leq 0) \to D (C) \leq 0$
91	6 1 4 17 20 88 89 90	deg1le0eq0	$⊢ (φ \land D (C) \leq 0) \to (C = 0_{P} \leftrightarrow {coe}_{1} (C) (0) = \underset{˙}{0})$
92	91	necon3bid	$⊢ (φ \land D (C) \leq 0) \to (C \neq 0_{P} \leftrightarrow {coe}_{1} (C) (0) \neq \underset{˙}{0})$
93	92	biimpa	$⊢ ((φ \land D (C) \leq 0) \land C \neq 0_{P}) \to {coe}_{1} (C) (0) \neq \underset{˙}{0}$
94	82 73 87 93	syl21anc	$⊢ (φ \land D (C) = 0) \to {coe}_{1} (C) (0) \neq \underset{˙}{0}$
95	1 2 3 4 77 81 94	ply1asclunit	$⊢ (φ \land D (C) = 0) \to A ({coe}_{1} (C) (0)) \in Unit (P)$
96	76 95	eqeltrd	$⊢ (φ \land D (C) = 0) \to C \in Unit (P)$
97	65 96	impbida	$⊢ φ \to (C \in Unit (P) \leftrightarrow D (C) = 0)$

Metamath Proof Explorer

Theorem ply1unit

Proof