Theorem zlmlem

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

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

Proof

Step	Hyp	Ref	Expression
1		zlmbas.w	|- W = ( ZMod ` G )
2		zlmlem.2	|- E = Slot N
3		zlmlem.3	|- N e. NN
4		zlmlem.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	syl5eq	|- ( -. 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 )