Metamath Proof Explorer

Theorem issubrng2

Description: Characterize the subrings of a ring by closure properties. (Contributed by AV, 15-Feb-2025)

Ref Expression
Hypotheses issubrng2.b 
|- B = ( Base ` R )
issubrng2.t 
|- .x. = ( .r ` R )
Assertion issubrng2 
|- ( R e. Rng -> ( A e. ( SubRng ` R ) <-> ( A e. ( SubGrp ` R ) /\ A. x e. A A. y e. A ( x .x. y ) e. A ) ) )

Proof

Step Hyp Ref Expression
1 issubrng2.b 
 |-  B = ( Base ` R )
2 issubrng2.t 
 |-  .x. = ( .r ` R )
3 subrngsubg 
 |-  ( A e. ( SubRng ` R ) -> A e. ( SubGrp ` R ) )
4 2 subrngmcl 
 |-  ( ( A e. ( SubRng ` R ) /\ x e. A /\ y e. A ) -> ( x .x. y ) e. A )
5 4 3expb 
 |-  ( ( A e. ( SubRng ` R ) /\ ( x e. A /\ y e. A ) ) -> ( x .x. y ) e. A )
6 5 ralrimivva 
 |-  ( A e. ( SubRng ` R ) -> A. x e. A A. y e. A ( x .x. y ) e. A )
7 3 6 jca 
 |-  ( A e. ( SubRng ` R ) -> ( A e. ( SubGrp ` R ) /\ A. x e. A A. y e. A ( x .x. y ) e. A ) )
8 simpl 
 |-  ( ( R e. Rng /\ ( A e. ( SubGrp ` R ) /\ A. x e. A A. y e. A ( x .x. y ) e. A ) ) -> R e. Rng )
9 simprl 
 |-  ( ( R e. Rng /\ ( A e. ( SubGrp ` R ) /\ A. x e. A A. y e. A ( x .x. y ) e. A ) ) -> A e. ( SubGrp ` R ) )
10 eqid 
 |-  ( R |`s A ) = ( R |`s A )
11 10 subgbas 
 |-  ( A e. ( SubGrp ` R ) -> A = ( Base ` ( R |`s A ) ) )
12 9 11 syl 
 |-  ( ( R e. Rng /\ ( A e. ( SubGrp ` R ) /\ A. x e. A A. y e. A ( x .x. y ) e. A ) ) -> A = ( Base ` ( R |`s A ) ) )
13 eqid 
 |-  ( +g ` R ) = ( +g ` R )
14 10 13 ressplusg 
 |-  ( A e. ( SubGrp ` R ) -> ( +g ` R ) = ( +g ` ( R |`s A ) ) )
15 9 14 syl 
 |-  ( ( R e. Rng /\ ( A e. ( SubGrp ` R ) /\ A. x e. A A. y e. A ( x .x. y ) e. A ) ) -> ( +g ` R ) = ( +g ` ( R |`s A ) ) )
16 10 2 ressmulr 
 |-  ( A e. ( SubGrp ` R ) -> .x. = ( .r ` ( R |`s A ) ) )
17 9 16 syl 
 |-  ( ( R e. Rng /\ ( A e. ( SubGrp ` R ) /\ A. x e. A A. y e. A ( x .x. y ) e. A ) ) -> .x. = ( .r ` ( R |`s A ) ) )
18 rngabl 
 |-  ( R e. Rng -> R e. Abel )
