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		eqid	$⊢ {Base}_{W} = {Base}_{W}$
11		eqid	$⊢ 1_{W} = 1_{W}$
12		assaring	$⊢ W \in AssAlg \to W \in Ring$
13	12	3ad2ant1	$⊢ (W \in AssAlg \land R \in K \land S \in K) \to W \in Ring$
14	10 11 13	ringidcld	$⊢ (W \in AssAlg \land R \in K \land S \in K) \to 1_{W} \in {Base}_{W}$
15		eqid	$⊢ \cdot_{W} = \cdot_{W}$
16	10 2 15 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})$
17	7 8 9 14 16	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})$
18	2	assasca	$⊢ W \in AssAlg \to F \in Ring$
19	3 5	ringcl	$⊢ (F \in Ring \land R \in K \land S \in K) \to R \underset{˙}{\cdot} S \in K$
20	18 19	syl3an1	$⊢ (W \in AssAlg \land R \in K \land S \in K) \to R \underset{˙}{\cdot} S \in K$
21	1 2 3 15 11	asclval	$⊢ R \underset{˙}{\cdot} S \in K \to A (R \underset{˙}{\cdot} S) = (R \underset{˙}{\cdot} S) \cdot_{W} 1_{W}$
22	20 21	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}$
23	1 2 12 6 3 10	asclf	$⊢ W \in AssAlg \to A : K ⟶ {Base}_{W}$
24	23	ffvelcdmda	$⊢ (W \in AssAlg \land S \in K) \to A (S) \in {Base}_{W}$
25	24	3adant2	$⊢ (W \in AssAlg \land R \in K \land S \in K) \to A (S) \in {Base}_{W}$
26	1 2 3 10 4 15	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)$
27	25 26	syld3an3	$⊢ (W \in AssAlg \land R \in K \land S \in K) \to A (R) \underset{˙}{\times} A (S) = R \cdot_{W} A (S)$
28	1 2 3 15 11	asclval	$⊢ S \in K \to A (S) = S \cdot_{W} 1_{W}$
29	28	3ad2ant3	$⊢ (W \in AssAlg \land R \in K \land S \in K) \to A (S) = S \cdot_{W} 1_{W}$
30	29	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})$
31	27 30	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})$
32	17 22 31	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