This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem sraaddg

Description: Additive operation of a subring algebra. (Contributed by Stefan O'Rear, 27-Nov-2014) (Revised by Mario Carneiro, 4-Oct-2015) (Revised by Thierry Arnoux, 16-Jun-2019) (Revised by AV, 29-Oct-2024)

	Ref	Expression
Hypotheses	srapart.a	$⊢ φ \to A = subringAlg (W) (S)$
	srapart.s	$⊢ φ \to S \subseteq {Base}_{W}$
Assertion	sraaddg	$⊢ φ \to +_{W} = +_{A}$

Proof

Step	Hyp	Ref	Expression
1		srapart.a	$⊢ φ \to A = subringAlg (W) (S)$
2		srapart.s	$⊢ φ \to S \subseteq {Base}_{W}$
3		plusgid	$⊢ +_{𝑔} = Slot +_{ndx}$
4		scandxnplusgndx	$⊢ Scalar (ndx) \neq +_{ndx}$
5		vscandxnplusgndx	$⊢ \cdot_{ndx} \neq +_{ndx}$
6		ipndxnplusgndx	$⊢ \cdot_{𝑖} (ndx) \neq +_{ndx}$
7	1 2 3 4 5 6	sralem	$⊢ φ \to +_{W} = +_{A}$