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	eqcomi	$⊢ Scalar (W) = F$
32	31	fveq2i	$⊢ {Base}_{Scalar (W)} = {Base}_{F}$
33	5 32	mgpbas	$⊢ {Base}_{Scalar (W)} = {Base}_{G}$
34	2	assasca	$⊢ W \in AssAlg \to F \in Ring$
35	5	ringmgp	$⊢ F \in Ring \to G \in Mnd$
36	34 35	syl	$⊢ W \in AssAlg \to G \in Mnd$
37	36	adantl	$⊢ ((A \in B \land X \in V) \land W \in AssAlg) \to G \in Mnd$
38	37	adantl	$⊢ (y \in ℕ_{0} \land ((A \in B \land X \in V) \land W \in AssAlg)) \to G \in Mnd$
39		simpl	$⊢ (y \in ℕ_{0} \land ((A \in B \land X \in V) \land W \in AssAlg)) \to y \in ℕ_{0}$
40	3	a1i	$⊢ W \in AssAlg \to B = {Base}_{F}$
41	2	fveq2i	$⊢ {Base}_{F} = {Base}_{Scalar (W)}$
42	40 41	eqtrdi	$⊢ W \in AssAlg \to B = {Base}_{Scalar (W)}$
43	42	eleq2d	$⊢ W \in AssAlg \to (A \in B \leftrightarrow A \in {Base}_{Scalar (W)})$
44	43	biimpcd	$⊢ A \in B \to (W \in AssAlg \to A \in {Base}_{Scalar (W)})$
45	44	adantr	$⊢ (A \in B \land X \in V) \to (W \in AssAlg \to A \in {Base}_{Scalar (W)})$
46	45	imp	$⊢ ((A \in B \land X \in V) \land W \in AssAlg) \to A \in {Base}_{Scalar (W)}$
47	46	adantl	$⊢ (y \in ℕ_{0} \land ((A \in B \land X \in V) \land W \in AssAlg)) \to A \in {Base}_{Scalar (W)}$
48	33 6 38 39 47	mulgnn0cld	$⊢ (y \in ℕ_{0} \land ((A \in B \land X \in V) \land W \in AssAlg)) \to y \underset{˙}{\times} A \in {Base}_{Scalar (W)}$
49		simprlr	$⊢ (y \in ℕ_{0} \land ((A \in B \land X \in V) \land W \in AssAlg)) \to X \in V$
50	24 8 13 39 49	mulgnn0cld	$⊢ (y \in ℕ_{0} \land ((A \in B \land X \in V) \land W \in AssAlg)) \to y E X \in V$
51		eqid	$⊢ Scalar (W) = Scalar (W)$
52		eqid	$⊢ {Base}_{Scalar (W)} = {Base}_{Scalar (W)}$
53	1 51 52 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))$
54	30 48 50 22 53	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))$
55	1 51 52 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)$
56	30 47 50 49 55	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)$
57	56	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))$
58	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$
59	13 39 49 58	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$
60	59	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$
61	60	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)$
62	61	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))$
63	17	adantl	$⊢ (y \in ℕ_{0} \land ((A \in B \land X \in V) \land W \in AssAlg)) \to W \in LMod$
64		peano2nn0	$⊢ y \in ℕ_{0} \to y + 1 \in ℕ_{0}$
65	64	adantr	$⊢ (y \in ℕ_{0} \land ((A \in B \land X \in V) \land W \in AssAlg)) \to y + 1 \in ℕ_{0}$
66	24 8 13 65 49	mulgnn0cld	$⊢ (y \in ℕ_{0} \land ((A \in B \land X \in V) \land W \in AssAlg)) \to (y + 1) E X \in V$
67		eqid	$⊢ \cdot_{Scalar (W)} = \cdot_{Scalar (W)}$
68	1 51 4 52 67	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))$
69	68	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)$
70	63 48 47 66 69	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)$
71	57 62 70	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)$
72		simprll	$⊢ (y \in ℕ_{0} \land ((A \in B \land X \in V) \land W \in AssAlg)) \to A \in B$
73	5 3	mgpbas	$⊢ B = {Base}_{G}$
74		eqid	$⊢ \cdot_{F} = \cdot_{F}$
75	5 74	mgpplusg	$⊢ \cdot_{F} = +_{G}$
76	73 6 75	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$
77	38 39 72 76	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$
78	2	a1i	$⊢ (y \in ℕ_{0} \land ((A \in B \land X \in V) \land W \in AssAlg)) \to F = Scalar (W)$
79	78	fveq2d	$⊢ (y \in ℕ_{0} \land ((A \in B \land X \in V) \land W \in AssAlg)) \to \cdot_{F} = \cdot_{Scalar (W)}$
80	79	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$
81	77 80	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$
82	81	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$
83	82	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)$
84	54 71 83	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)$
85	29 84	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)$
86	28 85	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)$
87	86	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