19 10 subgabl 
 |-  ( ( R e. Abel /\ A e. ( SubGrp ` R ) ) -> ( R |`s A ) e. Abel )
20 18 9 19 syl2an2r 
 |-  ( ( R e. Rng /\ ( A e. ( SubGrp ` R ) /\ A. x e. A A. y e. A ( x .x. y ) e. A ) ) -> ( R |`s A ) e. Abel )
21 simprr 
 |-  ( ( R e. Rng /\ ( A e. ( SubGrp ` R ) /\ 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 )
22 oveq1 
 |-  ( x = u -> ( x .x. y ) = ( u .x. y ) )
23 22 eleq1d 
 |-  ( x = u -> ( ( x .x. y ) e. A <-> ( u .x. y ) e. A ) )
24 oveq2 
 |-  ( y = v -> ( u .x. y ) = ( u .x. v ) )
25 24 eleq1d 
 |-  ( y = v -> ( ( u .x. y ) e. A <-> ( u .x. v ) e. A ) )
26 23 25 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 ) )
27 21 26 syl5com 
 |-  ( ( R e. Rng /\ ( A e. ( SubGrp ` R ) /\ A. x e. A A. y e. A ( x .x. y ) e. A ) ) -> ( ( u e. A /\ v e. A ) -> ( u .x. v ) e. A ) )
28 27 3impib 
 |-  ( ( ( R e. Rng /\ ( A e. ( SubGrp ` R ) /\ 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 1 subgss 
 |-  ( A e. ( SubGrp ` R ) -> A C_ B )
30 9 29 syl 
 |-  ( ( R e. Rng /\ ( A e. ( SubGrp ` R ) /\ A. x e. A A. y e. A ( x .x. y ) e. A ) ) -> A C_ B )
31 30 sseld 
 |-  ( ( R e. Rng /\ ( A e. ( SubGrp ` R ) /\ A. x e. A A. y e. A ( x .x. y ) e. A ) ) -> ( u e. A -> u e. B ) )
32 30 sseld 
 |-  ( ( R e. Rng /\ ( A e. ( SubGrp ` R ) /\ A. x e. A A. y e. A ( x .x. y ) e. A ) ) -> ( v e. A -> v e. B ) )
33 30 sseld 
 |-  ( ( R e. Rng /\ ( A e. ( SubGrp ` R ) /\ A. x e. A A. y e. A ( x .x. y ) e. A ) ) -> ( w e. A -> w e. B ) )
34 31 32 33 3anim123d 
 |-  ( ( R e. Rng /\ ( A e. ( SubGrp ` R ) /\ 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 ) ) )
35 34 imp 
 |-  ( ( ( R e. Rng /\ ( A e. ( SubGrp ` R ) /\ 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 1 2 rngass 
 |-  ( ( R e. Rng /\ ( u e. B /\ v e. B /\ w e. B ) ) -> ( ( u .x. v ) .x. w ) = ( u .x. ( v .x. w ) ) )
37 36 adantlr 
 |-  ( ( ( R e. Rng /\ ( A e. ( SubGrp ` R ) /\ 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 ) ) )
38 35 37 syldan 
 |-  ( ( ( R e. Rng /\ ( A e. ( SubGrp ` R ) /\ 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 ) ) )
39 1 13 2 rngdi 
 |-  ( ( R e. Rng /\ ( u e. B /\ v e. B /\ w e. B ) ) -> ( u .x. ( v ( +g ` R ) w ) ) = ( ( u .x. v ) ( +g ` R ) ( u .x. w ) ) )
40 39 adantlr 
 |-  ( ( ( R e. Rng /\ ( A e. ( SubGrp ` R ) /\ 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 ) ) )
41 35 40 syldan 
 |-  ( ( ( R e. Rng /\ ( A e. ( SubGrp ` R ) /\ 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 ) ) )
42 1 13 2 rngdir 
 |-  ( ( R e. Rng /\ ( u e. B /\ v e. B /\ w e. B ) ) -> ( ( u ( +g ` R ) v ) .x. w ) = ( ( u .x. w ) ( +g ` R ) ( v .x. w ) ) )
43 42 adantlr 
 |-  ( ( ( R e. Rng /\ ( A e. ( SubGrp ` R ) /\ 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 ) ) )
44 35 43 syldan 
 |-  ( ( ( R e. Rng /\ ( A e. ( SubGrp ` R ) /\ 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 ) ) )
45 12 15 17 20 28 38 41 44 isrngd 
 |-  ( ( R e. Rng /\ ( A e. ( SubGrp ` R ) /\ A. x e. A A. y e. A ( x .x. y ) e. A ) ) -> ( R |`s A ) e. Rng )
46 1 issubrng 
 |-  ( A e. ( SubRng ` R ) <-> ( R e. Rng /\ ( R |`s A ) e. Rng /\ A C_ B ) )
47 8 45 30 46 syl3anbrc 
 |-  ( ( R e. Rng /\ ( A e. ( SubGrp ` R ) /\ A. x e. A A. y e. A ( x .x. y ) e. A ) ) -> A e. ( SubRng ` R ) )
48 47 ex 
 |-  ( R e. Rng -> ( ( A e. ( SubGrp ` R ) /\ A. x e. A A. y e. A ( x .x. y ) e. A ) -> A e. ( SubRng ` R ) ) )
49 7 48 impbid2 
 |-  ( R e. Rng -> ( A e. ( SubRng ` R ) <-> ( A e. ( SubGrp ` R ) /\ A. x e. A A. y e. A ( x .x. y ) e. A ) ) )