Metamath Proof Explorer

Theorem zlmlem

Description: Lemma for zlmbas and zlmplusg . (Contributed by Mario Carneiro, 2-Oct-2015) (Revised by AV, 3-Nov-2024)

Ref Expression
Hypotheses zlmbas.w 
|- W = ( ZMod ` G )
zlmlem.2 
|- E = Slot ( E ` ndx )
zlmlem.3 
|- ( E ` ndx ) =/= ( Scalar ` ndx )
zlmlem.4 
|- ( E ` ndx ) =/= ( .s ` ndx )
Assertion zlmlem 
|- ( E ` G ) = ( E ` W )

Proof

Step Hyp Ref Expression
1 zlmbas.w 
 |-  W = ( ZMod ` G )
2 zlmlem.2 
 |-  E = Slot ( E ` ndx )
3 zlmlem.3 
 |-  ( E ` ndx ) =/= ( Scalar ` ndx )
4 zlmlem.4 
 |-  ( E ` ndx ) =/= ( .s ` ndx )
5 2 3 setsnid 
 |-  ( E ` G ) = ( E ` ( G sSet <. ( Scalar ` ndx ) , ZZring >. ) )
6 2 4 setsnid 
 |-  ( E ` ( G sSet <. ( Scalar ` ndx ) , ZZring >. ) ) = ( E ` ( ( G sSet <. ( Scalar ` ndx ) , ZZring >. ) sSet <. ( .s ` ndx ) , ( .g ` G ) >. ) )
7 5 6 eqtri 
 |-  ( E ` G ) = ( E ` ( ( G sSet <. ( Scalar ` ndx ) , ZZring >. ) sSet <. ( .s ` ndx ) , ( .g ` G ) >. ) )
8 eqid 
 |-  ( .g ` G ) = ( .g ` G )
9 1 8 zlmval 
 |-  ( G e. _V -> W = ( ( G sSet <. ( Scalar ` ndx ) , ZZring >. ) sSet <. ( .s ` ndx ) , ( .g ` G ) >. ) )
10 9 fveq2d 
 |-  ( G e. _V -> ( E ` W ) = ( E ` ( ( G sSet <. ( Scalar ` ndx ) , ZZring >. ) sSet <. ( .s ` ndx ) , ( .g ` G ) >. ) ) )
11 7 10 eqtr4id 
 |-  ( G e. _V -> ( E ` G ) = ( E ` W ) )
12 2 str0 
 |-  (/) = ( E ` (/) )
13 12 eqcomi 
 |-  ( E ` (/) ) = (/)
14 13 1 fveqprc 
 |-  ( -. G e. _V -> ( E ` G ) = ( E ` W ) )
15 11 14 pm2.61i 
 |-  ( E ` G ) = ( E ` W )