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
|- ( 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 ) )