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