ringvcl

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

	Ref	Expression
Hypotheses	ringvcl.b	$⊢ B = {Base}_{R}$
	ringvcl.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
Assertion	ringvcl	$⊢ (R \in Ring \land X \in (B^{I}) \land Y \in (B^{I})) \to X {\underset{˙}{\cdot}}_{f} Y \in (B^{I})$

Step	Hyp	Ref	Expression
1		ringvcl.b	$⊢ B = {Base}_{R}$
2		ringvcl.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
3		eqid	$⊢ {mulGrp}_{R} = {mulGrp}_{R}$
4	3	ringmgp	$⊢ R \in Ring \to {mulGrp}_{R} \in Mnd$
5	3 1	mgpbas	$⊢ B = {Base}_{{mulGrp}_{R}}$
6	3 2	mgpplusg	$⊢ \underset{˙}{\cdot} = +_{{mulGrp}_{R}}$
7	5 6	mndvcl	$⊢ ({mulGrp}_{R} \in Mnd \land X \in (B^{I}) \land Y \in (B^{I})) \to X {\underset{˙}{\cdot}}_{f} Y \in (B^{I})$
8	4 7	syl3an1	$⊢ (R \in Ring \land X \in (B^{I}) \land Y \in (B^{I})) \to X {\underset{˙}{\cdot}}_{f} Y \in (B^{I})$

Metamath Proof Explorer