# Metamath Proof Explorer

## Theorem zlmlem

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

Ref Expression
Hypotheses zlmbas.w ${⊢}{W}=\mathrm{ℤMod}\left({G}\right)$
zlmlem.2 ${⊢}{E}=\mathrm{Slot}{N}$
zlmlem.3 ${⊢}{N}\in ℕ$
zlmlem.4 ${⊢}{N}<5$
Assertion zlmlem ${⊢}{E}\left({G}\right)={E}\left({W}\right)$

### Proof

Step Hyp Ref Expression
1 zlmbas.w ${⊢}{W}=\mathrm{ℤMod}\left({G}\right)$
2 zlmlem.2 ${⊢}{E}=\mathrm{Slot}{N}$
3 zlmlem.3 ${⊢}{N}\in ℕ$
4 zlmlem.4 ${⊢}{N}<5$
5 2 3 ndxid ${⊢}{E}=\mathrm{Slot}{E}\left(\mathrm{ndx}\right)$
6 2 3 ndxarg ${⊢}{E}\left(\mathrm{ndx}\right)={N}$
7 3 nnrei ${⊢}{N}\in ℝ$
8 6 7 eqeltri ${⊢}{E}\left(\mathrm{ndx}\right)\in ℝ$
9 6 4 eqbrtri ${⊢}{E}\left(\mathrm{ndx}\right)<5$
10 8 9 ltneii ${⊢}{E}\left(\mathrm{ndx}\right)\ne 5$
11 scandx ${⊢}\mathrm{Scalar}\left(\mathrm{ndx}\right)=5$
12 10 11 neeqtrri ${⊢}{E}\left(\mathrm{ndx}\right)\ne \mathrm{Scalar}\left(\mathrm{ndx}\right)$
13 5 12 setsnid ${⊢}{E}\left({G}\right)={E}\left({G}\mathrm{sSet}⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),{ℤ}_{\mathrm{ring}}⟩\right)$
14 5lt6 ${⊢}5<6$
15 5re ${⊢}5\in ℝ$
16 6re ${⊢}6\in ℝ$
17 8 15 16 lttri ${⊢}\left({E}\left(\mathrm{ndx}\right)<5\wedge 5<6\right)\to {E}\left(\mathrm{ndx}\right)<6$
18 9 14 17 mp2an ${⊢}{E}\left(\mathrm{ndx}\right)<6$
19 8 18 ltneii ${⊢}{E}\left(\mathrm{ndx}\right)\ne 6$
20 vscandx ${⊢}{\cdot }_{\mathrm{ndx}}=6$
21 19 20 neeqtrri ${⊢}{E}\left(\mathrm{ndx}\right)\ne {\cdot }_{\mathrm{ndx}}$
22 5 21 setsnid ${⊢}{E}\left({G}\mathrm{sSet}⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),{ℤ}_{\mathrm{ring}}⟩\right)={E}\left(\left({G}\mathrm{sSet}⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),{ℤ}_{\mathrm{ring}}⟩\right)\mathrm{sSet}⟨{\cdot }_{\mathrm{ndx}},{\cdot }_{{G}}⟩\right)$
23 13 22 eqtri ${⊢}{E}\left({G}\right)={E}\left(\left({G}\mathrm{sSet}⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),{ℤ}_{\mathrm{ring}}⟩\right)\mathrm{sSet}⟨{\cdot }_{\mathrm{ndx}},{\cdot }_{{G}}⟩\right)$
24 eqid ${⊢}{\cdot }_{{G}}={\cdot }_{{G}}$
25 1 24 zlmval ${⊢}{G}\in \mathrm{V}\to {W}=\left({G}\mathrm{sSet}⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),{ℤ}_{\mathrm{ring}}⟩\right)\mathrm{sSet}⟨{\cdot }_{\mathrm{ndx}},{\cdot }_{{G}}⟩$
26 25 fveq2d ${⊢}{G}\in \mathrm{V}\to {E}\left({W}\right)={E}\left(\left({G}\mathrm{sSet}⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),{ℤ}_{\mathrm{ring}}⟩\right)\mathrm{sSet}⟨{\cdot }_{\mathrm{ndx}},{\cdot }_{{G}}⟩\right)$
27 23 26 eqtr4id ${⊢}{G}\in \mathrm{V}\to {E}\left({G}\right)={E}\left({W}\right)$
28 2 str0 ${⊢}\varnothing ={E}\left(\varnothing \right)$
29 fvprc ${⊢}¬{G}\in \mathrm{V}\to {E}\left({G}\right)=\varnothing$
30 fvprc ${⊢}¬{G}\in \mathrm{V}\to \mathrm{ℤMod}\left({G}\right)=\varnothing$
31 1 30 syl5eq ${⊢}¬{G}\in \mathrm{V}\to {W}=\varnothing$
32 31 fveq2d ${⊢}¬{G}\in \mathrm{V}\to {E}\left({W}\right)={E}\left(\varnothing \right)$
33 28 29 32 3eqtr4a ${⊢}¬{G}\in \mathrm{V}\to {E}\left({G}\right)={E}\left({W}\right)$
34 27 33 pm2.61i ${⊢}{E}\left({G}\right)={E}\left({W}\right)$