Metamath Proof Explorer

Theorem subrgint

Description: The intersection of a nonempty collection of subrings is a subring. (Contributed by Stefan O'Rear, 30-Nov-2014) (Revised by Mario Carneiro, 7-Dec-2014)

Ref Expression
Assertion subrgint 
|- ( ( S C_ ( SubRing ` R ) /\ S =/= (/) ) -> |^| S e. ( SubRing ` R ) )

Proof

Step Hyp Ref Expression
1 subrgsubg 
 |-  ( r e. ( SubRing ` R ) -> r e. ( SubGrp ` R ) )
2 1 ssriv 
 |-  ( SubRing ` R ) C_ ( SubGrp ` R )
3 sstr 
 |-  ( ( S C_ ( SubRing ` R ) /\ ( SubRing ` R ) C_ ( SubGrp ` R ) ) -> S C_ ( SubGrp ` R ) )
4 2 3 mpan2 
 |-  ( S C_ ( SubRing ` R ) -> S C_ ( SubGrp ` R ) )
5 subgint 
 |-  ( ( S C_ ( SubGrp ` R ) /\ S =/= (/) ) -> |^| S e. ( SubGrp ` R ) )
6 4 5 sylan 
 |-  ( ( S C_ ( SubRing ` R ) /\ S =/= (/) ) -> |^| S e. ( SubGrp ` R ) )
7 ssel2 
 |-  ( ( S C_ ( SubRing ` R ) /\ r e. S ) -> r e. ( SubRing ` R ) )
8 7 adantlr 
 |-  ( ( ( S C_ ( SubRing ` R ) /\ S =/= (/) ) /\ r e. S ) -> r e. ( SubRing ` R ) )
9 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
10 9 subrg1cl 
 |-  ( r e. ( SubRing ` R ) -> ( 1r ` R ) e. r )
11 8 10 syl 
 |-  ( ( ( S C_ ( SubRing ` R ) /\ S =/= (/) ) /\ r e. S ) -> ( 1r ` R ) e. r )
12 11 ralrimiva 
 |-  ( ( S C_ ( SubRing ` R ) /\ S =/= (/) ) -> A. r e. S ( 1r ` R ) e. r )
13 fvex 
 |-  ( 1r ` R ) e. _V
14 13 elint2 
 |-  ( ( 1r ` R ) e. |^| S <-> A. r e. S ( 1r ` R ) e. r )
15 12 14 sylibr 
 |-  ( ( S C_ ( SubRing ` R ) /\ S =/= (/) ) -> ( 1r ` R ) e. |^| S )
16 8 adantlr 
 |-  ( ( ( ( S C_ ( SubRing ` R ) /\ S =/= (/) ) /\ ( x e. |^| S /\ y e. |^| S ) ) /\ r e. S ) -> r e. ( SubRing ` R ) )
17 simprl 
 |-  ( ( ( S C_ ( SubRing ` R ) /\ S =/= (/) ) /\ ( x e. |^| S /\ y e. |^| S ) ) -> x e. |^| S )
18 elinti 
 |-  ( x e. |^| S -> ( r e. S -> x e. r ) )
19 18 imp 
 |-  ( ( x e. |^| S /\ r e. S ) -> x e. r )
20 17 19 sylan 
 |-  ( ( ( ( S C_ ( SubRing ` R ) /\ S =/= (/) ) /\ ( x e. |^| S /\ y e. |^| S ) ) /\ r e. S ) -> x e. r )
21 simprr 
 |-  ( ( ( S C_ ( SubRing ` R ) /\ S =/= (/) ) /\ ( x e. |^| S /\ y e. |^| S ) ) -> y e. |^| S )
22 elinti 
 |-  ( y e. |^| S -> ( r e. S -> y e. r ) )
23 22 imp 
 |-  ( ( y e. |^| S /\ r e. S ) -> y e. r )
24 21 23 sylan 
 |-  ( ( ( ( S C_ ( SubRing ` R ) /\ S =/= (/) ) /\ ( x e. |^| S /\ y e. |^| S ) ) /\ r e. S ) -> y e. r )
25 eqid 
 |-  ( .r ` R ) = ( .r ` R )
26 25 subrgmcl 
 |-  ( ( r e. ( SubRing ` R ) /\ x e. r /\ y e. r ) -> ( x ( .r ` R ) y ) e. r )
27 16 20 24 26 syl3anc 
 |-  ( ( ( ( S C_ ( SubRing ` R ) /\ S =/= (/) ) /\ ( x e. |^| S /\ y e. |^| S ) ) /\ r e. S ) -> ( x ( .r ` R ) y ) e. r )
28 27 ralrimiva 
 |-  ( ( ( S C_ ( SubRing ` R ) /\ S =/= (/) ) /\ ( x e. |^| S /\ y e. |^| S ) ) -> A. r e. S ( x ( .r ` R ) y ) e. r )
29 ovex 
 |-  ( x ( .r ` R ) y ) e. _V
30 29 elint2 
 |-  ( ( x ( .r ` R ) y ) e. |^| S <-> A. r e. S ( x ( .r ` R ) y ) e. r )
31 28 30 sylibr 
 |-  ( ( ( S C_ ( SubRing ` R ) /\ S =/= (/) ) /\ ( x e. |^| S /\ y e. |^| S ) ) -> ( x ( .r ` R ) y ) e. |^| S )
32 31 ralrimivva 
 |-  ( ( S C_ ( SubRing ` R ) /\ S =/= (/) ) -> A. x e. |^| S A. y e. |^| S ( x ( .r ` R ) y ) e. |^| S )
33 ssn0 
 |-  ( ( S C_ ( SubRing ` R ) /\ S =/= (/) ) -> ( SubRing ` R ) =/= (/) )
34 n0 
 |-  ( ( SubRing ` R ) =/= (/) <-> E. r r e. ( SubRing ` R ) )
35 subrgrcl 
 |-  ( r e. ( SubRing ` R ) -> R e. Ring )
36 35 exlimiv 
 |-  ( E. r r e. ( SubRing ` R ) -> R e. Ring )
37 34 36 sylbi 
 |-  ( ( SubRing ` R ) =/= (/) -> R e. Ring )
38 eqid 
 |-  ( Base ` R ) = ( Base ` R )
39 38 9 25 issubrg2 
 |-  ( R e. Ring -> ( |^| S e. ( SubRing ` R ) <-> ( |^| S e. ( SubGrp ` R ) /\ ( 1r ` R ) e. |^| S /\ A. x e. |^| S A. y e. |^| S ( x ( .r ` R ) y ) e. |^| S ) ) )
40 33 37 39 3syl 
 |-  ( ( S C_ ( SubRing ` R ) /\ S =/= (/) ) -> ( |^| S e. ( SubRing ` R ) <-> ( |^| S e. ( SubGrp ` R ) /\ ( 1r ` R ) e. |^| S /\ A. x e. |^| S A. y e. |^| S ( x ( .r ` R ) y ) e. |^| S ) ) )
41 6 15 32 40 mpbir3and 
 |-  ( ( S C_ ( SubRing ` R ) /\ S =/= (/) ) -> |^| S e. ( SubRing ` R ) )