Theorem zlmlem

Description: Lemma for zlmbas and zlmplusg . (Contributed by Mario Carneiro, 2-Oct-2015) (Revised by AV, 3-Nov-2024)

	Ref	Expression
Hypotheses	zlmbas.w	⊢ 𝑊 = ( ℤMod ‘ 𝐺 )
	zlmlem.2	⊢ 𝐸 = Slot ( 𝐸 ‘ ndx )
	zlmlem.3	⊢ ( 𝐸 ‘ ndx ) ≠ ( Scalar ‘ ndx )
	zlmlem.4	⊢ ( 𝐸 ‘ ndx ) ≠ ( ·𝑠 ‘ ndx )
Assertion	zlmlem	⊢ ( 𝐸 ‘ 𝐺 ) = ( 𝐸 ‘ 𝑊 )

Proof

Step	Hyp	Ref	Expression
1		zlmbas.w	⊢ 𝑊 = ( ℤMod ‘ 𝐺 )
2		zlmlem.2	⊢ 𝐸 = Slot ( 𝐸 ‘ ndx )
3		zlmlem.3	⊢ ( 𝐸 ‘ ndx ) ≠ ( Scalar ‘ ndx )
4		zlmlem.4	⊢ ( 𝐸 ‘ ndx ) ≠ ( ·𝑠 ‘ ndx )
5	2 3	setsnid	⊢ ( 𝐸 ‘ 𝐺 ) = ( 𝐸 ‘ ( 𝐺 sSet ⟨ ( Scalar ‘ ndx ) , ℤring ⟩ ) )
6	2 4	setsnid	⊢ ( 𝐸 ‘ ( 𝐺 sSet ⟨ ( Scalar ‘ ndx ) , ℤring ⟩ ) ) = ( 𝐸 ‘ ( ( 𝐺 sSet ⟨ ( Scalar ‘ ndx ) , ℤring ⟩ ) sSet ⟨ ( ·𝑠 ‘ ndx ) , ( .g ‘ 𝐺 ) ⟩ ) )
7	5 6	eqtri	⊢ ( 𝐸 ‘ 𝐺 ) = ( 𝐸 ‘ ( ( 𝐺 sSet ⟨ ( Scalar ‘ ndx ) , ℤring ⟩ ) sSet ⟨ ( ·𝑠 ‘ ndx ) , ( .g ‘ 𝐺 ) ⟩ ) )
8		eqid	⊢ ( .g ‘ 𝐺 ) = ( .g ‘ 𝐺 )
9	1 8	zlmval	⊢ ( 𝐺 ∈ V → 𝑊 = ( ( 𝐺 sSet ⟨ ( Scalar ‘ ndx ) , ℤring ⟩ ) sSet ⟨ ( ·𝑠 ‘ ndx ) , ( .g ‘ 𝐺 ) ⟩ ) )
10	9	fveq2d	⊢ ( 𝐺 ∈ V → ( 𝐸 ‘ 𝑊 ) = ( 𝐸 ‘ ( ( 𝐺 sSet ⟨ ( Scalar ‘ ndx ) , ℤring ⟩ ) sSet ⟨ ( ·𝑠 ‘ ndx ) , ( .g ‘ 𝐺 ) ⟩ ) ) )
11	7 10	eqtr4id	⊢ ( 𝐺 ∈ V → ( 𝐸 ‘ 𝐺 ) = ( 𝐸 ‘ 𝑊 ) )
12	2	str0	⊢ ∅ = ( 𝐸 ‘ ∅ )
13	12	eqcomi	⊢ ( 𝐸 ‘ ∅ ) = ∅
14	13 1	fveqprc	⊢ ( ¬ 𝐺 ∈ V → ( 𝐸 ‘ 𝐺 ) = ( 𝐸 ‘ 𝑊 ) )
15	11 14	pm2.61i	⊢ ( 𝐸 ‘ 𝐺 ) = ( 𝐸 ‘ 𝑊 )