Theorem assamulgscmlem2

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

	Ref	Expression
Hypotheses	assamulgscm.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
	assamulgscm.f	⊢ 𝐹 = ( Scalar ‘ 𝑊 )
	assamulgscm.b	⊢ 𝐵 = ( Base ‘ 𝐹 )
	assamulgscm.s	⊢ · = ( ·𝑠 ‘ 𝑊 )
	assamulgscm.g	⊢ 𝐺 = ( mulGrp ‘ 𝐹 )
	assamulgscm.p	⊢ ↑ = ( .g ‘ 𝐺 )
	assamulgscm.h	⊢ 𝐻 = ( mulGrp ‘ 𝑊 )
	assamulgscm.e	⊢ 𝐸 = ( .g ‘ 𝐻 )
Assertion	assamulgscmlem2	⊢ ( 𝑦 ∈ ℕ0 → ( ( ( 𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ AssAlg ) → ( ( 𝑦 𝐸 ( 𝐴 · 𝑋 ) ) = ( ( 𝑦 ↑ 𝐴 ) · ( 𝑦 𝐸 𝑋 ) ) → ( ( 𝑦 + 1 ) 𝐸 ( 𝐴 · 𝑋 ) ) = ( ( ( 𝑦 + 1 ) ↑ 𝐴 ) · ( ( 𝑦 + 1 ) 𝐸 𝑋 ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		assamulgscm.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
2		assamulgscm.f	⊢ 𝐹 = ( Scalar ‘ 𝑊 )
3		assamulgscm.b	⊢ 𝐵 = ( Base ‘ 𝐹 )
4		assamulgscm.s	⊢ · = ( ·𝑠 ‘ 𝑊 )
5		assamulgscm.g	⊢ 𝐺 = ( mulGrp ‘ 𝐹 )
6		assamulgscm.p	⊢ ↑ = ( .g ‘ 𝐺 )
7		assamulgscm.h	⊢ 𝐻 = ( mulGrp ‘ 𝑊 )
8		assamulgscm.e	⊢ 𝐸 = ( .g ‘ 𝐻 )
9		assaring	⊢ ( 𝑊 ∈ AssAlg → 𝑊 ∈ Ring )
10	7	ringmgp	⊢ ( 𝑊 ∈ Ring → 𝐻 ∈ Mnd )
11	9 10	syl	⊢ ( 𝑊 ∈ AssAlg → 𝐻 ∈ Mnd )
12	11	adantl	⊢ ( ( ( 𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ AssAlg ) → 𝐻 ∈ Mnd )
13	12	adantl	⊢ ( ( 𝑦 ∈ ℕ0 ∧ ( ( 𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ AssAlg ) ) → 𝐻 ∈ Mnd )
14	13	adantr	⊢ ( ( ( 𝑦 ∈ ℕ0 ∧ ( ( 𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ AssAlg ) ) ∧ ( 𝑦 𝐸 ( 𝐴 · 𝑋 ) ) = ( ( 𝑦 ↑ 𝐴 ) · ( 𝑦 𝐸 𝑋 ) ) ) → 𝐻 ∈ Mnd )
15		simpll	⊢ ( ( ( 𝑦 ∈ ℕ0 ∧ ( ( 𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ AssAlg ) ) ∧ ( 𝑦 𝐸 ( 𝐴 · 𝑋 ) ) = ( ( 𝑦 ↑ 𝐴 ) · ( 𝑦 𝐸 𝑋 ) ) ) → 𝑦 ∈ ℕ0 )
16		assalmod	⊢ ( 𝑊 ∈ AssAlg → 𝑊 ∈ LMod )
17	16	adantl	⊢ ( ( ( 𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ AssAlg ) → 𝑊 ∈ LMod )
18		simpll	⊢ ( ( ( 𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ AssAlg ) → 𝐴 ∈ 𝐵 )
19		simplr	⊢ ( ( ( 𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ AssAlg ) → 𝑋 ∈ 𝑉 )
20	1 2 4 3	lmodvscl	⊢ ( ( 𝑊 ∈ LMod ∧ 𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ) → ( 𝐴 · 𝑋 ) ∈ 𝑉 )
21	17 18 19 20	syl3anc	⊢ ( ( ( 𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ AssAlg ) → ( 𝐴 · 𝑋 ) ∈ 𝑉 )
22	21	adantl	⊢ ( ( 𝑦 ∈ ℕ0 ∧ ( ( 𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ AssAlg ) ) → ( 𝐴 · 𝑋 ) ∈ 𝑉 )
23	22	adantr	⊢ ( ( ( 𝑦 ∈ ℕ0 ∧ ( ( 𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ AssAlg ) ) ∧ ( 𝑦 𝐸 ( 𝐴 · 𝑋 ) ) = ( ( 𝑦 ↑ 𝐴 ) · ( 𝑦 𝐸 𝑋 ) ) ) → ( 𝐴 · 𝑋 ) ∈ 𝑉 )
24	7 1	mgpbas	⊢ 𝑉 = ( Base ‘ 𝐻 )
25		eqid	⊢ ( .r ‘ 𝑊 ) = ( .r ‘ 𝑊 )
26	7 25	mgpplusg	⊢ ( .r ‘ 𝑊 ) = ( +g ‘ 𝐻 )
27	24 8 26	mulgnn0p1	⊢ ( ( 𝐻 ∈ Mnd ∧ 𝑦 ∈ ℕ0 ∧ ( 𝐴 · 𝑋 ) ∈ 𝑉 ) → ( ( 𝑦 + 1 ) 𝐸 ( 𝐴 · 𝑋 ) ) = ( ( 𝑦 𝐸 ( 𝐴 · 𝑋 ) ) ( .r ‘ 𝑊 ) ( 𝐴 · 𝑋 ) ) )
28	14 15 23 27	syl3anc	⊢ ( ( ( 𝑦 ∈ ℕ0 ∧ ( ( 𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ AssAlg ) ) ∧ ( 𝑦 𝐸 ( 𝐴 · 𝑋 ) ) = ( ( 𝑦 ↑ 𝐴 ) · ( 𝑦 𝐸 𝑋 ) ) ) → ( ( 𝑦 + 1 ) 𝐸 ( 𝐴 · 𝑋 ) ) = ( ( 𝑦 𝐸 ( 𝐴 · 𝑋 ) ) ( .r ‘ 𝑊 ) ( 𝐴 · 𝑋 ) ) )
29		oveq1	⊢ ( ( 𝑦 𝐸 ( 𝐴 · 𝑋 ) ) = ( ( 𝑦 ↑ 𝐴 ) · ( 𝑦 𝐸 𝑋 ) ) → ( ( 𝑦 𝐸 ( 𝐴 · 𝑋 ) ) ( .r ‘ 𝑊 ) ( 𝐴 · 𝑋 ) ) = ( ( ( 𝑦 ↑ 𝐴 ) · ( 𝑦 𝐸 𝑋 ) ) ( .r ‘ 𝑊 ) ( 𝐴 · 𝑋 ) ) )
30		simprr	⊢ ( ( 𝑦 ∈ ℕ0 ∧ ( ( 𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ AssAlg ) ) → 𝑊 ∈ AssAlg )
31	2	eqcomi	⊢ ( Scalar ‘ 𝑊 ) = 𝐹
32	31	fveq2i	⊢ ( Base ‘ ( Scalar ‘ 𝑊 ) ) = ( Base ‘ 𝐹 )
33	5 32	mgpbas	⊢ ( Base ‘ ( Scalar ‘ 𝑊 ) ) = ( Base ‘ 𝐺 )
34	2	assasca	⊢ ( 𝑊 ∈ AssAlg → 𝐹 ∈ Ring )
35	5	ringmgp	⊢ ( 𝐹 ∈ Ring → 𝐺 ∈ Mnd )
36	34 35	syl	⊢ ( 𝑊 ∈ AssAlg → 𝐺 ∈ Mnd )
37	36	adantl	⊢ ( ( ( 𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ AssAlg ) → 𝐺 ∈ Mnd )
38	37	adantl	⊢ ( ( 𝑦 ∈ ℕ0 ∧ ( ( 𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ AssAlg ) ) → 𝐺 ∈ Mnd )
39		simpl	⊢ ( ( 𝑦 ∈ ℕ0 ∧ ( ( 𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ AssAlg ) ) → 𝑦 ∈ ℕ0 )
40	3	a1i	⊢ ( 𝑊 ∈ AssAlg → 𝐵 = ( Base ‘ 𝐹 ) )
41	2	fveq2i	⊢ ( Base ‘ 𝐹 ) = ( Base ‘ ( Scalar ‘ 𝑊 ) )
42	40 41	eqtrdi	⊢ ( 𝑊 ∈ AssAlg → 𝐵 = ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
43	42	eleq2d	⊢ ( 𝑊 ∈ AssAlg → ( 𝐴 ∈ 𝐵 ↔ 𝐴 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) )
44	43	biimpcd	⊢ ( 𝐴 ∈ 𝐵 → ( 𝑊 ∈ AssAlg → 𝐴 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) )
45	44	adantr	⊢ ( ( 𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ) → ( 𝑊 ∈ AssAlg → 𝐴 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) )
46	45	imp	⊢ ( ( ( 𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ AssAlg ) → 𝐴 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
47	46	adantl	⊢ ( ( 𝑦 ∈ ℕ0 ∧ ( ( 𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ AssAlg ) ) → 𝐴 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
48	33 6 38 39 47	mulgnn0cld	⊢ ( ( 𝑦 ∈ ℕ0 ∧ ( ( 𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ AssAlg ) ) → ( 𝑦 ↑ 𝐴 ) ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
49		simprlr	⊢ ( ( 𝑦 ∈ ℕ0 ∧ ( ( 𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ AssAlg ) ) → 𝑋 ∈ 𝑉 )
50	24 8 13 39 49	mulgnn0cld	⊢ ( ( 𝑦 ∈ ℕ0 ∧ ( ( 𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ AssAlg ) ) → ( 𝑦 𝐸 𝑋 ) ∈ 𝑉 )
51		eqid	⊢ ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑊 )
52		eqid	⊢ ( Base ‘ ( Scalar ‘ 𝑊 ) ) = ( Base ‘ ( Scalar ‘ 𝑊 ) )
53	1 51 52 4 25	assaass	⊢ ( ( 𝑊 ∈ AssAlg ∧ ( ( 𝑦 ↑ 𝐴 ) ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ ( 𝑦 𝐸 𝑋 ) ∈ 𝑉 ∧ ( 𝐴 · 𝑋 ) ∈ 𝑉 ) ) → ( ( ( 𝑦 ↑ 𝐴 ) · ( 𝑦 𝐸 𝑋 ) ) ( .r ‘ 𝑊 ) ( 𝐴 · 𝑋 ) ) = ( ( 𝑦 ↑ 𝐴 ) · ( ( 𝑦 𝐸 𝑋 ) ( .r ‘ 𝑊 ) ( 𝐴 · 𝑋 ) ) ) )
54	30 48 50 22 53	syl13anc	⊢ ( ( 𝑦 ∈ ℕ0 ∧ ( ( 𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ AssAlg ) ) → ( ( ( 𝑦 ↑ 𝐴 ) · ( 𝑦 𝐸 𝑋 ) ) ( .r ‘ 𝑊 ) ( 𝐴 · 𝑋 ) ) = ( ( 𝑦 ↑ 𝐴 ) · ( ( 𝑦 𝐸 𝑋 ) ( .r ‘ 𝑊 ) ( 𝐴 · 𝑋 ) ) ) )
55	1 51 52 4 25	assaassr	⊢ ( ( 𝑊 ∈ AssAlg ∧ ( 𝐴 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ ( 𝑦 𝐸 𝑋 ) ∈ 𝑉 ∧ 𝑋 ∈ 𝑉 ) ) → ( ( 𝑦 𝐸 𝑋 ) ( .r ‘ 𝑊 ) ( 𝐴 · 𝑋 ) ) = ( 𝐴 · ( ( 𝑦 𝐸 𝑋 ) ( .r ‘ 𝑊 ) 𝑋 ) ) )
56	30 47 50 49 55	syl13anc	⊢ ( ( 𝑦 ∈ ℕ0 ∧ ( ( 𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ AssAlg ) ) → ( ( 𝑦 𝐸 𝑋 ) ( .r ‘ 𝑊 ) ( 𝐴 · 𝑋 ) ) = ( 𝐴 · ( ( 𝑦 𝐸 𝑋 ) ( .r ‘ 𝑊 ) 𝑋 ) ) )
57	56	oveq2d	⊢ ( ( 𝑦 ∈ ℕ0 ∧ ( ( 𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ AssAlg ) ) → ( ( 𝑦 ↑ 𝐴 ) · ( ( 𝑦 𝐸 𝑋 ) ( .r ‘ 𝑊 ) ( 𝐴 · 𝑋 ) ) ) = ( ( 𝑦 ↑ 𝐴 ) · ( 𝐴 · ( ( 𝑦 𝐸 𝑋 ) ( .r ‘ 𝑊 ) 𝑋 ) ) ) )
58	24 8 26	mulgnn0p1	⊢ ( ( 𝐻 ∈ Mnd ∧ 𝑦 ∈ ℕ0 ∧ 𝑋 ∈ 𝑉 ) → ( ( 𝑦 + 1 ) 𝐸 𝑋 ) = ( ( 𝑦 𝐸 𝑋 ) ( .r ‘ 𝑊 ) 𝑋 ) )
59	13 39 49 58	syl3anc	⊢ ( ( 𝑦 ∈ ℕ0 ∧ ( ( 𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ AssAlg ) ) → ( ( 𝑦 + 1 ) 𝐸 𝑋 ) = ( ( 𝑦 𝐸 𝑋 ) ( .r ‘ 𝑊 ) 𝑋 ) )
60	59	eqcomd	⊢ ( ( 𝑦 ∈ ℕ0 ∧ ( ( 𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ AssAlg ) ) → ( ( 𝑦 𝐸 𝑋 ) ( .r ‘ 𝑊 ) 𝑋 ) = ( ( 𝑦 + 1 ) 𝐸 𝑋 ) )
61	60	oveq2d	⊢ ( ( 𝑦 ∈ ℕ0 ∧ ( ( 𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ AssAlg ) ) → ( 𝐴 · ( ( 𝑦 𝐸 𝑋 ) ( .r ‘ 𝑊 ) 𝑋 ) ) = ( 𝐴 · ( ( 𝑦 + 1 ) 𝐸 𝑋 ) ) )
62	61	oveq2d	⊢ ( ( 𝑦 ∈ ℕ0 ∧ ( ( 𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ AssAlg ) ) → ( ( 𝑦 ↑ 𝐴 ) · ( 𝐴 · ( ( 𝑦 𝐸 𝑋 ) ( .r ‘ 𝑊 ) 𝑋 ) ) ) = ( ( 𝑦 ↑ 𝐴 ) · ( 𝐴 · ( ( 𝑦 + 1 ) 𝐸 𝑋 ) ) ) )
63	17	adantl	⊢ ( ( 𝑦 ∈ ℕ0 ∧ ( ( 𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ AssAlg ) ) → 𝑊 ∈ LMod )
64		peano2nn0	⊢ ( 𝑦 ∈ ℕ0 → ( 𝑦 + 1 ) ∈ ℕ0 )
65	64	adantr	⊢ ( ( 𝑦 ∈ ℕ0 ∧ ( ( 𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ AssAlg ) ) → ( 𝑦 + 1 ) ∈ ℕ0 )
66	24 8 13 65 49	mulgnn0cld	⊢ ( ( 𝑦 ∈ ℕ0 ∧ ( ( 𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ AssAlg ) ) → ( ( 𝑦 + 1 ) 𝐸 𝑋 ) ∈ 𝑉 )
67		eqid	⊢ ( .r ‘ ( Scalar ‘ 𝑊 ) ) = ( .r ‘ ( Scalar ‘ 𝑊 ) )
68	1 51 4 52 67	lmodvsass	⊢ ( ( 𝑊 ∈ LMod ∧ ( ( 𝑦 ↑ 𝐴 ) ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝐴 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ ( ( 𝑦 + 1 ) 𝐸 𝑋 ) ∈ 𝑉 ) ) → ( ( ( 𝑦 ↑ 𝐴 ) ( .r ‘ ( Scalar ‘ 𝑊 ) ) 𝐴 ) · ( ( 𝑦 + 1 ) 𝐸 𝑋 ) ) = ( ( 𝑦 ↑ 𝐴 ) · ( 𝐴 · ( ( 𝑦 + 1 ) 𝐸 𝑋 ) ) ) )
69	68	eqcomd	⊢ ( ( 𝑊 ∈ LMod ∧ ( ( 𝑦 ↑ 𝐴 ) ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝐴 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ ( ( 𝑦 + 1 ) 𝐸 𝑋 ) ∈ 𝑉 ) ) → ( ( 𝑦 ↑ 𝐴 ) · ( 𝐴 · ( ( 𝑦 + 1 ) 𝐸 𝑋 ) ) ) = ( ( ( 𝑦 ↑ 𝐴 ) ( .r ‘ ( Scalar ‘ 𝑊 ) ) 𝐴 ) · ( ( 𝑦 + 1 ) 𝐸 𝑋 ) ) )
70	63 48 47 66 69	syl13anc	⊢ ( ( 𝑦 ∈ ℕ0 ∧ ( ( 𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ AssAlg ) ) → ( ( 𝑦 ↑ 𝐴 ) · ( 𝐴 · ( ( 𝑦 + 1 ) 𝐸 𝑋 ) ) ) = ( ( ( 𝑦 ↑ 𝐴 ) ( .r ‘ ( Scalar ‘ 𝑊 ) ) 𝐴 ) · ( ( 𝑦 + 1 ) 𝐸 𝑋 ) ) )
71	57 62 70	3eqtrd	⊢ ( ( 𝑦 ∈ ℕ0 ∧ ( ( 𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ AssAlg ) ) → ( ( 𝑦 ↑ 𝐴 ) · ( ( 𝑦 𝐸 𝑋 ) ( .r ‘ 𝑊 ) ( 𝐴 · 𝑋 ) ) ) = ( ( ( 𝑦 ↑ 𝐴 ) ( .r ‘ ( Scalar ‘ 𝑊 ) ) 𝐴 ) · ( ( 𝑦 + 1 ) 𝐸 𝑋 ) ) )
72		simprll	⊢ ( ( 𝑦 ∈ ℕ0 ∧ ( ( 𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ AssAlg ) ) → 𝐴 ∈ 𝐵 )
73	5 3	mgpbas	⊢ 𝐵 = ( Base ‘ 𝐺 )
74		eqid	⊢ ( .r ‘ 𝐹 ) = ( .r ‘ 𝐹 )
75	5 74	mgpplusg	⊢ ( .r ‘ 𝐹 ) = ( +g ‘ 𝐺 )
76	73 6 75	mulgnn0p1	⊢ ( ( 𝐺 ∈ Mnd ∧ 𝑦 ∈ ℕ0 ∧ 𝐴 ∈ 𝐵 ) → ( ( 𝑦 + 1 ) ↑ 𝐴 ) = ( ( 𝑦 ↑ 𝐴 ) ( .r ‘ 𝐹 ) 𝐴 ) )
77	38 39 72 76	syl3anc	⊢ ( ( 𝑦 ∈ ℕ0 ∧ ( ( 𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ AssAlg ) ) → ( ( 𝑦 + 1 ) ↑ 𝐴 ) = ( ( 𝑦 ↑ 𝐴 ) ( .r ‘ 𝐹 ) 𝐴 ) )
78	2	a1i	⊢ ( ( 𝑦 ∈ ℕ0 ∧ ( ( 𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ AssAlg ) ) → 𝐹 = ( Scalar ‘ 𝑊 ) )
79	78	fveq2d	⊢ ( ( 𝑦 ∈ ℕ0 ∧ ( ( 𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ AssAlg ) ) → ( .r ‘ 𝐹 ) = ( .r ‘ ( Scalar ‘ 𝑊 ) ) )
80	79	oveqd	⊢ ( ( 𝑦 ∈ ℕ0 ∧ ( ( 𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ AssAlg ) ) → ( ( 𝑦 ↑ 𝐴 ) ( .r ‘ 𝐹 ) 𝐴 ) = ( ( 𝑦 ↑ 𝐴 ) ( .r ‘ ( Scalar ‘ 𝑊 ) ) 𝐴 ) )
81	77 80	eqtrd	⊢ ( ( 𝑦 ∈ ℕ0 ∧ ( ( 𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ AssAlg ) ) → ( ( 𝑦 + 1 ) ↑ 𝐴 ) = ( ( 𝑦 ↑ 𝐴 ) ( .r ‘ ( Scalar ‘ 𝑊 ) ) 𝐴 ) )
82	81	eqcomd	⊢ ( ( 𝑦 ∈ ℕ0 ∧ ( ( 𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ AssAlg ) ) → ( ( 𝑦 ↑ 𝐴 ) ( .r ‘ ( Scalar ‘ 𝑊 ) ) 𝐴 ) = ( ( 𝑦 + 1 ) ↑ 𝐴 ) )
83	82	oveq1d	⊢ ( ( 𝑦 ∈ ℕ0 ∧ ( ( 𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ AssAlg ) ) → ( ( ( 𝑦 ↑ 𝐴 ) ( .r ‘ ( Scalar ‘ 𝑊 ) ) 𝐴 ) · ( ( 𝑦 + 1 ) 𝐸 𝑋 ) ) = ( ( ( 𝑦 + 1 ) ↑ 𝐴 ) · ( ( 𝑦 + 1 ) 𝐸 𝑋 ) ) )
84	54 71 83	3eqtrd	⊢ ( ( 𝑦 ∈ ℕ0 ∧ ( ( 𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ AssAlg ) ) → ( ( ( 𝑦 ↑ 𝐴 ) · ( 𝑦 𝐸 𝑋 ) ) ( .r ‘ 𝑊 ) ( 𝐴 · 𝑋 ) ) = ( ( ( 𝑦 + 1 ) ↑ 𝐴 ) · ( ( 𝑦 + 1 ) 𝐸 𝑋 ) ) )
85	29 84	sylan9eqr	⊢ ( ( ( 𝑦 ∈ ℕ0 ∧ ( ( 𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ AssAlg ) ) ∧ ( 𝑦 𝐸 ( 𝐴 · 𝑋 ) ) = ( ( 𝑦 ↑ 𝐴 ) · ( 𝑦 𝐸 𝑋 ) ) ) → ( ( 𝑦 𝐸 ( 𝐴 · 𝑋 ) ) ( .r ‘ 𝑊 ) ( 𝐴 · 𝑋 ) ) = ( ( ( 𝑦 + 1 ) ↑ 𝐴 ) · ( ( 𝑦 + 1 ) 𝐸 𝑋 ) ) )
86	28 85	eqtrd	⊢ ( ( ( 𝑦 ∈ ℕ0 ∧ ( ( 𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ AssAlg ) ) ∧ ( 𝑦 𝐸 ( 𝐴 · 𝑋 ) ) = ( ( 𝑦 ↑ 𝐴 ) · ( 𝑦 𝐸 𝑋 ) ) ) → ( ( 𝑦 + 1 ) 𝐸 ( 𝐴 · 𝑋 ) ) = ( ( ( 𝑦 + 1 ) ↑ 𝐴 ) · ( ( 𝑦 + 1 ) 𝐸 𝑋 ) ) )
87	86	exp31	⊢ ( 𝑦 ∈ ℕ0 → ( ( ( 𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑊 ∈ AssAlg ) → ( ( 𝑦 𝐸 ( 𝐴 · 𝑋 ) ) = ( ( 𝑦 ↑ 𝐴 ) · ( 𝑦 𝐸 𝑋 ) ) → ( ( 𝑦 + 1 ) 𝐸 ( 𝐴 · 𝑋 ) ) = ( ( ( 𝑦 + 1 ) ↑ 𝐴 ) · ( ( 𝑦 + 1 ) 𝐸 𝑋 ) ) ) ) )