This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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	$⊢ A = algSc (W)$
		ascl0.f	$⊢ F = Scalar (W)$
		ascl0.l	$⊢ φ \to W \in LMod$
		ascl0.r	$⊢ φ \to W \in Ring$
	Assertion	ascl1	$⊢ φ \to A (1_{F}) = 1_{W}$

Proof

Step	Hyp	Ref	Expression
1		ascl0.a	$⊢ A = algSc (W)$
2		ascl0.f	$⊢ F = Scalar (W)$
3		ascl0.l	$⊢ φ \to W \in LMod$
4		ascl0.r	$⊢ φ \to W \in Ring$
5	2	lmodring	$⊢ W \in LMod \to F \in Ring$
6		eqid	$⊢ {Base}_{F} = {Base}_{F}$
7		eqid	$⊢ 1_{F} = 1_{F}$
8	6 7	ringidcl	$⊢ F \in Ring \to 1_{F} \in {Base}_{F}$
9		eqid	$⊢ \cdot_{W} = \cdot_{W}$
10		eqid	$⊢ 1_{W} = 1_{W}$
11	1 2 6 9 10	asclval	$⊢ 1_{F} \in {Base}_{F} \to A (1_{F}) = 1_{F} \cdot_{W} 1_{W}$
12	3 5 8 11	4syl	$⊢ φ \to A (1_{F}) = 1_{F} \cdot_{W} 1_{W}$
13		eqid	$⊢ {Base}_{W} = {Base}_{W}$
14	13 10	ringidcl	$⊢ W \in Ring \to 1_{W} \in {Base}_{W}$
15	4 14	syl	$⊢ φ \to 1_{W} \in {Base}_{W}$
16	13 2 9 7	lmodvs1	$⊢ (W \in LMod \land 1_{W} \in {Base}_{W}) \to 1_{F} \cdot_{W} 1_{W} = 1_{W}$
17	3 15 16	syl2anc	$⊢ φ \to 1_{F} \cdot_{W} 1_{W} = 1_{W}$
18	12 17	eqtrd	$⊢ φ \to A (1_{F}) = 1_{W}$