Metamath Proof Explorer

Theorem zlmds

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

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 slotsdnscsi 
 |-  ( ( dist ` ndx ) =/= ( Scalar ` ndx ) /\ ( dist ` ndx ) =/= ( .s ` ndx ) /\ ( dist ` ndx ) =/= ( .i ` ndx ) )
8 7 simp1i 
 |-  ( dist ` ndx ) =/= ( Scalar ` ndx )
9 6 8 setsnid 
 |-  ( dist ` G ) = ( dist ` ( G sSet <. ( Scalar ` ndx ) , ZZring >. ) )
10 7 simp2i 
 |-  ( dist ` ndx ) =/= ( .s ` ndx )
11 6 10 setsnid 
 |-  ( dist ` ( G sSet <. ( Scalar ` ndx ) , ZZring >. ) ) = ( dist ` ( ( G sSet <. ( Scalar ` ndx ) , ZZring >. ) sSet <. ( .s ` ndx ) , ( .g ` G ) >. ) )
12 9 11 eqtri 
 |-  ( dist ` G ) = ( dist ` ( ( G sSet <. ( Scalar ` ndx ) , ZZring >. ) sSet <. ( .s ` ndx ) , ( .g ` G ) >. ) )
13 5 12 eqtr4di 
 |-  ( G e. V -> ( dist ` W ) = ( dist ` G ) )
14 2 13 eqtr4id 
 |-  ( G e. V -> D = ( dist ` W ) )