This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem subrngint

Description: The intersection of a nonempty collection of subrings is a subring. (Contributed by AV, 15-Feb-2025)

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

Proof

Step Hyp Ref Expression
1 subrngsubg 
 |-  ( r e. ( SubRng ` R ) -> r e. ( SubGrp ` R ) )
2 1 ssriv 
 |-  ( SubRng ` R ) C_ ( SubGrp ` R )
3 sstr 
 |-  ( ( S C_ ( SubRng ` R ) /\ ( SubRng ` R ) C_ ( SubGrp ` R ) ) -> S C_ ( SubGrp ` R ) )
4 2 3 mpan2 
 |-  ( S C_ ( SubRng ` R ) -> S C_ ( SubGrp ` R ) )
5 subgint 
 |-  ( ( S C_ ( SubGrp ` R ) /\ S =/= (/) ) -> |^| S e. ( SubGrp ` R ) )
6 4 5 sylan 
 |-  ( ( S C_ ( SubRng ` R ) /\ S =/= (/) ) -> |^| S e. ( SubGrp ` R ) )
7 ssel2 
 |-  ( ( S C_ ( SubRng ` R ) /\ r e. S ) -> r e. ( SubRng ` R ) )
8 7 ad4ant14 
 |-  ( ( ( ( S C_ ( SubRng ` R ) /\ S =/= (/) ) /\ ( x e. |^| S /\ y e. |^| S ) ) /\ r e. S ) -> r e. ( SubRng ` R ) )
9 simprl 
 |-  ( ( ( S C_ ( SubRng ` R ) /\ S =/= (/) ) /\ ( x e. |^| S /\ y e. |^| S ) ) -> x e. |^| S )
10 elinti 
 |-  ( x e. |^| S -> ( r e. S -> x e. r ) )
11 10 imp 
 |-  ( ( x e. |^| S /\ r e. S ) -> x e. r )
12 9 11 sylan 
 |-  ( ( ( ( S C_ ( SubRng ` R ) /\ S =/= (/) ) /\ ( x e. |^| S /\ y e. |^| S ) ) /\ r e. S ) -> x e. r )
13 simprr 
 |-  ( ( ( S C_ ( SubRng ` R ) /\ S =/= (/) ) /\ ( x e. |^| S /\ y e. |^| S ) ) -> y e. |^| S )
14 elinti 
 |-  ( y e. |^| S -> ( r e. S -> y e. r ) )
15 14 imp 
 |-  ( ( y e. |^| S /\ r e. S ) -> y e. r )
16 13 15 sylan 
 |-  ( ( ( ( S C_ ( SubRng ` R ) /\ S =/= (/) ) /\ ( x e. |^| S /\ y e. |^| S ) ) /\ r e. S ) -> y e. r )
17 eqid 
 |-  ( .r ` R ) = ( .r ` R )
18 17 subrngmcl 
 |-  ( ( r e. ( SubRng ` R ) /\ x e. r /\ y e. r ) -> ( x ( .r ` R ) y ) e. r )
19 8 12 16 18 syl3anc 
 |-  ( ( ( ( S C_ ( SubRng ` R ) /\ S =/= (/) ) /\ ( x e. |^| S /\ y e. |^| S ) ) /\ r e. S ) -> ( x ( .r ` R ) y ) e. r )
20 19 ralrimiva 
 |-  ( ( ( S C_ ( SubRng ` R ) /\ S =/= (/) ) /\ ( x e. |^| S /\ y e. |^| S ) ) -> A. r e. S ( x ( .r ` R ) y ) e. r )
21 ovex 
 |-  ( x ( .r ` R ) y ) e. _V
22 21 elint2 
 |-  ( ( x ( .r ` R ) y ) e. |^| S <-> A. r e. S ( x ( .r ` R ) y ) e. r )
23 20 22 sylibr 
 |-  ( ( ( S C_ ( SubRng ` R ) /\ S =/= (/) ) /\ ( x e. |^| S /\ y e. |^| S ) ) -> ( x ( .r ` R ) y ) e. |^| S )
24 23 ralrimivva 
 |-  ( ( S C_ ( SubRng ` R ) /\ S =/= (/) ) -> A. x e. |^| S A. y e. |^| S ( x ( .r ` R ) y ) e. |^| S )
25 ssn0 
 |-  ( ( S C_ ( SubRng ` R ) /\ S =/= (/) ) -> ( SubRng ` R ) =/= (/) )
26 n0 
 |-  ( ( SubRng ` R ) =/= (/) <-> E. r r e. ( SubRng ` R ) )
27 subrngrcl 
 |-  ( r e. ( SubRng ` R ) -> R e. Rng )
28 27 exlimiv 
 |-  ( E. r r e. ( SubRng ` R ) -> R e. Rng )
29 26 28 sylbi 
 |-  ( ( SubRng ` R ) =/= (/) -> R e. Rng )
30 eqid 
 |-  ( Base ` R ) = ( Base ` R )
31 30 17 issubrng2 
 |-  ( R e. Rng -> ( |^| S e. ( SubRng ` R ) <-> ( |^| S e. ( SubGrp ` R ) /\ A. x e. |^| S A. y e. |^| S ( x ( .r ` R ) y ) e. |^| S ) ) )
32 25 29 31 3syl 
 |-  ( ( S C_ ( SubRng ` R ) /\ S =/= (/) ) -> ( |^| S e. ( SubRng ` R ) <-> ( |^| S e. ( SubGrp ` R ) /\ A. x e. |^| S A. y e. |^| S ( x ( .r ` R ) y ) e. |^| S ) ) )
33 6 24 32 mpbir2and 
 |-  ( ( S C_ ( SubRng ` R ) /\ S =/= (/) ) -> |^| S e. ( SubRng ` R ) )