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