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 = ℤMod (G)$
	zlmlemOLD.2	$⊢ E = Slot N$
	zlmlemOLD.3	$⊢ N \in ℕ$
	zlmlemOLD.4	$⊢ N < 5$
Assertion	zlmlemOLD	$⊢ E (G) = E (W)$

Proof

Step	Hyp	Ref	Expression
1		zlmbas.w	$⊢ W = ℤMod (G)$
2		zlmlemOLD.2	$⊢ E = Slot N$
3		zlmlemOLD.3	$⊢ N \in ℕ$
4		zlmlemOLD.4	$⊢ N < 5$
5	2 3	ndxid	$⊢ E = Slot E (ndx)$
6	2 3	ndxarg	$⊢ E (ndx) = N$
7	3	nnrei	$⊢ N \in ℝ$
8	6 7	eqeltri	$⊢ E (ndx) \in ℝ$
9	6 4	eqbrtri	$⊢ E (ndx) < 5$
10	8 9	ltneii	$⊢ E (ndx) \neq 5$
11		scandx	$⊢ Scalar (ndx) = 5$
12	10 11	neeqtrri	$⊢ E (ndx) \neq Scalar (ndx)$
13	5 12	setsnid	$⊢ E (G) = E (G sSet ⟨Scalar (ndx), ℤ_{ring}⟩)$
14		5lt6	$⊢ 5 < 6$
15		5re	$⊢ 5 \in ℝ$
16		6re	$⊢ 6 \in ℝ$
17	8 15 16	lttri	$⊢ (E (ndx) < 5 \land 5 < 6) \to E (ndx) < 6$
18	9 14 17	mp2an	$⊢ E (ndx) < 6$
19	8 18	ltneii	$⊢ E (ndx) \neq 6$
20		vscandx	$⊢ \cdot_{ndx} = 6$
21	19 20	neeqtrri	$⊢ E (ndx) \neq \cdot_{ndx}$
22	5 21	setsnid	$⊢ E (G sSet ⟨Scalar (ndx), ℤ_{ring}⟩) = E ((G sSet ⟨Scalar (ndx), ℤ_{ring}⟩) sSet ⟨\cdot_{ndx}, \cdot_{G}⟩)$
23	13 22	eqtri	$⊢ E (G) = E ((G sSet ⟨Scalar (ndx), ℤ_{ring}⟩) sSet ⟨\cdot_{ndx}, \cdot_{G}⟩)$
24		eqid	$⊢ \cdot_{G} = \cdot_{G}$
25	1 24	zlmval	$⊢ G \in V \to W = (G sSet ⟨Scalar (ndx), ℤ_{ring}⟩) sSet ⟨\cdot_{ndx}, \cdot_{G}⟩$
26	25	fveq2d	$⊢ G \in V \to E (W) = E ((G sSet ⟨Scalar (ndx), ℤ_{ring}⟩) sSet ⟨\cdot_{ndx}, \cdot_{G}⟩)$
27	23 26	eqtr4id	$⊢ 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	eqtrid	$⊢ \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 zlmlemOLD

Proof