Theorem srads

Description: Distance function of a subring algebra. (Contributed by Mario Carneiro, 4-Oct-2015) (Revised by Thierry Arnoux, 16-Jun-2019)

	Ref	Expression
Hypotheses	srapart.a	$$⊢\phi \to A=\mathrm{subringAlg}\left(W\right)\left(S\right)$$
	srapart.s	$$⊢\phi \to S\subseteq {\mathrm{Base}}_W$$
Assertion	srads	$$⊢\phi \to \mathrm{dist}\left(W\right)=\mathrm{dist}\left(A\right)$$

Proof

Step	Hyp	Ref	Expression
1		srapart.a	$$⊢\phi \to A=\mathrm{subringAlg}\left(W\right)\left(S\right)$$
2		srapart.s	$$⊢\phi \to S\subseteq {\mathrm{Base}}_W$$
3		df-ds	$$⊢\mathrm{dist}=\mathrm{Slot}12$$
4		1nn0	$$⊢1\in {\mathbb{N}}_0$$
5		2nn	$$⊢2\in \mathbb{N}$$
6	4 5	decnncl	$$⊢12\in \mathbb{N}$$
7		1nn	$$⊢1\in \mathbb{N}$$
8		2nn0	$$⊢2\in {\mathbb{N}}_0$$
9		8nn0	$$⊢8\in {\mathbb{N}}_0$$
10		8lt10	$$⊢8<10$$
11	7 8 9 10	declti	$$⊢8<12$$
12	11	olci	$$⊢\left(12<5\vee 8<12\right)$$
13	1 2 3 6 12	sralem	$$⊢\phi \to \mathrm{dist}\left(W\right)=\mathrm{dist}\left(A\right)$$