Theorem zlmlem

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

	Ref	Expression
Hypotheses	zlmbas.w	⊢ 𝑊 = ( ℤMod ‘ 𝐺 )
	zlmlem.2	⊢ 𝐸 = Slot 𝑁
	zlmlem.3	⊢ 𝑁 ∈ ℕ
	zlmlem.4	⊢ 𝑁 < 5
Assertion	zlmlem	⊢ ( 𝐸 ‘ 𝐺 ) = ( 𝐸 ‘ 𝑊 )

Proof

Step	Hyp	Ref	Expression
1		zlmbas.w	⊢ 𝑊 = ( ℤMod ‘ 𝐺 )
2		zlmlem.2	⊢ 𝐸 = Slot 𝑁
3		zlmlem.3	⊢ 𝑁 ∈ ℕ
4		zlmlem.4	⊢ 𝑁 < 5
5	2 3	ndxid	⊢ 𝐸 = Slot ( 𝐸 ‘ ndx )
6	2 3	ndxarg	⊢ ( 𝐸 ‘ ndx ) = 𝑁
7	3	nnrei	⊢ 𝑁 ∈ ℝ
8	6 7	eqeltri	⊢ ( 𝐸 ‘ ndx ) ∈ ℝ
9	6 4	eqbrtri	⊢ ( 𝐸 ‘ ndx ) < 5
10	8 9	ltneii	⊢ ( 𝐸 ‘ ndx ) ≠ 5
11		scandx	⊢ ( Scalar ‘ ndx ) = 5
12	10 11	neeqtrri	⊢ ( 𝐸 ‘ ndx ) ≠ ( Scalar ‘ ndx )
13	5 12	setsnid	⊢ ( 𝐸 ‘ 𝐺 ) = ( 𝐸 ‘ ( 𝐺 sSet ⟨ ( Scalar ‘ ndx ) , ℤring ⟩ ) )
14		5lt6	⊢ 5 < 6
15		5re	⊢ 5 ∈ ℝ
16		6re	⊢ 6 ∈ ℝ
17	8 15 16	lttri	⊢ ( ( ( 𝐸 ‘ ndx ) < 5 ∧ 5 < 6 ) → ( 𝐸 ‘ ndx ) < 6 )
18	9 14 17	mp2an	⊢ ( 𝐸 ‘ ndx ) < 6
19	8 18	ltneii	⊢ ( 𝐸 ‘ ndx ) ≠ 6
20		vscandx	⊢ ( ·𝑠 ‘ ndx ) = 6
21	19 20	neeqtrri	⊢ ( 𝐸 ‘ ndx ) ≠ ( ·𝑠 ‘ ndx )
22	5 21	setsnid	⊢ ( 𝐸 ‘ ( 𝐺 sSet ⟨ ( Scalar ‘ ndx ) , ℤring ⟩ ) ) = ( 𝐸 ‘ ( ( 𝐺 sSet ⟨ ( Scalar ‘ ndx ) , ℤring ⟩ ) sSet ⟨ ( ·𝑠 ‘ ndx ) , ( .g ‘ 𝐺 ) ⟩ ) )
23	13 22	eqtri	⊢ ( 𝐸 ‘ 𝐺 ) = ( 𝐸 ‘ ( ( 𝐺 sSet ⟨ ( Scalar ‘ ndx ) , ℤring ⟩ ) sSet ⟨ ( ·𝑠 ‘ ndx ) , ( .g ‘ 𝐺 ) ⟩ ) )
24		eqid	⊢ ( .g ‘ 𝐺 ) = ( .g ‘ 𝐺 )
25	1 24	zlmval	⊢ ( 𝐺 ∈ V → 𝑊 = ( ( 𝐺 sSet ⟨ ( Scalar ‘ ndx ) , ℤring ⟩ ) sSet ⟨ ( ·𝑠 ‘ ndx ) , ( .g ‘ 𝐺 ) ⟩ ) )
26	25	fveq2d	⊢ ( 𝐺 ∈ V → ( 𝐸 ‘ 𝑊 ) = ( 𝐸 ‘ ( ( 𝐺 sSet ⟨ ( Scalar ‘ ndx ) , ℤring ⟩ ) sSet ⟨ ( ·𝑠 ‘ ndx ) , ( .g ‘ 𝐺 ) ⟩ ) ) )
27	23 26	eqtr4id	⊢ ( 𝐺 ∈ V → ( 𝐸 ‘ 𝐺 ) = ( 𝐸 ‘ 𝑊 ) )
28	2	str0	⊢ ∅ = ( 𝐸 ‘ ∅ )
29		fvprc	⊢ ( ¬ 𝐺 ∈ V → ( 𝐸 ‘ 𝐺 ) = ∅ )
30		fvprc	⊢ ( ¬ 𝐺 ∈ V → ( ℤMod ‘ 𝐺 ) = ∅ )
31	1 30	eqtrid	⊢ ( ¬ 𝐺 ∈ V → 𝑊 = ∅ )
32	31	fveq2d	⊢ ( ¬ 𝐺 ∈ V → ( 𝐸 ‘ 𝑊 ) = ( 𝐸 ‘ ∅ ) )
33	28 29 32	3eqtr4a	⊢ ( ¬ 𝐺 ∈ V → ( 𝐸 ‘ 𝐺 ) = ( 𝐸 ‘ 𝑊 ) )
34	27 33	pm2.61i	⊢ ( 𝐸 ‘ 𝐺 ) = ( 𝐸 ‘ 𝑊 )