Theorem ply1asclunit

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

	Ref	Expression
Hypotheses	ply1asclunit.1	$$⊢P={\mathrm{Poly}}_1\left(F\right)$$
	ply1asclunit.2	$$⊢A=\mathrm{algSc}\left(P\right)$$
	ply1asclunit.3	$$⊢B={\mathrm{Base}}_F$$
	ply1asclunit.4	$$⊢\underset{\dot{}}{0}=0_F$$
	ply1asclunit.5	$$⊢\phi \to F\in \mathrm{Field}$$
	ply1asclunit.6	$$⊢\phi \to Y\in B$$
	ply1asclunit.7	$$⊢\phi \to Y\ne \underset{\dot{}}{0}$$
Assertion	ply1asclunit	$$⊢\phi \to A\left(Y\right)\in \mathrm{Unit}\left(P\right)$$

Proof

Step	Hyp	Ref	Expression
1		ply1asclunit.1	$$⊢P={\mathrm{Poly}}_1\left(F\right)$$
2		ply1asclunit.2	$$⊢A=\mathrm{algSc}\left(P\right)$$
3		ply1asclunit.3	$$⊢B={\mathrm{Base}}_F$$
4		ply1asclunit.4	$$⊢\underset{\dot{}}{0}=0_F$$
5		ply1asclunit.5	$$⊢\phi \to F\in \mathrm{Field}$$
6		ply1asclunit.6	$$⊢\phi \to Y\in B$$
7		ply1asclunit.7	$$⊢\phi \to Y\ne \underset{\dot{}}{0}$$
8	5	fldcrngd	$$⊢\phi \to F\in \mathrm{CRing}$$
9	1	ply1assa	$$⊢F\in \mathrm{CRing}\to P\in \mathrm{AssAlg}$$
10		eqid	$$⊢\mathrm{Scalar}\left(P\right)=\mathrm{Scalar}\left(P\right)$$
11	2 10	asclrhm	$$⊢P\in \mathrm{AssAlg}\to A\in \left(\mathrm{Scalar}\left(P\right)\mathrm{RingHom}P\right)$$
12	8 9 11	3syl	$$⊢\phi \to A\in \left(\mathrm{Scalar}\left(P\right)\mathrm{RingHom}P\right)$$
13	1	ply1sca	$$⊢F\in \mathrm{Field}\to F=\mathrm{Scalar}\left(P\right)$$
14	5 13	syl	$$⊢\phi \to F=\mathrm{Scalar}\left(P\right)$$
15	14	oveq1d	$$⊢\phi \to F\mathrm{RingHom}P=\mathrm{Scalar}\left(P\right)\mathrm{RingHom}P$$
16	12 15	eleqtrrd	$$⊢\phi \to A\in \left(F\mathrm{RingHom}P\right)$$
17	5	flddrngd	$$⊢\phi \to F\in \mathrm{DivRing}$$
18		eqid	$$⊢\mathrm{Unit}\left(F\right)=\mathrm{Unit}\left(F\right)$$
19	3 18 4	drngunit	$$⊢F\in \mathrm{DivRing}\to \left(Y\in \mathrm{Unit}\left(F\right)\leftrightarrow \left(Y\in B\wedge Y\ne \underset{\dot{}}{0}\right)\right)$$
20	19	biimpar	$$⊢\left(F\in \mathrm{DivRing}\wedge \left(Y\in B\wedge Y\ne \underset{\dot{}}{0}\right)\right)\to Y\in \mathrm{Unit}\left(F\right)$$
21	17 6 7 20	syl12anc	$$⊢\phi \to Y\in \mathrm{Unit}\left(F\right)$$
22		elrhmunit	$$⊢\left(A\in \left(F\mathrm{RingHom}P\right)\wedge Y\in \mathrm{Unit}\left(F\right)\right)\to A\left(Y\right)\in \mathrm{Unit}\left(P\right)$$
23	16 21 22	syl2anc	$$⊢\phi \to A\left(Y\right)\in \mathrm{Unit}\left(P\right)$$