| Step |
Hyp |
Ref |
Expression |
| 1 |
|
ring1cl.1 |
|- X = ran ( 1st ` R ) |
| 2 |
|
ring1cl.2 |
|- H = ( 2nd ` R ) |
| 3 |
|
ring1cl.3 |
|- U = ( GId ` H ) |
| 4 |
2
|
rngomndo |
|- ( R e. RingOps -> H e. MndOp ) |
| 5 |
2
|
eleq1i |
|- ( H e. MndOp <-> ( 2nd ` R ) e. MndOp ) |
| 6 |
|
mndoismgmOLD |
|- ( ( 2nd ` R ) e. MndOp -> ( 2nd ` R ) e. Magma ) |
| 7 |
|
mndoisexid |
|- ( ( 2nd ` R ) e. MndOp -> ( 2nd ` R ) e. ExId ) |
| 8 |
6 7
|
jca |
|- ( ( 2nd ` R ) e. MndOp -> ( ( 2nd ` R ) e. Magma /\ ( 2nd ` R ) e. ExId ) ) |
| 9 |
5 8
|
sylbi |
|- ( H e. MndOp -> ( ( 2nd ` R ) e. Magma /\ ( 2nd ` R ) e. ExId ) ) |
| 10 |
4 9
|
syl |
|- ( R e. RingOps -> ( ( 2nd ` R ) e. Magma /\ ( 2nd ` R ) e. ExId ) ) |
| 11 |
|
elin |
|- ( ( 2nd ` R ) e. ( Magma i^i ExId ) <-> ( ( 2nd ` R ) e. Magma /\ ( 2nd ` R ) e. ExId ) ) |
| 12 |
10 11
|
sylibr |
|- ( R e. RingOps -> ( 2nd ` R ) e. ( Magma i^i ExId ) ) |
| 13 |
|
eqid |
|- ran ( 2nd ` R ) = ran ( 2nd ` R ) |
| 14 |
2
|
fveq2i |
|- ( GId ` H ) = ( GId ` ( 2nd ` R ) ) |
| 15 |
3 14
|
eqtri |
|- U = ( GId ` ( 2nd ` R ) ) |
| 16 |
13 15
|
iorlid |
|- ( ( 2nd ` R ) e. ( Magma i^i ExId ) -> U e. ran ( 2nd ` R ) ) |
| 17 |
12 16
|
syl |
|- ( R e. RingOps -> U e. ran ( 2nd ` R ) ) |
| 18 |
|
eqid |
|- ( 2nd ` R ) = ( 2nd ` R ) |
| 19 |
|
eqid |
|- ( 1st ` R ) = ( 1st ` R ) |
| 20 |
18 19
|
rngorn1eq |
|- ( R e. RingOps -> ran ( 1st ` R ) = ran ( 2nd ` R ) ) |
| 21 |
|
eqtr |
|- ( ( X = ran ( 1st ` R ) /\ ran ( 1st ` R ) = ran ( 2nd ` R ) ) -> X = ran ( 2nd ` R ) ) |
| 22 |
21
|
eleq2d |
|- ( ( X = ran ( 1st ` R ) /\ ran ( 1st ` R ) = ran ( 2nd ` R ) ) -> ( U e. X <-> U e. ran ( 2nd ` R ) ) ) |
| 23 |
1 20 22
|
sylancr |
|- ( R e. RingOps -> ( U e. X <-> U e. ran ( 2nd ` R ) ) ) |
| 24 |
17 23
|
mpbird |
|- ( R e. RingOps -> U e. X ) |