Metamath Proof Explorer

Theorem issubrg2

Description: Characterize the subrings of a ring by closure properties. (Contributed by Mario Carneiro, 3-Dec-2014)

Ref Expression
Hypotheses issubrg2.b 
|- B = ( Base ` R )
issubrg2.o 
|- .1. = ( 1r ` R )
issubrg2.t 
|- .x. = ( .r ` R )
Assertion issubrg2 
|- ( R e. Ring -> ( A e. ( SubRing ` R ) <-> ( A e. ( SubGrp ` R ) /\ .1. e. A /\ A. x e. A A. y e. A ( x .x. y ) e. A ) ) )

Proof

Step Hyp Ref Expression
1 issubrg2.b 
 |-  B = ( Base ` R )
2 issubrg2.o 
 |-  .1. = ( 1r ` R )
3 issubrg2.t 
 |-  .x. = ( .r ` R )
4 subrgsubg 
 |-  ( A e. ( SubRing ` R ) -> A e. ( SubGrp ` R ) )
5 2 subrg1cl 
 |-  ( A e. ( SubRing ` R ) -> .1. e. A )
6 3 subrgmcl 
 |-  ( ( A e. ( SubRing ` R ) /\ x e. A /\ y e. A ) -> ( x .x. y ) e. A )
7 6 3expb 
 |-  ( ( A e. ( SubRing ` R ) /\ ( x e. A /\ y e. A ) ) -> ( x .x. y ) e. A )
8 7 ralrimivva 
 |-  ( A e. ( SubRing ` R ) -> A. x e. A A. y e. A ( x .x. y ) e. A )
9 4 5 8 3jca 
 |-  ( A e. ( SubRing ` R ) -> ( A e. ( SubGrp ` R ) /\ .1. e. A /\ A. x e. A A. y e. A ( x .x. y ) e. A ) )
10 simpl 
 |-  ( ( R e. Ring /\ ( A e. ( SubGrp ` R ) /\ .1. e. A /\ A. x e. A A. y e. A ( x .x. y ) e. A ) ) -> R e. Ring )
11 simpr1 
 |-  ( ( R e. Ring /\ ( A e. ( SubGrp ` R ) /\ .1. e. A /\ A. x e. A A. y e. A ( x .x. y ) e. A ) ) -> A e. ( SubGrp ` R ) )
12 eqid 
 |-  ( R |`s A ) = ( R |`s A )
13 12 subgbas 
 |-  ( A e. ( SubGrp ` R ) -> A = ( Base ` ( R |`s A ) ) )
14 11 13 syl 
 |-  ( ( R e. Ring /\ ( A e. ( SubGrp ` R ) /\ .1. e. A /\ A. x e. A A. y e. A ( x .x. y ) e. A ) ) -> A = ( Base ` ( R |`s A ) ) )
15 eqid 
 |-  ( +g ` R ) = ( +g ` R )
16 12 15 ressplusg 
 |-  ( A e. ( SubGrp ` R ) -> ( +g ` R ) = ( +g ` ( R |`s A ) ) )
17 11 16 syl 
 |-  ( ( R e. Ring /\ ( A e. ( SubGrp ` R ) /\ .1. e. A /\ A. x e. A A. y e. A ( x .x. y ) e. A ) ) -> ( +g ` R ) = ( +g ` ( R |`s A ) ) )
18 12 3 ressmulr 
 |-  ( A e. ( SubGrp ` R ) -> .x. = ( .r ` ( R |`s A ) ) )
19 11 18 syl 
 |-  ( ( R e. Ring /\ ( A e. ( SubGrp ` R ) /\ .1. e. A /\ A. x e. A A. y e. A ( x .x. y ) e. A ) ) -> .x. = ( .r ` ( R |`s A ) ) )
20 12 subggrp 
 |-  ( A e. ( SubGrp ` R ) -> ( R |`s A ) e. Grp )
21 11 20 syl 
 |-  ( ( R e. Ring /\ ( A e. ( SubGrp ` R ) /\ .1. e. A /\ A. x e. A A. y e. A ( x .x. y ) e. A ) ) -> ( R |`s A ) e. Grp )
22 simpr3 
 |-  ( ( R e. Ring /\ ( A e. ( SubGrp ` R ) /\ .1. e. A /\ A. x e. A A. y e. A ( x .x. y ) e. A ) ) -> A. x e. A A. y e. A ( x .x. y ) e. A )
23 oveq1 
 |-  ( x = u -> ( x .x. y ) = ( u .x. y ) )
24 23 eleq1d 
 |-  ( x = u -> ( ( x .x. y ) e. A <-> ( u .x. y ) e. A ) )
25 oveq2 
 |-  ( y = v -> ( u .x. y ) = ( u .x. v ) )
26 25 eleq1d 
 |-  ( y = v -> ( ( u .x. y ) e. A <-> ( u .x. v ) e. A ) )
27 24 26 rspc2v 
 |-  ( ( u e. A /\ v e. A ) -> ( A. x e. A A. y e. A ( x .x. y ) e. A -> ( u .x. v ) e. A ) )
28 22 27 syl5com 
 |-  ( ( R e. Ring /\ ( A e. ( SubGrp ` R ) /\ .1. e. A /\ A. x e. A A. y e. A ( x .x. y ) e. A ) ) -> ( ( u e. A /\ v e. A ) -> ( u .x. v ) e. A ) )
29 28 3impib 
 |-  ( ( ( R e. Ring /\ ( A e. ( SubGrp ` R ) /\ .1. e. A /\ A. x e. A A. y e. A ( x .x. y ) e. A ) ) /\ u e. A /\ v e. A ) -> ( u .x. v ) e. A )
