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	|- ( ph -> A = ( ( subringAlg ` W ) ` S ) )
	srapart.s	|- ( ph -> S C_ ( Base ` W ) )
Assertion	srads	|- ( ph -> ( dist ` W ) = ( dist ` A ) )

Proof

Step	Hyp	Ref	Expression
1		srapart.a	|- ( ph -> A = ( ( subringAlg ` W ) ` S ) )
2		srapart.s	|- ( ph -> S C_ ( Base ` W ) )
3		dsid	|- dist = Slot ( dist ` ndx )
4		slotsdnscsi	|- ( ( dist ` ndx ) =/= ( Scalar ` ndx ) /\ ( dist ` ndx ) =/= ( .s ` ndx ) /\ ( dist ` ndx ) =/= ( .i ` ndx ) )
5	4	simp1i	|- ( dist ` ndx ) =/= ( Scalar ` ndx )
6	5	necomi	|- ( Scalar ` ndx ) =/= ( dist ` ndx )
7	4	simp2i	|- ( dist ` ndx ) =/= ( .s ` ndx )
8	7	necomi	|- ( .s ` ndx ) =/= ( dist ` ndx )
9	4	simp3i	|- ( dist ` ndx ) =/= ( .i ` ndx )
10	9	necomi	|- ( .i ` ndx ) =/= ( dist ` ndx )
11	1 2 3 6 8 10	sralem	|- ( ph -> ( dist ` W ) = ( dist ` A ) )