Step |
Hyp |
Ref |
Expression |
1 |
|
crngohomfo.1 |
|
2 |
|
crngohomfo.2 |
|
3 |
|
crngohomfo.3 |
|
4 |
|
crngohomfo.4 |
|
5 |
|
simplr |
Could not format ( ( ( R e. CRingOps /\ S e. RingOps ) /\ ( F e. ( R RingOpsHom S ) /\ F : X -onto-> Y ) ) -> S e. RingOps ) : No typesetting found for |- ( ( ( R e. CRingOps /\ S e. RingOps ) /\ ( F e. ( R RingOpsHom S ) /\ F : X -onto-> Y ) ) -> S e. RingOps ) with typecode |- |
6 |
|
foelrn |
|
7 |
6
|
ex |
|
8 |
|
foelrn |
|
9 |
8
|
ex |
|
10 |
7 9
|
anim12d |
|
11 |
|
reeanv |
|
12 |
10 11
|
imbitrrdi |
|
13 |
12
|
ad2antll |
Could not format ( ( ( R e. CRingOps /\ S e. RingOps ) /\ ( F e. ( R RingOpsHom S ) /\ F : X -onto-> Y ) ) -> ( ( y e. Y /\ z e. Y ) -> E. w e. X E. x e. X ( y = ( F ` w ) /\ z = ( F ` x ) ) ) ) : No typesetting found for |- ( ( ( R e. CRingOps /\ S e. RingOps ) /\ ( F e. ( R RingOpsHom S ) /\ F : X -onto-> Y ) ) -> ( ( y e. Y /\ z e. Y ) -> E. w e. X E. x e. X ( y = ( F ` w ) /\ z = ( F ` x ) ) ) ) with typecode |- |
14 |
|
eqid |
|
15 |
1 14 2
|
crngocom |
|
16 |
15
|
3expb |
|
17 |
16
|
3ad2antl1 |
Could not format ( ( ( R e. CRingOps /\ S e. RingOps /\ F e. ( R RingOpsHom S ) ) /\ ( w e. X /\ x e. X ) ) -> ( w ( 2nd ` R ) x ) = ( x ( 2nd ` R ) w ) ) : No typesetting found for |- ( ( ( R e. CRingOps /\ S e. RingOps /\ F e. ( R RingOpsHom S ) ) /\ ( w e. X /\ x e. X ) ) -> ( w ( 2nd ` R ) x ) = ( x ( 2nd ` R ) w ) ) with typecode |- |
18 |
17
|
fveq2d |
Could not format ( ( ( R e. CRingOps /\ S e. RingOps /\ F e. ( R RingOpsHom S ) ) /\ ( w e. X /\ x e. X ) ) -> ( F ` ( w ( 2nd ` R ) x ) ) = ( F ` ( x ( 2nd ` R ) w ) ) ) : No typesetting found for |- ( ( ( R e. CRingOps /\ S e. RingOps /\ F e. ( R RingOpsHom S ) ) /\ ( w e. X /\ x e. X ) ) -> ( F ` ( w ( 2nd ` R ) x ) ) = ( F ` ( x ( 2nd ` R ) w ) ) ) with typecode |- |
19 |
|
crngorngo |
|
20 |
|
eqid |
|
21 |
1 2 14 20
|
rngohommul |
Could not format ( ( ( R e. RingOps /\ S e. RingOps /\ F e. ( R RingOpsHom S ) ) /\ ( w e. X /\ x e. X ) ) -> ( F ` ( w ( 2nd ` R ) x ) ) = ( ( F ` w ) ( 2nd ` S ) ( F ` x ) ) ) : No typesetting found for |- ( ( ( R e. RingOps /\ S e. RingOps /\ F e. ( R RingOpsHom S ) ) /\ ( w e. X /\ x e. X ) ) -> ( F ` ( w ( 2nd ` R ) x ) ) = ( ( F ` w ) ( 2nd ` S ) ( F ` x ) ) ) with typecode |- |
22 |
19 21
|
syl3anl1 |
Could not format ( ( ( R e. CRingOps /\ S e. RingOps /\ F e. ( R RingOpsHom S ) ) /\ ( w e. X /\ x e. X ) ) -> ( F ` ( w ( 2nd ` R ) x ) ) = ( ( F ` w ) ( 2nd ` S ) ( F ` x ) ) ) : No typesetting found for |- ( ( ( R e. CRingOps /\ S e. RingOps /\ F e. ( R RingOpsHom S ) ) /\ ( w e. X /\ x e. X ) ) -> ( F ` ( w ( 2nd ` R ) x ) ) = ( ( F ` w ) ( 2nd ` S ) ( F ` x ) ) ) with typecode |- |
23 |
1 2 14 20
|
rngohommul |
Could not format ( ( ( R e. RingOps /\ S e. RingOps /\ F e. ( R RingOpsHom S ) ) /\ ( x e. X /\ w e. X ) ) -> ( F ` ( x ( 2nd ` R ) w ) ) = ( ( F ` x ) ( 2nd ` S ) ( F ` w ) ) ) : No typesetting found for |- ( ( ( R e. RingOps /\ S e. RingOps /\ F e. ( R RingOpsHom S ) ) /\ ( x e. X /\ w e. X ) ) -> ( F ` ( x ( 2nd ` R ) w ) ) = ( ( F ` x ) ( 2nd ` S ) ( F ` w ) ) ) with typecode |- |
24 |
23
|
ancom2s |
Could not format ( ( ( R e. RingOps /\ S e. RingOps /\ F e. ( R RingOpsHom S ) ) /\ ( w e. X /\ x e. X ) ) -> ( F ` ( x ( 2nd ` R ) w ) ) = ( ( F ` x ) ( 2nd ` S ) ( F ` w ) ) ) : No typesetting found for |- ( ( ( R e. RingOps /\ S e. RingOps /\ F e. ( R RingOpsHom S ) ) /\ ( w e. X /\ x e. X ) ) -> ( F ` ( x ( 2nd ` R ) w ) ) = ( ( F ` x ) ( 2nd ` S ) ( F ` w ) ) ) with typecode |- |
25 |
19 24
|
syl3anl1 |
Could not format ( ( ( R e. CRingOps /\ S e. RingOps /\ F e. ( R RingOpsHom S ) ) /\ ( w e. X /\ x e. X ) ) -> ( F ` ( x ( 2nd ` R ) w ) ) = ( ( F ` x ) ( 2nd ` S ) ( F ` w ) ) ) : No typesetting found for |- ( ( ( R e. CRingOps /\ S e. RingOps /\ F e. ( R RingOpsHom S ) ) /\ ( w e. X /\ x e. X ) ) -> ( F ` ( x ( 2nd ` R ) w ) ) = ( ( F ` x ) ( 2nd ` S ) ( F ` w ) ) ) with typecode |- |
26 |
18 22 25
|
3eqtr3d |
Could not format ( ( ( R e. CRingOps /\ S e. RingOps /\ F e. ( R RingOpsHom S ) ) /\ ( w e. X /\ x e. X ) ) -> ( ( F ` w ) ( 2nd ` S ) ( F ` x ) ) = ( ( F ` x ) ( 2nd ` S ) ( F ` w ) ) ) : No typesetting found for |- ( ( ( R e. CRingOps /\ S e. RingOps /\ F e. ( R RingOpsHom S ) ) /\ ( w e. X /\ x e. X ) ) -> ( ( F ` w ) ( 2nd ` S ) ( F ` x ) ) = ( ( F ` x ) ( 2nd ` S ) ( F ` w ) ) ) with typecode |- |
27 |
|
oveq12 |
|
28 |
|
oveq12 |
|
29 |
28
|
ancoms |
|
30 |
27 29
|
eqeq12d |
|
31 |
26 30
|
syl5ibrcom |
Could not format ( ( ( R e. CRingOps /\ S e. RingOps /\ F e. ( R RingOpsHom S ) ) /\ ( w e. X /\ x e. X ) ) -> ( ( y = ( F ` w ) /\ z = ( F ` x ) ) -> ( y ( 2nd ` S ) z ) = ( z ( 2nd ` S ) y ) ) ) : No typesetting found for |- ( ( ( R e. CRingOps /\ S e. RingOps /\ F e. ( R RingOpsHom S ) ) /\ ( w e. X /\ x e. X ) ) -> ( ( y = ( F ` w ) /\ z = ( F ` x ) ) -> ( y ( 2nd ` S ) z ) = ( z ( 2nd ` S ) y ) ) ) with typecode |- |
32 |
31
|
ex |
Could not format ( ( R e. CRingOps /\ S e. RingOps /\ F e. ( R RingOpsHom S ) ) -> ( ( w e. X /\ x e. X ) -> ( ( y = ( F ` w ) /\ z = ( F ` x ) ) -> ( y ( 2nd ` S ) z ) = ( z ( 2nd ` S ) y ) ) ) ) : No typesetting found for |- ( ( R e. CRingOps /\ S e. RingOps /\ F e. ( R RingOpsHom S ) ) -> ( ( w e. X /\ x e. X ) -> ( ( y = ( F ` w ) /\ z = ( F ` x ) ) -> ( y ( 2nd ` S ) z ) = ( z ( 2nd ` S ) y ) ) ) ) with typecode |- |
33 |
32
|
3expa |
Could not format ( ( ( R e. CRingOps /\ S e. RingOps ) /\ F e. ( R RingOpsHom S ) ) -> ( ( w e. X /\ x e. X ) -> ( ( y = ( F ` w ) /\ z = ( F ` x ) ) -> ( y ( 2nd ` S ) z ) = ( z ( 2nd ` S ) y ) ) ) ) : No typesetting found for |- ( ( ( R e. CRingOps /\ S e. RingOps ) /\ F e. ( R RingOpsHom S ) ) -> ( ( w e. X /\ x e. X ) -> ( ( y = ( F ` w ) /\ z = ( F ` x ) ) -> ( y ( 2nd ` S ) z ) = ( z ( 2nd ` S ) y ) ) ) ) with typecode |- |
34 |
33
|
adantrr |
Could not format ( ( ( R e. CRingOps /\ S e. RingOps ) /\ ( F e. ( R RingOpsHom S ) /\ F : X -onto-> Y ) ) -> ( ( w e. X /\ x e. X ) -> ( ( y = ( F ` w ) /\ z = ( F ` x ) ) -> ( y ( 2nd ` S ) z ) = ( z ( 2nd ` S ) y ) ) ) ) : No typesetting found for |- ( ( ( R e. CRingOps /\ S e. RingOps ) /\ ( F e. ( R RingOpsHom S ) /\ F : X -onto-> Y ) ) -> ( ( w e. X /\ x e. X ) -> ( ( y = ( F ` w ) /\ z = ( F ` x ) ) -> ( y ( 2nd ` S ) z ) = ( z ( 2nd ` S ) y ) ) ) ) with typecode |- |
35 |
34
|
rexlimdvv |
Could not format ( ( ( R e. CRingOps /\ S e. RingOps ) /\ ( F e. ( R RingOpsHom S ) /\ F : X -onto-> Y ) ) -> ( E. w e. X E. x e. X ( y = ( F ` w ) /\ z = ( F ` x ) ) -> ( y ( 2nd ` S ) z ) = ( z ( 2nd ` S ) y ) ) ) : No typesetting found for |- ( ( ( R e. CRingOps /\ S e. RingOps ) /\ ( F e. ( R RingOpsHom S ) /\ F : X -onto-> Y ) ) -> ( E. w e. X E. x e. X ( y = ( F ` w ) /\ z = ( F ` x ) ) -> ( y ( 2nd ` S ) z ) = ( z ( 2nd ` S ) y ) ) ) with typecode |- |
36 |
13 35
|
syld |
Could not format ( ( ( R e. CRingOps /\ S e. RingOps ) /\ ( F e. ( R RingOpsHom S ) /\ F : X -onto-> Y ) ) -> ( ( y e. Y /\ z e. Y ) -> ( y ( 2nd ` S ) z ) = ( z ( 2nd ` S ) y ) ) ) : No typesetting found for |- ( ( ( R e. CRingOps /\ S e. RingOps ) /\ ( F e. ( R RingOpsHom S ) /\ F : X -onto-> Y ) ) -> ( ( y e. Y /\ z e. Y ) -> ( y ( 2nd ` S ) z ) = ( z ( 2nd ` S ) y ) ) ) with typecode |- |
37 |
36
|
ralrimivv |
Could not format ( ( ( R e. CRingOps /\ S e. RingOps ) /\ ( F e. ( R RingOpsHom S ) /\ F : X -onto-> Y ) ) -> A. y e. Y A. z e. Y ( y ( 2nd ` S ) z ) = ( z ( 2nd ` S ) y ) ) : No typesetting found for |- ( ( ( R e. CRingOps /\ S e. RingOps ) /\ ( F e. ( R RingOpsHom S ) /\ F : X -onto-> Y ) ) -> A. y e. Y A. z e. Y ( y ( 2nd ` S ) z ) = ( z ( 2nd ` S ) y ) ) with typecode |- |
38 |
3 20 4
|
iscrngo2 |
|
39 |
5 37 38
|
sylanbrc |
Could not format ( ( ( R e. CRingOps /\ S e. RingOps ) /\ ( F e. ( R RingOpsHom S ) /\ F : X -onto-> Y ) ) -> S e. CRingOps ) : No typesetting found for |- ( ( ( R e. CRingOps /\ S e. RingOps ) /\ ( F e. ( R RingOpsHom S ) /\ F : X -onto-> Y ) ) -> S e. CRingOps ) with typecode |- |