Theorem ply1asclunit

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

	Ref	Expression
Hypotheses	ply1asclunit.1	|- P = ( Poly1 ` F )
	ply1asclunit.2	|- A = ( algSc ` P )
	ply1asclunit.3	|- B = ( Base ` F )
	ply1asclunit.4	|- .0. = ( 0g ` F )
	ply1asclunit.5	|- ( ph -> F e. Field )
	ply1asclunit.6	|- ( ph -> Y e. B )
	ply1asclunit.7	|- ( ph -> Y =/= .0. )
Assertion	ply1asclunit	|- ( ph -> ( A ` Y ) e. ( Unit ` P ) )

Proof

Step	Hyp	Ref	Expression
1		ply1asclunit.1	|- P = ( Poly1 ` F )
2		ply1asclunit.2	|- A = ( algSc ` P )
3		ply1asclunit.3	|- B = ( Base ` F )
4		ply1asclunit.4	|- .0. = ( 0g ` F )
5		ply1asclunit.5	|- ( ph -> F e. Field )
6		ply1asclunit.6	|- ( ph -> Y e. B )
7		ply1asclunit.7	|- ( ph -> Y =/= .0. )
8	5	fldcrngd	|- ( ph -> F e. CRing )
9	1	ply1assa	|- ( F e. CRing -> P e. AssAlg )
10		eqid	|- ( Scalar ` P ) = ( Scalar ` P )
11	2 10	asclrhm	|- ( P e. AssAlg -> A e. ( ( Scalar ` P ) RingHom P ) )
12	8 9 11	3syl	|- ( ph -> A e. ( ( Scalar ` P ) RingHom P ) )
13	1	ply1sca	|- ( F e. Field -> F = ( Scalar ` P ) )
14	5 13	syl	|- ( ph -> F = ( Scalar ` P ) )
15	14	oveq1d	|- ( ph -> ( F RingHom P ) = ( ( Scalar ` P ) RingHom P ) )
16	12 15	eleqtrrd	|- ( ph -> A e. ( F RingHom P ) )
17	5	flddrngd	|- ( ph -> F e. DivRing )
18		eqid	|- ( Unit ` F ) = ( Unit ` F )
19	3 18 4	drngunit	|- ( F e. DivRing -> ( Y e. ( Unit ` F ) <-> ( Y e. B /\ Y =/= .0. ) ) )
20	19	biimpar	|- ( ( F e. DivRing /\ ( Y e. B /\ Y =/= .0. ) ) -> Y e. ( Unit ` F ) )
21	17 6 7 20	syl12anc	|- ( ph -> Y e. ( Unit ` F ) )
22		elrhmunit	|- ( ( A e. ( F RingHom P ) /\ Y e. ( Unit ` F ) ) -> ( A ` Y ) e. ( Unit ` P ) )
23	16 21 22	syl2anc	|- ( ph -> ( A ` Y ) e. ( Unit ` P ) )