Metamath Proof Explorer

Theorem zlmds

Description: Distance in a ZZ -module (if present). (Contributed by Thierry Arnoux, 8-Nov-2017)

Ref Expression
Hypotheses zlmlem2.1 
|- W = ( ZMod ` G )
zlmds.1 
|- D = ( dist ` G )
Assertion zlmds 
|- ( G e. V -> D = ( dist ` W ) )

Proof

Step Hyp Ref Expression
1 zlmlem2.1 
 |-  W = ( ZMod ` G )
2 zlmds.1 
 |-  D = ( dist ` G )
3 eqid 
 |-  ( .g ` G ) = ( .g ` G )
4 1 3 zlmval 
 |-  ( G e. V -> W = ( ( G sSet <. ( Scalar ` ndx ) , ZZring >. ) sSet <. ( .s ` ndx ) , ( .g ` G ) >. ) )
5 4 fveq2d 
 |-  ( G e. V -> ( dist ` W ) = ( dist ` ( ( G sSet <. ( Scalar ` ndx ) , ZZring >. ) sSet <. ( .s ` ndx ) , ( .g ` G ) >. ) ) )
6 dsid 
 |-  dist = Slot ( dist ` ndx )
7 5re 
 |-  5 e. RR
8 1nn 
 |-  1 e. NN
9 2nn0 
 |-  2 e. NN0
10 5nn0 
 |-  5 e. NN0
11 5lt10 
 |-  5 < ; 1 0
12 8 9 10 11 declti 
 |-  5 < ; 1 2
13 7 12 gtneii 
 |-  ; 1 2 =/= 5
14 dsndx 
 |-  ( dist ` ndx ) = ; 1 2
15 scandx 
 |-  ( Scalar ` ndx ) = 5
16 14 15 neeq12i 
 |-  ( ( dist ` ndx ) =/= ( Scalar ` ndx ) <-> ; 1 2 =/= 5 )
17 13 16 mpbir 
 |-  ( dist ` ndx ) =/= ( Scalar ` ndx )
18 6 17 setsnid 
 |-  ( dist ` G ) = ( dist ` ( G sSet <. ( Scalar ` ndx ) , ZZring >. ) )
19 6re 
 |-  6 e. RR
20 6nn0 
 |-  6 e. NN0
21 6lt10 
 |-  6 < ; 1 0
22 8 9 20 21 declti 
 |-  6 < ; 1 2
23 19 22 gtneii 
 |-  ; 1 2 =/= 6
24 vscandx 
 |-  ( .s ` ndx ) = 6
25 14 24 neeq12i 
 |-  ( ( dist ` ndx ) =/= ( .s ` ndx ) <-> ; 1 2 =/= 6 )
26 23 25 mpbir 
 |-  ( dist ` ndx ) =/= ( .s ` ndx )
27 6 26 setsnid 
 |-  ( dist ` ( G sSet <. ( Scalar ` ndx ) , ZZring >. ) ) = ( dist ` ( ( G sSet <. ( Scalar ` ndx ) , ZZring >. ) sSet <. ( .s ` ndx ) , ( .g ` G ) >. ) )
28 18 27 eqtri 
 |-  ( dist ` G ) = ( dist ` ( ( G sSet <. ( Scalar ` ndx ) , ZZring >. ) sSet <. ( .s ` ndx ) , ( .g ` G ) >. ) )
29 5 28 eqtr4di 
 |-  ( G e. V -> ( dist ` W ) = ( dist ` G ) )
30 2 29 eqtr4id 
 |-  ( G e. V -> D = ( dist ` W ) )