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)

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 df-ds
 |-  dist = Slot ; 1 2
4 1nn0
 |-  1 e. NN0
5 2nn
 |-  2 e. NN
6 4 5 decnncl
 |-  ; 1 2 e. NN
7 1nn
 |-  1 e. NN
8 2nn0
 |-  2 e. NN0
9 8nn0
 |-  8 e. NN0
10 8lt10
 |-  8 < ; 1 0
11 7 8 9 10 declti
 |-  8 < ; 1 2
12 11 olci
 |-  ( ; 1 2 < 5 \/ 8 < ; 1 2 )
13 1 2 3 6 12 sralem
 |-  ( ph -> ( dist ` W ) = ( dist ` A ) )