MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  assamulgscmlem2 Structured version   Visualization version   GIF version
Theorem assamulgscmlem2 21837
Description: Lemma for assamulgscm 21838 (induction step). (Contributed by AV, 26-Aug-2019.)
Hypotheses
Ref Expression
assamulgscm.v 𝑉 = (Baseβ€˜π‘Š)
assamulgscm.f 𝐹 = (Scalarβ€˜π‘Š)
assamulgscm.b 𝐡 = (Baseβ€˜πΉ)
assamulgscm.s Β· = ( ·𝑠 β€˜π‘Š)
assamulgscm.g 𝐺 = (mulGrpβ€˜πΉ)
assamulgscm.p ↑ = (.gβ€˜πΊ)
assamulgscm.h 𝐻 = (mulGrpβ€˜π‘Š)
assamulgscm.e 𝐸 = (.gβ€˜π»)
Assertion
Ref Expression
assamulgscmlem2 (𝑦 ∈ β„•0 β†’ (((𝐴 ∈ 𝐡 ∧ 𝑋 ∈ 𝑉) ∧ π‘Š ∈ AssAlg) β†’ ((𝑦𝐸(𝐴 Β· 𝑋)) = ((𝑦 ↑ 𝐴) Β· (𝑦𝐸𝑋)) β†’ ((𝑦 + 1)𝐸(𝐴 Β· 𝑋)) = (((𝑦 + 1) ↑ 𝐴) Β· ((𝑦 + 1)𝐸𝑋)))))
Proof of Theorem assamulgscmlem2
StepHypRef Expression
1 assaring 21799 . . . . . . . 8 (π‘Š ∈ AssAlg β†’ π‘Š ∈ Ring)
2 assamulgscm.h . . . . . . . . 9 𝐻 = (mulGrpβ€˜π‘Š)
32ringmgp 20183 . . . . . . . 8 (π‘Š ∈ Ring β†’ 𝐻 ∈ Mnd)
41, 3syl 17 . . . . . . 7 (π‘Š ∈ AssAlg β†’ 𝐻 ∈ Mnd)
54adantl 480 . . . . . 6 (((𝐴 ∈ 𝐡 ∧ 𝑋 ∈ 𝑉) ∧ π‘Š ∈ AssAlg) β†’ 𝐻 ∈ Mnd)
65adantl 480 . . . . 5 ((𝑦 ∈ β„•0 ∧ ((𝐴 ∈ 𝐡 ∧ 𝑋 ∈ 𝑉) ∧ π‘Š ∈ AssAlg)) β†’ 𝐻 ∈ Mnd)
76adantr 479 . . . 4 (((𝑦 ∈ β„•0 ∧ ((𝐴 ∈ 𝐡 ∧ 𝑋 ∈ 𝑉) ∧ π‘Š ∈ AssAlg)) ∧ (𝑦𝐸(𝐴 Β· 𝑋)) = ((𝑦 ↑ 𝐴) Β· (𝑦𝐸𝑋))) β†’ 𝐻 ∈ Mnd)
8 simpll 765 . . . 4 (((𝑦 ∈ β„•0 ∧ ((𝐴 ∈ 𝐡 ∧ 𝑋 ∈ 𝑉) ∧ π‘Š ∈ AssAlg)) ∧ (𝑦𝐸(𝐴 Β· 𝑋)) = ((𝑦 ↑ 𝐴) Β· (𝑦𝐸𝑋))) β†’ 𝑦 ∈ β„•0)
9 assalmod 21798 . . . . . . . 8 (π‘Š ∈ AssAlg β†’ π‘Š ∈ LMod)
109adantl 480 . . . . . . 7 (((𝐴 ∈ 𝐡 ∧ 𝑋 ∈ 𝑉) ∧ π‘Š ∈ AssAlg) β†’ π‘Š ∈ LMod)
11 simpll 765 . . . . . . 7 (((𝐴 ∈ 𝐡 ∧ 𝑋 ∈ 𝑉) ∧ π‘Š ∈ AssAlg) β†’ 𝐴 ∈ 𝐡)
12 simplr 767 . . . . . . 7 (((𝐴 ∈ 𝐡 ∧ 𝑋 ∈ 𝑉) ∧ π‘Š ∈ AssAlg) β†’ 𝑋 ∈ 𝑉)
13 assamulgscm.v . . . . . . . 8 𝑉 = (Baseβ€˜π‘Š)
14 assamulgscm.f . . . . . . . 8 𝐹 = (Scalarβ€˜π‘Š)
15 assamulgscm.s . . . . . . . 8 Β· = ( ·𝑠 β€˜π‘Š)
16 assamulgscm.b . . . . . . . 8 𝐡 = (Baseβ€˜πΉ)
1713, 14, 15, 16lmodvscl 20765 . . . . . . 7 ((π‘Š ∈ LMod ∧ 𝐴 ∈ 𝐡 ∧ 𝑋 ∈ 𝑉) β†’ (𝐴 Β· 𝑋) ∈ 𝑉)
1810, 11, 12, 17syl3anc 1368 . . . . . 6 (((𝐴 ∈ 𝐡 ∧ 𝑋 ∈ 𝑉) ∧ π‘Š ∈ AssAlg) β†’ (𝐴 Β· 𝑋) ∈ 𝑉)
1918adantl 480 . . . . 5 ((𝑦 ∈ β„•0 ∧ ((𝐴 ∈ 𝐡 ∧ 𝑋 ∈ 𝑉) ∧ π‘Š ∈ AssAlg)) β†’ (𝐴 Β· 𝑋) ∈ 𝑉)
2019adantr 479 . . . 4 (((𝑦 ∈ β„•0 ∧ ((𝐴 ∈ 𝐡 ∧ 𝑋 ∈ 𝑉) ∧ π‘Š ∈ AssAlg)) ∧ (𝑦𝐸(𝐴 Β· 𝑋)) = ((𝑦 ↑ 𝐴) Β· (𝑦𝐸𝑋))) β†’ (𝐴 Β· 𝑋) ∈ 𝑉)
212, 13mgpbas 20084 . . . . 5 𝑉 = (Baseβ€˜π»)
22 assamulgscm.e . . . . 5 𝐸 = (.gβ€˜π»)
23 eqid 2725 . . . . . 6 (.rβ€˜π‘Š) = (.rβ€˜π‘Š)
242, 23mgpplusg 20082 . . . . 5 (.rβ€˜π‘Š) = (+gβ€˜π»)
2521, 22, 24mulgnn0p1 19044 . . . 4 ((𝐻 ∈ Mnd ∧ 𝑦 ∈ β„•0 ∧ (𝐴 Β· 𝑋) ∈ 𝑉) β†’ ((𝑦 + 1)𝐸(𝐴 Β· 𝑋)) = ((𝑦𝐸(𝐴 Β· 𝑋))(.rβ€˜π‘Š)(𝐴 Β· 𝑋)))
267, 8, 20, 25syl3anc 1368 . . 3 (((𝑦 ∈ β„•0 ∧ ((𝐴 ∈ 𝐡 ∧ 𝑋 ∈ 𝑉) ∧ π‘Š ∈ AssAlg)) ∧ (𝑦𝐸(𝐴 Β· 𝑋)) = ((𝑦 ↑ 𝐴) Β· (𝑦𝐸𝑋))) β†’ ((𝑦 + 1)𝐸(𝐴 Β· 𝑋)) = ((𝑦𝐸(𝐴 Β· 𝑋))(.rβ€˜π‘Š)(𝐴 Β· 𝑋)))
27 oveq1 7424 . . . 4 ((𝑦𝐸(𝐴 Β· 𝑋)) = ((𝑦 ↑ 𝐴) Β· (𝑦𝐸𝑋)) β†’ ((𝑦𝐸(𝐴 Β· 𝑋))(.rβ€˜π‘Š)(𝐴 Β· 𝑋)) = (((𝑦 ↑ 𝐴) Β· (𝑦𝐸𝑋))(.rβ€˜π‘Š)(𝐴 Β· 𝑋)))
28 simprr 771 . . . . . 6 ((𝑦 ∈ β„•0 ∧ ((𝐴 ∈ 𝐡 ∧ 𝑋 ∈ 𝑉) ∧ π‘Š ∈ AssAlg)) β†’ π‘Š ∈ AssAlg)
29 assamulgscm.g . . . . . . . 8 𝐺 = (mulGrpβ€˜πΉ)
3014eqcomi 2734 . . . . . . . . 9 (Scalarβ€˜π‘Š) = 𝐹
3130fveq2i 6897 . . . . . . . 8 (Baseβ€˜(Scalarβ€˜π‘Š)) = (Baseβ€˜πΉ)
3229, 31mgpbas 20084 . . . . . . 7 (Baseβ€˜(Scalarβ€˜π‘Š)) = (Baseβ€˜πΊ)
33 assamulgscm.p . . . . . . 7 ↑ = (.gβ€˜πΊ)
3414assasca 21800 . . . . . . . . . 10 (π‘Š ∈ AssAlg β†’ 𝐹 ∈ Ring)
3529ringmgp 20183 . . . . . . . . . 10 (𝐹 ∈ Ring β†’ 𝐺 ∈ Mnd)
3634, 35syl 17 . . . . . . . . 9 (π‘Š ∈ AssAlg β†’ 𝐺 ∈ Mnd)
3736adantl 480 . . . . . . . 8 (((𝐴 ∈ 𝐡 ∧ 𝑋 ∈ 𝑉) ∧ π‘Š ∈ AssAlg) β†’ 𝐺 ∈ Mnd)
3837adantl 480 . . . . . . 7 ((𝑦 ∈ β„•0 ∧ ((𝐴 ∈ 𝐡 ∧ 𝑋 ∈ 𝑉) ∧ π‘Š ∈ AssAlg)) β†’ 𝐺 ∈ Mnd)
39 simpl 481 . . . . . . 7 ((𝑦 ∈ β„•0 ∧ ((𝐴 ∈ 𝐡 ∧ 𝑋 ∈ 𝑉) ∧ π‘Š ∈ AssAlg)) β†’ 𝑦 ∈ β„•0)
4016a1i 11 . . . . . . . . . . . . 13 (π‘Š ∈ AssAlg β†’ 𝐡 = (Baseβ€˜πΉ))
4114fveq2i 6897 . . . . . . . . . . . . 13 (Baseβ€˜πΉ) = (Baseβ€˜(Scalarβ€˜π‘Š))
4240, 41eqtrdi 2781 . . . . . . . . . . . 12 (π‘Š ∈ AssAlg β†’ 𝐡 = (Baseβ€˜(Scalarβ€˜π‘Š)))
4342eleq2d 2811 . . . . . . . . . . 11 (π‘Š ∈ AssAlg β†’ (𝐴 ∈ 𝐡 ↔ 𝐴 ∈ (Baseβ€˜(Scalarβ€˜π‘Š))))
4443biimpcd 248 . . . . . . . . . 10 (𝐴 ∈ 𝐡 β†’ (π‘Š ∈ AssAlg β†’ 𝐴 ∈ (Baseβ€˜(Scalarβ€˜π‘Š))))
4544adantr 479 . . . . . . . . 9 ((𝐴 ∈ 𝐡 ∧ 𝑋 ∈ 𝑉) β†’ (π‘Š ∈ AssAlg β†’ 𝐴 ∈ (Baseβ€˜(Scalarβ€˜π‘Š))))
4645imp 405 . . . . . . . 8 (((𝐴 ∈ 𝐡 ∧ 𝑋 ∈ 𝑉) ∧ π‘Š ∈ AssAlg) β†’ 𝐴 ∈ (Baseβ€˜(Scalarβ€˜π‘Š)))
4746adantl 480 . . . . . . 7 ((𝑦 ∈ β„•0 ∧ ((𝐴 ∈ 𝐡 ∧ 𝑋 ∈ 𝑉) ∧ π‘Š ∈ AssAlg)) β†’ 𝐴 ∈ (Baseβ€˜(Scalarβ€˜π‘Š)))
4832, 33, 38, 39, 47mulgnn0cld 19054 . . . . . 6 ((𝑦 ∈ β„•0 ∧ ((𝐴 ∈ 𝐡 ∧ 𝑋 ∈ 𝑉) ∧ π‘Š ∈ AssAlg)) β†’ (𝑦 ↑ 𝐴) ∈ (Baseβ€˜(Scalarβ€˜π‘Š)))
49 simprlr 778 . . . . . . 7 ((𝑦 ∈ β„•0 ∧ ((𝐴 ∈ 𝐡 ∧ 𝑋 ∈ 𝑉) ∧ π‘Š ∈ AssAlg)) β†’ 𝑋 ∈ 𝑉)
5021, 22, 6, 39, 49mulgnn0cld 19054 . . . . . 6 ((𝑦 ∈ β„•0 ∧ ((𝐴 ∈ 𝐡 ∧ 𝑋 ∈ 𝑉) ∧ π‘Š ∈ AssAlg)) β†’ (𝑦𝐸𝑋) ∈ 𝑉)
51 eqid 2725 . . . . . . 7 (Scalarβ€˜π‘Š) = (Scalarβ€˜π‘Š)
52 eqid 2725 . . . . . . 7 (Baseβ€˜(Scalarβ€˜π‘Š)) = (Baseβ€˜(Scalarβ€˜π‘Š))
5313, 51, 52, 15, 23assaass 21796 . . . . . 6 ((π‘Š ∈ AssAlg ∧ ((𝑦 ↑ 𝐴) ∈ (Baseβ€˜(Scalarβ€˜π‘Š)) ∧ (𝑦𝐸𝑋) ∈ 𝑉 ∧ (𝐴 Β· 𝑋) ∈ 𝑉)) β†’ (((𝑦 ↑ 𝐴) Β· (𝑦𝐸𝑋))(.rβ€˜π‘Š)(𝐴 Β· 𝑋)) = ((𝑦 ↑ 𝐴) Β· ((𝑦𝐸𝑋)(.rβ€˜π‘Š)(𝐴 Β· 𝑋))))
5428, 48, 50, 19, 53syl13anc 1369 . . . . 5 ((𝑦 ∈ β„•0 ∧ ((𝐴 ∈ 𝐡 ∧ 𝑋 ∈ 𝑉) ∧ π‘Š ∈ AssAlg)) β†’ (((𝑦 ↑ 𝐴) Β· (𝑦𝐸𝑋))(.rβ€˜π‘Š)(𝐴 Β· 𝑋)) = ((𝑦 ↑ 𝐴) Β· ((𝑦𝐸𝑋)(.rβ€˜π‘Š)(𝐴 Β· 𝑋))))
5513, 51, 52, 15, 23assaassr 21797 . . . . . . . 8 ((π‘Š ∈ AssAlg ∧ (𝐴 ∈ (Baseβ€˜(Scalarβ€˜π‘Š)) ∧ (𝑦𝐸𝑋) ∈ 𝑉 ∧ 𝑋 ∈ 𝑉)) β†’ ((𝑦𝐸𝑋)(.rβ€˜π‘Š)(𝐴 Β· 𝑋)) = (𝐴 Β· ((𝑦𝐸𝑋)(.rβ€˜π‘Š)𝑋)))
5628, 47, 50, 49, 55syl13anc 1369 . . . . . . 7 ((𝑦 ∈ β„•0 ∧ ((𝐴 ∈ 𝐡 ∧ 𝑋 ∈ 𝑉) ∧ π‘Š ∈ AssAlg)) β†’ ((𝑦𝐸𝑋)(.rβ€˜π‘Š)(𝐴 Β· 𝑋)) = (𝐴 Β· ((𝑦𝐸𝑋)(.rβ€˜π‘Š)𝑋)))
5756oveq2d 7433 . . . . . 6 ((𝑦 ∈ β„•0 ∧ ((𝐴 ∈ 𝐡 ∧ 𝑋 ∈ 𝑉) ∧ π‘Š ∈ AssAlg)) β†’ ((𝑦 ↑ 𝐴) Β· ((𝑦𝐸𝑋)(.rβ€˜π‘Š)(𝐴 Β· 𝑋))) = ((𝑦 ↑ 𝐴) Β· (𝐴 Β· ((𝑦𝐸𝑋)(.rβ€˜π‘Š)𝑋))))
5821, 22, 24mulgnn0p1 19044 . . . . . . . . . 10 ((𝐻 ∈ Mnd ∧ 𝑦 ∈ β„•0 ∧ 𝑋 ∈ 𝑉) β†’ ((𝑦 + 1)𝐸𝑋) = ((𝑦𝐸𝑋)(.rβ€˜π‘Š)𝑋))
596, 39, 49, 58syl3anc 1368 . . . . . . . . 9 ((𝑦 ∈ β„•0 ∧ ((𝐴 ∈ 𝐡 ∧ 𝑋 ∈ 𝑉) ∧ π‘Š ∈ AssAlg)) β†’ ((𝑦 + 1)𝐸𝑋) = ((𝑦𝐸𝑋)(.rβ€˜π‘Š)𝑋))
6059eqcomd 2731 . . . . . . . 8 ((𝑦 ∈ β„•0 ∧ ((𝐴 ∈ 𝐡 ∧ 𝑋 ∈ 𝑉) ∧ π‘Š ∈ AssAlg)) β†’ ((𝑦𝐸𝑋)(.rβ€˜π‘Š)𝑋) = ((𝑦 + 1)𝐸𝑋))
6160oveq2d 7433 . . . . . . 7 ((𝑦 ∈ β„•0 ∧ ((𝐴 ∈ 𝐡 ∧ 𝑋 ∈ 𝑉) ∧ π‘Š ∈ AssAlg)) β†’ (𝐴 Β· ((𝑦𝐸𝑋)(.rβ€˜π‘Š)𝑋)) = (𝐴 Β· ((𝑦 + 1)𝐸𝑋)))
6261oveq2d 7433 . . . . . 6 ((𝑦 ∈ β„•0 ∧ ((𝐴 ∈ 𝐡 ∧ 𝑋 ∈ 𝑉) ∧ π‘Š ∈ AssAlg)) β†’ ((𝑦 ↑ 𝐴) Β· (𝐴 Β· ((𝑦𝐸𝑋)(.rβ€˜π‘Š)𝑋))) = ((𝑦 ↑ 𝐴) Β· (𝐴 Β· ((𝑦 + 1)𝐸𝑋))))
6310adantl 480 . . . . . . 7 ((𝑦 ∈ β„•0 ∧ ((𝐴 ∈ 𝐡 ∧ 𝑋 ∈ 𝑉) ∧ π‘Š ∈ AssAlg)) β†’ π‘Š ∈ LMod)
64 peano2nn0 12542 . . . . . . . . 9 (𝑦 ∈ β„•0 β†’ (𝑦 + 1) ∈ β„•0)
6564adantr 479 . . . . . . . 8 ((𝑦 ∈ β„•0 ∧ ((𝐴 ∈ 𝐡 ∧ 𝑋 ∈ 𝑉) ∧ π‘Š ∈ AssAlg)) β†’ (𝑦 + 1) ∈ β„•0)
6621, 22, 6, 65, 49mulgnn0cld 19054 . . . . . . 7 ((𝑦 ∈ β„•0 ∧ ((𝐴 ∈ 𝐡 ∧ 𝑋 ∈ 𝑉) ∧ π‘Š ∈ AssAlg)) β†’ ((𝑦 + 1)𝐸𝑋) ∈ 𝑉)
67 eqid 2725 . . . . . . . . 9 (.rβ€˜(Scalarβ€˜π‘Š)) = (.rβ€˜(Scalarβ€˜π‘Š))
6813, 51, 15, 52, 67lmodvsass 20774 . . . . . . . 8 ((π‘Š ∈ LMod ∧ ((𝑦 ↑ 𝐴) ∈ (Baseβ€˜(Scalarβ€˜π‘Š)) ∧ 𝐴 ∈ (Baseβ€˜(Scalarβ€˜π‘Š)) ∧ ((𝑦 + 1)𝐸𝑋) ∈ 𝑉)) β†’ (((𝑦 ↑ 𝐴)(.rβ€˜(Scalarβ€˜π‘Š))𝐴) Β· ((𝑦 + 1)𝐸𝑋)) = ((𝑦 ↑ 𝐴) Β· (𝐴 Β· ((𝑦 + 1)𝐸𝑋))))
6968eqcomd 2731 . . . . . . 7 ((π‘Š ∈ LMod ∧ ((𝑦 ↑ 𝐴) ∈ (Baseβ€˜(Scalarβ€˜π‘Š)) ∧ 𝐴 ∈ (Baseβ€˜(Scalarβ€˜π‘Š)) ∧ ((𝑦 + 1)𝐸𝑋) ∈ 𝑉)) β†’ ((𝑦 ↑ 𝐴) Β· (𝐴 Β· ((𝑦 + 1)𝐸𝑋))) = (((𝑦 ↑ 𝐴)(.rβ€˜(Scalarβ€˜π‘Š))𝐴) Β· ((𝑦 + 1)𝐸𝑋)))
7063, 48, 47, 66, 69syl13anc 1369 . . . . . 6 ((𝑦 ∈ β„•0 ∧ ((𝐴 ∈ 𝐡 ∧ 𝑋 ∈ 𝑉) ∧ π‘Š ∈ AssAlg)) β†’ ((𝑦 ↑ 𝐴) Β· (𝐴 Β· ((𝑦 + 1)𝐸𝑋))) = (((𝑦 ↑ 𝐴)(.rβ€˜(Scalarβ€˜π‘Š))𝐴) Β· ((𝑦 + 1)𝐸𝑋)))
7157, 62, 703eqtrd 2769 . . . . 5 ((𝑦 ∈ β„•0 ∧ ((𝐴 ∈ 𝐡 ∧ 𝑋 ∈ 𝑉) ∧ π‘Š ∈ AssAlg)) β†’ ((𝑦 ↑ 𝐴) Β· ((𝑦𝐸𝑋)(.rβ€˜π‘Š)(𝐴 Β· 𝑋))) = (((𝑦 ↑ 𝐴)(.rβ€˜(Scalarβ€˜π‘Š))𝐴) Β· ((𝑦 + 1)𝐸𝑋)))
72 simprll 777 . . . . . . . . 9 ((𝑦 ∈ β„•0 ∧ ((𝐴 ∈ 𝐡 ∧ 𝑋 ∈ 𝑉) ∧ π‘Š ∈ AssAlg)) β†’ 𝐴 ∈ 𝐡)
7329, 16mgpbas 20084 . . . . . . . . . 10 𝐡 = (Baseβ€˜πΊ)
74 eqid 2725 . . . . . . . . . . 11 (.rβ€˜πΉ) = (.rβ€˜πΉ)
7529, 74mgpplusg 20082 . . . . . . . . . 10 (.rβ€˜πΉ) = (+gβ€˜πΊ)
7673, 33, 75mulgnn0p1 19044 . . . . . . . . 9 ((𝐺 ∈ Mnd ∧ 𝑦 ∈ β„•0 ∧ 𝐴 ∈ 𝐡) β†’ ((𝑦 + 1) ↑ 𝐴) = ((𝑦 ↑ 𝐴)(.rβ€˜πΉ)𝐴))
7738, 39, 72, 76syl3anc 1368 . . . . . . . 8 ((𝑦 ∈ β„•0 ∧ ((𝐴 ∈ 𝐡 ∧ 𝑋 ∈ 𝑉) ∧ π‘Š ∈ AssAlg)) β†’ ((𝑦 + 1) ↑ 𝐴) = ((𝑦 ↑ 𝐴)(.rβ€˜πΉ)𝐴))
7814a1i 11 . . . . . . . . . 10 ((𝑦 ∈ β„•0 ∧ ((𝐴 ∈ 𝐡 ∧ 𝑋 ∈ 𝑉) ∧ π‘Š ∈ AssAlg)) β†’ 𝐹 = (Scalarβ€˜π‘Š))
7978fveq2d 6898 . . . . . . . . 9 ((𝑦 ∈ β„•0 ∧ ((𝐴 ∈ 𝐡 ∧ 𝑋 ∈ 𝑉) ∧ π‘Š ∈ AssAlg)) β†’ (.rβ€˜πΉ) = (.rβ€˜(Scalarβ€˜π‘Š)))
8079oveqd 7434 . . . . . . . 8 ((𝑦 ∈ β„•0 ∧ ((𝐴 ∈ 𝐡 ∧ 𝑋 ∈ 𝑉) ∧ π‘Š ∈ AssAlg)) β†’ ((𝑦 ↑ 𝐴)(.rβ€˜πΉ)𝐴) = ((𝑦 ↑ 𝐴)(.rβ€˜(Scalarβ€˜π‘Š))𝐴))
8177, 80eqtrd 2765 . . . . . . 7 ((𝑦 ∈ β„•0 ∧ ((𝐴 ∈ 𝐡 ∧ 𝑋 ∈ 𝑉) ∧ π‘Š ∈ AssAlg)) β†’ ((𝑦 + 1) ↑ 𝐴) = ((𝑦 ↑ 𝐴)(.rβ€˜(Scalarβ€˜π‘Š))𝐴))
8281eqcomd 2731 . . . . . 6 ((𝑦 ∈ β„•0 ∧ ((𝐴 ∈ 𝐡 ∧ 𝑋 ∈ 𝑉) ∧ π‘Š ∈ AssAlg)) β†’ ((𝑦 ↑ 𝐴)(.rβ€˜(Scalarβ€˜π‘Š))𝐴) = ((𝑦 + 1) ↑ 𝐴))
8382oveq1d 7432 . . . . 5 ((𝑦 ∈ β„•0 ∧ ((𝐴 ∈ 𝐡 ∧ 𝑋 ∈ 𝑉) ∧ π‘Š ∈ AssAlg)) β†’ (((𝑦 ↑ 𝐴)(.rβ€˜(Scalarβ€˜π‘Š))𝐴) Β· ((𝑦 + 1)𝐸𝑋)) = (((𝑦 + 1) ↑ 𝐴) Β· ((𝑦 + 1)𝐸𝑋)))
8454, 71, 833eqtrd 2769 . . . 4 ((𝑦 ∈ β„•0 ∧ ((𝐴 ∈ 𝐡 ∧ 𝑋 ∈ 𝑉) ∧ π‘Š ∈ AssAlg)) β†’ (((𝑦 ↑ 𝐴) Β· (𝑦𝐸𝑋))(.rβ€˜π‘Š)(𝐴 Β· 𝑋)) = (((𝑦 + 1) ↑ 𝐴) Β· ((𝑦 + 1)𝐸𝑋)))
8527, 84sylan9eqr 2787 . . 3 (((𝑦 ∈ β„•0 ∧ ((𝐴 ∈ 𝐡 ∧ 𝑋 ∈ 𝑉) ∧ π‘Š ∈ AssAlg)) ∧ (𝑦𝐸(𝐴 Β· 𝑋)) = ((𝑦 ↑ 𝐴) Β· (𝑦𝐸𝑋))) β†’ ((𝑦𝐸(𝐴 Β· 𝑋))(.rβ€˜π‘Š)(𝐴 Β· 𝑋)) = (((𝑦 + 1) ↑ 𝐴) Β· ((𝑦 + 1)𝐸𝑋)))
8626, 85eqtrd 2765 . 2 (((𝑦 ∈ β„•0 ∧ ((𝐴 ∈ 𝐡 ∧ 𝑋 ∈ 𝑉) ∧ π‘Š ∈ AssAlg)) ∧ (𝑦𝐸(𝐴 Β· 𝑋)) = ((𝑦 ↑ 𝐴) Β· (𝑦𝐸𝑋))) β†’ ((𝑦 + 1)𝐸(𝐴 Β· 𝑋)) = (((𝑦 + 1) ↑ 𝐴) Β· ((𝑦 + 1)𝐸𝑋)))
8786exp31 418 1 (𝑦 ∈ β„•0 β†’ (((𝐴 ∈ 𝐡 ∧ 𝑋 ∈ 𝑉) ∧ π‘Š ∈ AssAlg) β†’ ((𝑦𝐸(𝐴 Β· 𝑋)) = ((𝑦 ↑ 𝐴) Β· (𝑦𝐸𝑋)) β†’ ((𝑦 + 1)𝐸(𝐴 Β· 𝑋)) = (((𝑦 + 1) ↑ 𝐴) Β· ((𝑦 + 1)𝐸𝑋)))))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ∧ wa 394   ∧ w3a 1084   = wceq 1533   ∈ wcel 2098  β€˜cfv 6547  (class class class)co 7417  1c1 11139   + caddc 11141  β„•0cn0 12502  Basecbs 17179  .rcmulr 17233  Scalarcsca 17235   ·𝑠 cvsca 17236  Mndcmnd 18693  .gcmg 19027  mulGrpcmgp 20078  Ringcrg 20177  LModclmod 20747  AssAlgcasa 21788
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2696  ax-sep 5299  ax-nul 5306  ax-pow 5364  ax-pr 5428  ax-un 7739  ax-cnex 11194  ax-resscn 11195  ax-1cn 11196  ax-icn 11197  ax-addcl 11198  ax-addrcl 11199  ax-mulcl 11200  ax-mulrcl 11201  ax-mulcom 11202  ax-addass 11203  ax-mulass 11204  ax-distr 11205  ax-i2m1 11206  ax-1ne0 11207  ax-1rid 11208  ax-rnegex 11209  ax-rrecex 11210  ax-cnre 11211  ax-pre-lttri 11212  ax-pre-lttrn 11213  ax-pre-ltadd 11214  ax-pre-mulgt0 11215
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-ne 2931  df-nel 3037  df-ral 3052  df-rex 3061  df-rmo 3364  df-reu 3365  df-rab 3420  df-v 3465  df-sbc 3775  df-csb 3891  df-dif 3948  df-un 3950  df-in 3952  df-ss 3962  df-pss 3965  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4909  df-iun 4998  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5575  df-eprel 5581  df-po 5589  df-so 5590  df-fr 5632  df-we 5634  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-pred 6305  df-ord 6372  df-on 6373  df-lim 6374  df-suc 6375  df-iota 6499  df-fun 6549  df-fn 6550  df-f 6551  df-f1 6552  df-fo 6553  df-f1o 6554  df-fv 6555  df-riota 7373  df-ov 7420  df-oprab 7421  df-mpo 7422  df-om 7870  df-1st 7992  df-2nd 7993  df-frecs 8285  df-wrecs 8316  df-recs 8390  df-rdg 8429  df-er 8723  df-en 8963  df-dom 8964  df-sdom 8965  df-pnf 11280  df-mnf 11281  df-xr 11282  df-ltxr 11283  df-le 11284  df-sub 11476  df-neg 11477  df-nn 12243  df-2 12305  df-n0 12503  df-z 12589  df-uz 12853  df-fz 13517  df-seq 13999  df-sets 17132  df-slot 17150  df-ndx 17162  df-base 17180  df-plusg 17245  df-0g 17422  df-mgm 18599  df-sgrp 18678  df-mnd 18694  df-mulg 19028  df-mgp 20079  df-ring 20179  df-lmod 20749  df-assa 21791
This theorem is referenced by:  assamulgscm  21838
  Copyright terms: Public domain W3C validator