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