| Step |
Hyp |
Ref |
Expression |
| 1 |
|
drgext.b |
|- B = ( ( subringAlg ` E ) ` U ) |
| 2 |
|
drgext.1 |
|- ( ph -> E e. DivRing ) |
| 3 |
|
drgext.2 |
|- ( ph -> U e. ( SubRing ` E ) ) |
| 4 |
|
drngring |
|- ( E e. DivRing -> E e. Ring ) |
| 5 |
|
ringmnd |
|- ( E e. Ring -> E e. Mnd ) |
| 6 |
2 4 5
|
3syl |
|- ( ph -> E e. Mnd ) |
| 7 |
|
subrgsubg |
|- ( U e. ( SubRing ` E ) -> U e. ( SubGrp ` E ) ) |
| 8 |
|
eqid |
|- ( 0g ` E ) = ( 0g ` E ) |
| 9 |
8
|
subg0cl |
|- ( U e. ( SubGrp ` E ) -> ( 0g ` E ) e. U ) |
| 10 |
3 7 9
|
3syl |
|- ( ph -> ( 0g ` E ) e. U ) |
| 11 |
|
eqid |
|- ( Base ` E ) = ( Base ` E ) |
| 12 |
11
|
subrgss |
|- ( U e. ( SubRing ` E ) -> U C_ ( Base ` E ) ) |
| 13 |
3 12
|
syl |
|- ( ph -> U C_ ( Base ` E ) ) |
| 14 |
|
eqid |
|- ( E |`s U ) = ( E |`s U ) |
| 15 |
14 11 8
|
ress0g |
|- ( ( E e. Mnd /\ ( 0g ` E ) e. U /\ U C_ ( Base ` E ) ) -> ( 0g ` E ) = ( 0g ` ( E |`s U ) ) ) |
| 16 |
6 10 13 15
|
syl3anc |
|- ( ph -> ( 0g ` E ) = ( 0g ` ( E |`s U ) ) ) |
| 17 |
1 2 3
|
drgext0g |
|- ( ph -> ( 0g ` E ) = ( 0g ` B ) ) |
| 18 |
1
|
a1i |
|- ( ph -> B = ( ( subringAlg ` E ) ` U ) ) |
| 19 |
18 13
|
srasca |
|- ( ph -> ( E |`s U ) = ( Scalar ` B ) ) |
| 20 |
19
|
fveq2d |
|- ( ph -> ( 0g ` ( E |`s U ) ) = ( 0g ` ( Scalar ` B ) ) ) |
| 21 |
16 17 20
|
3eqtr3d |
|- ( ph -> ( 0g ` B ) = ( 0g ` ( Scalar ` B ) ) ) |