asclmul1

Description: Left multiplication by a lifted scalar is the same as the scalar operation. (Contributed by Mario Carneiro, 9-Mar-2015)

	Ref	Expression
Hypotheses	asclmul1.a	$⊢ A = algSc (W)$
	asclmul1.f	$⊢ F = Scalar (W)$
	asclmul1.k	$⊢ K = {Base}_{F}$
	asclmul1.v	$⊢ V = {Base}_{W}$
	asclmul1.t	$⊢ \underset{˙}{\times} = \cdot_{W}$
	asclmul1.s	$⊢ \underset{˙}{\cdot} = \cdot_{W}$
Assertion	asclmul1	$⊢ (W \in AssAlg \land R \in K \land X \in V) \to A (R) \underset{˙}{\times} X = R \underset{˙}{\cdot} X$

Proof

Step	Hyp	Ref	Expression
1		asclmul1.a	$⊢ A = algSc (W)$
2		asclmul1.f	$⊢ F = Scalar (W)$
3		asclmul1.k	$⊢ K = {Base}_{F}$
4		asclmul1.v	$⊢ V = {Base}_{W}$
5		asclmul1.t	$⊢ \underset{˙}{\times} = \cdot_{W}$
6		asclmul1.s	$⊢ \underset{˙}{\cdot} = \cdot_{W}$
7		eqid	$⊢ 1_{W} = 1_{W}$
8	1 2 3 6 7	asclval	$⊢ R \in K \to A (R) = R \underset{˙}{\cdot} 1_{W}$
9	8	3ad2ant2	$⊢ (W \in AssAlg \land R \in K \land X \in V) \to A (R) = R \underset{˙}{\cdot} 1_{W}$
10	9	oveq1d	$⊢ (W \in AssAlg \land R \in K \land X \in V) \to A (R) \underset{˙}{\times} X = (R \underset{˙}{\cdot} 1_{W}) \underset{˙}{\times} X$
11		simp1	$⊢ (W \in AssAlg \land R \in K \land X \in V) \to W \in AssAlg$
12		simp2	$⊢ (W \in AssAlg \land R \in K \land X \in V) \to R \in K$
13		assaring	$⊢ W \in AssAlg \to W \in Ring$
14	13	3ad2ant1	$⊢ (W \in AssAlg \land R \in K \land X \in V) \to W \in Ring$
15	4 7	ringidcl	$⊢ W \in Ring \to 1_{W} \in V$
16	14 15	syl	$⊢ (W \in AssAlg \land R \in K \land X \in V) \to 1_{W} \in V$
17		simp3	$⊢ (W \in AssAlg \land R \in K \land X \in V) \to X \in V$
18	4 2 3 6 5	assaass	$⊢ (W \in AssAlg \land (R \in K \land 1_{W} \in V \land X \in V)) \to (R \underset{˙}{\cdot} 1_{W}) \underset{˙}{\times} X = R \underset{˙}{\cdot} (1_{W} \underset{˙}{\times} X)$
19	11 12 16 17 18	syl13anc	$⊢ (W \in AssAlg \land R \in K \land X \in V) \to (R \underset{˙}{\cdot} 1_{W}) \underset{˙}{\times} X = R \underset{˙}{\cdot} (1_{W} \underset{˙}{\times} X)$
20	4 5 7	ringlidm	$⊢ (W \in Ring \land X \in V) \to 1_{W} \underset{˙}{\times} X = X$
21	14 17 20	syl2anc	$⊢ (W \in AssAlg \land R \in K \land X \in V) \to 1_{W} \underset{˙}{\times} X = X$
22	21	oveq2d	$⊢ (W \in AssAlg \land R \in K \land X \in V) \to R \underset{˙}{\cdot} (1_{W} \underset{˙}{\times} X) = R \underset{˙}{\cdot} X$
23	10 19 22	3eqtrd	$⊢ (W \in AssAlg \land R \in K \land X \in V) \to A (R) \underset{˙}{\times} X = R \underset{˙}{\cdot} X$

Metamath Proof Explorer

Theorem asclmul1

Proof