30 1 subgss 
 |-  ( A e. ( SubGrp ` R ) -> A C_ B )
31 11 30 syl 
 |-  ( ( R e. Ring /\ ( A e. ( SubGrp ` R ) /\ .1. e. A /\ A. x e. A A. y e. A ( x .x. y ) e. A ) ) -> A C_ B )
32 31 sseld 
 |-  ( ( R e. Ring /\ ( A e. ( SubGrp ` R ) /\ .1. e. A /\ A. x e. A A. y e. A ( x .x. y ) e. A ) ) -> ( u e. A -> u e. B ) )
33 31 sseld 
 |-  ( ( R e. Ring /\ ( A e. ( SubGrp ` R ) /\ .1. e. A /\ A. x e. A A. y e. A ( x .x. y ) e. A ) ) -> ( v e. A -> v e. B ) )
34 31 sseld 
 |-  ( ( R e. Ring /\ ( A e. ( SubGrp ` R ) /\ .1. e. A /\ A. x e. A A. y e. A ( x .x. y ) e. A ) ) -> ( w e. A -> w e. B ) )
35 32 33 34 3anim123d 
 |-  ( ( R e. Ring /\ ( A e. ( SubGrp ` R ) /\ .1. e. A /\ A. x e. A A. y e. A ( x .x. y ) e. A ) ) -> ( ( u e. A /\ v e. A /\ w e. A ) -> ( u e. B /\ v e. B /\ w e. B ) ) )
36 35 imp 
 |-  ( ( ( R e. Ring /\ ( A e. ( SubGrp ` R ) /\ .1. e. A /\ A. x e. A A. y e. A ( x .x. y ) e. A ) ) /\ ( u e. A /\ v e. A /\ w e. A ) ) -> ( u e. B /\ v e. B /\ w e. B ) )
37 1 3 ringass 
 |-  ( ( R e. Ring /\ ( u e. B /\ v e. B /\ w e. B ) ) -> ( ( u .x. v ) .x. w ) = ( u .x. ( v .x. w ) ) )
38 37 adantlr 
 |-  ( ( ( R e. Ring /\ ( A e. ( SubGrp ` R ) /\ .1. e. A /\ A. x e. A A. y e. A ( x .x. y ) e. A ) ) /\ ( u e. B /\ v e. B /\ w e. B ) ) -> ( ( u .x. v ) .x. w ) = ( u .x. ( v .x. w ) ) )
39 36 38 syldan 
 |-  ( ( ( R e. Ring /\ ( A e. ( SubGrp ` R ) /\ .1. e. A /\ A. x e. A A. y e. A ( x .x. y ) e. A ) ) /\ ( u e. A /\ v e. A /\ w e. A ) ) -> ( ( u .x. v ) .x. w ) = ( u .x. ( v .x. w ) ) )
40 1 15 3 ringdi 
 |-  ( ( R e. Ring /\ ( u e. B /\ v e. B /\ w e. B ) ) -> ( u .x. ( v ( +g ` R ) w ) ) = ( ( u .x. v ) ( +g ` R ) ( u .x. w ) ) )
41 40 adantlr 
 |-  ( ( ( R e. Ring /\ ( A e. ( SubGrp ` R ) /\ .1. e. A /\ A. x e. A A. y e. A ( x .x. y ) e. A ) ) /\ ( u e. B /\ v e. B /\ w e. B ) ) -> ( u .x. ( v ( +g ` R ) w ) ) = ( ( u .x. v ) ( +g ` R ) ( u .x. w ) ) )
