asclmul2

Description: Right 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	asclmul2	$⊢ (W \in AssAlg \land R \in K \land X \in V) \to X \underset{˙}{\times} A (R) = 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	oveq2d	$⊢ (W \in AssAlg \land R \in K \land X \in V) \to X \underset{˙}{\times} A (R) = X \underset{˙}{\times} (R \underset{˙}{\cdot} 1_{W})$
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		simp3	$⊢ (W \in AssAlg \land R \in K \land X \in V) \to X \in V$
14		assaring	$⊢ W \in AssAlg \to W \in Ring$
15	14	3ad2ant1	$⊢ (W \in AssAlg \land R \in K \land X \in V) \to W \in Ring$
16	4 7	ringidcl	$⊢ W \in Ring \to 1_{W} \in V$
17	15 16	syl	$⊢ (W \in AssAlg \land R \in K \land X \in V) \to 1_{W} \in V$
18	4 2 3 6 5	assaassr	$⊢ (W \in AssAlg \land (R \in K \land X \in V \land 1_{W} \in V)) \to X \underset{˙}{\times} (R \underset{˙}{\cdot} 1_{W}) = R \underset{˙}{\cdot} (X \underset{˙}{\times} 1_{W})$
19	11 12 13 17 18	syl13anc	$⊢ (W \in AssAlg \land R \in K \land X \in V) \to X \underset{˙}{\times} (R \underset{˙}{\cdot} 1_{W}) = R \underset{˙}{\cdot} (X \underset{˙}{\times} 1_{W})$
20	4 5 7	ringridm	$⊢ (W \in Ring \land X \in V) \to X \underset{˙}{\times} 1_{W} = X$
21	15 13 20	syl2anc	$⊢ (W \in AssAlg \land R \in K \land X \in V) \to X \underset{˙}{\times} 1_{W} = X$
22	21	oveq2d	$⊢ (W \in AssAlg \land R \in K \land X \in V) \to R \underset{˙}{\cdot} (X \underset{˙}{\times} 1_{W}) = R \underset{˙}{\cdot} X$
23	10 19 22	3eqtrd	$⊢ (W \in AssAlg \land R \in K \land X \in V) \to X \underset{˙}{\times} A (R) = R \underset{˙}{\cdot} X$

Metamath Proof Explorer

Theorem asclmul2

Proof