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

Metamath Proof Explorer

Theorem srads

Description: Distance function of a subring algebra. (Contributed 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	srads	$⊢ φ \to dist (W) = dist (A)$

Proof

Step	Hyp	Ref	Expression
1		srapart.a	$⊢ φ \to A = subringAlg (W) (S)$
2		srapart.s	$⊢ φ \to S \subseteq {Base}_{W}$
3		dsid	$⊢ dist = Slot dist (ndx)$
4		slotsdnscsi	$⊢ (dist (ndx) \neq Scalar (ndx) \land dist (ndx) \neq \cdot_{ndx} \land dist (ndx) \neq \cdot_{𝑖} (ndx))$
5	4	simp1i	$⊢ dist (ndx) \neq Scalar (ndx)$
6	5	necomi	$⊢ Scalar (ndx) \neq dist (ndx)$
7	4	simp2i	$⊢ dist (ndx) \neq \cdot_{ndx}$
8	7	necomi	$⊢ \cdot_{ndx} \neq dist (ndx)$
9	4	simp3i	$⊢ dist (ndx) \neq \cdot_{𝑖} (ndx)$
10	9	necomi	$⊢ \cdot_{𝑖} (ndx) \neq dist (ndx)$
11	1 2 3 6 8 10	sralem	$⊢ φ \to dist (W) = dist (A)$