Step |
Hyp |
Ref |
Expression |
1 |
|
srgz.b |
|- B = ( Base ` R ) |
2 |
|
srgz.t |
|- .x. = ( .r ` R ) |
3 |
|
srgz.z |
|- .0. = ( 0g ` R ) |
4 |
|
srgisid.1 |
|- ( ph -> R e. SRing ) |
5 |
|
srgisid.2 |
|- ( ph -> Z e. B ) |
6 |
|
srgisid.3 |
|- ( ( ph /\ x e. B ) -> ( Z .x. x ) = Z ) |
7 |
6
|
ralrimiva |
|- ( ph -> A. x e. B ( Z .x. x ) = Z ) |
8 |
1 3
|
srg0cl |
|- ( R e. SRing -> .0. e. B ) |
9 |
|
oveq2 |
|- ( x = .0. -> ( Z .x. x ) = ( Z .x. .0. ) ) |
10 |
9
|
eqeq1d |
|- ( x = .0. -> ( ( Z .x. x ) = Z <-> ( Z .x. .0. ) = Z ) ) |
11 |
10
|
rspcv |
|- ( .0. e. B -> ( A. x e. B ( Z .x. x ) = Z -> ( Z .x. .0. ) = Z ) ) |
12 |
4 8 11
|
3syl |
|- ( ph -> ( A. x e. B ( Z .x. x ) = Z -> ( Z .x. .0. ) = Z ) ) |
13 |
7 12
|
mpd |
|- ( ph -> ( Z .x. .0. ) = Z ) |
14 |
1 2 3
|
srgrz |
|- ( ( R e. SRing /\ Z e. B ) -> ( Z .x. .0. ) = .0. ) |
15 |
4 5 14
|
syl2anc |
|- ( ph -> ( Z .x. .0. ) = .0. ) |
16 |
13 15
|
eqtr3d |
|- ( ph -> Z = .0. ) |