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

Metamath Proof Explorer

Theorem subrngin

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

Ref Expression
Assertion subrngin 
|- ( ( A e. ( SubRng ` R ) /\ B e. ( SubRng ` R ) ) -> ( A i^i B ) e. ( SubRng ` R ) )

Proof

Step Hyp Ref Expression
1 intprg 
 |-  ( ( A e. ( SubRng ` R ) /\ B e. ( SubRng ` R ) ) -> |^| { A , B } = ( A i^i B ) )
2 prssi 
 |-  ( ( A e. ( SubRng ` R ) /\ B e. ( SubRng ` R ) ) -> { A , B } C_ ( SubRng ` R ) )
3 prnzg 
 |-  ( A e. ( SubRng ` R ) -> { A , B } =/= (/) )
4 3 adantr 
 |-  ( ( A e. ( SubRng ` R ) /\ B e. ( SubRng ` R ) ) -> { A , B } =/= (/) )
5 subrngint 
 |-  ( ( { A , B } C_ ( SubRng ` R ) /\ { A , B } =/= (/) ) -> |^| { A , B } e. ( SubRng ` R ) )
6 2 4 5 syl2anc 
 |-  ( ( A e. ( SubRng ` R ) /\ B e. ( SubRng ` R ) ) -> |^| { A , B } e. ( SubRng ` R ) )
7 1 6 eqeltrrd 
 |-  ( ( A e. ( SubRng ` R ) /\ B e. ( SubRng ` R ) ) -> ( A i^i B ) e. ( SubRng ` R ) )