Metamath Proof Explorer


Theorem coe1mul2

Description: The coefficient vector of multiplication in the univariate power series ring. (Contributed by Stefan O'Rear, 25-Mar-2015)

Ref Expression
Hypotheses coe1mul2.s 𝑆 = ( PwSer1𝑅 )
coe1mul2.t = ( .r𝑆 )
coe1mul2.u · = ( .r𝑅 )
coe1mul2.b 𝐵 = ( Base ‘ 𝑆 )
Assertion coe1mul2 ( ( 𝑅 ∈ Ring ∧ 𝐹𝐵𝐺𝐵 ) → ( coe1 ‘ ( 𝐹 𝐺 ) ) = ( 𝑘 ∈ ℕ0 ↦ ( 𝑅 Σg ( 𝑥 ∈ ( 0 ... 𝑘 ) ↦ ( ( ( coe1𝐹 ) ‘ 𝑥 ) · ( ( coe1𝐺 ) ‘ ( 𝑘𝑥 ) ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 coe1mul2.s 𝑆 = ( PwSer1𝑅 )
2 coe1mul2.t = ( .r𝑆 )
3 coe1mul2.u · = ( .r𝑅 )
4 coe1mul2.b 𝐵 = ( Base ‘ 𝑆 )
5 fconst6g ( 𝑘 ∈ ℕ0 → ( 1o × { 𝑘 } ) : 1o ⟶ ℕ0 )
6 nn0ex 0 ∈ V
7 1on 1o ∈ On
8 7 elexi 1o ∈ V
9 6 8 elmap ( ( 1o × { 𝑘 } ) ∈ ( ℕ0m 1o ) ↔ ( 1o × { 𝑘 } ) : 1o ⟶ ℕ0 )
10 5 9 sylibr ( 𝑘 ∈ ℕ0 → ( 1o × { 𝑘 } ) ∈ ( ℕ0m 1o ) )
11 10 adantl ( ( ( 𝑅 ∈ Ring ∧ 𝐹𝐵𝐺𝐵 ) ∧ 𝑘 ∈ ℕ0 ) → ( 1o × { 𝑘 } ) ∈ ( ℕ0m 1o ) )
12 eqidd ( ( 𝑅 ∈ Ring ∧ 𝐹𝐵𝐺𝐵 ) → ( 𝑘 ∈ ℕ0 ↦ ( 1o × { 𝑘 } ) ) = ( 𝑘 ∈ ℕ0 ↦ ( 1o × { 𝑘 } ) ) )
13 eqid ( 1o mPwSer 𝑅 ) = ( 1o mPwSer 𝑅 )
14 1 4 13 psr1bas2 𝐵 = ( Base ‘ ( 1o mPwSer 𝑅 ) )
15 1 13 2 psr1mulr = ( .r ‘ ( 1o mPwSer 𝑅 ) )
16 psr1baslem ( ℕ0m 1o ) = { 𝑎 ∈ ( ℕ0m 1o ) ∣ ( 𝑎 “ ℕ ) ∈ Fin }
17 simp2 ( ( 𝑅 ∈ Ring ∧ 𝐹𝐵𝐺𝐵 ) → 𝐹𝐵 )
18 simp3 ( ( 𝑅 ∈ Ring ∧ 𝐹𝐵𝐺𝐵 ) → 𝐺𝐵 )
19 13 14 3 15 16 17 18 psrmulfval ( ( 𝑅 ∈ Ring ∧ 𝐹𝐵𝐺𝐵 ) → ( 𝐹 𝐺 ) = ( 𝑏 ∈ ( ℕ0m 1o ) ↦ ( 𝑅 Σg ( 𝑐 ∈ { 𝑑 ∈ ( ℕ0m 1o ) ∣ 𝑑r𝑏 } ↦ ( ( 𝐹𝑐 ) · ( 𝐺 ‘ ( 𝑏f𝑐 ) ) ) ) ) ) )
20 breq2 ( 𝑏 = ( 1o × { 𝑘 } ) → ( 𝑑r𝑏𝑑r ≤ ( 1o × { 𝑘 } ) ) )
21 20 rabbidv ( 𝑏 = ( 1o × { 𝑘 } ) → { 𝑑 ∈ ( ℕ0m 1o ) ∣ 𝑑r𝑏 } = { 𝑑 ∈ ( ℕ0m 1o ) ∣ 𝑑r ≤ ( 1o × { 𝑘 } ) } )
22 fvoveq1 ( 𝑏 = ( 1o × { 𝑘 } ) → ( 𝐺 ‘ ( 𝑏f𝑐 ) ) = ( 𝐺 ‘ ( ( 1o × { 𝑘 } ) ∘f𝑐 ) ) )
23 22 oveq2d ( 𝑏 = ( 1o × { 𝑘 } ) → ( ( 𝐹𝑐 ) · ( 𝐺 ‘ ( 𝑏f𝑐 ) ) ) = ( ( 𝐹𝑐 ) · ( 𝐺 ‘ ( ( 1o × { 𝑘 } ) ∘f𝑐 ) ) ) )
24 21 23 mpteq12dv ( 𝑏 = ( 1o × { 𝑘 } ) → ( 𝑐 ∈ { 𝑑 ∈ ( ℕ0m 1o ) ∣ 𝑑r𝑏 } ↦ ( ( 𝐹𝑐 ) · ( 𝐺 ‘ ( 𝑏f𝑐 ) ) ) ) = ( 𝑐 ∈ { 𝑑 ∈ ( ℕ0m 1o ) ∣ 𝑑r ≤ ( 1o × { 𝑘 } ) } ↦ ( ( 𝐹𝑐 ) · ( 𝐺 ‘ ( ( 1o × { 𝑘 } ) ∘f𝑐 ) ) ) ) )
25 24 oveq2d ( 𝑏 = ( 1o × { 𝑘 } ) → ( 𝑅 Σg ( 𝑐 ∈ { 𝑑 ∈ ( ℕ0m 1o ) ∣ 𝑑r𝑏 } ↦ ( ( 𝐹𝑐 ) · ( 𝐺 ‘ ( 𝑏f𝑐 ) ) ) ) ) = ( 𝑅 Σg ( 𝑐 ∈ { 𝑑 ∈ ( ℕ0m 1o ) ∣ 𝑑r ≤ ( 1o × { 𝑘 } ) } ↦ ( ( 𝐹𝑐 ) · ( 𝐺 ‘ ( ( 1o × { 𝑘 } ) ∘f𝑐 ) ) ) ) ) )
26 11 12 19 25 fmptco ( ( 𝑅 ∈ Ring ∧ 𝐹𝐵𝐺𝐵 ) → ( ( 𝐹 𝐺 ) ∘ ( 𝑘 ∈ ℕ0 ↦ ( 1o × { 𝑘 } ) ) ) = ( 𝑘 ∈ ℕ0 ↦ ( 𝑅 Σg ( 𝑐 ∈ { 𝑑 ∈ ( ℕ0m 1o ) ∣ 𝑑r ≤ ( 1o × { 𝑘 } ) } ↦ ( ( 𝐹𝑐 ) · ( 𝐺 ‘ ( ( 1o × { 𝑘 } ) ∘f𝑐 ) ) ) ) ) ) )
27 1 psr1ring ( 𝑅 ∈ Ring → 𝑆 ∈ Ring )
28 4 2 ringcl ( ( 𝑆 ∈ Ring ∧ 𝐹𝐵𝐺𝐵 ) → ( 𝐹 𝐺 ) ∈ 𝐵 )
29 27 28 syl3an1 ( ( 𝑅 ∈ Ring ∧ 𝐹𝐵𝐺𝐵 ) → ( 𝐹 𝐺 ) ∈ 𝐵 )
30 eqid ( coe1 ‘ ( 𝐹 𝐺 ) ) = ( coe1 ‘ ( 𝐹 𝐺 ) )
31 eqid ( 𝑘 ∈ ℕ0 ↦ ( 1o × { 𝑘 } ) ) = ( 𝑘 ∈ ℕ0 ↦ ( 1o × { 𝑘 } ) )
32 30 4 1 31 coe1fval3 ( ( 𝐹 𝐺 ) ∈ 𝐵 → ( coe1 ‘ ( 𝐹 𝐺 ) ) = ( ( 𝐹 𝐺 ) ∘ ( 𝑘 ∈ ℕ0 ↦ ( 1o × { 𝑘 } ) ) ) )
33 29 32 syl ( ( 𝑅 ∈ Ring ∧ 𝐹𝐵𝐺𝐵 ) → ( coe1 ‘ ( 𝐹 𝐺 ) ) = ( ( 𝐹 𝐺 ) ∘ ( 𝑘 ∈ ℕ0 ↦ ( 1o × { 𝑘 } ) ) ) )
34 eqid ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
35 eqid ( 0g𝑅 ) = ( 0g𝑅 )
36 simpl1 ( ( ( 𝑅 ∈ Ring ∧ 𝐹𝐵𝐺𝐵 ) ∧ 𝑘 ∈ ℕ0 ) → 𝑅 ∈ Ring )
37 ringcmn ( 𝑅 ∈ Ring → 𝑅 ∈ CMnd )
38 36 37 syl ( ( ( 𝑅 ∈ Ring ∧ 𝐹𝐵𝐺𝐵 ) ∧ 𝑘 ∈ ℕ0 ) → 𝑅 ∈ CMnd )
39 fzfi ( 0 ... 𝑘 ) ∈ Fin
40 39 a1i ( ( ( 𝑅 ∈ Ring ∧ 𝐹𝐵𝐺𝐵 ) ∧ 𝑘 ∈ ℕ0 ) → ( 0 ... 𝑘 ) ∈ Fin )
41 simpll1 ( ( ( ( 𝑅 ∈ Ring ∧ 𝐹𝐵𝐺𝐵 ) ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑥 ∈ ( 0 ... 𝑘 ) ) → 𝑅 ∈ Ring )
42 simpll2 ( ( ( ( 𝑅 ∈ Ring ∧ 𝐹𝐵𝐺𝐵 ) ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑥 ∈ ( 0 ... 𝑘 ) ) → 𝐹𝐵 )
43 eqid ( coe1𝐹 ) = ( coe1𝐹 )
44 43 4 1 34 coe1f2 ( 𝐹𝐵 → ( coe1𝐹 ) : ℕ0 ⟶ ( Base ‘ 𝑅 ) )
45 42 44 syl ( ( ( ( 𝑅 ∈ Ring ∧ 𝐹𝐵𝐺𝐵 ) ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑥 ∈ ( 0 ... 𝑘 ) ) → ( coe1𝐹 ) : ℕ0 ⟶ ( Base ‘ 𝑅 ) )
46 elfznn0 ( 𝑥 ∈ ( 0 ... 𝑘 ) → 𝑥 ∈ ℕ0 )
47 46 adantl ( ( ( ( 𝑅 ∈ Ring ∧ 𝐹𝐵𝐺𝐵 ) ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑥 ∈ ( 0 ... 𝑘 ) ) → 𝑥 ∈ ℕ0 )
48 45 47 ffvelrnd ( ( ( ( 𝑅 ∈ Ring ∧ 𝐹𝐵𝐺𝐵 ) ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑥 ∈ ( 0 ... 𝑘 ) ) → ( ( coe1𝐹 ) ‘ 𝑥 ) ∈ ( Base ‘ 𝑅 ) )
49 simpll3 ( ( ( ( 𝑅 ∈ Ring ∧ 𝐹𝐵𝐺𝐵 ) ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑥 ∈ ( 0 ... 𝑘 ) ) → 𝐺𝐵 )
50 eqid ( coe1𝐺 ) = ( coe1𝐺 )
51 50 4 1 34 coe1f2 ( 𝐺𝐵 → ( coe1𝐺 ) : ℕ0 ⟶ ( Base ‘ 𝑅 ) )
52 49 51 syl ( ( ( ( 𝑅 ∈ Ring ∧ 𝐹𝐵𝐺𝐵 ) ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑥 ∈ ( 0 ... 𝑘 ) ) → ( coe1𝐺 ) : ℕ0 ⟶ ( Base ‘ 𝑅 ) )
53 fznn0sub ( 𝑥 ∈ ( 0 ... 𝑘 ) → ( 𝑘𝑥 ) ∈ ℕ0 )
54 53 adantl ( ( ( ( 𝑅 ∈ Ring ∧ 𝐹𝐵𝐺𝐵 ) ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑥 ∈ ( 0 ... 𝑘 ) ) → ( 𝑘𝑥 ) ∈ ℕ0 )
55 52 54 ffvelrnd ( ( ( ( 𝑅 ∈ Ring ∧ 𝐹𝐵𝐺𝐵 ) ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑥 ∈ ( 0 ... 𝑘 ) ) → ( ( coe1𝐺 ) ‘ ( 𝑘𝑥 ) ) ∈ ( Base ‘ 𝑅 ) )
56 34 3 ringcl ( ( 𝑅 ∈ Ring ∧ ( ( coe1𝐹 ) ‘ 𝑥 ) ∈ ( Base ‘ 𝑅 ) ∧ ( ( coe1𝐺 ) ‘ ( 𝑘𝑥 ) ) ∈ ( Base ‘ 𝑅 ) ) → ( ( ( coe1𝐹 ) ‘ 𝑥 ) · ( ( coe1𝐺 ) ‘ ( 𝑘𝑥 ) ) ) ∈ ( Base ‘ 𝑅 ) )
57 41 48 55 56 syl3anc ( ( ( ( 𝑅 ∈ Ring ∧ 𝐹𝐵𝐺𝐵 ) ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑥 ∈ ( 0 ... 𝑘 ) ) → ( ( ( coe1𝐹 ) ‘ 𝑥 ) · ( ( coe1𝐺 ) ‘ ( 𝑘𝑥 ) ) ) ∈ ( Base ‘ 𝑅 ) )
58 57 fmpttd ( ( ( 𝑅 ∈ Ring ∧ 𝐹𝐵𝐺𝐵 ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝑥 ∈ ( 0 ... 𝑘 ) ↦ ( ( ( coe1𝐹 ) ‘ 𝑥 ) · ( ( coe1𝐺 ) ‘ ( 𝑘𝑥 ) ) ) ) : ( 0 ... 𝑘 ) ⟶ ( Base ‘ 𝑅 ) )
59 39 elexi ( 0 ... 𝑘 ) ∈ V
60 59 mptex ( 𝑥 ∈ ( 0 ... 𝑘 ) ↦ ( ( ( coe1𝐹 ) ‘ 𝑥 ) · ( ( coe1𝐺 ) ‘ ( 𝑘𝑥 ) ) ) ) ∈ V
61 funmpt Fun ( 𝑥 ∈ ( 0 ... 𝑘 ) ↦ ( ( ( coe1𝐹 ) ‘ 𝑥 ) · ( ( coe1𝐺 ) ‘ ( 𝑘𝑥 ) ) ) )
62 fvex ( 0g𝑅 ) ∈ V
63 60 61 62 3pm3.2i ( ( 𝑥 ∈ ( 0 ... 𝑘 ) ↦ ( ( ( coe1𝐹 ) ‘ 𝑥 ) · ( ( coe1𝐺 ) ‘ ( 𝑘𝑥 ) ) ) ) ∈ V ∧ Fun ( 𝑥 ∈ ( 0 ... 𝑘 ) ↦ ( ( ( coe1𝐹 ) ‘ 𝑥 ) · ( ( coe1𝐺 ) ‘ ( 𝑘𝑥 ) ) ) ) ∧ ( 0g𝑅 ) ∈ V )
64 suppssdm ( ( 𝑥 ∈ ( 0 ... 𝑘 ) ↦ ( ( ( coe1𝐹 ) ‘ 𝑥 ) · ( ( coe1𝐺 ) ‘ ( 𝑘𝑥 ) ) ) ) supp ( 0g𝑅 ) ) ⊆ dom ( 𝑥 ∈ ( 0 ... 𝑘 ) ↦ ( ( ( coe1𝐹 ) ‘ 𝑥 ) · ( ( coe1𝐺 ) ‘ ( 𝑘𝑥 ) ) ) )
65 eqid ( 𝑥 ∈ ( 0 ... 𝑘 ) ↦ ( ( ( coe1𝐹 ) ‘ 𝑥 ) · ( ( coe1𝐺 ) ‘ ( 𝑘𝑥 ) ) ) ) = ( 𝑥 ∈ ( 0 ... 𝑘 ) ↦ ( ( ( coe1𝐹 ) ‘ 𝑥 ) · ( ( coe1𝐺 ) ‘ ( 𝑘𝑥 ) ) ) )
66 65 dmmptss dom ( 𝑥 ∈ ( 0 ... 𝑘 ) ↦ ( ( ( coe1𝐹 ) ‘ 𝑥 ) · ( ( coe1𝐺 ) ‘ ( 𝑘𝑥 ) ) ) ) ⊆ ( 0 ... 𝑘 )
67 64 66 sstri ( ( 𝑥 ∈ ( 0 ... 𝑘 ) ↦ ( ( ( coe1𝐹 ) ‘ 𝑥 ) · ( ( coe1𝐺 ) ‘ ( 𝑘𝑥 ) ) ) ) supp ( 0g𝑅 ) ) ⊆ ( 0 ... 𝑘 )
68 39 67 pm3.2i ( ( 0 ... 𝑘 ) ∈ Fin ∧ ( ( 𝑥 ∈ ( 0 ... 𝑘 ) ↦ ( ( ( coe1𝐹 ) ‘ 𝑥 ) · ( ( coe1𝐺 ) ‘ ( 𝑘𝑥 ) ) ) ) supp ( 0g𝑅 ) ) ⊆ ( 0 ... 𝑘 ) )
69 suppssfifsupp ( ( ( ( 𝑥 ∈ ( 0 ... 𝑘 ) ↦ ( ( ( coe1𝐹 ) ‘ 𝑥 ) · ( ( coe1𝐺 ) ‘ ( 𝑘𝑥 ) ) ) ) ∈ V ∧ Fun ( 𝑥 ∈ ( 0 ... 𝑘 ) ↦ ( ( ( coe1𝐹 ) ‘ 𝑥 ) · ( ( coe1𝐺 ) ‘ ( 𝑘𝑥 ) ) ) ) ∧ ( 0g𝑅 ) ∈ V ) ∧ ( ( 0 ... 𝑘 ) ∈ Fin ∧ ( ( 𝑥 ∈ ( 0 ... 𝑘 ) ↦ ( ( ( coe1𝐹 ) ‘ 𝑥 ) · ( ( coe1𝐺 ) ‘ ( 𝑘𝑥 ) ) ) ) supp ( 0g𝑅 ) ) ⊆ ( 0 ... 𝑘 ) ) ) → ( 𝑥 ∈ ( 0 ... 𝑘 ) ↦ ( ( ( coe1𝐹 ) ‘ 𝑥 ) · ( ( coe1𝐺 ) ‘ ( 𝑘𝑥 ) ) ) ) finSupp ( 0g𝑅 ) )
70 63 68 69 mp2an ( 𝑥 ∈ ( 0 ... 𝑘 ) ↦ ( ( ( coe1𝐹 ) ‘ 𝑥 ) · ( ( coe1𝐺 ) ‘ ( 𝑘𝑥 ) ) ) ) finSupp ( 0g𝑅 )
71 70 a1i ( ( ( 𝑅 ∈ Ring ∧ 𝐹𝐵𝐺𝐵 ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝑥 ∈ ( 0 ... 𝑘 ) ↦ ( ( ( coe1𝐹 ) ‘ 𝑥 ) · ( ( coe1𝐺 ) ‘ ( 𝑘𝑥 ) ) ) ) finSupp ( 0g𝑅 ) )
72 eqid { 𝑑 ∈ ( ℕ0m 1o ) ∣ 𝑑r ≤ ( 1o × { 𝑘 } ) } = { 𝑑 ∈ ( ℕ0m 1o ) ∣ 𝑑r ≤ ( 1o × { 𝑘 } ) }
73 72 coe1mul2lem2 ( 𝑘 ∈ ℕ0 → ( 𝑐 ∈ { 𝑑 ∈ ( ℕ0m 1o ) ∣ 𝑑r ≤ ( 1o × { 𝑘 } ) } ↦ ( 𝑐 ‘ ∅ ) ) : { 𝑑 ∈ ( ℕ0m 1o ) ∣ 𝑑r ≤ ( 1o × { 𝑘 } ) } –1-1-onto→ ( 0 ... 𝑘 ) )
74 73 adantl ( ( ( 𝑅 ∈ Ring ∧ 𝐹𝐵𝐺𝐵 ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝑐 ∈ { 𝑑 ∈ ( ℕ0m 1o ) ∣ 𝑑r ≤ ( 1o × { 𝑘 } ) } ↦ ( 𝑐 ‘ ∅ ) ) : { 𝑑 ∈ ( ℕ0m 1o ) ∣ 𝑑r ≤ ( 1o × { 𝑘 } ) } –1-1-onto→ ( 0 ... 𝑘 ) )
75 34 35 38 40 58 71 74 gsumf1o ( ( ( 𝑅 ∈ Ring ∧ 𝐹𝐵𝐺𝐵 ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝑅 Σg ( 𝑥 ∈ ( 0 ... 𝑘 ) ↦ ( ( ( coe1𝐹 ) ‘ 𝑥 ) · ( ( coe1𝐺 ) ‘ ( 𝑘𝑥 ) ) ) ) ) = ( 𝑅 Σg ( ( 𝑥 ∈ ( 0 ... 𝑘 ) ↦ ( ( ( coe1𝐹 ) ‘ 𝑥 ) · ( ( coe1𝐺 ) ‘ ( 𝑘𝑥 ) ) ) ) ∘ ( 𝑐 ∈ { 𝑑 ∈ ( ℕ0m 1o ) ∣ 𝑑r ≤ ( 1o × { 𝑘 } ) } ↦ ( 𝑐 ‘ ∅ ) ) ) ) )
76 breq1 ( 𝑑 = 𝑐 → ( 𝑑r ≤ ( 1o × { 𝑘 } ) ↔ 𝑐r ≤ ( 1o × { 𝑘 } ) ) )
77 76 elrab ( 𝑐 ∈ { 𝑑 ∈ ( ℕ0m 1o ) ∣ 𝑑r ≤ ( 1o × { 𝑘 } ) } ↔ ( 𝑐 ∈ ( ℕ0m 1o ) ∧ 𝑐r ≤ ( 1o × { 𝑘 } ) ) )
78 77 simprbi ( 𝑐 ∈ { 𝑑 ∈ ( ℕ0m 1o ) ∣ 𝑑r ≤ ( 1o × { 𝑘 } ) } → 𝑐r ≤ ( 1o × { 𝑘 } ) )
79 78 adantl ( ( ( ( 𝑅 ∈ Ring ∧ 𝐹𝐵𝐺𝐵 ) ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑐 ∈ { 𝑑 ∈ ( ℕ0m 1o ) ∣ 𝑑r ≤ ( 1o × { 𝑘 } ) } ) → 𝑐r ≤ ( 1o × { 𝑘 } ) )
80 simplr ( ( ( ( 𝑅 ∈ Ring ∧ 𝐹𝐵𝐺𝐵 ) ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑐 ∈ { 𝑑 ∈ ( ℕ0m 1o ) ∣ 𝑑r ≤ ( 1o × { 𝑘 } ) } ) → 𝑘 ∈ ℕ0 )
81 elrabi ( 𝑐 ∈ { 𝑑 ∈ ( ℕ0m 1o ) ∣ 𝑑r ≤ ( 1o × { 𝑘 } ) } → 𝑐 ∈ ( ℕ0m 1o ) )
82 81 adantl ( ( ( ( 𝑅 ∈ Ring ∧ 𝐹𝐵𝐺𝐵 ) ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑐 ∈ { 𝑑 ∈ ( ℕ0m 1o ) ∣ 𝑑r ≤ ( 1o × { 𝑘 } ) } ) → 𝑐 ∈ ( ℕ0m 1o ) )
83 coe1mul2lem1 ( ( 𝑘 ∈ ℕ0𝑐 ∈ ( ℕ0m 1o ) ) → ( 𝑐r ≤ ( 1o × { 𝑘 } ) ↔ ( 𝑐 ‘ ∅ ) ∈ ( 0 ... 𝑘 ) ) )
84 80 82 83 syl2anc ( ( ( ( 𝑅 ∈ Ring ∧ 𝐹𝐵𝐺𝐵 ) ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑐 ∈ { 𝑑 ∈ ( ℕ0m 1o ) ∣ 𝑑r ≤ ( 1o × { 𝑘 } ) } ) → ( 𝑐r ≤ ( 1o × { 𝑘 } ) ↔ ( 𝑐 ‘ ∅ ) ∈ ( 0 ... 𝑘 ) ) )
85 79 84 mpbid ( ( ( ( 𝑅 ∈ Ring ∧ 𝐹𝐵𝐺𝐵 ) ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑐 ∈ { 𝑑 ∈ ( ℕ0m 1o ) ∣ 𝑑r ≤ ( 1o × { 𝑘 } ) } ) → ( 𝑐 ‘ ∅ ) ∈ ( 0 ... 𝑘 ) )
86 eqidd ( ( ( 𝑅 ∈ Ring ∧ 𝐹𝐵𝐺𝐵 ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝑐 ∈ { 𝑑 ∈ ( ℕ0m 1o ) ∣ 𝑑r ≤ ( 1o × { 𝑘 } ) } ↦ ( 𝑐 ‘ ∅ ) ) = ( 𝑐 ∈ { 𝑑 ∈ ( ℕ0m 1o ) ∣ 𝑑r ≤ ( 1o × { 𝑘 } ) } ↦ ( 𝑐 ‘ ∅ ) ) )
87 eqidd ( ( ( 𝑅 ∈ Ring ∧ 𝐹𝐵𝐺𝐵 ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝑥 ∈ ( 0 ... 𝑘 ) ↦ ( ( ( coe1𝐹 ) ‘ 𝑥 ) · ( ( coe1𝐺 ) ‘ ( 𝑘𝑥 ) ) ) ) = ( 𝑥 ∈ ( 0 ... 𝑘 ) ↦ ( ( ( coe1𝐹 ) ‘ 𝑥 ) · ( ( coe1𝐺 ) ‘ ( 𝑘𝑥 ) ) ) ) )
88 fveq2 ( 𝑥 = ( 𝑐 ‘ ∅ ) → ( ( coe1𝐹 ) ‘ 𝑥 ) = ( ( coe1𝐹 ) ‘ ( 𝑐 ‘ ∅ ) ) )
89 oveq2 ( 𝑥 = ( 𝑐 ‘ ∅ ) → ( 𝑘𝑥 ) = ( 𝑘 − ( 𝑐 ‘ ∅ ) ) )
90 89 fveq2d ( 𝑥 = ( 𝑐 ‘ ∅ ) → ( ( coe1𝐺 ) ‘ ( 𝑘𝑥 ) ) = ( ( coe1𝐺 ) ‘ ( 𝑘 − ( 𝑐 ‘ ∅ ) ) ) )
91 88 90 oveq12d ( 𝑥 = ( 𝑐 ‘ ∅ ) → ( ( ( coe1𝐹 ) ‘ 𝑥 ) · ( ( coe1𝐺 ) ‘ ( 𝑘𝑥 ) ) ) = ( ( ( coe1𝐹 ) ‘ ( 𝑐 ‘ ∅ ) ) · ( ( coe1𝐺 ) ‘ ( 𝑘 − ( 𝑐 ‘ ∅ ) ) ) ) )
92 85 86 87 91 fmptco ( ( ( 𝑅 ∈ Ring ∧ 𝐹𝐵𝐺𝐵 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝑥 ∈ ( 0 ... 𝑘 ) ↦ ( ( ( coe1𝐹 ) ‘ 𝑥 ) · ( ( coe1𝐺 ) ‘ ( 𝑘𝑥 ) ) ) ) ∘ ( 𝑐 ∈ { 𝑑 ∈ ( ℕ0m 1o ) ∣ 𝑑r ≤ ( 1o × { 𝑘 } ) } ↦ ( 𝑐 ‘ ∅ ) ) ) = ( 𝑐 ∈ { 𝑑 ∈ ( ℕ0m 1o ) ∣ 𝑑r ≤ ( 1o × { 𝑘 } ) } ↦ ( ( ( coe1𝐹 ) ‘ ( 𝑐 ‘ ∅ ) ) · ( ( coe1𝐺 ) ‘ ( 𝑘 − ( 𝑐 ‘ ∅ ) ) ) ) ) )
93 simpll2 ( ( ( ( 𝑅 ∈ Ring ∧ 𝐹𝐵𝐺𝐵 ) ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑐 ∈ { 𝑑 ∈ ( ℕ0m 1o ) ∣ 𝑑r ≤ ( 1o × { 𝑘 } ) } ) → 𝐹𝐵 )
94 43 fvcoe1 ( ( 𝐹𝐵𝑐 ∈ ( ℕ0m 1o ) ) → ( 𝐹𝑐 ) = ( ( coe1𝐹 ) ‘ ( 𝑐 ‘ ∅ ) ) )
95 93 82 94 syl2anc ( ( ( ( 𝑅 ∈ Ring ∧ 𝐹𝐵𝐺𝐵 ) ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑐 ∈ { 𝑑 ∈ ( ℕ0m 1o ) ∣ 𝑑r ≤ ( 1o × { 𝑘 } ) } ) → ( 𝐹𝑐 ) = ( ( coe1𝐹 ) ‘ ( 𝑐 ‘ ∅ ) ) )
96 df1o2 1o = { ∅ }
97 0ex ∅ ∈ V
98 96 6 97 mapsnconst ( 𝑐 ∈ ( ℕ0m 1o ) → 𝑐 = ( 1o × { ( 𝑐 ‘ ∅ ) } ) )
99 82 98 syl ( ( ( ( 𝑅 ∈ Ring ∧ 𝐹𝐵𝐺𝐵 ) ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑐 ∈ { 𝑑 ∈ ( ℕ0m 1o ) ∣ 𝑑r ≤ ( 1o × { 𝑘 } ) } ) → 𝑐 = ( 1o × { ( 𝑐 ‘ ∅ ) } ) )
100 99 oveq2d ( ( ( ( 𝑅 ∈ Ring ∧ 𝐹𝐵𝐺𝐵 ) ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑐 ∈ { 𝑑 ∈ ( ℕ0m 1o ) ∣ 𝑑r ≤ ( 1o × { 𝑘 } ) } ) → ( ( 1o × { 𝑘 } ) ∘f𝑐 ) = ( ( 1o × { 𝑘 } ) ∘f − ( 1o × { ( 𝑐 ‘ ∅ ) } ) ) )
101 7 a1i ( ( ( ( 𝑅 ∈ Ring ∧ 𝐹𝐵𝐺𝐵 ) ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑐 ∈ { 𝑑 ∈ ( ℕ0m 1o ) ∣ 𝑑r ≤ ( 1o × { 𝑘 } ) } ) → 1o ∈ On )
102 vex 𝑘 ∈ V
103 102 a1i ( ( ( ( 𝑅 ∈ Ring ∧ 𝐹𝐵𝐺𝐵 ) ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑐 ∈ { 𝑑 ∈ ( ℕ0m 1o ) ∣ 𝑑r ≤ ( 1o × { 𝑘 } ) } ) → 𝑘 ∈ V )
104 fvexd ( ( ( ( 𝑅 ∈ Ring ∧ 𝐹𝐵𝐺𝐵 ) ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑐 ∈ { 𝑑 ∈ ( ℕ0m 1o ) ∣ 𝑑r ≤ ( 1o × { 𝑘 } ) } ) → ( 𝑐 ‘ ∅ ) ∈ V )
105 101 103 104 ofc12 ( ( ( ( 𝑅 ∈ Ring ∧ 𝐹𝐵𝐺𝐵 ) ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑐 ∈ { 𝑑 ∈ ( ℕ0m 1o ) ∣ 𝑑r ≤ ( 1o × { 𝑘 } ) } ) → ( ( 1o × { 𝑘 } ) ∘f − ( 1o × { ( 𝑐 ‘ ∅ ) } ) ) = ( 1o × { ( 𝑘 − ( 𝑐 ‘ ∅ ) ) } ) )
106 100 105 eqtrd ( ( ( ( 𝑅 ∈ Ring ∧ 𝐹𝐵𝐺𝐵 ) ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑐 ∈ { 𝑑 ∈ ( ℕ0m 1o ) ∣ 𝑑r ≤ ( 1o × { 𝑘 } ) } ) → ( ( 1o × { 𝑘 } ) ∘f𝑐 ) = ( 1o × { ( 𝑘 − ( 𝑐 ‘ ∅ ) ) } ) )
107 106 fveq2d ( ( ( ( 𝑅 ∈ Ring ∧ 𝐹𝐵𝐺𝐵 ) ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑐 ∈ { 𝑑 ∈ ( ℕ0m 1o ) ∣ 𝑑r ≤ ( 1o × { 𝑘 } ) } ) → ( 𝐺 ‘ ( ( 1o × { 𝑘 } ) ∘f𝑐 ) ) = ( 𝐺 ‘ ( 1o × { ( 𝑘 − ( 𝑐 ‘ ∅ ) ) } ) ) )
108 simpll3 ( ( ( ( 𝑅 ∈ Ring ∧ 𝐹𝐵𝐺𝐵 ) ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑐 ∈ { 𝑑 ∈ ( ℕ0m 1o ) ∣ 𝑑r ≤ ( 1o × { 𝑘 } ) } ) → 𝐺𝐵 )
109 fznn0sub ( ( 𝑐 ‘ ∅ ) ∈ ( 0 ... 𝑘 ) → ( 𝑘 − ( 𝑐 ‘ ∅ ) ) ∈ ℕ0 )
110 85 109 syl ( ( ( ( 𝑅 ∈ Ring ∧ 𝐹𝐵𝐺𝐵 ) ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑐 ∈ { 𝑑 ∈ ( ℕ0m 1o ) ∣ 𝑑r ≤ ( 1o × { 𝑘 } ) } ) → ( 𝑘 − ( 𝑐 ‘ ∅ ) ) ∈ ℕ0 )
111 50 coe1fv ( ( 𝐺𝐵 ∧ ( 𝑘 − ( 𝑐 ‘ ∅ ) ) ∈ ℕ0 ) → ( ( coe1𝐺 ) ‘ ( 𝑘 − ( 𝑐 ‘ ∅ ) ) ) = ( 𝐺 ‘ ( 1o × { ( 𝑘 − ( 𝑐 ‘ ∅ ) ) } ) ) )
112 108 110 111 syl2anc ( ( ( ( 𝑅 ∈ Ring ∧ 𝐹𝐵𝐺𝐵 ) ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑐 ∈ { 𝑑 ∈ ( ℕ0m 1o ) ∣ 𝑑r ≤ ( 1o × { 𝑘 } ) } ) → ( ( coe1𝐺 ) ‘ ( 𝑘 − ( 𝑐 ‘ ∅ ) ) ) = ( 𝐺 ‘ ( 1o × { ( 𝑘 − ( 𝑐 ‘ ∅ ) ) } ) ) )
113 107 112 eqtr4d ( ( ( ( 𝑅 ∈ Ring ∧ 𝐹𝐵𝐺𝐵 ) ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑐 ∈ { 𝑑 ∈ ( ℕ0m 1o ) ∣ 𝑑r ≤ ( 1o × { 𝑘 } ) } ) → ( 𝐺 ‘ ( ( 1o × { 𝑘 } ) ∘f𝑐 ) ) = ( ( coe1𝐺 ) ‘ ( 𝑘 − ( 𝑐 ‘ ∅ ) ) ) )
114 95 113 oveq12d ( ( ( ( 𝑅 ∈ Ring ∧ 𝐹𝐵𝐺𝐵 ) ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑐 ∈ { 𝑑 ∈ ( ℕ0m 1o ) ∣ 𝑑r ≤ ( 1o × { 𝑘 } ) } ) → ( ( 𝐹𝑐 ) · ( 𝐺 ‘ ( ( 1o × { 𝑘 } ) ∘f𝑐 ) ) ) = ( ( ( coe1𝐹 ) ‘ ( 𝑐 ‘ ∅ ) ) · ( ( coe1𝐺 ) ‘ ( 𝑘 − ( 𝑐 ‘ ∅ ) ) ) ) )
115 114 mpteq2dva ( ( ( 𝑅 ∈ Ring ∧ 𝐹𝐵𝐺𝐵 ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝑐 ∈ { 𝑑 ∈ ( ℕ0m 1o ) ∣ 𝑑r ≤ ( 1o × { 𝑘 } ) } ↦ ( ( 𝐹𝑐 ) · ( 𝐺 ‘ ( ( 1o × { 𝑘 } ) ∘f𝑐 ) ) ) ) = ( 𝑐 ∈ { 𝑑 ∈ ( ℕ0m 1o ) ∣ 𝑑r ≤ ( 1o × { 𝑘 } ) } ↦ ( ( ( coe1𝐹 ) ‘ ( 𝑐 ‘ ∅ ) ) · ( ( coe1𝐺 ) ‘ ( 𝑘 − ( 𝑐 ‘ ∅ ) ) ) ) ) )
116 92 115 eqtr4d ( ( ( 𝑅 ∈ Ring ∧ 𝐹𝐵𝐺𝐵 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝑥 ∈ ( 0 ... 𝑘 ) ↦ ( ( ( coe1𝐹 ) ‘ 𝑥 ) · ( ( coe1𝐺 ) ‘ ( 𝑘𝑥 ) ) ) ) ∘ ( 𝑐 ∈ { 𝑑 ∈ ( ℕ0m 1o ) ∣ 𝑑r ≤ ( 1o × { 𝑘 } ) } ↦ ( 𝑐 ‘ ∅ ) ) ) = ( 𝑐 ∈ { 𝑑 ∈ ( ℕ0m 1o ) ∣ 𝑑r ≤ ( 1o × { 𝑘 } ) } ↦ ( ( 𝐹𝑐 ) · ( 𝐺 ‘ ( ( 1o × { 𝑘 } ) ∘f𝑐 ) ) ) ) )
117 116 oveq2d ( ( ( 𝑅 ∈ Ring ∧ 𝐹𝐵𝐺𝐵 ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝑅 Σg ( ( 𝑥 ∈ ( 0 ... 𝑘 ) ↦ ( ( ( coe1𝐹 ) ‘ 𝑥 ) · ( ( coe1𝐺 ) ‘ ( 𝑘𝑥 ) ) ) ) ∘ ( 𝑐 ∈ { 𝑑 ∈ ( ℕ0m 1o ) ∣ 𝑑r ≤ ( 1o × { 𝑘 } ) } ↦ ( 𝑐 ‘ ∅ ) ) ) ) = ( 𝑅 Σg ( 𝑐 ∈ { 𝑑 ∈ ( ℕ0m 1o ) ∣ 𝑑r ≤ ( 1o × { 𝑘 } ) } ↦ ( ( 𝐹𝑐 ) · ( 𝐺 ‘ ( ( 1o × { 𝑘 } ) ∘f𝑐 ) ) ) ) ) )
118 75 117 eqtrd ( ( ( 𝑅 ∈ Ring ∧ 𝐹𝐵𝐺𝐵 ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝑅 Σg ( 𝑥 ∈ ( 0 ... 𝑘 ) ↦ ( ( ( coe1𝐹 ) ‘ 𝑥 ) · ( ( coe1𝐺 ) ‘ ( 𝑘𝑥 ) ) ) ) ) = ( 𝑅 Σg ( 𝑐 ∈ { 𝑑 ∈ ( ℕ0m 1o ) ∣ 𝑑r ≤ ( 1o × { 𝑘 } ) } ↦ ( ( 𝐹𝑐 ) · ( 𝐺 ‘ ( ( 1o × { 𝑘 } ) ∘f𝑐 ) ) ) ) ) )
119 118 mpteq2dva ( ( 𝑅 ∈ Ring ∧ 𝐹𝐵𝐺𝐵 ) → ( 𝑘 ∈ ℕ0 ↦ ( 𝑅 Σg ( 𝑥 ∈ ( 0 ... 𝑘 ) ↦ ( ( ( coe1𝐹 ) ‘ 𝑥 ) · ( ( coe1𝐺 ) ‘ ( 𝑘𝑥 ) ) ) ) ) ) = ( 𝑘 ∈ ℕ0 ↦ ( 𝑅 Σg ( 𝑐 ∈ { 𝑑 ∈ ( ℕ0m 1o ) ∣ 𝑑r ≤ ( 1o × { 𝑘 } ) } ↦ ( ( 𝐹𝑐 ) · ( 𝐺 ‘ ( ( 1o × { 𝑘 } ) ∘f𝑐 ) ) ) ) ) ) )
120 26 33 119 3eqtr4d ( ( 𝑅 ∈ Ring ∧ 𝐹𝐵𝐺𝐵 ) → ( coe1 ‘ ( 𝐹 𝐺 ) ) = ( 𝑘 ∈ ℕ0 ↦ ( 𝑅 Σg ( 𝑥 ∈ ( 0 ... 𝑘 ) ↦ ( ( ( coe1𝐹 ) ‘ 𝑥 ) · ( ( coe1𝐺 ) ‘ ( 𝑘𝑥 ) ) ) ) ) ) )