Metamath Proof Explorer


Theorem evl1gsumd

Description: Polynomial evaluation builder for a finite group sum of polynomials. (Contributed by AV, 17-Sep-2019)

Ref Expression
Hypotheses evl1gsumd.q 𝑂 = ( eval1𝑅 )
evl1gsumd.p 𝑃 = ( Poly1𝑅 )
evl1gsumd.b 𝐵 = ( Base ‘ 𝑅 )
evl1gsumd.u 𝑈 = ( Base ‘ 𝑃 )
evl1gsumd.r ( 𝜑𝑅 ∈ CRing )
evl1gsumd.y ( 𝜑𝑌𝐵 )
evl1gsumd.m ( 𝜑 → ∀ 𝑥𝑁 𝑀𝑈 )
evl1gsumd.n ( 𝜑𝑁 ∈ Fin )
Assertion evl1gsumd ( 𝜑 → ( ( 𝑂 ‘ ( 𝑃 Σg ( 𝑥𝑁𝑀 ) ) ) ‘ 𝑌 ) = ( 𝑅 Σg ( 𝑥𝑁 ↦ ( ( 𝑂𝑀 ) ‘ 𝑌 ) ) ) )

Proof

Step Hyp Ref Expression
1 evl1gsumd.q 𝑂 = ( eval1𝑅 )
2 evl1gsumd.p 𝑃 = ( Poly1𝑅 )
3 evl1gsumd.b 𝐵 = ( Base ‘ 𝑅 )
4 evl1gsumd.u 𝑈 = ( Base ‘ 𝑃 )
5 evl1gsumd.r ( 𝜑𝑅 ∈ CRing )
6 evl1gsumd.y ( 𝜑𝑌𝐵 )
7 evl1gsumd.m ( 𝜑 → ∀ 𝑥𝑁 𝑀𝑈 )
8 evl1gsumd.n ( 𝜑𝑁 ∈ Fin )
9 raleq ( 𝑛 = ∅ → ( ∀ 𝑥𝑛 𝑀𝑈 ↔ ∀ 𝑥 ∈ ∅ 𝑀𝑈 ) )
10 9 anbi2d ( 𝑛 = ∅ → ( ( 𝜑 ∧ ∀ 𝑥𝑛 𝑀𝑈 ) ↔ ( 𝜑 ∧ ∀ 𝑥 ∈ ∅ 𝑀𝑈 ) ) )
11 mpteq1 ( 𝑛 = ∅ → ( 𝑥𝑛𝑀 ) = ( 𝑥 ∈ ∅ ↦ 𝑀 ) )
12 11 oveq2d ( 𝑛 = ∅ → ( 𝑃 Σg ( 𝑥𝑛𝑀 ) ) = ( 𝑃 Σg ( 𝑥 ∈ ∅ ↦ 𝑀 ) ) )
13 12 fveq2d ( 𝑛 = ∅ → ( 𝑂 ‘ ( 𝑃 Σg ( 𝑥𝑛𝑀 ) ) ) = ( 𝑂 ‘ ( 𝑃 Σg ( 𝑥 ∈ ∅ ↦ 𝑀 ) ) ) )
14 13 fveq1d ( 𝑛 = ∅ → ( ( 𝑂 ‘ ( 𝑃 Σg ( 𝑥𝑛𝑀 ) ) ) ‘ 𝑌 ) = ( ( 𝑂 ‘ ( 𝑃 Σg ( 𝑥 ∈ ∅ ↦ 𝑀 ) ) ) ‘ 𝑌 ) )
15 mpteq1 ( 𝑛 = ∅ → ( 𝑥𝑛 ↦ ( ( 𝑂𝑀 ) ‘ 𝑌 ) ) = ( 𝑥 ∈ ∅ ↦ ( ( 𝑂𝑀 ) ‘ 𝑌 ) ) )
16 15 oveq2d ( 𝑛 = ∅ → ( 𝑅 Σg ( 𝑥𝑛 ↦ ( ( 𝑂𝑀 ) ‘ 𝑌 ) ) ) = ( 𝑅 Σg ( 𝑥 ∈ ∅ ↦ ( ( 𝑂𝑀 ) ‘ 𝑌 ) ) ) )
17 14 16 eqeq12d ( 𝑛 = ∅ → ( ( ( 𝑂 ‘ ( 𝑃 Σg ( 𝑥𝑛𝑀 ) ) ) ‘ 𝑌 ) = ( 𝑅 Σg ( 𝑥𝑛 ↦ ( ( 𝑂𝑀 ) ‘ 𝑌 ) ) ) ↔ ( ( 𝑂 ‘ ( 𝑃 Σg ( 𝑥 ∈ ∅ ↦ 𝑀 ) ) ) ‘ 𝑌 ) = ( 𝑅 Σg ( 𝑥 ∈ ∅ ↦ ( ( 𝑂𝑀 ) ‘ 𝑌 ) ) ) ) )
18 10 17 imbi12d ( 𝑛 = ∅ → ( ( ( 𝜑 ∧ ∀ 𝑥𝑛 𝑀𝑈 ) → ( ( 𝑂 ‘ ( 𝑃 Σg ( 𝑥𝑛𝑀 ) ) ) ‘ 𝑌 ) = ( 𝑅 Σg ( 𝑥𝑛 ↦ ( ( 𝑂𝑀 ) ‘ 𝑌 ) ) ) ) ↔ ( ( 𝜑 ∧ ∀ 𝑥 ∈ ∅ 𝑀𝑈 ) → ( ( 𝑂 ‘ ( 𝑃 Σg ( 𝑥 ∈ ∅ ↦ 𝑀 ) ) ) ‘ 𝑌 ) = ( 𝑅 Σg ( 𝑥 ∈ ∅ ↦ ( ( 𝑂𝑀 ) ‘ 𝑌 ) ) ) ) ) )
19 raleq ( 𝑛 = 𝑚 → ( ∀ 𝑥𝑛 𝑀𝑈 ↔ ∀ 𝑥𝑚 𝑀𝑈 ) )
20 19 anbi2d ( 𝑛 = 𝑚 → ( ( 𝜑 ∧ ∀ 𝑥𝑛 𝑀𝑈 ) ↔ ( 𝜑 ∧ ∀ 𝑥𝑚 𝑀𝑈 ) ) )
21 mpteq1 ( 𝑛 = 𝑚 → ( 𝑥𝑛𝑀 ) = ( 𝑥𝑚𝑀 ) )
22 21 oveq2d ( 𝑛 = 𝑚 → ( 𝑃 Σg ( 𝑥𝑛𝑀 ) ) = ( 𝑃 Σg ( 𝑥𝑚𝑀 ) ) )
23 22 fveq2d ( 𝑛 = 𝑚 → ( 𝑂 ‘ ( 𝑃 Σg ( 𝑥𝑛𝑀 ) ) ) = ( 𝑂 ‘ ( 𝑃 Σg ( 𝑥𝑚𝑀 ) ) ) )
24 23 fveq1d ( 𝑛 = 𝑚 → ( ( 𝑂 ‘ ( 𝑃 Σg ( 𝑥𝑛𝑀 ) ) ) ‘ 𝑌 ) = ( ( 𝑂 ‘ ( 𝑃 Σg ( 𝑥𝑚𝑀 ) ) ) ‘ 𝑌 ) )
25 mpteq1 ( 𝑛 = 𝑚 → ( 𝑥𝑛 ↦ ( ( 𝑂𝑀 ) ‘ 𝑌 ) ) = ( 𝑥𝑚 ↦ ( ( 𝑂𝑀 ) ‘ 𝑌 ) ) )
26 25 oveq2d ( 𝑛 = 𝑚 → ( 𝑅 Σg ( 𝑥𝑛 ↦ ( ( 𝑂𝑀 ) ‘ 𝑌 ) ) ) = ( 𝑅 Σg ( 𝑥𝑚 ↦ ( ( 𝑂𝑀 ) ‘ 𝑌 ) ) ) )
27 24 26 eqeq12d ( 𝑛 = 𝑚 → ( ( ( 𝑂 ‘ ( 𝑃 Σg ( 𝑥𝑛𝑀 ) ) ) ‘ 𝑌 ) = ( 𝑅 Σg ( 𝑥𝑛 ↦ ( ( 𝑂𝑀 ) ‘ 𝑌 ) ) ) ↔ ( ( 𝑂 ‘ ( 𝑃 Σg ( 𝑥𝑚𝑀 ) ) ) ‘ 𝑌 ) = ( 𝑅 Σg ( 𝑥𝑚 ↦ ( ( 𝑂𝑀 ) ‘ 𝑌 ) ) ) ) )
28 20 27 imbi12d ( 𝑛 = 𝑚 → ( ( ( 𝜑 ∧ ∀ 𝑥𝑛 𝑀𝑈 ) → ( ( 𝑂 ‘ ( 𝑃 Σg ( 𝑥𝑛𝑀 ) ) ) ‘ 𝑌 ) = ( 𝑅 Σg ( 𝑥𝑛 ↦ ( ( 𝑂𝑀 ) ‘ 𝑌 ) ) ) ) ↔ ( ( 𝜑 ∧ ∀ 𝑥𝑚 𝑀𝑈 ) → ( ( 𝑂 ‘ ( 𝑃 Σg ( 𝑥𝑚𝑀 ) ) ) ‘ 𝑌 ) = ( 𝑅 Σg ( 𝑥𝑚 ↦ ( ( 𝑂𝑀 ) ‘ 𝑌 ) ) ) ) ) )
29 raleq ( 𝑛 = ( 𝑚 ∪ { 𝑎 } ) → ( ∀ 𝑥𝑛 𝑀𝑈 ↔ ∀ 𝑥 ∈ ( 𝑚 ∪ { 𝑎 } ) 𝑀𝑈 ) )
30 29 anbi2d ( 𝑛 = ( 𝑚 ∪ { 𝑎 } ) → ( ( 𝜑 ∧ ∀ 𝑥𝑛 𝑀𝑈 ) ↔ ( 𝜑 ∧ ∀ 𝑥 ∈ ( 𝑚 ∪ { 𝑎 } ) 𝑀𝑈 ) ) )
31 mpteq1 ( 𝑛 = ( 𝑚 ∪ { 𝑎 } ) → ( 𝑥𝑛𝑀 ) = ( 𝑥 ∈ ( 𝑚 ∪ { 𝑎 } ) ↦ 𝑀 ) )
32 31 oveq2d ( 𝑛 = ( 𝑚 ∪ { 𝑎 } ) → ( 𝑃 Σg ( 𝑥𝑛𝑀 ) ) = ( 𝑃 Σg ( 𝑥 ∈ ( 𝑚 ∪ { 𝑎 } ) ↦ 𝑀 ) ) )
33 32 fveq2d ( 𝑛 = ( 𝑚 ∪ { 𝑎 } ) → ( 𝑂 ‘ ( 𝑃 Σg ( 𝑥𝑛𝑀 ) ) ) = ( 𝑂 ‘ ( 𝑃 Σg ( 𝑥 ∈ ( 𝑚 ∪ { 𝑎 } ) ↦ 𝑀 ) ) ) )
34 33 fveq1d ( 𝑛 = ( 𝑚 ∪ { 𝑎 } ) → ( ( 𝑂 ‘ ( 𝑃 Σg ( 𝑥𝑛𝑀 ) ) ) ‘ 𝑌 ) = ( ( 𝑂 ‘ ( 𝑃 Σg ( 𝑥 ∈ ( 𝑚 ∪ { 𝑎 } ) ↦ 𝑀 ) ) ) ‘ 𝑌 ) )
35 mpteq1 ( 𝑛 = ( 𝑚 ∪ { 𝑎 } ) → ( 𝑥𝑛 ↦ ( ( 𝑂𝑀 ) ‘ 𝑌 ) ) = ( 𝑥 ∈ ( 𝑚 ∪ { 𝑎 } ) ↦ ( ( 𝑂𝑀 ) ‘ 𝑌 ) ) )
36 35 oveq2d ( 𝑛 = ( 𝑚 ∪ { 𝑎 } ) → ( 𝑅 Σg ( 𝑥𝑛 ↦ ( ( 𝑂𝑀 ) ‘ 𝑌 ) ) ) = ( 𝑅 Σg ( 𝑥 ∈ ( 𝑚 ∪ { 𝑎 } ) ↦ ( ( 𝑂𝑀 ) ‘ 𝑌 ) ) ) )
37 34 36 eqeq12d ( 𝑛 = ( 𝑚 ∪ { 𝑎 } ) → ( ( ( 𝑂 ‘ ( 𝑃 Σg ( 𝑥𝑛𝑀 ) ) ) ‘ 𝑌 ) = ( 𝑅 Σg ( 𝑥𝑛 ↦ ( ( 𝑂𝑀 ) ‘ 𝑌 ) ) ) ↔ ( ( 𝑂 ‘ ( 𝑃 Σg ( 𝑥 ∈ ( 𝑚 ∪ { 𝑎 } ) ↦ 𝑀 ) ) ) ‘ 𝑌 ) = ( 𝑅 Σg ( 𝑥 ∈ ( 𝑚 ∪ { 𝑎 } ) ↦ ( ( 𝑂𝑀 ) ‘ 𝑌 ) ) ) ) )
38 30 37 imbi12d ( 𝑛 = ( 𝑚 ∪ { 𝑎 } ) → ( ( ( 𝜑 ∧ ∀ 𝑥𝑛 𝑀𝑈 ) → ( ( 𝑂 ‘ ( 𝑃 Σg ( 𝑥𝑛𝑀 ) ) ) ‘ 𝑌 ) = ( 𝑅 Σg ( 𝑥𝑛 ↦ ( ( 𝑂𝑀 ) ‘ 𝑌 ) ) ) ) ↔ ( ( 𝜑 ∧ ∀ 𝑥 ∈ ( 𝑚 ∪ { 𝑎 } ) 𝑀𝑈 ) → ( ( 𝑂 ‘ ( 𝑃 Σg ( 𝑥 ∈ ( 𝑚 ∪ { 𝑎 } ) ↦ 𝑀 ) ) ) ‘ 𝑌 ) = ( 𝑅 Σg ( 𝑥 ∈ ( 𝑚 ∪ { 𝑎 } ) ↦ ( ( 𝑂𝑀 ) ‘ 𝑌 ) ) ) ) ) )
39 raleq ( 𝑛 = 𝑁 → ( ∀ 𝑥𝑛 𝑀𝑈 ↔ ∀ 𝑥𝑁 𝑀𝑈 ) )
40 39 anbi2d ( 𝑛 = 𝑁 → ( ( 𝜑 ∧ ∀ 𝑥𝑛 𝑀𝑈 ) ↔ ( 𝜑 ∧ ∀ 𝑥𝑁 𝑀𝑈 ) ) )
41 mpteq1 ( 𝑛 = 𝑁 → ( 𝑥𝑛𝑀 ) = ( 𝑥𝑁𝑀 ) )
42 41 oveq2d ( 𝑛 = 𝑁 → ( 𝑃 Σg ( 𝑥𝑛𝑀 ) ) = ( 𝑃 Σg ( 𝑥𝑁𝑀 ) ) )
43 42 fveq2d ( 𝑛 = 𝑁 → ( 𝑂 ‘ ( 𝑃 Σg ( 𝑥𝑛𝑀 ) ) ) = ( 𝑂 ‘ ( 𝑃 Σg ( 𝑥𝑁𝑀 ) ) ) )
44 43 fveq1d ( 𝑛 = 𝑁 → ( ( 𝑂 ‘ ( 𝑃 Σg ( 𝑥𝑛𝑀 ) ) ) ‘ 𝑌 ) = ( ( 𝑂 ‘ ( 𝑃 Σg ( 𝑥𝑁𝑀 ) ) ) ‘ 𝑌 ) )
45 mpteq1 ( 𝑛 = 𝑁 → ( 𝑥𝑛 ↦ ( ( 𝑂𝑀 ) ‘ 𝑌 ) ) = ( 𝑥𝑁 ↦ ( ( 𝑂𝑀 ) ‘ 𝑌 ) ) )
46 45 oveq2d ( 𝑛 = 𝑁 → ( 𝑅 Σg ( 𝑥𝑛 ↦ ( ( 𝑂𝑀 ) ‘ 𝑌 ) ) ) = ( 𝑅 Σg ( 𝑥𝑁 ↦ ( ( 𝑂𝑀 ) ‘ 𝑌 ) ) ) )
47 44 46 eqeq12d ( 𝑛 = 𝑁 → ( ( ( 𝑂 ‘ ( 𝑃 Σg ( 𝑥𝑛𝑀 ) ) ) ‘ 𝑌 ) = ( 𝑅 Σg ( 𝑥𝑛 ↦ ( ( 𝑂𝑀 ) ‘ 𝑌 ) ) ) ↔ ( ( 𝑂 ‘ ( 𝑃 Σg ( 𝑥𝑁𝑀 ) ) ) ‘ 𝑌 ) = ( 𝑅 Σg ( 𝑥𝑁 ↦ ( ( 𝑂𝑀 ) ‘ 𝑌 ) ) ) ) )
48 40 47 imbi12d ( 𝑛 = 𝑁 → ( ( ( 𝜑 ∧ ∀ 𝑥𝑛 𝑀𝑈 ) → ( ( 𝑂 ‘ ( 𝑃 Σg ( 𝑥𝑛𝑀 ) ) ) ‘ 𝑌 ) = ( 𝑅 Σg ( 𝑥𝑛 ↦ ( ( 𝑂𝑀 ) ‘ 𝑌 ) ) ) ) ↔ ( ( 𝜑 ∧ ∀ 𝑥𝑁 𝑀𝑈 ) → ( ( 𝑂 ‘ ( 𝑃 Σg ( 𝑥𝑁𝑀 ) ) ) ‘ 𝑌 ) = ( 𝑅 Σg ( 𝑥𝑁 ↦ ( ( 𝑂𝑀 ) ‘ 𝑌 ) ) ) ) ) )
49 mpt0 ( 𝑥 ∈ ∅ ↦ 𝑀 ) = ∅
50 49 oveq2i ( 𝑃 Σg ( 𝑥 ∈ ∅ ↦ 𝑀 ) ) = ( 𝑃 Σg ∅ )
51 eqid ( 0g𝑃 ) = ( 0g𝑃 )
52 51 gsum0 ( 𝑃 Σg ∅ ) = ( 0g𝑃 )
53 50 52 eqtri ( 𝑃 Σg ( 𝑥 ∈ ∅ ↦ 𝑀 ) ) = ( 0g𝑃 )
54 53 fveq2i ( 𝑂 ‘ ( 𝑃 Σg ( 𝑥 ∈ ∅ ↦ 𝑀 ) ) ) = ( 𝑂 ‘ ( 0g𝑃 ) )
55 crngring ( 𝑅 ∈ CRing → 𝑅 ∈ Ring )
56 5 55 syl ( 𝜑𝑅 ∈ Ring )
57 eqid ( algSc ‘ 𝑃 ) = ( algSc ‘ 𝑃 )
58 eqid ( 0g𝑅 ) = ( 0g𝑅 )
59 2 57 58 51 ply1scl0 ( 𝑅 ∈ Ring → ( ( algSc ‘ 𝑃 ) ‘ ( 0g𝑅 ) ) = ( 0g𝑃 ) )
60 56 59 syl ( 𝜑 → ( ( algSc ‘ 𝑃 ) ‘ ( 0g𝑅 ) ) = ( 0g𝑃 ) )
61 60 eqcomd ( 𝜑 → ( 0g𝑃 ) = ( ( algSc ‘ 𝑃 ) ‘ ( 0g𝑅 ) ) )
62 61 fveq2d ( 𝜑 → ( 𝑂 ‘ ( 0g𝑃 ) ) = ( 𝑂 ‘ ( ( algSc ‘ 𝑃 ) ‘ ( 0g𝑅 ) ) ) )
63 54 62 syl5eq ( 𝜑 → ( 𝑂 ‘ ( 𝑃 Σg ( 𝑥 ∈ ∅ ↦ 𝑀 ) ) ) = ( 𝑂 ‘ ( ( algSc ‘ 𝑃 ) ‘ ( 0g𝑅 ) ) ) )
64 63 fveq1d ( 𝜑 → ( ( 𝑂 ‘ ( 𝑃 Σg ( 𝑥 ∈ ∅ ↦ 𝑀 ) ) ) ‘ 𝑌 ) = ( ( 𝑂 ‘ ( ( algSc ‘ 𝑃 ) ‘ ( 0g𝑅 ) ) ) ‘ 𝑌 ) )
65 ringgrp ( 𝑅 ∈ Ring → 𝑅 ∈ Grp )
66 56 65 syl ( 𝜑𝑅 ∈ Grp )
67 3 58 grpidcl ( 𝑅 ∈ Grp → ( 0g𝑅 ) ∈ 𝐵 )
68 66 67 syl ( 𝜑 → ( 0g𝑅 ) ∈ 𝐵 )
69 1 2 3 57 4 5 68 6 evl1scad ( 𝜑 → ( ( ( algSc ‘ 𝑃 ) ‘ ( 0g𝑅 ) ) ∈ 𝑈 ∧ ( ( 𝑂 ‘ ( ( algSc ‘ 𝑃 ) ‘ ( 0g𝑅 ) ) ) ‘ 𝑌 ) = ( 0g𝑅 ) ) )
70 69 simprd ( 𝜑 → ( ( 𝑂 ‘ ( ( algSc ‘ 𝑃 ) ‘ ( 0g𝑅 ) ) ) ‘ 𝑌 ) = ( 0g𝑅 ) )
71 64 70 eqtrd ( 𝜑 → ( ( 𝑂 ‘ ( 𝑃 Σg ( 𝑥 ∈ ∅ ↦ 𝑀 ) ) ) ‘ 𝑌 ) = ( 0g𝑅 ) )
72 mpt0 ( 𝑥 ∈ ∅ ↦ ( ( 𝑂𝑀 ) ‘ 𝑌 ) ) = ∅
73 72 oveq2i ( 𝑅 Σg ( 𝑥 ∈ ∅ ↦ ( ( 𝑂𝑀 ) ‘ 𝑌 ) ) ) = ( 𝑅 Σg ∅ )
74 58 gsum0 ( 𝑅 Σg ∅ ) = ( 0g𝑅 )
75 73 74 eqtri ( 𝑅 Σg ( 𝑥 ∈ ∅ ↦ ( ( 𝑂𝑀 ) ‘ 𝑌 ) ) ) = ( 0g𝑅 )
76 71 75 eqtr4di ( 𝜑 → ( ( 𝑂 ‘ ( 𝑃 Σg ( 𝑥 ∈ ∅ ↦ 𝑀 ) ) ) ‘ 𝑌 ) = ( 𝑅 Σg ( 𝑥 ∈ ∅ ↦ ( ( 𝑂𝑀 ) ‘ 𝑌 ) ) ) )
77 76 adantr ( ( 𝜑 ∧ ∀ 𝑥 ∈ ∅ 𝑀𝑈 ) → ( ( 𝑂 ‘ ( 𝑃 Σg ( 𝑥 ∈ ∅ ↦ 𝑀 ) ) ) ‘ 𝑌 ) = ( 𝑅 Σg ( 𝑥 ∈ ∅ ↦ ( ( 𝑂𝑀 ) ‘ 𝑌 ) ) ) )
78 1 2 3 4 5 6 evl1gsumdlem ( ( 𝑚 ∈ Fin ∧ ¬ 𝑎𝑚𝜑 ) → ( ( ∀ 𝑥𝑚 𝑀𝑈 → ( ( 𝑂 ‘ ( 𝑃 Σg ( 𝑥𝑚𝑀 ) ) ) ‘ 𝑌 ) = ( 𝑅 Σg ( 𝑥𝑚 ↦ ( ( 𝑂𝑀 ) ‘ 𝑌 ) ) ) ) → ( ∀ 𝑥 ∈ ( 𝑚 ∪ { 𝑎 } ) 𝑀𝑈 → ( ( 𝑂 ‘ ( 𝑃 Σg ( 𝑥 ∈ ( 𝑚 ∪ { 𝑎 } ) ↦ 𝑀 ) ) ) ‘ 𝑌 ) = ( 𝑅 Σg ( 𝑥 ∈ ( 𝑚 ∪ { 𝑎 } ) ↦ ( ( 𝑂𝑀 ) ‘ 𝑌 ) ) ) ) ) )
79 78 3expia ( ( 𝑚 ∈ Fin ∧ ¬ 𝑎𝑚 ) → ( 𝜑 → ( ( ∀ 𝑥𝑚 𝑀𝑈 → ( ( 𝑂 ‘ ( 𝑃 Σg ( 𝑥𝑚𝑀 ) ) ) ‘ 𝑌 ) = ( 𝑅 Σg ( 𝑥𝑚 ↦ ( ( 𝑂𝑀 ) ‘ 𝑌 ) ) ) ) → ( ∀ 𝑥 ∈ ( 𝑚 ∪ { 𝑎 } ) 𝑀𝑈 → ( ( 𝑂 ‘ ( 𝑃 Σg ( 𝑥 ∈ ( 𝑚 ∪ { 𝑎 } ) ↦ 𝑀 ) ) ) ‘ 𝑌 ) = ( 𝑅 Σg ( 𝑥 ∈ ( 𝑚 ∪ { 𝑎 } ) ↦ ( ( 𝑂𝑀 ) ‘ 𝑌 ) ) ) ) ) ) )
80 79 a2d ( ( 𝑚 ∈ Fin ∧ ¬ 𝑎𝑚 ) → ( ( 𝜑 → ( ∀ 𝑥𝑚 𝑀𝑈 → ( ( 𝑂 ‘ ( 𝑃 Σg ( 𝑥𝑚𝑀 ) ) ) ‘ 𝑌 ) = ( 𝑅 Σg ( 𝑥𝑚 ↦ ( ( 𝑂𝑀 ) ‘ 𝑌 ) ) ) ) ) → ( 𝜑 → ( ∀ 𝑥 ∈ ( 𝑚 ∪ { 𝑎 } ) 𝑀𝑈 → ( ( 𝑂 ‘ ( 𝑃 Σg ( 𝑥 ∈ ( 𝑚 ∪ { 𝑎 } ) ↦ 𝑀 ) ) ) ‘ 𝑌 ) = ( 𝑅 Σg ( 𝑥 ∈ ( 𝑚 ∪ { 𝑎 } ) ↦ ( ( 𝑂𝑀 ) ‘ 𝑌 ) ) ) ) ) ) )
81 impexp ( ( ( 𝜑 ∧ ∀ 𝑥𝑚 𝑀𝑈 ) → ( ( 𝑂 ‘ ( 𝑃 Σg ( 𝑥𝑚𝑀 ) ) ) ‘ 𝑌 ) = ( 𝑅 Σg ( 𝑥𝑚 ↦ ( ( 𝑂𝑀 ) ‘ 𝑌 ) ) ) ) ↔ ( 𝜑 → ( ∀ 𝑥𝑚 𝑀𝑈 → ( ( 𝑂 ‘ ( 𝑃 Σg ( 𝑥𝑚𝑀 ) ) ) ‘ 𝑌 ) = ( 𝑅 Σg ( 𝑥𝑚 ↦ ( ( 𝑂𝑀 ) ‘ 𝑌 ) ) ) ) ) )
82 impexp ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ ( 𝑚 ∪ { 𝑎 } ) 𝑀𝑈 ) → ( ( 𝑂 ‘ ( 𝑃 Σg ( 𝑥 ∈ ( 𝑚 ∪ { 𝑎 } ) ↦ 𝑀 ) ) ) ‘ 𝑌 ) = ( 𝑅 Σg ( 𝑥 ∈ ( 𝑚 ∪ { 𝑎 } ) ↦ ( ( 𝑂𝑀 ) ‘ 𝑌 ) ) ) ) ↔ ( 𝜑 → ( ∀ 𝑥 ∈ ( 𝑚 ∪ { 𝑎 } ) 𝑀𝑈 → ( ( 𝑂 ‘ ( 𝑃 Σg ( 𝑥 ∈ ( 𝑚 ∪ { 𝑎 } ) ↦ 𝑀 ) ) ) ‘ 𝑌 ) = ( 𝑅 Σg ( 𝑥 ∈ ( 𝑚 ∪ { 𝑎 } ) ↦ ( ( 𝑂𝑀 ) ‘ 𝑌 ) ) ) ) ) )
83 80 81 82 3imtr4g ( ( 𝑚 ∈ Fin ∧ ¬ 𝑎𝑚 ) → ( ( ( 𝜑 ∧ ∀ 𝑥𝑚 𝑀𝑈 ) → ( ( 𝑂 ‘ ( 𝑃 Σg ( 𝑥𝑚𝑀 ) ) ) ‘ 𝑌 ) = ( 𝑅 Σg ( 𝑥𝑚 ↦ ( ( 𝑂𝑀 ) ‘ 𝑌 ) ) ) ) → ( ( 𝜑 ∧ ∀ 𝑥 ∈ ( 𝑚 ∪ { 𝑎 } ) 𝑀𝑈 ) → ( ( 𝑂 ‘ ( 𝑃 Σg ( 𝑥 ∈ ( 𝑚 ∪ { 𝑎 } ) ↦ 𝑀 ) ) ) ‘ 𝑌 ) = ( 𝑅 Σg ( 𝑥 ∈ ( 𝑚 ∪ { 𝑎 } ) ↦ ( ( 𝑂𝑀 ) ‘ 𝑌 ) ) ) ) ) )
84 18 28 38 48 77 83 findcard2s ( 𝑁 ∈ Fin → ( ( 𝜑 ∧ ∀ 𝑥𝑁 𝑀𝑈 ) → ( ( 𝑂 ‘ ( 𝑃 Σg ( 𝑥𝑁𝑀 ) ) ) ‘ 𝑌 ) = ( 𝑅 Σg ( 𝑥𝑁 ↦ ( ( 𝑂𝑀 ) ‘ 𝑌 ) ) ) ) )
85 84 expd ( 𝑁 ∈ Fin → ( 𝜑 → ( ∀ 𝑥𝑁 𝑀𝑈 → ( ( 𝑂 ‘ ( 𝑃 Σg ( 𝑥𝑁𝑀 ) ) ) ‘ 𝑌 ) = ( 𝑅 Σg ( 𝑥𝑁 ↦ ( ( 𝑂𝑀 ) ‘ 𝑌 ) ) ) ) ) )
86 8 85 mpcom ( 𝜑 → ( ∀ 𝑥𝑁 𝑀𝑈 → ( ( 𝑂 ‘ ( 𝑃 Σg ( 𝑥𝑁𝑀 ) ) ) ‘ 𝑌 ) = ( 𝑅 Σg ( 𝑥𝑁 ↦ ( ( 𝑂𝑀 ) ‘ 𝑌 ) ) ) ) )
87 7 86 mpd ( 𝜑 → ( ( 𝑂 ‘ ( 𝑃 Σg ( 𝑥𝑁𝑀 ) ) ) ‘ 𝑌 ) = ( 𝑅 Σg ( 𝑥𝑁 ↦ ( ( 𝑂𝑀 ) ‘ 𝑌 ) ) ) )