Step |
Hyp |
Ref |
Expression |
1 |
|
unmnd.1 |
|- H = ( 2nd ` R ) |
2 |
|
eqid |
|- ( 1st ` R ) = ( 1st ` R ) |
3 |
|
eqid |
|- ran ( 1st ` R ) = ran ( 1st ` R ) |
4 |
2 1 3
|
rngosm |
|- ( R e. RingOps -> H : ( ran ( 1st ` R ) X. ran ( 1st ` R ) ) --> ran ( 1st ` R ) ) |
5 |
2 1 3
|
rngoass |
|- ( ( R e. RingOps /\ ( x e. ran ( 1st ` R ) /\ y e. ran ( 1st ` R ) /\ z e. ran ( 1st ` R ) ) ) -> ( ( x H y ) H z ) = ( x H ( y H z ) ) ) |
6 |
5
|
ralrimivvva |
|- ( R e. RingOps -> A. x e. ran ( 1st ` R ) A. y e. ran ( 1st ` R ) A. z e. ran ( 1st ` R ) ( ( x H y ) H z ) = ( x H ( y H z ) ) ) |
7 |
2 1 3
|
rngoi |
|- ( R e. RingOps -> ( ( ( 1st ` R ) e. AbelOp /\ H : ( ran ( 1st ` R ) X. ran ( 1st ` R ) ) --> ran ( 1st ` R ) ) /\ ( A. x e. ran ( 1st ` R ) A. y e. ran ( 1st ` R ) A. z e. ran ( 1st ` R ) ( ( ( x H y ) H z ) = ( x H ( y H z ) ) /\ ( x H ( y ( 1st ` R ) z ) ) = ( ( x H y ) ( 1st ` R ) ( x H z ) ) /\ ( ( x ( 1st ` R ) y ) H z ) = ( ( x H z ) ( 1st ` R ) ( y H z ) ) ) /\ E. x e. ran ( 1st ` R ) A. y e. ran ( 1st ` R ) ( ( x H y ) = y /\ ( y H x ) = y ) ) ) ) |
8 |
7
|
simprrd |
|- ( R e. RingOps -> E. x e. ran ( 1st ` R ) A. y e. ran ( 1st ` R ) ( ( x H y ) = y /\ ( y H x ) = y ) ) |
9 |
1 2
|
rngorn1 |
|- ( R e. RingOps -> ran ( 1st ` R ) = dom dom H ) |
10 |
|
xpid11 |
|- ( ( dom dom H X. dom dom H ) = ( ran ( 1st ` R ) X. ran ( 1st ` R ) ) <-> dom dom H = ran ( 1st ` R ) ) |
11 |
10
|
biimpri |
|- ( dom dom H = ran ( 1st ` R ) -> ( dom dom H X. dom dom H ) = ( ran ( 1st ` R ) X. ran ( 1st ` R ) ) ) |
12 |
|
feq23 |
|- ( ( ( dom dom H X. dom dom H ) = ( ran ( 1st ` R ) X. ran ( 1st ` R ) ) /\ dom dom H = ran ( 1st ` R ) ) -> ( H : ( dom dom H X. dom dom H ) --> dom dom H <-> H : ( ran ( 1st ` R ) X. ran ( 1st ` R ) ) --> ran ( 1st ` R ) ) ) |
13 |
11 12
|
mpancom |
|- ( dom dom H = ran ( 1st ` R ) -> ( H : ( dom dom H X. dom dom H ) --> dom dom H <-> H : ( ran ( 1st ` R ) X. ran ( 1st ` R ) ) --> ran ( 1st ` R ) ) ) |
14 |
|
raleq |
|- ( dom dom H = ran ( 1st ` R ) -> ( A. z e. dom dom H ( ( x H y ) H z ) = ( x H ( y H z ) ) <-> A. z e. ran ( 1st ` R ) ( ( x H y ) H z ) = ( x H ( y H z ) ) ) ) |
15 |
14
|
raleqbi1dv |
|- ( dom dom H = ran ( 1st ` R ) -> ( A. y e. dom dom H A. z e. dom dom H ( ( x H y ) H z ) = ( x H ( y H z ) ) <-> A. y e. ran ( 1st ` R ) A. z e. ran ( 1st ` R ) ( ( x H y ) H z ) = ( x H ( y H z ) ) ) ) |
16 |
15
|
raleqbi1dv |
|- ( dom dom H = ran ( 1st ` R ) -> ( A. x e. dom dom H A. y e. dom dom H A. z e. dom dom H ( ( x H y ) H z ) = ( x H ( y H z ) ) <-> A. x e. ran ( 1st ` R ) A. y e. ran ( 1st ` R ) A. z e. ran ( 1st ` R ) ( ( x H y ) H z ) = ( x H ( y H z ) ) ) ) |
17 |
|
raleq |
|- ( dom dom H = ran ( 1st ` R ) -> ( A. y e. dom dom H ( ( x H y ) = y /\ ( y H x ) = y ) <-> A. y e. ran ( 1st ` R ) ( ( x H y ) = y /\ ( y H x ) = y ) ) ) |
18 |
17
|
rexeqbi1dv |
|- ( dom dom H = ran ( 1st ` R ) -> ( E. x e. dom dom H A. y e. dom dom H ( ( x H y ) = y /\ ( y H x ) = y ) <-> E. x e. ran ( 1st ` R ) A. y e. ran ( 1st ` R ) ( ( x H y ) = y /\ ( y H x ) = y ) ) ) |
19 |
13 16 18
|
3anbi123d |
|- ( dom dom H = ran ( 1st ` R ) -> ( ( H : ( dom dom H X. dom dom H ) --> dom dom H /\ A. x e. dom dom H A. y e. dom dom H A. z e. dom dom H ( ( x H y ) H z ) = ( x H ( y H z ) ) /\ E. x e. dom dom H A. y e. dom dom H ( ( x H y ) = y /\ ( y H x ) = y ) ) <-> ( H : ( ran ( 1st ` R ) X. ran ( 1st ` R ) ) --> ran ( 1st ` R ) /\ A. x e. ran ( 1st ` R ) A. y e. ran ( 1st ` R ) A. z e. ran ( 1st ` R ) ( ( x H y ) H z ) = ( x H ( y H z ) ) /\ E. x e. ran ( 1st ` R ) A. y e. ran ( 1st ` R ) ( ( x H y ) = y /\ ( y H x ) = y ) ) ) ) |
20 |
19
|
eqcoms |
|- ( ran ( 1st ` R ) = dom dom H -> ( ( H : ( dom dom H X. dom dom H ) --> dom dom H /\ A. x e. dom dom H A. y e. dom dom H A. z e. dom dom H ( ( x H y ) H z ) = ( x H ( y H z ) ) /\ E. x e. dom dom H A. y e. dom dom H ( ( x H y ) = y /\ ( y H x ) = y ) ) <-> ( H : ( ran ( 1st ` R ) X. ran ( 1st ` R ) ) --> ran ( 1st ` R ) /\ A. x e. ran ( 1st ` R ) A. y e. ran ( 1st ` R ) A. z e. ran ( 1st ` R ) ( ( x H y ) H z ) = ( x H ( y H z ) ) /\ E. x e. ran ( 1st ` R ) A. y e. ran ( 1st ` R ) ( ( x H y ) = y /\ ( y H x ) = y ) ) ) ) |
21 |
9 20
|
syl |
|- ( R e. RingOps -> ( ( H : ( dom dom H X. dom dom H ) --> dom dom H /\ A. x e. dom dom H A. y e. dom dom H A. z e. dom dom H ( ( x H y ) H z ) = ( x H ( y H z ) ) /\ E. x e. dom dom H A. y e. dom dom H ( ( x H y ) = y /\ ( y H x ) = y ) ) <-> ( H : ( ran ( 1st ` R ) X. ran ( 1st ` R ) ) --> ran ( 1st ` R ) /\ A. x e. ran ( 1st ` R ) A. y e. ran ( 1st ` R ) A. z e. ran ( 1st ` R ) ( ( x H y ) H z ) = ( x H ( y H z ) ) /\ E. x e. ran ( 1st ` R ) A. y e. ran ( 1st ` R ) ( ( x H y ) = y /\ ( y H x ) = y ) ) ) ) |
22 |
4 6 8 21
|
mpbir3and |
|- ( R e. RingOps -> ( H : ( dom dom H X. dom dom H ) --> dom dom H /\ A. x e. dom dom H A. y e. dom dom H A. z e. dom dom H ( ( x H y ) H z ) = ( x H ( y H z ) ) /\ E. x e. dom dom H A. y e. dom dom H ( ( x H y ) = y /\ ( y H x ) = y ) ) ) |
23 |
|
fvex |
|- ( 2nd ` R ) e. _V |
24 |
|
eleq1 |
|- ( H = ( 2nd ` R ) -> ( H e. _V <-> ( 2nd ` R ) e. _V ) ) |
25 |
23 24
|
mpbiri |
|- ( H = ( 2nd ` R ) -> H e. _V ) |
26 |
|
eqid |
|- dom dom H = dom dom H |
27 |
26
|
ismndo1 |
|- ( H e. _V -> ( H e. MndOp <-> ( H : ( dom dom H X. dom dom H ) --> dom dom H /\ A. x e. dom dom H A. y e. dom dom H A. z e. dom dom H ( ( x H y ) H z ) = ( x H ( y H z ) ) /\ E. x e. dom dom H A. y e. dom dom H ( ( x H y ) = y /\ ( y H x ) = y ) ) ) ) |
28 |
1 25 27
|
mp2b |
|- ( H e. MndOp <-> ( H : ( dom dom H X. dom dom H ) --> dom dom H /\ A. x e. dom dom H A. y e. dom dom H A. z e. dom dom H ( ( x H y ) H z ) = ( x H ( y H z ) ) /\ E. x e. dom dom H A. y e. dom dom H ( ( x H y ) = y /\ ( y H x ) = y ) ) ) |
29 |
22 28
|
sylibr |
|- ( R e. RingOps -> H e. MndOp ) |