Metamath Proof Explorer


Theorem zlmlem

Description: Lemma for zlmbas and zlmplusg . (Contributed by Mario Carneiro, 2-Oct-2015)

Ref Expression
Hypotheses zlmbas.w W = ℤMod G
zlmlem.2 E = Slot N
zlmlem.3 N
zlmlem.4 N < 5
Assertion zlmlem E G = E W

Proof

Step Hyp Ref Expression
1 zlmbas.w W = ℤMod G
2 zlmlem.2 E = Slot N
3 zlmlem.3 N
4 zlmlem.4 N < 5
5 2 3 ndxid E = Slot E ndx
6 2 3 ndxarg E ndx = N
7 3 nnrei N
8 6 7 eqeltri E ndx
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 ring
14 5lt6 5 < 6
15 5re 5
16 6re 6
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 ndx = 6
21 19 20 neeqtrri E ndx ndx
22 5 21 setsnid E G sSet Scalar ndx ring = E G sSet Scalar ndx ring sSet ndx G
23 13 22 eqtri E G = E G sSet Scalar ndx ring sSet ndx G
24 eqid G = G
25 1 24 zlmval G V W = G sSet Scalar ndx ring sSet ndx G
26 25 fveq2d G V E W = E G sSet Scalar ndx ring sSet ndx G
27 23 26 eqtr4id G V E G = E W
28 2 str0 = E
29 fvprc ¬ G V E G =
30 fvprc ¬ G V ℤMod G =
31 1 30 eqtrid ¬ G V W =
32 31 fveq2d ¬ G V E W = E
33 28 29 32 3eqtr4a ¬ G V E G = E W
34 27 33 pm2.61i E G = E W