assamulgscmlem2

Description: Lemma for assamulgscm (induction step). (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	assamulgscmlem2	$⊢ y \in ℕ_{0} \to (((A \in B \land X \in V) \land W \in AssAlg) \to (y E (A \underset{˙}{\cdot} X) = (y \underset{˙}{\times} A) \underset{˙}{\cdot} (y E X) \to (y + 1) E (A \underset{˙}{\cdot} X) = ((y + 1) \underset{˙}{\times} A) \underset{˙}{\cdot} ((y + 1) 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		assaring	$⊢ W \in AssAlg \to W \in Ring$
10	7	ringmgp	$⊢ W \in Ring \to H \in Mnd$
11	9 10	syl	$⊢ W \in AssAlg \to H \in Mnd$
12	11	adantl	$⊢ ((A \in B \land X \in V) \land W \in AssAlg) \to H \in Mnd$
13	12	adantl	$⊢ (y \in ℕ_{0} \land ((A \in B \land X \in V) \land W \in AssAlg)) \to H \in Mnd$
14	13	adantr	$⊢ ((y \in ℕ_{0} \land ((A \in B \land X \in V) \land W \in AssAlg)) \land y E (A \underset{˙}{\cdot} X) = (y \underset{˙}{\times} A) \underset{˙}{\cdot} (y E X)) \to H \in Mnd$
15		simpll	$⊢ ((y \in ℕ_{0} \land ((A \in B \land X \in V) \land W \in AssAlg)) \land y E (A \underset{˙}{\cdot} X) = (y \underset{˙}{\times} A) \underset{˙}{\cdot} (y E X)) \to y \in ℕ_{0}$
16		assalmod	$⊢ W \in AssAlg \to W \in LMod$
17	16	adantl	$⊢ ((A \in B \land X \in V) \land W \in AssAlg) \to W \in LMod$
18		simpll	$⊢ ((A \in B \land X \in V) \land W \in AssAlg) \to A \in B$
19		simplr	$⊢ ((A \in B \land X \in V) \land W \in AssAlg) \to X \in V$
20	1 2 4 3	lmodvscl	$⊢ (W \in LMod \land A \in B \land X \in V) \to A \underset{˙}{\cdot} X \in V$
21	17 18 19 20	syl3anc	$⊢ ((A \in B \land X \in V) \land W \in AssAlg) \to A \underset{˙}{\cdot} X \in V$
22	21	adantl	$⊢ (y \in ℕ_{0} \land ((A \in B \land X \in V) \land W \in AssAlg)) \to A \underset{˙}{\cdot} X \in V$
23	22	adantr	$⊢ ((y \in ℕ_{0} \land ((A \in B \land X \in V) \land W \in AssAlg)) \land y E (A \underset{˙}{\cdot} X) = (y \underset{˙}{\times} A) \underset{˙}{\cdot} (y E X)) \to A \underset{˙}{\cdot} X \in V$
24	7 1	mgpbas	$⊢ V = {Base}_{H}$
25		eqid	$⊢ \cdot_{W} = \cdot_{W}$
26	7 25	mgpplusg	$⊢ \cdot_{W} = +_{H}$
27	24 8 26	mulgnn0p1	$⊢ (H \in Mnd \land y \in ℕ_{0} \land A \underset{˙}{\cdot} X \in V) \to (y + 1) E (A \underset{˙}{\cdot} X) = (y E (A \underset{˙}{\cdot} X)) \cdot_{W} (A \underset{˙}{\cdot} X)$
28	14 15 23 27	syl3anc	$⊢ ((y \in ℕ_{0} \land ((A \in B \land X \in V) \land W \in AssAlg)) \land y E (A \underset{˙}{\cdot} X) = (y \underset{˙}{\times} A) \underset{˙}{\cdot} (y E X)) \to (y + 1) E (A \underset{˙}{\cdot} X) = (y E (A \underset{˙}{\cdot} X)) \cdot_{W} (A \underset{˙}{\cdot} X)$
29		oveq1	$⊢ y E (A \underset{˙}{\cdot} X) = (y \underset{˙}{\times} A) \underset{˙}{\cdot} (y E X) \to (y E (A \underset{˙}{\cdot} X)) \cdot_{W} (A \underset{˙}{\cdot} X) = ((y \underset{˙}{\times} A) \underset{˙}{\cdot} (y E X)) \cdot_{W} (A \underset{˙}{\cdot} X)$
30		simprr	$⊢ (y \in ℕ_{0} \land ((A \in B \land X \in V) \land W \in AssAlg)) \to W \in AssAlg$
31	2	assasca	$⊢ W \in AssAlg \to F \in CRing$
32		crngring	$⊢ F \in CRing \to F \in Ring$
33	5	ringmgp	$⊢ F \in Ring \to G \in Mnd$
34	31 32 33	3syl	$⊢ W \in AssAlg \to G \in Mnd$
35	34	adantl	$⊢ ((A \in B \land X \in V) \land W \in AssAlg) \to G \in Mnd$
36	35	adantl	$⊢ (y \in ℕ_{0} \land ((A \in B \land X \in V) \land W \in AssAlg)) \to G \in Mnd$
37		simpl	$⊢ (y \in ℕ_{0} \land ((A \in B \land X \in V) \land W \in AssAlg)) \to y \in ℕ_{0}$
38	3	a1i	$⊢ W \in AssAlg \to B = {Base}_{F}$
39	2	fveq2i	$⊢ {Base}_{F} = {Base}_{Scalar (W)}$
40	38 39	eqtrdi	$⊢ W \in AssAlg \to B = {Base}_{Scalar (W)}$
41	40	eleq2d	$⊢ W \in AssAlg \to (A \in B \leftrightarrow A \in {Base}_{Scalar (W)})$
42	41	biimpcd	$⊢ A \in B \to (W \in AssAlg \to A \in {Base}_{Scalar (W)})$
43	42	adantr	$⊢ (A \in B \land X \in V) \to (W \in AssAlg \to A \in {Base}_{Scalar (W)})$
44	43	imp	$⊢ ((A \in B \land X \in V) \land W \in AssAlg) \to A \in {Base}_{Scalar (W)}$
45	44	adantl	$⊢ (y \in ℕ_{0} \land ((A \in B \land X \in V) \land W \in AssAlg)) \to A \in {Base}_{Scalar (W)}$
46	2	eqcomi	$⊢ Scalar (W) = F$
47	46	fveq2i	$⊢ {Base}_{Scalar (W)} = {Base}_{F}$
48	5 47	mgpbas	$⊢ {Base}_{Scalar (W)} = {Base}_{G}$
49	48 6	mulgnn0cl	$⊢ (G \in Mnd \land y \in ℕ_{0} \land A \in {Base}_{Scalar (W)}) \to y \underset{˙}{\times} A \in {Base}_{Scalar (W)}$
50	36 37 45 49	syl3anc	$⊢ (y \in ℕ_{0} \land ((A \in B \land X \in V) \land W \in AssAlg)) \to y \underset{˙}{\times} A \in {Base}_{Scalar (W)}$
51		simprlr	$⊢ (y \in ℕ_{0} \land ((A \in B \land X \in V) \land W \in AssAlg)) \to X \in V$
52	24 8	mulgnn0cl	$⊢ (H \in Mnd \land y \in ℕ_{0} \land X \in V) \to y E X \in V$
53	13 37 51 52	syl3anc	$⊢ (y \in ℕ_{0} \land ((A \in B \land X \in V) \land W \in AssAlg)) \to y E X \in V$
54		eqid	$⊢ Scalar (W) = Scalar (W)$
55		eqid	$⊢ {Base}_{Scalar (W)} = {Base}_{Scalar (W)}$
56	1 54 55 4 25	assaass	$⊢ (W \in AssAlg \land (y \underset{˙}{\times} A \in {Base}_{Scalar (W)} \land y E X \in V \land A \underset{˙}{\cdot} X \in V)) \to ((y \underset{˙}{\times} A) \underset{˙}{\cdot} (y E X)) \cdot_{W} (A \underset{˙}{\cdot} X) = (y \underset{˙}{\times} A) \underset{˙}{\cdot} ((y E X) \cdot_{W} (A \underset{˙}{\cdot} X))$
57	30 50 53 22 56	syl13anc	$⊢ (y \in ℕ_{0} \land ((A \in B \land X \in V) \land W \in AssAlg)) \to ((y \underset{˙}{\times} A) \underset{˙}{\cdot} (y E X)) \cdot_{W} (A \underset{˙}{\cdot} X) = (y \underset{˙}{\times} A) \underset{˙}{\cdot} ((y E X) \cdot_{W} (A \underset{˙}{\cdot} X))$
58	1 54 55 4 25	assaassr	$⊢ (W \in AssAlg \land (A \in {Base}_{Scalar (W)} \land y E X \in V \land X \in V)) \to (y E X) \cdot_{W} (A \underset{˙}{\cdot} X) = A \underset{˙}{\cdot} ((y E X) \cdot_{W} X)$
59	30 45 53 51 58	syl13anc	$⊢ (y \in ℕ_{0} \land ((A \in B \land X \in V) \land W \in AssAlg)) \to (y E X) \cdot_{W} (A \underset{˙}{\cdot} X) = A \underset{˙}{\cdot} ((y E X) \cdot_{W} X)$
60	59	oveq2d	$⊢ (y \in ℕ_{0} \land ((A \in B \land X \in V) \land W \in AssAlg)) \to (y \underset{˙}{\times} A) \underset{˙}{\cdot} ((y E X) \cdot_{W} (A \underset{˙}{\cdot} X)) = (y \underset{˙}{\times} A) \underset{˙}{\cdot} (A \underset{˙}{\cdot} ((y E X) \cdot_{W} X))$
61	24 8 26	mulgnn0p1	$⊢ (H \in Mnd \land y \in ℕ_{0} \land X \in V) \to (y + 1) E X = (y E X) \cdot_{W} X$
62	13 37 51 61	syl3anc	$⊢ (y \in ℕ_{0} \land ((A \in B \land X \in V) \land W \in AssAlg)) \to (y + 1) E X = (y E X) \cdot_{W} X$
63	62	eqcomd	$⊢ (y \in ℕ_{0} \land ((A \in B \land X \in V) \land W \in AssAlg)) \to (y E X) \cdot_{W} X = (y + 1) E X$
64	63	oveq2d	$⊢ (y \in ℕ_{0} \land ((A \in B \land X \in V) \land W \in AssAlg)) \to A \underset{˙}{\cdot} ((y E X) \cdot_{W} X) = A \underset{˙}{\cdot} ((y + 1) E X)$
65	64	oveq2d	$⊢ (y \in ℕ_{0} \land ((A \in B \land X \in V) \land W \in AssAlg)) \to (y \underset{˙}{\times} A) \underset{˙}{\cdot} (A \underset{˙}{\cdot} ((y E X) \cdot_{W} X)) = (y \underset{˙}{\times} A) \underset{˙}{\cdot} (A \underset{˙}{\cdot} ((y + 1) E X))$
66	17	adantl	$⊢ (y \in ℕ_{0} \land ((A \in B \land X \in V) \land W \in AssAlg)) \to W \in LMod$
67		peano2nn0	$⊢ y \in ℕ_{0} \to y + 1 \in ℕ_{0}$
68	67	adantr	$⊢ (y \in ℕ_{0} \land ((A \in B \land X \in V) \land W \in AssAlg)) \to y + 1 \in ℕ_{0}$
69	24 8	mulgnn0cl	$⊢ (H \in Mnd \land y + 1 \in ℕ_{0} \land X \in V) \to (y + 1) E X \in V$
70	13 68 51 69	syl3anc	$⊢ (y \in ℕ_{0} \land ((A \in B \land X \in V) \land W \in AssAlg)) \to (y + 1) E X \in V$
71		eqid	$⊢ \cdot_{Scalar (W)} = \cdot_{Scalar (W)}$
72	1 54 4 55 71	lmodvsass	$⊢ (W \in LMod \land (y \underset{˙}{\times} A \in {Base}_{Scalar (W)} \land A \in {Base}_{Scalar (W)} \land (y + 1) E X \in V)) \to ((y \underset{˙}{\times} A) \cdot_{Scalar (W)} A) \underset{˙}{\cdot} ((y + 1) E X) = (y \underset{˙}{\times} A) \underset{˙}{\cdot} (A \underset{˙}{\cdot} ((y + 1) E X))$
73	72	eqcomd	$⊢ (W \in LMod \land (y \underset{˙}{\times} A \in {Base}_{Scalar (W)} \land A \in {Base}_{Scalar (W)} \land (y + 1) E X \in V)) \to (y \underset{˙}{\times} A) \underset{˙}{\cdot} (A \underset{˙}{\cdot} ((y + 1) E X)) = ((y \underset{˙}{\times} A) \cdot_{Scalar (W)} A) \underset{˙}{\cdot} ((y + 1) E X)$
74	66 50 45 70 73	syl13anc	$⊢ (y \in ℕ_{0} \land ((A \in B \land X \in V) \land W \in AssAlg)) \to (y \underset{˙}{\times} A) \underset{˙}{\cdot} (A \underset{˙}{\cdot} ((y + 1) E X)) = ((y \underset{˙}{\times} A) \cdot_{Scalar (W)} A) \underset{˙}{\cdot} ((y + 1) E X)$
75	60 65 74	3eqtrd	$⊢ (y \in ℕ_{0} \land ((A \in B \land X \in V) \land W \in AssAlg)) \to (y \underset{˙}{\times} A) \underset{˙}{\cdot} ((y E X) \cdot_{W} (A \underset{˙}{\cdot} X)) = ((y \underset{˙}{\times} A) \cdot_{Scalar (W)} A) \underset{˙}{\cdot} ((y + 1) E X)$
76		simprll	$⊢ (y \in ℕ_{0} \land ((A \in B \land X \in V) \land W \in AssAlg)) \to A \in B$
77	5 3	mgpbas	$⊢ B = {Base}_{G}$
78		eqid	$⊢ \cdot_{F} = \cdot_{F}$
79	5 78	mgpplusg	$⊢ \cdot_{F} = +_{G}$
80	77 6 79	mulgnn0p1	$⊢ (G \in Mnd \land y \in ℕ_{0} \land A \in B) \to (y + 1) \underset{˙}{\times} A = (y \underset{˙}{\times} A) \cdot_{F} A$
81	36 37 76 80	syl3anc	$⊢ (y \in ℕ_{0} \land ((A \in B \land X \in V) \land W \in AssAlg)) \to (y + 1) \underset{˙}{\times} A = (y \underset{˙}{\times} A) \cdot_{F} A$
82	2	a1i	$⊢ (y \in ℕ_{0} \land ((A \in B \land X \in V) \land W \in AssAlg)) \to F = Scalar (W)$
83	82	fveq2d	$⊢ (y \in ℕ_{0} \land ((A \in B \land X \in V) \land W \in AssAlg)) \to \cdot_{F} = \cdot_{Scalar (W)}$
84	83	oveqd	$⊢ (y \in ℕ_{0} \land ((A \in B \land X \in V) \land W \in AssAlg)) \to (y \underset{˙}{\times} A) \cdot_{F} A = (y \underset{˙}{\times} A) \cdot_{Scalar (W)} A$
85	81 84	eqtrd	$⊢ (y \in ℕ_{0} \land ((A \in B \land X \in V) \land W \in AssAlg)) \to (y + 1) \underset{˙}{\times} A = (y \underset{˙}{\times} A) \cdot_{Scalar (W)} A$
86	85	eqcomd	$⊢ (y \in ℕ_{0} \land ((A \in B \land X \in V) \land W \in AssAlg)) \to (y \underset{˙}{\times} A) \cdot_{Scalar (W)} A = (y + 1) \underset{˙}{\times} A$
87	86	oveq1d	$⊢ (y \in ℕ_{0} \land ((A \in B \land X \in V) \land W \in AssAlg)) \to ((y \underset{˙}{\times} A) \cdot_{Scalar (W)} A) \underset{˙}{\cdot} ((y + 1) E X) = ((y + 1) \underset{˙}{\times} A) \underset{˙}{\cdot} ((y + 1) E X)$
88	57 75 87	3eqtrd	$⊢ (y \in ℕ_{0} \land ((A \in B \land X \in V) \land W \in AssAlg)) \to ((y \underset{˙}{\times} A) \underset{˙}{\cdot} (y E X)) \cdot_{W} (A \underset{˙}{\cdot} X) = ((y + 1) \underset{˙}{\times} A) \underset{˙}{\cdot} ((y + 1) E X)$
89	29 88	sylan9eqr	$⊢ ((y \in ℕ_{0} \land ((A \in B \land X \in V) \land W \in AssAlg)) \land y E (A \underset{˙}{\cdot} X) = (y \underset{˙}{\times} A) \underset{˙}{\cdot} (y E X)) \to (y E (A \underset{˙}{\cdot} X)) \cdot_{W} (A \underset{˙}{\cdot} X) = ((y + 1) \underset{˙}{\times} A) \underset{˙}{\cdot} ((y + 1) E X)$
90	28 89	eqtrd	$⊢ ((y \in ℕ_{0} \land ((A \in B \land X \in V) \land W \in AssAlg)) \land y E (A \underset{˙}{\cdot} X) = (y \underset{˙}{\times} A) \underset{˙}{\cdot} (y E X)) \to (y + 1) E (A \underset{˙}{\cdot} X) = ((y + 1) \underset{˙}{\times} A) \underset{˙}{\cdot} ((y + 1) E X)$
91	90	exp31	$⊢ y \in ℕ_{0} \to (((A \in B \land X \in V) \land W \in AssAlg) \to (y E (A \underset{˙}{\cdot} X) = (y \underset{˙}{\times} A) \underset{˙}{\cdot} (y E X) \to (y + 1) E (A \underset{˙}{\cdot} X) = ((y + 1) \underset{˙}{\times} A) \underset{˙}{\cdot} ((y + 1) E X)))$

Metamath Proof Explorer

Theorem assamulgscmlem2

Proof