Theorem assaascl1

Description: The scalar 1 embedded into an associative algebra corresponds to the 1 of the an associative algebra. (Contributed by AV, 31-Jul-2019)

	Ref	Expression
Hypotheses	assaascl0.a	⊢ 𝐴 = ( algSc ‘ 𝑊 )
	assaascl0.f	⊢ 𝐹 = ( Scalar ‘ 𝑊 )
	assaascl0.w	⊢ ( 𝜑 → 𝑊 ∈ AssAlg )
Assertion	assaascl1	⊢ ( 𝜑 → ( 𝐴 ‘ ( 1r ‘ 𝐹 ) ) = ( 1r ‘ 𝑊 ) )

Proof

Step	Hyp	Ref	Expression
1		assaascl0.a	⊢ 𝐴 = ( algSc ‘ 𝑊 )
2		assaascl0.f	⊢ 𝐹 = ( Scalar ‘ 𝑊 )
3		assaascl0.w	⊢ ( 𝜑 → 𝑊 ∈ AssAlg )
4		assalmod	⊢ ( 𝑊 ∈ AssAlg → 𝑊 ∈ LMod )
5	3 4	syl	⊢ ( 𝜑 → 𝑊 ∈ LMod )
6		assaring	⊢ ( 𝑊 ∈ AssAlg → 𝑊 ∈ Ring )
7	3 6	syl	⊢ ( 𝜑 → 𝑊 ∈ Ring )
8	1 2 5 7	ascl1	⊢ ( 𝜑 → ( 𝐴 ‘ ( 1r ‘ 𝐹 ) ) = ( 1r ‘ 𝑊 ) )