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 ‘ 𝑊 ) )