Metamath Proof Explorer

Theorem sdrgint

Description: The intersection of a nonempty collection of sub division rings is a sub division ring. (Contributed by Thierry Arnoux, 21-Aug-2023)

Ref Expression
Assertion sdrgint 
|- ( ( R e. DivRing /\ S C_ ( SubDRing ` R ) /\ S =/= (/) ) -> |^| S e. ( SubDRing ` R ) )

Proof

Step Hyp Ref Expression
1 simp1 
 |-  ( ( R e. DivRing /\ S C_ ( SubDRing ` R ) /\ S =/= (/) ) -> R e. DivRing )
2 simp2 
 |-  ( ( R e. DivRing /\ S C_ ( SubDRing ` R ) /\ S =/= (/) ) -> S C_ ( SubDRing ` R ) )
3 issdrg 
 |-  ( s e. ( SubDRing ` R ) <-> ( R e. DivRing /\ s e. ( SubRing ` R ) /\ ( R |`s s ) e. DivRing ) )
4 3 simp2bi 
 |-  ( s e. ( SubDRing ` R ) -> s e. ( SubRing ` R ) )
5 4 ssriv 
 |-  ( SubDRing ` R ) C_ ( SubRing ` R )
6 2 5 sstrdi 
 |-  ( ( R e. DivRing /\ S C_ ( SubDRing ` R ) /\ S =/= (/) ) -> S C_ ( SubRing ` R ) )
7 simp3 
 |-  ( ( R e. DivRing /\ S C_ ( SubDRing ` R ) /\ S =/= (/) ) -> S =/= (/) )
8 subrgint 
 |-  ( ( S C_ ( SubRing ` R ) /\ S =/= (/) ) -> |^| S e. ( SubRing ` R ) )
9 6 7 8 syl2anc 
 |-  ( ( R e. DivRing /\ S C_ ( SubDRing ` R ) /\ S =/= (/) ) -> |^| S e. ( SubRing ` R ) )
10 eqid 
 |-  ( R |`s |^| S ) = ( R |`s |^| S )
11 2 sselda 
 |-  ( ( ( R e. DivRing /\ S C_ ( SubDRing ` R ) /\ S =/= (/) ) /\ s e. S ) -> s e. ( SubDRing ` R ) )
12 3 simp3bi 
 |-  ( s e. ( SubDRing ` R ) -> ( R |`s s ) e. DivRing )
13 11 12 syl 
 |-  ( ( ( R e. DivRing /\ S C_ ( SubDRing ` R ) /\ S =/= (/) ) /\ s e. S ) -> ( R |`s s ) e. DivRing )
14 10 1 6 7 13 subdrgint 
 |-  ( ( R e. DivRing /\ S C_ ( SubDRing ` R ) /\ S =/= (/) ) -> ( R |`s |^| S ) e. DivRing )
15 issdrg 
 |-  ( |^| S e. ( SubDRing ` R ) <-> ( R e. DivRing /\ |^| S e. ( SubRing ` R ) /\ ( R |`s |^| S ) e. DivRing ) )
16 1 9 14 15 syl3anbrc 
 |-  ( ( R e. DivRing /\ S C_ ( SubDRing ` R ) /\ S =/= (/) ) -> |^| S e. ( SubDRing ` R ) )