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

Metamath Proof Explorer

Theorem ascl1

Description: The scalar 1 embedded into a left module corresponds to the 1 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 ascl1 ( 𝜑 → ( 𝐴 ‘ ( 1r ‘ 𝐹 ) ) = ( 1r ‘ 𝑊 ) )

Proof

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