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	3 5	syl	⊢ ( 𝜑 → 𝐹 ∈ Grp )
7		eqid	⊢ ( Base ‘ 𝐹 ) = ( Base ‘ 𝐹 )
8		eqid	⊢ ( 0g ‘ 𝐹 ) = ( 0g ‘ 𝐹 )
9	7 8	grpidcl	⊢ ( 𝐹 ∈ Grp → ( 0g ‘ 𝐹 ) ∈ ( Base ‘ 𝐹 ) )
10	6 9	syl	⊢ ( 𝜑 → ( 0g ‘ 𝐹 ) ∈ ( Base ‘ 𝐹 ) )
11		eqid	⊢ ( ·𝑠 ‘ 𝑊 ) = ( ·𝑠 ‘ 𝑊 )
12		eqid	⊢ ( 1r ‘ 𝑊 ) = ( 1r ‘ 𝑊 )
13	1 2 7 11 12	asclval	⊢ ( ( 0g ‘ 𝐹 ) ∈ ( Base ‘ 𝐹 ) → ( 𝐴 ‘ ( 0g ‘ 𝐹 ) ) = ( ( 0g ‘ 𝐹 ) ( ·𝑠 ‘ 𝑊 ) ( 1r ‘ 𝑊 ) ) )
14	10 13	syl	⊢ ( 𝜑 → ( 𝐴 ‘ ( 0g ‘ 𝐹 ) ) = ( ( 0g ‘ 𝐹 ) ( ·𝑠 ‘ 𝑊 ) ( 1r ‘ 𝑊 ) ) )
15		eqid	⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
16	15 12	ringidcl	⊢ ( 𝑊 ∈ Ring → ( 1r ‘ 𝑊 ) ∈ ( Base ‘ 𝑊 ) )
17	4 16	syl	⊢ ( 𝜑 → ( 1r ‘ 𝑊 ) ∈ ( Base ‘ 𝑊 ) )
18		eqid	⊢ ( 0g ‘ 𝑊 ) = ( 0g ‘ 𝑊 )
19	15 2 11 8 18	lmod0vs	⊢ ( ( 𝑊 ∈ LMod ∧ ( 1r ‘ 𝑊 ) ∈ ( Base ‘ 𝑊 ) ) → ( ( 0g ‘ 𝐹 ) ( ·𝑠 ‘ 𝑊 ) ( 1r ‘ 𝑊 ) ) = ( 0g ‘ 𝑊 ) )
20	3 17 19	syl2anc	⊢ ( 𝜑 → ( ( 0g ‘ 𝐹 ) ( ·𝑠 ‘ 𝑊 ) ( 1r ‘ 𝑊 ) ) = ( 0g ‘ 𝑊 ) )
21	14 20	eqtrd	⊢ ( 𝜑 → ( 𝐴 ‘ ( 0g ‘ 𝐹 ) ) = ( 0g ‘ 𝑊 ) )