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

Metamath Proof Explorer

Theorem subrgin

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

Ref Expression
Assertion subrgin ( ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ 𝐵 ∈ ( SubRing ‘ 𝑅 ) ) → ( 𝐴 ∩ 𝐵 ) ∈ ( SubRing ‘ 𝑅 ) )

Proof

Step Hyp Ref Expression
1 intprg ⊢ ( ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ 𝐵 ∈ ( SubRing ‘ 𝑅 ) ) → ∩ { 𝐴 , 𝐵 } = ( 𝐴 ∩ 𝐵 ) )
2 prssi ⊢ ( ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ 𝐵 ∈ ( SubRing ‘ 𝑅 ) ) → { 𝐴 , 𝐵 } ⊆ ( SubRing ‘ 𝑅 ) )
3 prnzg ⊢ ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) → { 𝐴 , 𝐵 } ≠ ∅ )
4 3 adantr ⊢ ( ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ 𝐵 ∈ ( SubRing ‘ 𝑅 ) ) → { 𝐴 , 𝐵 } ≠ ∅ )
5 subrgint ⊢ ( ( { 𝐴 , 𝐵 } ⊆ ( SubRing ‘ 𝑅 ) ∧ { 𝐴 , 𝐵 } ≠ ∅ ) → ∩ { 𝐴 , 𝐵 } ∈ ( SubRing ‘ 𝑅 ) )
6 2 4 5 syl2anc ⊢ ( ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ 𝐵 ∈ ( SubRing ‘ 𝑅 ) ) → ∩ { 𝐴 , 𝐵 } ∈ ( SubRing ‘ 𝑅 ) )
7 1 6 eqeltrrd ⊢ ( ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) ∧ 𝐵 ∈ ( SubRing ‘ 𝑅 ) ) → ( 𝐴 ∩ 𝐵 ) ∈ ( SubRing ‘ 𝑅 ) )