ascldimul

Description: The algebra scalar lifting function distributes over multiplication. (Contributed by Mario Carneiro, 8-Mar-2015) (Proof shortened by SN, 5-Nov-2023)

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

Proof

Step	Hyp	Ref	Expression
1		ascldimul.a	$⊢ A = algSc (W)$
2		ascldimul.f	$⊢ F = Scalar (W)$
3		ascldimul.k	$⊢ K = {Base}_{F}$
4		ascldimul.t	$⊢ \underset{˙}{\times} = \cdot_{W}$
5		ascldimul.s	$⊢ \underset{˙}{\cdot} = \cdot_{F}$
6		assalmod	$⊢ W \in AssAlg \to W \in LMod$
7	6	3ad2ant1	$⊢ (W \in AssAlg \land R \in K \land S \in K) \to W \in LMod$
8		simp2	$⊢ (W \in AssAlg \land R \in K \land S \in K) \to R \in K$
9		simp3	$⊢ (W \in AssAlg \land R \in K \land S \in K) \to S \in K$
10		assaring	$⊢ W \in AssAlg \to W \in Ring$
11	10	3ad2ant1	$⊢ (W \in AssAlg \land R \in K \land S \in K) \to W \in Ring$
12		eqid	$⊢ {Base}_{W} = {Base}_{W}$
13		eqid	$⊢ 1_{W} = 1_{W}$
14	12 13	ringidcl	$⊢ W \in Ring \to 1_{W} \in {Base}_{W}$
15	11 14	syl	$⊢ (W \in AssAlg \land R \in K \land S \in K) \to 1_{W} \in {Base}_{W}$
16		eqid	$⊢ \cdot_{W} = \cdot_{W}$
17	12 2 16 3 5	lmodvsass	$⊢ (W \in LMod \land (R \in K \land S \in K \land 1_{W} \in {Base}_{W})) \to (R \underset{˙}{\cdot} S) \cdot_{W} 1_{W} = R \cdot_{W} (S \cdot_{W} 1_{W})$
18	7 8 9 15 17	syl13anc	$⊢ (W \in AssAlg \land R \in K \land S \in K) \to (R \underset{˙}{\cdot} S) \cdot_{W} 1_{W} = R \cdot_{W} (S \cdot_{W} 1_{W})$
19	2	lmodring	$⊢ W \in LMod \to F \in Ring$
20	6 19	syl	$⊢ W \in AssAlg \to F \in Ring$
21	3 5	ringcl	$⊢ (F \in Ring \land R \in K \land S \in K) \to R \underset{˙}{\cdot} S \in K$
22	20 21	syl3an1	$⊢ (W \in AssAlg \land R \in K \land S \in K) \to R \underset{˙}{\cdot} S \in K$
23	1 2 3 16 13	asclval	$⊢ R \underset{˙}{\cdot} S \in K \to A (R \underset{˙}{\cdot} S) = (R \underset{˙}{\cdot} S) \cdot_{W} 1_{W}$
24	22 23	syl	$⊢ (W \in AssAlg \land R \in K \land S \in K) \to A (R \underset{˙}{\cdot} S) = (R \underset{˙}{\cdot} S) \cdot_{W} 1_{W}$
25	1 2 10 6 3 12	asclf	$⊢ W \in AssAlg \to A : K ⟶ {Base}_{W}$
26	25	ffvelcdmda	$⊢ (W \in AssAlg \land S \in K) \to A (S) \in {Base}_{W}$
27	26	3adant2	$⊢ (W \in AssAlg \land R \in K \land S \in K) \to A (S) \in {Base}_{W}$
28	1 2 3 12 4 16	asclmul1	$⊢ (W \in AssAlg \land R \in K \land A (S) \in {Base}_{W}) \to A (R) \underset{˙}{\times} A (S) = R \cdot_{W} A (S)$
29	27 28	syld3an3	$⊢ (W \in AssAlg \land R \in K \land S \in K) \to A (R) \underset{˙}{\times} A (S) = R \cdot_{W} A (S)$
30	1 2 3 16 13	asclval	$⊢ S \in K \to A (S) = S \cdot_{W} 1_{W}$
31	30	3ad2ant3	$⊢ (W \in AssAlg \land R \in K \land S \in K) \to A (S) = S \cdot_{W} 1_{W}$
32	31	oveq2d	$⊢ (W \in AssAlg \land R \in K \land S \in K) \to R \cdot_{W} A (S) = R \cdot_{W} (S \cdot_{W} 1_{W})$
33	29 32	eqtrd	$⊢ (W \in AssAlg \land R \in K \land S \in K) \to A (R) \underset{˙}{\times} A (S) = R \cdot_{W} (S \cdot_{W} 1_{W})$
34	18 24 33	3eqtr4d	$⊢ (W \in AssAlg \land R \in K \land S \in K) \to A (R \underset{˙}{\cdot} S) = A (R) \underset{˙}{\times} A (S)$

Metamath Proof Explorer

Theorem ascldimul

Proof