rnascl

Description: The set of lifted scalars is also interpretable as the span of the identity. (Contributed by Mario Carneiro, 9-Mar-2015)

Step	Hyp	Ref	Expression
1		rnascl.a	$⊢ A = algSc (W)$
2		rnascl.o	$⊢ \underset{˙}{1} = 1_{W}$
3		rnascl.n	$⊢ N = LSpan (W)$
4		eqid	$⊢ Scalar (W) = Scalar (W)$
5		eqid	$⊢ {Base}_{Scalar (W)} = {Base}_{Scalar (W)}$
6		eqid	$⊢ \cdot_{W} = \cdot_{W}$
7	1 4 5 6 2	asclfval	$⊢ A = (y \in {Base}_{Scalar (W)} ⟼ y \cdot_{W} \underset{˙}{1})$
8	7	rnmpt	$⊢ ran A = \{x \| \exists y \in {Base}_{Scalar (W)} x = y \cdot_{W} \underset{˙}{1}\}$
9		assalmod	$⊢ W \in AssAlg \to W \in LMod$
10		assaring	$⊢ W \in AssAlg \to W \in Ring$
11		eqid	$⊢ {Base}_{W} = {Base}_{W}$
12	11 2	ringidcl	$⊢ W \in Ring \to \underset{˙}{1} \in {Base}_{W}$
13	10 12	syl	$⊢ W \in AssAlg \to \underset{˙}{1} \in {Base}_{W}$
14	4 5 11 6 3	lspsn	$⊢ (W \in LMod \land \underset{˙}{1} \in {Base}_{W}) \to N (\{\underset{˙}{1}\}) = \{x \| \exists y \in {Base}_{Scalar (W)} x = y \cdot_{W} \underset{˙}{1}\}$
15	9 13 14	syl2anc	$⊢ W \in AssAlg \to N (\{\underset{˙}{1}\}) = \{x \| \exists y \in {Base}_{Scalar (W)} x = y \cdot_{W} \underset{˙}{1}\}$
16	8 15	eqtr4id	$⊢ W \in AssAlg \to ran A = N (\{\underset{˙}{1}\})$

Metamath Proof Explorer