ascldimulOLD

Description: Obsolete version of ascldimul as of 5-Nov-2023. (Contributed by Mario Carneiro, 8-Mar-2015) (Proof modification is discouraged.) (New usage is discouraged.)

	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	ascldimulOLD	$⊢ (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		assaring	$⊢ W \in AssAlg \to W \in Ring$
7		eqid	$⊢ {Base}_{W} = {Base}_{W}$
8		eqid	$⊢ 1_{W} = 1_{W}$
9	7 8	ringidcl	$⊢ W \in Ring \to 1_{W} \in {Base}_{W}$
10	6 9	syl	$⊢ W \in AssAlg \to 1_{W} \in {Base}_{W}$
11	7 4 8	ringlidm	$⊢ (W \in Ring \land 1_{W} \in {Base}_{W}) \to 1_{W} \underset{˙}{\times} 1_{W} = 1_{W}$
12	6 10 11	syl2anc	$⊢ W \in AssAlg \to 1_{W} \underset{˙}{\times} 1_{W} = 1_{W}$
13	12	oveq2d	$⊢ W \in AssAlg \to S \cdot_{W} (1_{W} \underset{˙}{\times} 1_{W}) = S \cdot_{W} 1_{W}$
14	13	oveq2d	$⊢ W \in AssAlg \to R \cdot_{W} (S \cdot_{W} (1_{W} \underset{˙}{\times} 1_{W})) = R \cdot_{W} (S \cdot_{W} 1_{W})$
15	14	3ad2ant1	$⊢ (W \in AssAlg \land R \in K \land S \in K) \to R \cdot_{W} (S \cdot_{W} (1_{W} \underset{˙}{\times} 1_{W})) = R \cdot_{W} (S \cdot_{W} 1_{W})$
16		simp1	$⊢ (W \in AssAlg \land R \in K \land S \in K) \to W \in AssAlg$
17		simp2	$⊢ (W \in AssAlg \land R \in K \land S \in K) \to R \in K$
18	10	3ad2ant1	$⊢ (W \in AssAlg \land R \in K \land S \in K) \to 1_{W} \in {Base}_{W}$
19		assalmod	$⊢ W \in AssAlg \to W \in LMod$
20	19	3ad2ant1	$⊢ (W \in AssAlg \land R \in K \land S \in K) \to W \in LMod$
21		simp3	$⊢ (W \in AssAlg \land R \in K \land S \in K) \to S \in K$
22		eqid	$⊢ \cdot_{W} = \cdot_{W}$
23	7 2 22 3	lmodvscl	$⊢ (W \in LMod \land S \in K \land 1_{W} \in {Base}_{W}) \to S \cdot_{W} 1_{W} \in {Base}_{W}$
24	20 21 18 23	syl3anc	$⊢ (W \in AssAlg \land R \in K \land S \in K) \to S \cdot_{W} 1_{W} \in {Base}_{W}$
25	7 2 3 22 4	assaass	$⊢ (W \in AssAlg \land (R \in K \land 1_{W} \in {Base}_{W} \land S \cdot_{W} 1_{W} \in {Base}_{W})) \to (R \cdot_{W} 1_{W}) \underset{˙}{\times} (S \cdot_{W} 1_{W}) = R \cdot_{W} (1_{W} \underset{˙}{\times} (S \cdot_{W} 1_{W}))$
26	16 17 18 24 25	syl13anc	$⊢ (W \in AssAlg \land R \in K \land S \in K) \to (R \cdot_{W} 1_{W}) \underset{˙}{\times} (S \cdot_{W} 1_{W}) = R \cdot_{W} (1_{W} \underset{˙}{\times} (S \cdot_{W} 1_{W}))$
27	7 2 3 22 4	assaassr	$⊢ (W \in AssAlg \land (S \in K \land 1_{W} \in {Base}_{W} \land 1_{W} \in {Base}_{W})) \to 1_{W} \underset{˙}{\times} (S \cdot_{W} 1_{W}) = S \cdot_{W} (1_{W} \underset{˙}{\times} 1_{W})$
28	16 21 18 18 27	syl13anc	$⊢ (W \in AssAlg \land R \in K \land S \in K) \to 1_{W} \underset{˙}{\times} (S \cdot_{W} 1_{W}) = S \cdot_{W} (1_{W} \underset{˙}{\times} 1_{W})$
29	28	oveq2d	$⊢ (W \in AssAlg \land R \in K \land S \in K) \to R \cdot_{W} (1_{W} \underset{˙}{\times} (S \cdot_{W} 1_{W})) = R \cdot_{W} (S \cdot_{W} (1_{W} \underset{˙}{\times} 1_{W}))$
30	26 29	eqtrd	$⊢ (W \in AssAlg \land R \in K \land S \in K) \to (R \cdot_{W} 1_{W}) \underset{˙}{\times} (S \cdot_{W} 1_{W}) = R \cdot_{W} (S \cdot_{W} (1_{W} \underset{˙}{\times} 1_{W}))$
31	7 2 22 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})$
32	20 17 21 18 31	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})$
33	15 30 32	3eqtr4rd	$⊢ (W \in AssAlg \land R \in K \land S \in K) \to (R \underset{˙}{\cdot} S) \cdot_{W} 1_{W} = (R \cdot_{W} 1_{W}) \underset{˙}{\times} (S \cdot_{W} 1_{W})$
34	2	assasca	$⊢ W \in AssAlg \to F \in CRing$
35		crngring	$⊢ F \in CRing \to F \in Ring$
36	34 35	syl	$⊢ W \in AssAlg \to F \in Ring$
37	3 5	ringcl	$⊢ (F \in Ring \land R \in K \land S \in K) \to R \underset{˙}{\cdot} S \in K$
38	36 37	syl3an1	$⊢ (W \in AssAlg \land R \in K \land S \in K) \to R \underset{˙}{\cdot} S \in K$
39	1 2 3 22 8	asclval	$⊢ R \underset{˙}{\cdot} S \in K \to A (R \underset{˙}{\cdot} S) = (R \underset{˙}{\cdot} S) \cdot_{W} 1_{W}$
40	38 39	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}$
41	1 2 3 22 8	asclval	$⊢ R \in K \to A (R) = R \cdot_{W} 1_{W}$
42	17 41	syl	$⊢ (W \in AssAlg \land R \in K \land S \in K) \to A (R) = R \cdot_{W} 1_{W}$
43	1 2 3 22 8	asclval	$⊢ S \in K \to A (S) = S \cdot_{W} 1_{W}$
44	21 43	syl	$⊢ (W \in AssAlg \land R \in K \land S \in K) \to A (S) = S \cdot_{W} 1_{W}$
45	42 44	oveq12d	$⊢ (W \in AssAlg \land R \in K \land S \in K) \to A (R) \underset{˙}{\times} A (S) = (R \cdot_{W} 1_{W}) \underset{˙}{\times} (S \cdot_{W} 1_{W})$
46	33 40 45	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 ascldimulOLD

Proof