assamulgscmlem1

Description: Lemma 1 for assamulgscm (induction base). (Contributed by AV, 26-Aug-2019)

	Ref	Expression
Hypotheses	assamulgscm.v	$⊢ V = {Base}_{W}$
	assamulgscm.f	$⊢ F = Scalar (W)$
	assamulgscm.b	$⊢ B = {Base}_{F}$
	assamulgscm.s	$⊢ \underset{˙}{\cdot} = \cdot_{W}$
	assamulgscm.g	$⊢ G = {mulGrp}_{F}$
	assamulgscm.p	$⊢ \underset{˙}{\times} = \cdot_{G}$
	assamulgscm.h	$⊢ H = {mulGrp}_{W}$
	assamulgscm.e	$⊢ E = \cdot_{H}$
Assertion	assamulgscmlem1	$⊢ ((A \in B \land X \in V) \land W \in AssAlg) \to 0 E (A \underset{˙}{\cdot} X) = (0 \underset{˙}{\times} A) \underset{˙}{\cdot} (0 E X)$

Proof

Step	Hyp	Ref	Expression
1		assamulgscm.v	$⊢ V = {Base}_{W}$
2		assamulgscm.f	$⊢ F = Scalar (W)$
3		assamulgscm.b	$⊢ B = {Base}_{F}$
4		assamulgscm.s	$⊢ \underset{˙}{\cdot} = \cdot_{W}$
5		assamulgscm.g	$⊢ G = {mulGrp}_{F}$
6		assamulgscm.p	$⊢ \underset{˙}{\times} = \cdot_{G}$
7		assamulgscm.h	$⊢ H = {mulGrp}_{W}$
8		assamulgscm.e	$⊢ E = \cdot_{H}$
9		assalmod	$⊢ W \in AssAlg \to W \in LMod$
10		assaring	$⊢ W \in AssAlg \to W \in Ring$
11		eqid	$⊢ 1_{W} = 1_{W}$
12	1 11	ringidcl	$⊢ W \in Ring \to 1_{W} \in V$
13	10 12	syl	$⊢ W \in AssAlg \to 1_{W} \in V$
14		eqid	$⊢ 1_{F} = 1_{F}$
15	1 2 4 14	lmodvs1	$⊢ (W \in LMod \land 1_{W} \in V) \to 1_{F} \underset{˙}{\cdot} 1_{W} = 1_{W}$
16	15	eqcomd	$⊢ (W \in LMod \land 1_{W} \in V) \to 1_{W} = 1_{F} \underset{˙}{\cdot} 1_{W}$
17	9 13 16	syl2anc	$⊢ W \in AssAlg \to 1_{W} = 1_{F} \underset{˙}{\cdot} 1_{W}$
18	17	adantl	$⊢ ((A \in B \land X \in V) \land W \in AssAlg) \to 1_{W} = 1_{F} \underset{˙}{\cdot} 1_{W}$
19	9	adantl	$⊢ ((A \in B \land X \in V) \land W \in AssAlg) \to W \in LMod$
20		simpll	$⊢ ((A \in B \land X \in V) \land W \in AssAlg) \to A \in B$
21		simplr	$⊢ ((A \in B \land X \in V) \land W \in AssAlg) \to X \in V$
22	1 2 4 3	lmodvscl	$⊢ (W \in LMod \land A \in B \land X \in V) \to A \underset{˙}{\cdot} X \in V$
23	19 20 21 22	syl3anc	$⊢ ((A \in B \land X \in V) \land W \in AssAlg) \to A \underset{˙}{\cdot} X \in V$
24	7 1	mgpbas	$⊢ V = {Base}_{H}$
25	7 11	ringidval	$⊢ 1_{W} = 0_{H}$
26	24 25 8	mulg0	$⊢ A \underset{˙}{\cdot} X \in V \to 0 E (A \underset{˙}{\cdot} X) = 1_{W}$
27	23 26	syl	$⊢ ((A \in B \land X \in V) \land W \in AssAlg) \to 0 E (A \underset{˙}{\cdot} X) = 1_{W}$
28	5 3	mgpbas	$⊢ B = {Base}_{G}$
29	5 14	ringidval	$⊢ 1_{F} = 0_{G}$
30	28 29 6	mulg0	$⊢ A \in B \to 0 \underset{˙}{\times} A = 1_{F}$
31	20 30	syl	$⊢ ((A \in B \land X \in V) \land W \in AssAlg) \to 0 \underset{˙}{\times} A = 1_{F}$
32	24 25 8	mulg0	$⊢ X \in V \to 0 E X = 1_{W}$
33	21 32	syl	$⊢ ((A \in B \land X \in V) \land W \in AssAlg) \to 0 E X = 1_{W}$
34	31 33	oveq12d	$⊢ ((A \in B \land X \in V) \land W \in AssAlg) \to (0 \underset{˙}{\times} A) \underset{˙}{\cdot} (0 E X) = 1_{F} \underset{˙}{\cdot} 1_{W}$
35	18 27 34	3eqtr4d	$⊢ ((A \in B \land X \in V) \land W \in AssAlg) \to 0 E (A \underset{˙}{\cdot} X) = (0 \underset{˙}{\times} A) \underset{˙}{\cdot} (0 E X)$

Metamath Proof Explorer

Theorem assamulgscmlem1

Proof