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 ‘ 𝑅 ) )