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