42 36 41 syldan 
 |-  ( ( ( R e. Ring /\ ( A e. ( SubGrp ` R ) /\ .1. e. A /\ A. x e. A A. y e. A ( x .x. y ) e. A ) ) /\ ( u e. A /\ v e. A /\ w e. A ) ) -> ( u .x. ( v ( +g ` R ) w ) ) = ( ( u .x. v ) ( +g ` R ) ( u .x. w ) ) )
43 1 15 3 ringdir 
 |-  ( ( R e. Ring /\ ( u e. B /\ v e. B /\ w e. B ) ) -> ( ( u ( +g ` R ) v ) .x. w ) = ( ( u .x. w ) ( +g ` R ) ( v .x. w ) ) )
44 43 adantlr 
 |-  ( ( ( R e. Ring /\ ( A e. ( SubGrp ` R ) /\ .1. e. A /\ A. x e. A A. y e. A ( x .x. y ) e. A ) ) /\ ( u e. B /\ v e. B /\ w e. B ) ) -> ( ( u ( +g ` R ) v ) .x. w ) = ( ( u .x. w ) ( +g ` R ) ( v .x. w ) ) )
45 36 44 syldan 
 |-  ( ( ( R e. Ring /\ ( A e. ( SubGrp ` R ) /\ .1. e. A /\ A. x e. A A. y e. A ( x .x. y ) e. A ) ) /\ ( u e. A /\ v e. A /\ w e. A ) ) -> ( ( u ( +g ` R ) v ) .x. w ) = ( ( u .x. w ) ( +g ` R ) ( v .x. w ) ) )
46 simpr2 
 |-  ( ( R e. Ring /\ ( A e. ( SubGrp ` R ) /\ .1. e. A /\ A. x e. A A. y e. A ( x .x. y ) e. A ) ) -> .1. e. A )
47 32 imp 
 |-  ( ( ( R e. Ring /\ ( A e. ( SubGrp ` R ) /\ .1. e. A /\ A. x e. A A. y e. A ( x .x. y ) e. A ) ) /\ u e. A ) -> u e. B )
48 1 3 2 ringlidm 
 |-  ( ( R e. Ring /\ u e. B ) -> ( .1. .x. u ) = u )
49 48 adantlr 
 |-  ( ( ( R e. Ring /\ ( A e. ( SubGrp ` R ) /\ .1. e. A /\ A. x e. A A. y e. A ( x .x. y ) e. A ) ) /\ u e. B ) -> ( .1. .x. u ) = u )
50 47 49 syldan 
 |-  ( ( ( R e. Ring /\ ( A e. ( SubGrp ` R ) /\ .1. e. A /\ A. x e. A A. y e. A ( x .x. y ) e. A ) ) /\ u e. A ) -> ( .1. .x. u ) = u )
51 1 3 2 ringridm 
 |-  ( ( R e. Ring /\ u e. B ) -> ( u .x. .1. ) = u )
52 51 adantlr 
 |-  ( ( ( R e. Ring /\ ( A e. ( SubGrp ` R ) /\ .1. e. A /\ A. x e. A A. y e. A ( x .x. y ) e. A ) ) /\ u e. B ) -> ( u .x. .1. ) = u )
53 47 52 syldan 
 |-  ( ( ( R e. Ring /\ ( A e. ( SubGrp ` R ) /\ .1. e. A /\ A. x e. A A. y e. A ( x .x. y ) e. A ) ) /\ u e. A ) -> ( u .x. .1. ) = u )
54 14 17 19 21 29 39 42 45 46 50 53 isringd 
 |-  ( ( R e. Ring /\ ( A e. ( SubGrp ` R ) /\ .1. e. A /\ A. x e. A A. y e. A ( x .x. y ) e. A ) ) -> ( R |`s A ) e. Ring )
55 31 46 jca 
 |-  ( ( R e. Ring /\ ( A e. ( SubGrp ` R ) /\ .1. e. A /\ A. x e. A A. y e. A ( x .x. y ) e. A ) ) -> ( A C_ B /\ .1. e. A ) )
56 1 2 issubrg 
 |-  ( A e. ( SubRing ` R ) <-> ( ( R e. Ring /\ ( R |`s A ) e. Ring ) /\ ( A C_ B /\ .1. e. A ) ) )
57 10 54 55 56 syl21anbrc 
 |-  ( ( R e. Ring /\ ( A e. ( SubGrp ` R ) /\ .1. e. A /\ A. x e. A A. y e. A ( x .x. y ) e. A ) ) -> A e. ( SubRing ` R ) )
58 57 ex 
 |-  ( R e. Ring -> ( ( A e. ( SubGrp ` R ) /\ .1. e. A /\ A. x e. A A. y e. A ( x .x. y ) e. A ) -> A e. ( SubRing ` R ) ) )
59 9 58 impbid2 
 |-  ( R e. Ring -> ( A e. ( SubRing ` R ) <-> ( A e. ( SubGrp ` R ) /\ .1. e. A /\ A. x e. A A. y e. A ( x .x. y ) e. A ) ) )