Metamath Proof Explorer


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 ) )