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