Theorem ringvcl

Description: Tuple-wise multiplication closure in monoids. (Contributed by Stefan O'Rear, 5-Sep-2015)

	Ref	Expression
Hypotheses	ringvcl.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
	ringvcl.t	⊢ · = ( .r ‘ 𝑅 )
Assertion	ringvcl	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ ( 𝐵 ↑m 𝐼 ) ∧ 𝑌 ∈ ( 𝐵 ↑m 𝐼 ) ) → ( 𝑋 ∘f · 𝑌 ) ∈ ( 𝐵 ↑m 𝐼 ) )

Proof

Step	Hyp	Ref	Expression
1		ringvcl.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
2		ringvcl.t	⊢ · = ( .r ‘ 𝑅 )
3		eqid	⊢ ( mulGrp ‘ 𝑅 ) = ( mulGrp ‘ 𝑅 )
4	3	ringmgp	⊢ ( 𝑅 ∈ Ring → ( mulGrp ‘ 𝑅 ) ∈ Mnd )
5	3 1	mgpbas	⊢ 𝐵 = ( Base ‘ ( mulGrp ‘ 𝑅 ) )
6	3 2	mgpplusg	⊢ · = ( +g ‘ ( mulGrp ‘ 𝑅 ) )
7	5 6	mndvcl	⊢ ( ( ( mulGrp ‘ 𝑅 ) ∈ Mnd ∧ 𝑋 ∈ ( 𝐵 ↑m 𝐼 ) ∧ 𝑌 ∈ ( 𝐵 ↑m 𝐼 ) ) → ( 𝑋 ∘f · 𝑌 ) ∈ ( 𝐵 ↑m 𝐼 ) )
8	4 7	syl3an1	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ ( 𝐵 ↑m 𝐼 ) ∧ 𝑌 ∈ ( 𝐵 ↑m 𝐼 ) ) → ( 𝑋 ∘f · 𝑌 ) ∈ ( 𝐵 ↑m 𝐼 ) )