This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( 𝐸 ‘ 𝐺 ) = ( 𝐸 ‘ 𝑊 )