Theorem subrngint

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

	Ref	Expression
Assertion	subrngint	Could not format assertion : No typesetting found for |- ( ( S C_ ( SubRng ` R ) /\ S =/= (/) ) -> |^| S e. ( SubRng ` R ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		subrngsubg	Could not format ( r e. ( SubRng ` R ) -> r e. ( SubGrp ` R ) ) : No typesetting found for |- ( r e. ( SubRng ` R ) -> r e. ( SubGrp ` R ) ) with typecode |-
2	1	ssriv	Could not format ( SubRng ` R ) C_ ( SubGrp ` R ) : No typesetting found for |- ( SubRng ` R ) C_ ( SubGrp ` R ) with typecode |-
3		sstr	Could not format ( ( S C_ ( SubRng ` R ) /\ ( SubRng ` R ) C_ ( SubGrp ` R ) ) -> S C_ ( SubGrp ` R ) ) : No typesetting found for |- ( ( S C_ ( SubRng ` R ) /\ ( SubRng ` R ) C_ ( SubGrp ` R ) ) -> S C_ ( SubGrp ` R ) ) with typecode |-
4	2 3	mpan2	Could not format ( S C_ ( SubRng ` R ) -> S C_ ( SubGrp ` R ) ) : No typesetting found for |- ( S C_ ( SubRng ` R ) -> S C_ ( SubGrp ` R ) ) with typecode |-
5		subgint	$$⊢\left(S\subseteq \mathrm{SubGrp}\left(R\right)\wedge S\ne \varnothing \right)\to \bigcap S\in \mathrm{SubGrp}\left(R\right)$$
6	4 5	sylan	Could not format ( ( S C_ ( SubRng ` R ) /\ S =/= (/) ) -> |^| S e. ( SubGrp ` R ) ) : No typesetting found for |- ( ( S C_ ( SubRng ` R ) /\ S =/= (/) ) -> |^| S e. ( SubGrp ` R ) ) with typecode |-
7		ssel2	Could not format ( ( S C_ ( SubRng ` R ) /\ r e. S ) -> r e. ( SubRng ` R ) ) : No typesetting found for |- ( ( S C_ ( SubRng ` R ) /\ r e. S ) -> r e. ( SubRng ` R ) ) with typecode |-
8	7	ad4ant14	Could not format ( ( ( ( S C_ ( SubRng ` R ) /\ S =/= (/) ) /\ ( x e. |^| S /\ y e. |^| S ) ) /\ r e. S ) -> r e. ( SubRng ` R ) ) : No typesetting found for |- ( ( ( ( S C_ ( SubRng ` R ) /\ S =/= (/) ) /\ ( x e. |^| S /\ y e. |^| S ) ) /\ r e. S ) -> r e. ( SubRng ` R ) ) with typecode |-
9		simprl	Could not format ( ( ( S C_ ( SubRng ` R ) /\ S =/= (/) ) /\ ( x e. |^| S /\ y e. |^| S ) ) -> x e. |^| S ) : No typesetting found for |- ( ( ( S C_ ( SubRng ` R ) /\ S =/= (/) ) /\ ( x e. |^| S /\ y e. |^| S ) ) -> x e. |^| S ) with typecode |-
10		elinti	$$⊢x\in \bigcap S\to \left(r\in S\to x\in r\right)$$
11	10	imp	$$⊢\left(x\in \bigcap S\wedge r\in S\right)\to x\in r$$
12	9 11	sylan	Could not format ( ( ( ( S C_ ( SubRng ` R ) /\ S =/= (/) ) /\ ( x e. |^| S /\ y e. |^| S ) ) /\ r e. S ) -> x e. r ) : No typesetting found for |- ( ( ( ( S C_ ( SubRng ` R ) /\ S =/= (/) ) /\ ( x e. |^| S /\ y e. |^| S ) ) /\ r e. S ) -> x e. r ) with typecode |-
13		simprr	Could not format ( ( ( S C_ ( SubRng ` R ) /\ S =/= (/) ) /\ ( x e. |^| S /\ y e. |^| S ) ) -> y e. |^| S ) : No typesetting found for |- ( ( ( S C_ ( SubRng ` R ) /\ S =/= (/) ) /\ ( x e. |^| S /\ y e. |^| S ) ) -> y e. |^| S ) with typecode |-
14		elinti	$$⊢y\in \bigcap S\to \left(r\in S\to y\in r\right)$$
15	14	imp	$$⊢\left(y\in \bigcap S\wedge r\in S\right)\to y\in r$$
16	13 15	sylan	Could not format ( ( ( ( S C_ ( SubRng ` R ) /\ S =/= (/) ) /\ ( x e. |^| S /\ y e. |^| S ) ) /\ r e. S ) -> y e. r ) : No typesetting found for |- ( ( ( ( S C_ ( SubRng ` R ) /\ S =/= (/) ) /\ ( x e. |^| S /\ y e. |^| S ) ) /\ r e. S ) -> y e. r ) with typecode |-
17		eqid	$$⊢{\cdot }_R={\cdot }_R$$
18	17	subrngmcl	Could not format ( ( r e. ( SubRng ` R ) /\ x e. r /\ y e. r ) -> ( x ( .r ` R ) y ) e. r ) : No typesetting found for |- ( ( r e. ( SubRng ` R ) /\ x e. r /\ y e. r ) -> ( x ( .r ` R ) y ) e. r ) with typecode |-
19	8 12 16 18	syl3anc	Could not format ( ( ( ( S C_ ( SubRng ` R ) /\ S =/= (/) ) /\ ( x e. |^| S /\ y e. |^| S ) ) /\ r e. S ) -> ( x ( .r ` R ) y ) e. r ) : No typesetting found for |- ( ( ( ( S C_ ( SubRng ` R ) /\ S =/= (/) ) /\ ( x e. |^| S /\ y e. |^| S ) ) /\ r e. S ) -> ( x ( .r ` R ) y ) e. r ) with typecode |-
20	19	ralrimiva	Could not format ( ( ( S C_ ( SubRng ` R ) /\ S =/= (/) ) /\ ( x e. |^| S /\ y e. |^| S ) ) -> A. r e. S ( x ( .r ` R ) y ) e. r ) : No typesetting found for |- ( ( ( S C_ ( SubRng ` R ) /\ S =/= (/) ) /\ ( x e. |^| S /\ y e. |^| S ) ) -> A. r e. S ( x ( .r ` R ) y ) e. r ) with typecode |-
21		ovex	$$⊢x{\cdot }_{R}y\in \mathrm{V}$$
22	21	elint2	$$⊢x{\cdot }_{R}y\in \bigcap S\leftrightarrow \forall r\in Sx{\cdot }_{R}y\in r$$
23	20 22	sylibr	Could not format ( ( ( S C_ ( SubRng ` R ) /\ S =/= (/) ) /\ ( x e. |^| S /\ y e. |^| S ) ) -> ( x ( .r ` R ) y ) e. |^| S ) : No typesetting found for |- ( ( ( S C_ ( SubRng ` R ) /\ S =/= (/) ) /\ ( x e. |^| S /\ y e. |^| S ) ) -> ( x ( .r ` R ) y ) e. |^| S ) with typecode |-
24	23	ralrimivva	Could not format ( ( S C_ ( SubRng ` R ) /\ S =/= (/) ) -> A. x e. |^| S A. y e. |^| S ( x ( .r ` R ) y ) e. |^| S ) : No typesetting found for |- ( ( S C_ ( SubRng ` R ) /\ S =/= (/) ) -> A. x e. |^| S A. y e. |^| S ( x ( .r ` R ) y ) e. |^| S ) with typecode |-
25		ssn0	Could not format ( ( S C_ ( SubRng ` R ) /\ S =/= (/) ) -> ( SubRng ` R ) =/= (/) ) : No typesetting found for |- ( ( S C_ ( SubRng ` R ) /\ S =/= (/) ) -> ( SubRng ` R ) =/= (/) ) with typecode |-
26		n0	Could not format ( ( SubRng ` R ) =/= (/) <-> E. r r e. ( SubRng ` R ) ) : No typesetting found for |- ( ( SubRng ` R ) =/= (/) <-> E. r r e. ( SubRng ` R ) ) with typecode |-
27		subrngrcl	Could not format ( r e. ( SubRng ` R ) -> R e. Rng ) : No typesetting found for |- ( r e. ( SubRng ` R ) -> R e. Rng ) with typecode |-
28	27	exlimiv	Could not format ( E. r r e. ( SubRng ` R ) -> R e. Rng ) : No typesetting found for |- ( E. r r e. ( SubRng ` R ) -> R e. Rng ) with typecode |-
29	26 28	sylbi	Could not format ( ( SubRng ` R ) =/= (/) -> R e. Rng ) : No typesetting found for |- ( ( SubRng ` R ) =/= (/) -> R e. Rng ) with typecode |-
30		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
31	30 17	issubrng2	Could not format ( R e. Rng -> ( |^| S e. ( SubRng ` R ) <-> ( |^| S e. ( SubGrp ` R ) /\ A. x e. |^| S A. y e. |^| S ( x ( .r ` R ) y ) e. |^| S ) ) ) : No typesetting found for |- ( R e. Rng -> ( |^| S e. ( SubRng ` R ) <-> ( |^| S e. ( SubGrp ` R ) /\ A. x e. |^| S A. y e. |^| S ( x ( .r ` R ) y ) e. |^| S ) ) ) with typecode |-
32	25 29 31	3syl	Could not format ( ( S C_ ( SubRng ` R ) /\ S =/= (/) ) -> ( |^| S e. ( SubRng ` R ) <-> ( |^| S e. ( SubGrp ` R ) /\ A. x e. |^| S A. y e. |^| S ( x ( .r ` R ) y ) e. |^| S ) ) ) : No typesetting found for |- ( ( S C_ ( SubRng ` R ) /\ S =/= (/) ) -> ( |^| S e. ( SubRng ` R ) <-> ( |^| S e. ( SubGrp ` R ) /\ A. x e. |^| S A. y e. |^| S ( x ( .r ` R ) y ) e. |^| S ) ) ) with typecode |-
33	6 24 32	mpbir2and	Could not format ( ( S C_ ( SubRng ` R ) /\ S =/= (/) ) -> |^| S e. ( SubRng ` R ) ) : No typesetting found for |- ( ( S C_ ( SubRng ` R ) /\ S =/= (/) ) -> |^| S e. ( SubRng ` R ) ) with typecode |-