Theorem subrngmcl

Description: A subgroup is closed under multiplication. (Contributed by Mario Carneiro, 2-Dec-2014) Generalization of subrgmcl . (Revised by AV, 14-Feb-2025)

	Ref	Expression
Hypothesis	subrngmcl.p	⊢ · = ( .r ‘ 𝑅 )
Assertion	subrngmcl	⊢ ( ( 𝐴 ∈ ( SubRng ‘ 𝑅 ) ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) → ( 𝑋 · 𝑌 ) ∈ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		subrngmcl.p	⊢ · = ( .r ‘ 𝑅 )
2		eqid	⊢ ( 𝑅 ↾s 𝐴 ) = ( 𝑅 ↾s 𝐴 )
3	2	subrngrng	⊢ ( 𝐴 ∈ ( SubRng ‘ 𝑅 ) → ( 𝑅 ↾s 𝐴 ) ∈ Rng )
4	3	3ad2ant1	⊢ ( ( 𝐴 ∈ ( SubRng ‘ 𝑅 ) ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) → ( 𝑅 ↾s 𝐴 ) ∈ Rng )
5		simp2	⊢ ( ( 𝐴 ∈ ( SubRng ‘ 𝑅 ) ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) → 𝑋 ∈ 𝐴 )
6	2	subrngbas	⊢ ( 𝐴 ∈ ( SubRng ‘ 𝑅 ) → 𝐴 = ( Base ‘ ( 𝑅 ↾s 𝐴 ) ) )
7	6	3ad2ant1	⊢ ( ( 𝐴 ∈ ( SubRng ‘ 𝑅 ) ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) → 𝐴 = ( Base ‘ ( 𝑅 ↾s 𝐴 ) ) )
8	5 7	eleqtrd	⊢ ( ( 𝐴 ∈ ( SubRng ‘ 𝑅 ) ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) → 𝑋 ∈ ( Base ‘ ( 𝑅 ↾s 𝐴 ) ) )
9		simp3	⊢ ( ( 𝐴 ∈ ( SubRng ‘ 𝑅 ) ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) → 𝑌 ∈ 𝐴 )
10	9 7	eleqtrd	⊢ ( ( 𝐴 ∈ ( SubRng ‘ 𝑅 ) ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) → 𝑌 ∈ ( Base ‘ ( 𝑅 ↾s 𝐴 ) ) )
11		eqid	⊢ ( Base ‘ ( 𝑅 ↾s 𝐴 ) ) = ( Base ‘ ( 𝑅 ↾s 𝐴 ) )
12		eqid	⊢ ( .r ‘ ( 𝑅 ↾s 𝐴 ) ) = ( .r ‘ ( 𝑅 ↾s 𝐴 ) )
13	11 12	rngcl	⊢ ( ( ( 𝑅 ↾s 𝐴 ) ∈ Rng ∧ 𝑋 ∈ ( Base ‘ ( 𝑅 ↾s 𝐴 ) ) ∧ 𝑌 ∈ ( Base ‘ ( 𝑅 ↾s 𝐴 ) ) ) → ( 𝑋 ( .r ‘ ( 𝑅 ↾s 𝐴 ) ) 𝑌 ) ∈ ( Base ‘ ( 𝑅 ↾s 𝐴 ) ) )
14	4 8 10 13	syl3anc	⊢ ( ( 𝐴 ∈ ( SubRng ‘ 𝑅 ) ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) → ( 𝑋 ( .r ‘ ( 𝑅 ↾s 𝐴 ) ) 𝑌 ) ∈ ( Base ‘ ( 𝑅 ↾s 𝐴 ) ) )
15	2 1	ressmulr	⊢ ( 𝐴 ∈ ( SubRng ‘ 𝑅 ) → · = ( .r ‘ ( 𝑅 ↾s 𝐴 ) ) )
16	15	3ad2ant1	⊢ ( ( 𝐴 ∈ ( SubRng ‘ 𝑅 ) ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) → · = ( .r ‘ ( 𝑅 ↾s 𝐴 ) ) )
17	16	oveqd	⊢ ( ( 𝐴 ∈ ( SubRng ‘ 𝑅 ) ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) → ( 𝑋 · 𝑌 ) = ( 𝑋 ( .r ‘ ( 𝑅 ↾s 𝐴 ) ) 𝑌 ) )
18	14 17 7	3eltr4d	⊢ ( ( 𝐴 ∈ ( SubRng ‘ 𝑅 ) ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ) → ( 𝑋 · 𝑌 ) ∈ 𝐴 )