Metamath Proof Explorer

Theorem zlmvsca

Description: Scalar multiplication operation of a ZZ -module. (Contributed by Mario Carneiro, 2-Oct-2015)

Ref Expression
Hypotheses zlmbas.w ⊢ 𝑊 = ( ℤMod ‘ 𝐺 )
zlmvsca.2 ⊢ · = ( .g ‘ 𝐺 )
Assertion zlmvsca · = ( ·𝑠 ‘ 𝑊 )

Proof

Step Hyp Ref Expression
1 zlmbas.w ⊢ 𝑊 = ( ℤMod ‘ 𝐺 )
2 zlmvsca.2 ⊢ · = ( .g ‘ 𝐺 )
3 ovex ⊢ ( 𝐺 sSet ⟨ ( Scalar ‘ ndx ) , ℤring ⟩ ) ∈ V
4 2 fvexi ⊢ · ∈ V
5 vscaid ⊢ ·𝑠 = Slot ( ·𝑠 ‘ ndx )
6 5 setsid ⊢ ( ( ( 𝐺 sSet ⟨ ( Scalar ‘ ndx ) , ℤring ⟩ ) ∈ V ∧ · ∈ V ) → · = ( ·𝑠 ‘ ( ( 𝐺 sSet ⟨ ( Scalar ‘ ndx ) , ℤring ⟩ ) sSet ⟨ ( ·𝑠 ‘ ndx ) , · ⟩ ) ) )
7 3 4 6 mp2an ⊢ · = ( ·𝑠 ‘ ( ( 𝐺 sSet ⟨ ( Scalar ‘ ndx ) , ℤring ⟩ ) sSet ⟨ ( ·𝑠 ‘ ndx ) , · ⟩ ) )
8 1 2 zlmval ⊢ ( 𝐺 ∈ V → 𝑊 = ( ( 𝐺 sSet ⟨ ( Scalar ‘ ndx ) , ℤring ⟩ ) sSet ⟨ ( ·𝑠 ‘ ndx ) , · ⟩ ) )
9 8 fveq2d ⊢ ( 𝐺 ∈ V → ( ·𝑠 ‘ 𝑊 ) = ( ·𝑠 ‘ ( ( 𝐺 sSet ⟨ ( Scalar ‘ ndx ) , ℤring ⟩ ) sSet ⟨ ( ·𝑠 ‘ ndx ) , · ⟩ ) ) )
10 7 9 eqtr4id ⊢ ( 𝐺 ∈ V → · = ( ·𝑠 ‘ 𝑊 ) )
11 5 str0 ⊢ ∅ = ( ·𝑠 ‘ ∅ )
12 fvprc ⊢ ( ¬ 𝐺 ∈ V → ( .g ‘ 𝐺 ) = ∅ )
13 2 12 syl5eq ⊢ ( ¬ 𝐺 ∈ V → · = ∅ )
14 fvprc ⊢ ( ¬ 𝐺 ∈ V → ( ℤMod ‘ 𝐺 ) = ∅ )
15 1 14 syl5eq ⊢ ( ¬ 𝐺 ∈ V → 𝑊 = ∅ )
16 15 fveq2d ⊢ ( ¬ 𝐺 ∈ V → ( ·𝑠 ‘ 𝑊 ) = ( ·𝑠 ‘ ∅ ) )
17 11 13 16 3eqtr4a ⊢ ( ¬ 𝐺 ∈ V → · = ( ·𝑠 ‘ 𝑊 ) )
18 10 17 pm2.61i ⊢ · = ( ·𝑠 ‘ 𝑊 )