Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  suborng Structured version   Unicode version

Theorem suborng 26288
Description: Every subring of an ordered ring is also an ordered ring. (Contributed by Thierry Arnoux, 21-Jan-2018.)
Assertion
Ref Expression
suborng  |-  ( ( R  e. oRing  /\  ( Rs  A )  e.  Ring )  ->  ( Rs  A )  e. oRing )

Proof of Theorem suborng
Dummy variables  a 
b are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simpr 461 . . 3  |-  ( ( R  e. oRing  /\  ( Rs  A )  e.  Ring )  ->  ( Rs  A )  e.  Ring )
2 rnggrp 16655 . . . . . 6  |-  ( ( Rs  A )  e.  Ring  -> 
( Rs  A )  e.  Grp )
31, 2syl 16 . . . . 5  |-  ( ( R  e. oRing  /\  ( Rs  A )  e.  Ring )  ->  ( Rs  A )  e.  Grp )
4 orngogrp 26274 . . . . . . . 8  |-  ( R  e. oRing  ->  R  e. oGrp )
5 isogrp 26170 . . . . . . . . 9  |-  ( R  e. oGrp 
<->  ( R  e.  Grp  /\  R  e. oMnd ) )
65simprbi 464 . . . . . . . 8  |-  ( R  e. oGrp  ->  R  e. oMnd )
74, 6syl 16 . . . . . . 7  |-  ( R  e. oRing  ->  R  e. oMnd )
8 rngmnd 16659 . . . . . . 7  |-  ( ( Rs  A )  e.  Ring  -> 
( Rs  A )  e.  Mnd )
97, 8anim12i 566 . . . . . 6  |-  ( ( R  e. oRing  /\  ( Rs  A )  e.  Ring )  ->  ( R  e. oMnd  /\  ( Rs  A )  e.  Mnd ) )
10 submomnd 26178 . . . . . 6  |-  ( ( R  e. oMnd  /\  ( Rs  A )  e.  Mnd )  ->  ( Rs  A )  e. oMnd )
119, 10syl 16 . . . . 5  |-  ( ( R  e. oRing  /\  ( Rs  A )  e.  Ring )  ->  ( Rs  A )  e. oMnd )
123, 11jca 532 . . . 4  |-  ( ( R  e. oRing  /\  ( Rs  A )  e.  Ring )  ->  ( ( Rs  A )  e.  Grp  /\  ( Rs  A )  e. oMnd )
)
13 isogrp 26170 . . . 4  |-  ( ( Rs  A )  e. oGrp  <->  ( ( Rs  A )  e.  Grp  /\  ( Rs  A )  e. oMnd )
)
1412, 13sylibr 212 . . 3  |-  ( ( R  e. oRing  /\  ( Rs  A )  e.  Ring )  ->  ( Rs  A )  e. oGrp )
15 simp-4l 765 . . . . . . . 8  |-  ( ( ( ( ( R  e. oRing  /\  ( Rs  A
)  e.  Ring )  /\  a  e.  ( Base `  ( Rs  A ) ) )  /\  b  e.  ( Base `  ( Rs  A ) ) )  /\  ( ( 0g
`  ( Rs  A ) ) ( le `  ( Rs  A ) ) a  /\  ( 0g `  ( Rs  A ) ) ( le `  ( Rs  A ) ) b ) )  ->  R  e. oRing )
16 reldmress 14229 . . . . . . . . . . . . . . . . 17  |-  Rel  doms
1716ovprc2 6125 . . . . . . . . . . . . . . . 16  |-  ( -.  A  e.  _V  ->  ( Rs  A )  =  (/) )
1817fveq2d 5700 . . . . . . . . . . . . . . 15  |-  ( -.  A  e.  _V  ->  (
Base `  ( Rs  A
) )  =  (
Base `  (/) ) )
1918adantl 466 . . . . . . . . . . . . . 14  |-  ( ( ( R  e. oRing  /\  ( Rs  A )  e.  Ring )  /\  -.  A  e. 
_V )  ->  ( Base `  ( Rs  A ) )  =  ( Base `  (/) ) )
20 base0 14218 . . . . . . . . . . . . . 14  |-  (/)  =  (
Base `  (/) )
2119, 20syl6eqr 2493 . . . . . . . . . . . . 13  |-  ( ( ( R  e. oRing  /\  ( Rs  A )  e.  Ring )  /\  -.  A  e. 
_V )  ->  ( Base `  ( Rs  A ) )  =  (/) )
22 eqid 2443 . . . . . . . . . . . . . . . . 17  |-  ( Base `  ( Rs  A ) )  =  ( Base `  ( Rs  A ) )
23 eqid 2443 . . . . . . . . . . . . . . . . 17  |-  ( 1r
`  ( Rs  A ) )  =  ( 1r
`  ( Rs  A ) )
2422, 23rngidcl 16670 . . . . . . . . . . . . . . . 16  |-  ( ( Rs  A )  e.  Ring  -> 
( 1r `  ( Rs  A ) )  e.  ( Base `  ( Rs  A ) ) )
25 ne0i 3648 . . . . . . . . . . . . . . . 16  |-  ( ( 1r `  ( Rs  A ) )  e.  (
Base `  ( Rs  A
) )  ->  ( Base `  ( Rs  A ) )  =/=  (/) )
2624, 25syl 16 . . . . . . . . . . . . . . 15  |-  ( ( Rs  A )  e.  Ring  -> 
( Base `  ( Rs  A
) )  =/=  (/) )
2726ad2antlr 726 . . . . . . . . . . . . . 14  |-  ( ( ( R  e. oRing  /\  ( Rs  A )  e.  Ring )  /\  -.  A  e. 
_V )  ->  ( Base `  ( Rs  A ) )  =/=  (/) )
2827neneqd 2629 . . . . . . . . . . . . 13  |-  ( ( ( R  e. oRing  /\  ( Rs  A )  e.  Ring )  /\  -.  A  e. 
_V )  ->  -.  ( Base `  ( Rs  A
) )  =  (/) )
2921, 28condan 792 . . . . . . . . . . . 12  |-  ( ( R  e. oRing  /\  ( Rs  A )  e.  Ring )  ->  A  e.  _V )
30 eqid 2443 . . . . . . . . . . . . . 14  |-  ( Rs  A )  =  ( Rs  A )
31 eqid 2443 . . . . . . . . . . . . . 14  |-  ( Base `  R )  =  (
Base `  R )
3230, 31ressbas 14233 . . . . . . . . . . . . 13  |-  ( A  e.  _V  ->  ( A  i^i  ( Base `  R
) )  =  (
Base `  ( Rs  A
) ) )
33 inss2 3576 . . . . . . . . . . . . 13  |-  ( A  i^i  ( Base `  R
) )  C_  ( Base `  R )
3432, 33syl6eqssr 3412 . . . . . . . . . . . 12  |-  ( A  e.  _V  ->  ( Base `  ( Rs  A ) )  C_  ( Base `  R ) )
3529, 34syl 16 . . . . . . . . . . 11  |-  ( ( R  e. oRing  /\  ( Rs  A )  e.  Ring )  ->  ( Base `  ( Rs  A ) )  C_  ( Base `  R )
)
3635ad3antrrr 729 . . . . . . . . . 10  |-  ( ( ( ( ( R  e. oRing  /\  ( Rs  A
)  e.  Ring )  /\  a  e.  ( Base `  ( Rs  A ) ) )  /\  b  e.  ( Base `  ( Rs  A ) ) )  /\  ( ( 0g
`  ( Rs  A ) ) ( le `  ( Rs  A ) ) a  /\  ( 0g `  ( Rs  A ) ) ( le `  ( Rs  A ) ) b ) )  ->  ( Base `  ( Rs  A ) )  C_  ( Base `  R )
)
37 simpllr 758 . . . . . . . . . 10  |-  ( ( ( ( ( R  e. oRing  /\  ( Rs  A
)  e.  Ring )  /\  a  e.  ( Base `  ( Rs  A ) ) )  /\  b  e.  ( Base `  ( Rs  A ) ) )  /\  ( ( 0g
`  ( Rs  A ) ) ( le `  ( Rs  A ) ) a  /\  ( 0g `  ( Rs  A ) ) ( le `  ( Rs  A ) ) b ) )  ->  a  e.  ( Base `  ( Rs  A
) ) )
3836, 37sseldd 3362 . . . . . . . . 9  |-  ( ( ( ( ( R  e. oRing  /\  ( Rs  A
)  e.  Ring )  /\  a  e.  ( Base `  ( Rs  A ) ) )  /\  b  e.  ( Base `  ( Rs  A ) ) )  /\  ( ( 0g
`  ( Rs  A ) ) ( le `  ( Rs  A ) ) a  /\  ( 0g `  ( Rs  A ) ) ( le `  ( Rs  A ) ) b ) )  ->  a  e.  ( Base `  R )
)
39 simprl 755 . . . . . . . . . 10  |-  ( ( ( ( ( R  e. oRing  /\  ( Rs  A
)  e.  Ring )  /\  a  e.  ( Base `  ( Rs  A ) ) )  /\  b  e.  ( Base `  ( Rs  A ) ) )  /\  ( ( 0g
`  ( Rs  A ) ) ( le `  ( Rs  A ) ) a  /\  ( 0g `  ( Rs  A ) ) ( le `  ( Rs  A ) ) b ) )  ->  ( 0g `  ( Rs  A ) ) ( le `  ( Rs  A ) ) a )
40 orngrng 26273 . . . . . . . . . . . . . . . . . . 19  |-  ( R  e. oRing  ->  R  e.  Ring )
41 rnggrp 16655 . . . . . . . . . . . . . . . . . . 19  |-  ( R  e.  Ring  ->  R  e. 
Grp )
4240, 41syl 16 . . . . . . . . . . . . . . . . . 18  |-  ( R  e. oRing  ->  R  e.  Grp )
4342adantr 465 . . . . . . . . . . . . . . . . 17  |-  ( ( R  e. oRing  /\  ( Rs  A )  e.  Ring )  ->  R  e.  Grp )
4431ressinbas 14239 . . . . . . . . . . . . . . . . . . . 20  |-  ( A  e.  _V  ->  ( Rs  A )  =  ( Rs  ( A  i^i  ( Base `  R ) ) ) )
4532oveq2d 6112 . . . . . . . . . . . . . . . . . . . 20  |-  ( A  e.  _V  ->  ( Rs  ( A  i^i  ( Base `  R ) ) )  =  ( Rs  (
Base `  ( Rs  A
) ) ) )
4644, 45eqtrd 2475 . . . . . . . . . . . . . . . . . . 19  |-  ( A  e.  _V  ->  ( Rs  A )  =  ( Rs  ( Base `  ( Rs  A ) ) ) )
4729, 46syl 16 . . . . . . . . . . . . . . . . . 18  |-  ( ( R  e. oRing  /\  ( Rs  A )  e.  Ring )  ->  ( Rs  A )  =  ( Rs  ( Base `  ( Rs  A ) ) ) )
4847, 3eqeltrrd 2518 . . . . . . . . . . . . . . . . 17  |-  ( ( R  e. oRing  /\  ( Rs  A )  e.  Ring )  ->  ( Rs  ( Base `  ( Rs  A ) ) )  e.  Grp )
4943, 35, 483jca 1168 . . . . . . . . . . . . . . . 16  |-  ( ( R  e. oRing  /\  ( Rs  A )  e.  Ring )  ->  ( R  e. 
Grp  /\  ( Base `  ( Rs  A ) )  C_  ( Base `  R )  /\  ( Rs  ( Base `  ( Rs  A ) ) )  e.  Grp ) )
5031issubg 15686 . . . . . . . . . . . . . . . 16  |-  ( (
Base `  ( Rs  A
) )  e.  (SubGrp `  R )  <->  ( R  e.  Grp  /\  ( Base `  ( Rs  A ) )  C_  ( Base `  R )  /\  ( Rs  ( Base `  ( Rs  A ) ) )  e.  Grp ) )
5149, 50sylibr 212 . . . . . . . . . . . . . . 15  |-  ( ( R  e. oRing  /\  ( Rs  A )  e.  Ring )  ->  ( Base `  ( Rs  A ) )  e.  (SubGrp `  R )
)
52 eqid 2443 . . . . . . . . . . . . . . . 16  |-  ( Rs  (
Base `  ( Rs  A
) ) )  =  ( Rs  ( Base `  ( Rs  A ) ) )
53 eqid 2443 . . . . . . . . . . . . . . . 16  |-  ( 0g
`  R )  =  ( 0g `  R
)
5452, 53subg0 15692 . . . . . . . . . . . . . . 15  |-  ( (
Base `  ( Rs  A
) )  e.  (SubGrp `  R )  ->  ( 0g `  R )  =  ( 0g `  ( Rs  ( Base `  ( Rs  A
) ) ) ) )
5551, 54syl 16 . . . . . . . . . . . . . 14  |-  ( ( R  e. oRing  /\  ( Rs  A )  e.  Ring )  ->  ( 0g `  R )  =  ( 0g `  ( Rs  (
Base `  ( Rs  A
) ) ) ) )
5647fveq2d 5700 . . . . . . . . . . . . . 14  |-  ( ( R  e. oRing  /\  ( Rs  A )  e.  Ring )  ->  ( 0g `  ( Rs  A ) )  =  ( 0g `  ( Rs  ( Base `  ( Rs  A
) ) ) ) )
5755, 56eqtr4d 2478 . . . . . . . . . . . . 13  |-  ( ( R  e. oRing  /\  ( Rs  A )  e.  Ring )  ->  ( 0g `  R )  =  ( 0g `  ( Rs  A ) ) )
5857ad2antrr 725 . . . . . . . . . . . 12  |-  ( ( ( ( R  e. oRing  /\  ( Rs  A )  e.  Ring )  /\  a  e.  (
Base `  ( Rs  A
) ) )  /\  b  e.  ( Base `  ( Rs  A ) ) )  ->  ( 0g `  R )  =  ( 0g `  ( Rs  A ) ) )
5929ad2antrr 725 . . . . . . . . . . . . 13  |-  ( ( ( ( R  e. oRing  /\  ( Rs  A )  e.  Ring )  /\  a  e.  (
Base `  ( Rs  A
) ) )  /\  b  e.  ( Base `  ( Rs  A ) ) )  ->  A  e.  _V )
60 eqid 2443 . . . . . . . . . . . . . 14  |-  ( le
`  R )  =  ( le `  R
)
6130, 60ressle 14343 . . . . . . . . . . . . 13  |-  ( A  e.  _V  ->  ( le `  R )  =  ( le `  ( Rs  A ) ) )
6259, 61syl 16 . . . . . . . . . . . 12  |-  ( ( ( ( R  e. oRing  /\  ( Rs  A )  e.  Ring )  /\  a  e.  (
Base `  ( Rs  A
) ) )  /\  b  e.  ( Base `  ( Rs  A ) ) )  ->  ( le `  R )  =  ( le `  ( Rs  A ) ) )
63 eqidd 2444 . . . . . . . . . . . 12  |-  ( ( ( ( R  e. oRing  /\  ( Rs  A )  e.  Ring )  /\  a  e.  (
Base `  ( Rs  A
) ) )  /\  b  e.  ( Base `  ( Rs  A ) ) )  ->  a  =  a )
6458, 62, 63breq123d 4311 . . . . . . . . . . 11  |-  ( ( ( ( R  e. oRing  /\  ( Rs  A )  e.  Ring )  /\  a  e.  (
Base `  ( Rs  A
) ) )  /\  b  e.  ( Base `  ( Rs  A ) ) )  ->  ( ( 0g
`  R ) ( le `  R ) a  <->  ( 0g `  ( Rs  A ) ) ( le `  ( Rs  A ) ) a ) )
6564adantr 465 . . . . . . . . . 10  |-  ( ( ( ( ( R  e. oRing  /\  ( Rs  A
)  e.  Ring )  /\  a  e.  ( Base `  ( Rs  A ) ) )  /\  b  e.  ( Base `  ( Rs  A ) ) )  /\  ( ( 0g
`  ( Rs  A ) ) ( le `  ( Rs  A ) ) a  /\  ( 0g `  ( Rs  A ) ) ( le `  ( Rs  A ) ) b ) )  ->  ( ( 0g `  R ) ( le `  R ) a  <->  ( 0g `  ( Rs  A ) ) ( le `  ( Rs  A ) ) a ) )
6639, 65mpbird 232 . . . . . . . . 9  |-  ( ( ( ( ( R  e. oRing  /\  ( Rs  A
)  e.  Ring )  /\  a  e.  ( Base `  ( Rs  A ) ) )  /\  b  e.  ( Base `  ( Rs  A ) ) )  /\  ( ( 0g
`  ( Rs  A ) ) ( le `  ( Rs  A ) ) a  /\  ( 0g `  ( Rs  A ) ) ( le `  ( Rs  A ) ) b ) )  ->  ( 0g `  R ) ( le
`  R ) a )
6738, 66jca 532 . . . . . . . 8  |-  ( ( ( ( ( R  e. oRing  /\  ( Rs  A
)  e.  Ring )  /\  a  e.  ( Base `  ( Rs  A ) ) )  /\  b  e.  ( Base `  ( Rs  A ) ) )  /\  ( ( 0g
`  ( Rs  A ) ) ( le `  ( Rs  A ) ) a  /\  ( 0g `  ( Rs  A ) ) ( le `  ( Rs  A ) ) b ) )  ->  ( a  e.  ( Base `  R
)  /\  ( 0g `  R ) ( le
`  R ) a ) )
68 simplr 754 . . . . . . . . . 10  |-  ( ( ( ( ( R  e. oRing  /\  ( Rs  A
)  e.  Ring )  /\  a  e.  ( Base `  ( Rs  A ) ) )  /\  b  e.  ( Base `  ( Rs  A ) ) )  /\  ( ( 0g
`  ( Rs  A ) ) ( le `  ( Rs  A ) ) a  /\  ( 0g `  ( Rs  A ) ) ( le `  ( Rs  A ) ) b ) )  ->  b  e.  ( Base `  ( Rs  A
) ) )
6936, 68sseldd 3362 . . . . . . . . 9  |-  ( ( ( ( ( R  e. oRing  /\  ( Rs  A
)  e.  Ring )  /\  a  e.  ( Base `  ( Rs  A ) ) )  /\  b  e.  ( Base `  ( Rs  A ) ) )  /\  ( ( 0g
`  ( Rs  A ) ) ( le `  ( Rs  A ) ) a  /\  ( 0g `  ( Rs  A ) ) ( le `  ( Rs  A ) ) b ) )  ->  b  e.  ( Base `  R )
)
70 simprr 756 . . . . . . . . . 10  |-  ( ( ( ( ( R  e. oRing  /\  ( Rs  A
)  e.  Ring )  /\  a  e.  ( Base `  ( Rs  A ) ) )  /\  b  e.  ( Base `  ( Rs  A ) ) )  /\  ( ( 0g
`  ( Rs  A ) ) ( le `  ( Rs  A ) ) a  /\  ( 0g `  ( Rs  A ) ) ( le `  ( Rs  A ) ) b ) )  ->  ( 0g `  ( Rs  A ) ) ( le `  ( Rs  A ) ) b )
71 eqidd 2444 . . . . . . . . . . . 12  |-  ( ( ( ( R  e. oRing  /\  ( Rs  A )  e.  Ring )  /\  a  e.  (
Base `  ( Rs  A
) ) )  /\  b  e.  ( Base `  ( Rs  A ) ) )  ->  b  =  b )
7258, 62, 71breq123d 4311 . . . . . . . . . . 11  |-  ( ( ( ( R  e. oRing  /\  ( Rs  A )  e.  Ring )  /\  a  e.  (
Base `  ( Rs  A
) ) )  /\  b  e.  ( Base `  ( Rs  A ) ) )  ->  ( ( 0g
`  R ) ( le `  R ) b  <->  ( 0g `  ( Rs  A ) ) ( le `  ( Rs  A ) ) b ) )
7372adantr 465 . . . . . . . . . 10  |-  ( ( ( ( ( R  e. oRing  /\  ( Rs  A
)  e.  Ring )  /\  a  e.  ( Base `  ( Rs  A ) ) )  /\  b  e.  ( Base `  ( Rs  A ) ) )  /\  ( ( 0g
`  ( Rs  A ) ) ( le `  ( Rs  A ) ) a  /\  ( 0g `  ( Rs  A ) ) ( le `  ( Rs  A ) ) b ) )  ->  ( ( 0g `  R ) ( le `  R ) b  <->  ( 0g `  ( Rs  A ) ) ( le `  ( Rs  A ) ) b ) )
7470, 73mpbird 232 . . . . . . . . 9  |-  ( ( ( ( ( R  e. oRing  /\  ( Rs  A
)  e.  Ring )  /\  a  e.  ( Base `  ( Rs  A ) ) )  /\  b  e.  ( Base `  ( Rs  A ) ) )  /\  ( ( 0g
`  ( Rs  A ) ) ( le `  ( Rs  A ) ) a  /\  ( 0g `  ( Rs  A ) ) ( le `  ( Rs  A ) ) b ) )  ->  ( 0g `  R ) ( le
`  R ) b )
7569, 74jca 532 . . . . . . . 8  |-  ( ( ( ( ( R  e. oRing  /\  ( Rs  A
)  e.  Ring )  /\  a  e.  ( Base `  ( Rs  A ) ) )  /\  b  e.  ( Base `  ( Rs  A ) ) )  /\  ( ( 0g
`  ( Rs  A ) ) ( le `  ( Rs  A ) ) a  /\  ( 0g `  ( Rs  A ) ) ( le `  ( Rs  A ) ) b ) )  ->  ( b  e.  ( Base `  R
)  /\  ( 0g `  R ) ( le
`  R ) b ) )
76 eqid 2443 . . . . . . . . 9  |-  ( .r
`  R )  =  ( .r `  R
)
7731, 60, 53, 76orngmul 26276 . . . . . . . 8  |-  ( ( R  e. oRing  /\  (
a  e.  ( Base `  R )  /\  ( 0g `  R ) ( le `  R ) a )  /\  (
b  e.  ( Base `  R )  /\  ( 0g `  R ) ( le `  R ) b ) )  -> 
( 0g `  R
) ( le `  R ) ( a ( .r `  R
) b ) )
7815, 67, 75, 77syl3anc 1218 . . . . . . 7  |-  ( ( ( ( ( R  e. oRing  /\  ( Rs  A
)  e.  Ring )  /\  a  e.  ( Base `  ( Rs  A ) ) )  /\  b  e.  ( Base `  ( Rs  A ) ) )  /\  ( ( 0g
`  ( Rs  A ) ) ( le `  ( Rs  A ) ) a  /\  ( 0g `  ( Rs  A ) ) ( le `  ( Rs  A ) ) b ) )  ->  ( 0g `  R ) ( le
`  R ) ( a ( .r `  R ) b ) )
7958adantr 465 . . . . . . . 8  |-  ( ( ( ( ( R  e. oRing  /\  ( Rs  A
)  e.  Ring )  /\  a  e.  ( Base `  ( Rs  A ) ) )  /\  b  e.  ( Base `  ( Rs  A ) ) )  /\  ( ( 0g
`  ( Rs  A ) ) ( le `  ( Rs  A ) ) a  /\  ( 0g `  ( Rs  A ) ) ( le `  ( Rs  A ) ) b ) )  ->  ( 0g `  R )  =  ( 0g `  ( Rs  A ) ) )
8062adantr 465 . . . . . . . 8  |-  ( ( ( ( ( R  e. oRing  /\  ( Rs  A
)  e.  Ring )  /\  a  e.  ( Base `  ( Rs  A ) ) )  /\  b  e.  ( Base `  ( Rs  A ) ) )  /\  ( ( 0g
`  ( Rs  A ) ) ( le `  ( Rs  A ) ) a  /\  ( 0g `  ( Rs  A ) ) ( le `  ( Rs  A ) ) b ) )  ->  ( le `  R )  =  ( le `  ( Rs  A ) ) )
8159adantr 465 . . . . . . . . . 10  |-  ( ( ( ( ( R  e. oRing  /\  ( Rs  A
)  e.  Ring )  /\  a  e.  ( Base `  ( Rs  A ) ) )  /\  b  e.  ( Base `  ( Rs  A ) ) )  /\  ( ( 0g
`  ( Rs  A ) ) ( le `  ( Rs  A ) ) a  /\  ( 0g `  ( Rs  A ) ) ( le `  ( Rs  A ) ) b ) )  ->  A  e.  _V )
8230, 76ressmulr 14296 . . . . . . . . . 10  |-  ( A  e.  _V  ->  ( .r `  R )  =  ( .r `  ( Rs  A ) ) )
8381, 82syl 16 . . . . . . . . 9  |-  ( ( ( ( ( R  e. oRing  /\  ( Rs  A
)  e.  Ring )  /\  a  e.  ( Base `  ( Rs  A ) ) )  /\  b  e.  ( Base `  ( Rs  A ) ) )  /\  ( ( 0g
`  ( Rs  A ) ) ( le `  ( Rs  A ) ) a  /\  ( 0g `  ( Rs  A ) ) ( le `  ( Rs  A ) ) b ) )  ->  ( .r `  R )  =  ( .r `  ( Rs  A ) ) )
8483oveqd 6113 . . . . . . . 8  |-  ( ( ( ( ( R  e. oRing  /\  ( Rs  A
)  e.  Ring )  /\  a  e.  ( Base `  ( Rs  A ) ) )  /\  b  e.  ( Base `  ( Rs  A ) ) )  /\  ( ( 0g
`  ( Rs  A ) ) ( le `  ( Rs  A ) ) a  /\  ( 0g `  ( Rs  A ) ) ( le `  ( Rs  A ) ) b ) )  ->  ( a
( .r `  R
) b )  =  ( a ( .r
`  ( Rs  A ) ) b ) )
8579, 80, 84breq123d 4311 . . . . . . 7  |-  ( ( ( ( ( R  e. oRing  /\  ( Rs  A
)  e.  Ring )  /\  a  e.  ( Base `  ( Rs  A ) ) )  /\  b  e.  ( Base `  ( Rs  A ) ) )  /\  ( ( 0g
`  ( Rs  A ) ) ( le `  ( Rs  A ) ) a  /\  ( 0g `  ( Rs  A ) ) ( le `  ( Rs  A ) ) b ) )  ->  ( ( 0g `  R ) ( le `  R ) ( a ( .r
`  R ) b )  <->  ( 0g `  ( Rs  A ) ) ( le `  ( Rs  A ) ) ( a ( .r `  ( Rs  A ) ) b ) ) )
8678, 85mpbid 210 . . . . . 6  |-  ( ( ( ( ( R  e. oRing  /\  ( Rs  A
)  e.  Ring )  /\  a  e.  ( Base `  ( Rs  A ) ) )  /\  b  e.  ( Base `  ( Rs  A ) ) )  /\  ( ( 0g
`  ( Rs  A ) ) ( le `  ( Rs  A ) ) a  /\  ( 0g `  ( Rs  A ) ) ( le `  ( Rs  A ) ) b ) )  ->  ( 0g `  ( Rs  A ) ) ( le `  ( Rs  A ) ) ( a ( .r `  ( Rs  A ) ) b ) )
8786ex 434 . . . . 5  |-  ( ( ( ( R  e. oRing  /\  ( Rs  A )  e.  Ring )  /\  a  e.  (
Base `  ( Rs  A
) ) )  /\  b  e.  ( Base `  ( Rs  A ) ) )  ->  ( ( ( 0g `  ( Rs  A ) ) ( le
`  ( Rs  A ) ) a  /\  ( 0g `  ( Rs  A ) ) ( le `  ( Rs  A ) ) b )  ->  ( 0g `  ( Rs  A ) ) ( le `  ( Rs  A ) ) ( a ( .r `  ( Rs  A ) ) b ) ) )
8887anasss 647 . . . 4  |-  ( ( ( R  e. oRing  /\  ( Rs  A )  e.  Ring )  /\  ( a  e.  ( Base `  ( Rs  A ) )  /\  b  e.  ( Base `  ( Rs  A ) ) ) )  ->  ( (
( 0g `  ( Rs  A ) ) ( le `  ( Rs  A ) ) a  /\  ( 0g `  ( Rs  A ) ) ( le
`  ( Rs  A ) ) b )  -> 
( 0g `  ( Rs  A ) ) ( le `  ( Rs  A ) ) ( a ( .r `  ( Rs  A ) ) b ) ) )
8988ralrimivva 2813 . . 3  |-  ( ( R  e. oRing  /\  ( Rs  A )  e.  Ring )  ->  A. a  e.  (
Base `  ( Rs  A
) ) A. b  e.  ( Base `  ( Rs  A ) ) ( ( ( 0g `  ( Rs  A ) ) ( le `  ( Rs  A ) ) a  /\  ( 0g `  ( Rs  A ) ) ( le
`  ( Rs  A ) ) b )  -> 
( 0g `  ( Rs  A ) ) ( le `  ( Rs  A ) ) ( a ( .r `  ( Rs  A ) ) b ) ) )
901, 14, 893jca 1168 . 2  |-  ( ( R  e. oRing  /\  ( Rs  A )  e.  Ring )  ->  ( ( Rs  A )  e.  Ring  /\  ( Rs  A )  e. oGrp  /\  A. a  e.  ( Base `  ( Rs  A ) ) A. b  e.  ( Base `  ( Rs  A ) ) ( ( ( 0g `  ( Rs  A ) ) ( le `  ( Rs  A ) ) a  /\  ( 0g `  ( Rs  A ) ) ( le
`  ( Rs  A ) ) b )  -> 
( 0g `  ( Rs  A ) ) ( le `  ( Rs  A ) ) ( a ( .r `  ( Rs  A ) ) b ) ) ) )
91 eqid 2443 . . 3  |-  ( 0g
`  ( Rs  A ) )  =  ( 0g
`  ( Rs  A ) )
92 eqid 2443 . . 3  |-  ( .r
`  ( Rs  A ) )  =  ( .r
`  ( Rs  A ) )
93 eqid 2443 . . 3  |-  ( le
`  ( Rs  A ) )  =  ( le
`  ( Rs  A ) )
9422, 91, 92, 93isorng 26272 . 2  |-  ( ( Rs  A )  e. oRing  <->  ( ( Rs  A )  e.  Ring  /\  ( Rs  A )  e. oGrp  /\  A. a  e.  ( Base `  ( Rs  A ) ) A. b  e.  ( Base `  ( Rs  A ) ) ( ( ( 0g `  ( Rs  A ) ) ( le `  ( Rs  A ) ) a  /\  ( 0g `  ( Rs  A ) ) ( le
`  ( Rs  A ) ) b )  -> 
( 0g `  ( Rs  A ) ) ( le `  ( Rs  A ) ) ( a ( .r `  ( Rs  A ) ) b ) ) ) )
9590, 94sylibr 212 1  |-  ( ( R  e. oRing  /\  ( Rs  A )  e.  Ring )  ->  ( Rs  A )  e. oRing )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 184    /\ wa 369    /\ w3a 965    = wceq 1369    e. wcel 1756    =/= wne 2611   A.wral 2720   _Vcvv 2977    i^i cin 3332    C_ wss 3333   (/)c0 3642   class class class wbr 4297   ` cfv 5423  (class class class)co 6096   Basecbs 14179   ↾s cress 14180   .rcmulr 14244   lecple 14250   0gc0g 14383   Mndcmnd 15414   Grpcgrp 15415  SubGrpcsubg 15680   1rcur 16608   Ringcrg 16650  oMndcomnd 26165  oGrpcogrp 26166  oRingcorng 26268
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-sep 4418  ax-nul 4426  ax-pow 4475  ax-pr 4536  ax-un 6377  ax-cnex 9343  ax-resscn 9344  ax-1cn 9345  ax-icn 9346  ax-addcl 9347  ax-addrcl 9348  ax-mulcl 9349  ax-mulrcl 9350  ax-mulcom 9351  ax-addass 9352  ax-mulass 9353  ax-distr 9354  ax-i2m1 9355  ax-1ne0 9356  ax-1rid 9357  ax-rnegex 9358  ax-rrecex 9359  ax-cnre 9360  ax-pre-lttri 9361  ax-pre-lttrn 9362  ax-pre-ltadd 9363  ax-pre-mulgt0 9364
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2573  df-ne 2613  df-nel 2614  df-ral 2725  df-rex 2726  df-reu 2727  df-rmo 2728  df-rab 2729  df-v 2979  df-sbc 3192  df-csb 3294  df-dif 3336  df-un 3338  df-in 3340  df-ss 3347  df-pss 3349  df-nul 3643  df-if 3797  df-pw 3867  df-sn 3883  df-pr 3885  df-tp 3887  df-op 3889  df-uni 4097  df-iun 4178  df-br 4298  df-opab 4356  df-mpt 4357  df-tr 4391  df-eprel 4637  df-id 4641  df-po 4646  df-so 4647  df-fr 4684  df-we 4686  df-ord 4727  df-on 4728  df-lim 4729  df-suc 4730  df-xp 4851  df-rel 4852  df-cnv 4853  df-co 4854  df-dm 4855  df-rn 4856  df-res 4857  df-ima 4858  df-iota 5386  df-fun 5425  df-fn 5426  df-f 5427  df-f1 5428  df-fo 5429  df-f1o 5430  df-fv 5431  df-riota 6057  df-ov 6099  df-oprab 6100  df-mpt2 6101  df-om 6482  df-recs 6837  df-rdg 6871  df-er 7106  df-en 7316  df-dom 7317  df-sdom 7318  df-pnf 9425  df-mnf 9426  df-xr 9427  df-ltxr 9428  df-le 9429  df-sub 9602  df-neg 9603  df-nn 10328  df-2 10385  df-3 10386  df-4 10387  df-5 10388  df-6 10389  df-7 10390  df-8 10391  df-9 10392  df-10 10393  df-ndx 14182  df-slot 14183  df-base 14184  df-sets 14185  df-ress 14186  df-plusg 14256  df-mulr 14257  df-ple 14263  df-0g 14385  df-poset 15121  df-toset 15209  df-mnd 15420  df-grp 15550  df-subg 15683  df-mgp 16597  df-ur 16609  df-rng 16652  df-omnd 26167  df-ogrp 26168  df-orng 26270
This theorem is referenced by:  subofld  26289
  Copyright terms: Public domain W3C validator