zlmlem

	Ref	Expression
Hypotheses	zlmbas.w	$⊢ W = ℤMod (G)$
	zlmlem.2	$⊢ E = Slot N$
	zlmlem.3	$⊢ N \in ℕ$
	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 \in ℕ$
4		zlmlem.4	$⊢ N < 5$
5		eqid	$⊢ \cdot_{G} = \cdot_{G}$
6	1 5	zlmval	$⊢ G \in V \to W = (G sSet ⟨Scalar (ndx), ℤ_{ring}⟩) sSet ⟨\cdot_{ndx}, \cdot_{G}⟩$
7	6	fveq2d	$⊢ G \in V \to E (W) = E ((G sSet ⟨Scalar (ndx), ℤ_{ring}⟩) sSet ⟨\cdot_{ndx}, \cdot_{G}⟩)$
8	2 3	ndxid	$⊢ E = Slot E (ndx)$
9	2 3	ndxarg	$⊢ E (ndx) = N$
10	3	nnrei	$⊢ N \in ℝ$
11	9 10	eqeltri	$⊢ E (ndx) \in ℝ$
12	9 4	eqbrtri	$⊢ E (ndx) < 5$
13	11 12	ltneii	$⊢ E (ndx) \neq 5$
14		scandx	$⊢ Scalar (ndx) = 5$
15	13 14	neeqtrri	$⊢ E (ndx) \neq Scalar (ndx)$
16	8 15	setsnid	$⊢ E (G) = E (G sSet ⟨Scalar (ndx), ℤ_{ring}⟩)$
17		5lt6	$⊢ 5 < 6$
18		5re	$⊢ 5 \in ℝ$
19		6re	$⊢ 6 \in ℝ$
20	11 18 19	lttri	$⊢ (E (ndx) < 5 \land 5 < 6) \to E (ndx) < 6$
21	12 17 20	mp2an	$⊢ E (ndx) < 6$
22	11 21	ltneii	$⊢ E (ndx) \neq 6$
23		vscandx	$⊢ \cdot_{ndx} = 6$
24	22 23	neeqtrri	$⊢ E (ndx) \neq \cdot_{ndx}$
25	8 24	setsnid	$⊢ E (G sSet ⟨Scalar (ndx), ℤ_{ring}⟩) = E ((G sSet ⟨Scalar (ndx), ℤ_{ring}⟩) sSet ⟨\cdot_{ndx}, \cdot_{G}⟩)$
26	16 25	eqtri	$⊢ E (G) = E ((G sSet ⟨Scalar (ndx), ℤ_{ring}⟩) sSet ⟨\cdot_{ndx}, \cdot_{G}⟩)$
27	7 26	syl6reqr	$⊢ G \in V \to E (G) = E (W)$
28	2	str0	$⊢ \emptyset = E (\emptyset)$
29		fvprc	$⊢ \neg G \in V \to E (G) = \emptyset$
30		fvprc	$⊢ \neg G \in V \to ℤMod (G) = \emptyset$
31	1 30	syl5eq	$⊢ \neg G \in V \to W = \emptyset$
32	31	fveq2d	$⊢ \neg G \in V \to E (W) = E (\emptyset)$
33	28 29 32	3eqtr4a	$⊢ \neg G \in V \to E (G) = E (W)$
34	27 33	pm2.61i	$⊢ E (G) = E (W)$

Metamath Proof Explorer

Theorem zlmlem

Proof