ply1asclunit

Description: A non-zero scalar polynomial over a field F is a unit. (Contributed by Thierry Arnoux, 22-Mar-2025)

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		ply1asclunit.6	$⊢ φ \to Y \in B$
7		ply1asclunit.7	$⊢ φ \to Y \neq \underset{˙}{0}$
8	5	fldcrngd	$⊢ φ \to F \in CRing$
9	1	ply1assa	$⊢ F \in CRing \to P \in AssAlg$
10		eqid	$⊢ Scalar (P) = Scalar (P)$
11	2 10	asclrhm	$⊢ P \in AssAlg \to A \in (Scalar (P) RingHom P)$
12	8 9 11	3syl	$⊢ φ \to A \in (Scalar (P) RingHom P)$
13	1	ply1sca	$⊢ F \in Field \to F = Scalar (P)$
14	5 13	syl	$⊢ φ \to F = Scalar (P)$
15	14	oveq1d	$⊢ φ \to F RingHom P = Scalar (P) RingHom P$
16	12 15	eleqtrrd	$⊢ φ \to A \in (F RingHom P)$
17	5	flddrngd	$⊢ φ \to F \in DivRing$
18		eqid	$⊢ Unit (F) = Unit (F)$
19	3 18 4	drngunit	$⊢ F \in DivRing \to (Y \in Unit (F) \leftrightarrow (Y \in B \land Y \neq \underset{˙}{0}))$
20	19	biimpar	$⊢ (F \in DivRing \land (Y \in B \land Y \neq \underset{˙}{0})) \to Y \in Unit (F)$
21	17 6 7 20	syl12anc	$⊢ φ \to Y \in Unit (F)$
22		elrhmunit	$⊢ (A \in (F RingHom P) \land Y \in Unit (F)) \to A (Y) \in Unit (P)$
23	16 21 22	syl2anc	$⊢ φ \to A (Y) \in Unit (P)$

Metamath Proof Explorer