Theorem subrngmcl

Description: A subgroup is closed under multiplication. (Contributed by AV, 14-Feb-2025)

	Ref	Expression
Hypothesis	subrngmcl.p	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
Assertion	subrngmcl	Could not format assertion : No typesetting found for |- ( ( A e. ( SubRng ` R ) /\ X e. A /\ Y e. A ) -> ( X .x. Y ) e. A ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		subrngmcl.p	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
2		eqid	$$⊢R{\upharpoonright }_{𝑠}A=R{\upharpoonright }_{𝑠}A$$
3	2	subrngrng	Could not format ( A e. ( SubRng ` R ) -> ( R |`s A ) e. Rng ) : No typesetting found for |- ( A e. ( SubRng ` R ) -> ( R |`s A ) e. Rng ) with typecode |-
4	3	3ad2ant1	Could not format ( ( A e. ( SubRng ` R ) /\ X e. A /\ Y e. A ) -> ( R |`s A ) e. Rng ) : No typesetting found for |- ( ( A e. ( SubRng ` R ) /\ X e. A /\ Y e. A ) -> ( R |`s A ) e. Rng ) with typecode |-
5		simp2	Could not format ( ( A e. ( SubRng ` R ) /\ X e. A /\ Y e. A ) -> X e. A ) : No typesetting found for |- ( ( A e. ( SubRng ` R ) /\ X e. A /\ Y e. A ) -> X e. A ) with typecode |-
6	2	subrngbas	Could not format ( A e. ( SubRng ` R ) -> A = ( Base ` ( R |`s A ) ) ) : No typesetting found for |- ( A e. ( SubRng ` R ) -> A = ( Base ` ( R |`s A ) ) ) with typecode |-
7	6	3ad2ant1	Could not format ( ( A e. ( SubRng ` R ) /\ X e. A /\ Y e. A ) -> A = ( Base ` ( R |`s A ) ) ) : No typesetting found for |- ( ( A e. ( SubRng ` R ) /\ X e. A /\ Y e. A ) -> A = ( Base ` ( R |`s A ) ) ) with typecode |-
8	5 7	eleqtrd	Could not format ( ( A e. ( SubRng ` R ) /\ X e. A /\ Y e. A ) -> X e. ( Base ` ( R |`s A ) ) ) : No typesetting found for |- ( ( A e. ( SubRng ` R ) /\ X e. A /\ Y e. A ) -> X e. ( Base ` ( R |`s A ) ) ) with typecode |-
9		simp3	Could not format ( ( A e. ( SubRng ` R ) /\ X e. A /\ Y e. A ) -> Y e. A ) : No typesetting found for |- ( ( A e. ( SubRng ` R ) /\ X e. A /\ Y e. A ) -> Y e. A ) with typecode |-
10	9 7	eleqtrd	Could not format ( ( A e. ( SubRng ` R ) /\ X e. A /\ Y e. A ) -> Y e. ( Base ` ( R |`s A ) ) ) : No typesetting found for |- ( ( A e. ( SubRng ` R ) /\ X e. A /\ Y e. A ) -> Y e. ( Base ` ( R |`s A ) ) ) with typecode |-
11		eqid	$$⊢{\mathrm{Base}}_{\left(R{\upharpoonright }_{𝑠}A\right)}={\mathrm{Base}}_{\left(R{\upharpoonright }_{𝑠}A\right)}$$
12		eqid	$$⊢{\cdot }_{\left(R{\upharpoonright }_{𝑠}A\right)}={\cdot }_{\left(R{\upharpoonright }_{𝑠}A\right)}$$
13	11 12	rngcl	$$⊢\left(R{\upharpoonright }_{𝑠}A\in \mathrm{Rng}\wedge X\in {\mathrm{Base}}_{\left(R{\upharpoonright }_{𝑠}A\right)}\wedge Y\in {\mathrm{Base}}_{\left(R{\upharpoonright }_{𝑠}A\right)}\right)\to X{\cdot }_{\left(R{\upharpoonright }_{𝑠}A\right)}Y\in {\mathrm{Base}}_{\left(R{\upharpoonright }_{𝑠}A\right)}$$
14	4 8 10 13	syl3anc	Could not format ( ( A e. ( SubRng ` R ) /\ X e. A /\ Y e. A ) -> ( X ( .r ` ( R |`s A ) ) Y ) e. ( Base ` ( R |`s A ) ) ) : No typesetting found for |- ( ( A e. ( SubRng ` R ) /\ X e. A /\ Y e. A ) -> ( X ( .r ` ( R |`s A ) ) Y ) e. ( Base ` ( R |`s A ) ) ) with typecode |-
15	2 1	ressmulr	Could not format ( A e. ( SubRng ` R ) -> .x. = ( .r ` ( R |`s A ) ) ) : No typesetting found for |- ( A e. ( SubRng ` R ) -> .x. = ( .r ` ( R |`s A ) ) ) with typecode |-
16	15	3ad2ant1	Could not format ( ( A e. ( SubRng ` R ) /\ X e. A /\ Y e. A ) -> .x. = ( .r ` ( R |`s A ) ) ) : No typesetting found for |- ( ( A e. ( SubRng ` R ) /\ X e. A /\ Y e. A ) -> .x. = ( .r ` ( R |`s A ) ) ) with typecode |-
17	16	oveqd	Could not format ( ( A e. ( SubRng ` R ) /\ X e. A /\ Y e. A ) -> ( X .x. Y ) = ( X ( .r ` ( R |`s A ) ) Y ) ) : No typesetting found for |- ( ( A e. ( SubRng ` R ) /\ X e. A /\ Y e. A ) -> ( X .x. Y ) = ( X ( .r ` ( R |`s A ) ) Y ) ) with typecode |-
18	14 17 7	3eltr4d	Could not format ( ( A e. ( SubRng ` R ) /\ X e. A /\ Y e. A ) -> ( X .x. Y ) e. A ) : No typesetting found for |- ( ( A e. ( SubRng ` R ) /\ X e. A /\ Y e. A ) -> ( X .x. Y ) e. A ) with typecode |-