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

Metamath Proof Explorer

Theorem ascl0

Description: The scalar 0 embedded into a left module corresponds to the 0 of the left module if the left module is also a ring. (Contributed by AV, 31-Jul-2019)

Ref Expression
Hypotheses ascl0.a ⊢ 𝐴 = ( algSc ‘ 𝑊 )
ascl0.f ⊢ 𝐹 = ( Scalar ‘ 𝑊 )
ascl0.l ⊢ ( 𝜑 → 𝑊 ∈ LMod )
ascl0.r ⊢ ( 𝜑 → 𝑊 ∈ Ring )
Assertion ascl0 ( 𝜑 → ( 𝐴 ‘ ( 0g ‘ 𝐹 ) ) = ( 0g ‘ 𝑊 ) )

Proof

Step Hyp Ref Expression
1 ascl0.a ⊢ 𝐴 = ( algSc ‘ 𝑊 )
2 ascl0.f ⊢ 𝐹 = ( Scalar ‘ 𝑊 )
3 ascl0.l ⊢ ( 𝜑 → 𝑊 ∈ LMod )
4 ascl0.r ⊢ ( 𝜑 → 𝑊 ∈ Ring )
5 2 lmodfgrp ⊢ ( 𝑊 ∈ LMod → 𝐹 ∈ Grp )
6 eqid ⊢ ( Base ‘ 𝐹 ) = ( Base ‘ 𝐹 )
7 eqid ⊢ ( 0g ‘ 𝐹 ) = ( 0g ‘ 𝐹 )
8 6 7 grpidcl ⊢ ( 𝐹 ∈ Grp → ( 0g ‘ 𝐹 ) ∈ ( Base ‘ 𝐹 ) )
9 eqid ⊢ ( ·𝑠 ‘ 𝑊 ) = ( ·𝑠 ‘ 𝑊 )
10 eqid ⊢ ( 1r ‘ 𝑊 ) = ( 1r ‘ 𝑊 )
11 1 2 6 9 10 asclval ⊢ ( ( 0g ‘ 𝐹 ) ∈ ( Base ‘ 𝐹 ) → ( 𝐴 ‘ ( 0g ‘ 𝐹 ) ) = ( ( 0g ‘ 𝐹 ) ( ·𝑠 ‘ 𝑊 ) ( 1r ‘ 𝑊 ) ) )
12 3 5 8 11 4syl ⊢ ( 𝜑 → ( 𝐴 ‘ ( 0g ‘ 𝐹 ) ) = ( ( 0g ‘ 𝐹 ) ( ·𝑠 ‘ 𝑊 ) ( 1r ‘ 𝑊 ) ) )
13 eqid ⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
14 13 10 ringidcl ⊢ ( 𝑊 ∈ Ring → ( 1r ‘ 𝑊 ) ∈ ( Base ‘ 𝑊 ) )
15 4 14 syl ⊢ ( 𝜑 → ( 1r ‘ 𝑊 ) ∈ ( Base ‘ 𝑊 ) )
16 eqid ⊢ ( 0g ‘ 𝑊 ) = ( 0g ‘ 𝑊 )
17 13 2 9 7 16 lmod0vs ⊢ ( ( 𝑊 ∈ LMod ∧ ( 1r ‘ 𝑊 ) ∈ ( Base ‘ 𝑊 ) ) → ( ( 0g ‘ 𝐹 ) ( ·𝑠 ‘ 𝑊 ) ( 1r ‘ 𝑊 ) ) = ( 0g ‘ 𝑊 ) )
18 3 15 17 syl2anc ⊢ ( 𝜑 → ( ( 0g ‘ 𝐹 ) ( ·𝑠 ‘ 𝑊 ) ( 1r ‘ 𝑊 ) ) = ( 0g ‘ 𝑊 ) )
19 12 18 eqtrd ⊢ ( 𝜑 → ( 𝐴 ‘ ( 0g ‘ 𝐹 ) ) = ( 0g ‘ 𝑊 ) )