Theorem subrngin

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

	Ref	Expression
Assertion	subrngin	⊢ ( ( 𝐴 ∈ ( SubRng ‘ 𝑅 ) ∧ 𝐵 ∈ ( SubRng ‘ 𝑅 ) ) → ( 𝐴 ∩ 𝐵 ) ∈ ( SubRng ‘ 𝑅 ) )

Proof

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