Metamath Proof Explorer

Theorem zlmlemOLD

Description: Obsolete version of zlmlem as of 3-Nov-2024. Lemma for zlmbas and zlmplusg . (Contributed by Mario Carneiro, 2-Oct-2015) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Hypotheses zlmbas.w 
|- W = ( ZMod ` G )
zlmlemOLD.2 
|- E = Slot N
zlmlemOLD.3 
|- N e. NN
zlmlemOLD.4 
|- N < 5
Assertion zlmlemOLD 
|- ( E ` G ) = ( E ` W )

Proof

Step Hyp Ref Expression
1 zlmbas.w 
 |-  W = ( ZMod ` G )
2 zlmlemOLD.2 
 |-  E = Slot N
3 zlmlemOLD.3 
 |-  N e. NN
4 zlmlemOLD.4 
 |-  N < 5
5 2 3 ndxid 
 |-  E = Slot ( E ` ndx )
6 2 3 ndxarg 
 |-  ( E ` ndx ) = N
7 3 nnrei 
 |-  N e. RR
8 6 7 eqeltri 
 |-  ( E ` ndx ) e. RR
9 6 4 eqbrtri 
 |-  ( E ` ndx ) < 5
10 8 9 ltneii 
 |-  ( E ` ndx ) =/= 5
11 scandx 
 |-  ( Scalar ` ndx ) = 5
12 10 11 neeqtrri 
 |-  ( E ` ndx ) =/= ( Scalar ` ndx )
13 5 12 setsnid 
 |-  ( E ` G ) = ( E ` ( G sSet <. ( Scalar ` ndx ) , ZZring >. ) )
14 5lt6 
 |-  5 < 6
15 5re 
 |-  5 e. RR
16 6re 
 |-  6 e. RR
17 8 15 16 lttri 
 |-  ( ( ( E ` ndx ) < 5 /\ 5 < 6 ) -> ( E ` ndx ) < 6 )
18 9 14 17 mp2an 
 |-  ( E ` ndx ) < 6
19 8 18 ltneii 
 |-  ( E ` ndx ) =/= 6
20 vscandx 
 |-  ( .s ` ndx ) = 6
21 19 20 neeqtrri 
 |-  ( E ` ndx ) =/= ( .s ` ndx )
22 5 21 setsnid 
 |-  ( E ` ( G sSet <. ( Scalar ` ndx ) , ZZring >. ) ) = ( E ` ( ( G sSet <. ( Scalar ` ndx ) , ZZring >. ) sSet <. ( .s ` ndx ) , ( .g ` G ) >. ) )
23 13 22 eqtri 
 |-  ( E ` G ) = ( E ` ( ( G sSet <. ( Scalar ` ndx ) , ZZring >. ) sSet <. ( .s ` ndx ) , ( .g ` G ) >. ) )
24 eqid 
 |-  ( .g ` G ) = ( .g ` G )
25 1 24 zlmval 
 |-  ( G e. _V -> W = ( ( G sSet <. ( Scalar ` ndx ) , ZZring >. ) sSet <. ( .s ` ndx ) , ( .g ` G ) >. ) )
26 25 fveq2d 
 |-  ( G e. _V -> ( E ` W ) = ( E ` ( ( G sSet <. ( Scalar ` ndx ) , ZZring >. ) sSet <. ( .s ` ndx ) , ( .g ` G ) >. ) ) )
27 23 26 eqtr4id 
 |-  ( G e. _V -> ( E ` G ) = ( E ` W ) )
28 2 str0 
 |-  (/) = ( E ` (/) )
29 fvprc 
 |-  ( -. G e. _V -> ( E ` G ) = (/) )
30 fvprc 
 |-  ( -. G e. _V -> ( ZMod ` G ) = (/) )
31 1 30 eqtrid 
 |-  ( -. G e. _V -> W = (/) )
32 31 fveq2d 
 |-  ( -. G e. _V -> ( E ` W ) = ( E ` (/) ) )
33 28 29 32 3eqtr4a 
 |-  ( -. G e. _V -> ( E ` G ) = ( E ` W ) )
34 27 33 pm2.61i 
 |-  ( E ` G ) = ( E ` W )