Metamath Proof Explorer


Theorem coe1fzgsumd

Description: Value of an evaluated coefficient in a finite group sum of polynomials. (Contributed by AV, 8-Oct-2019)

Ref Expression
Hypotheses coe1fzgsumd.p 𝑃 = ( Poly1𝑅 )
coe1fzgsumd.b 𝐵 = ( Base ‘ 𝑃 )
coe1fzgsumd.r ( 𝜑𝑅 ∈ Ring )
coe1fzgsumd.k ( 𝜑𝐾 ∈ ℕ0 )
coe1fzgsumd.m ( 𝜑 → ∀ 𝑥𝑁 𝑀𝐵 )
coe1fzgsumd.n ( 𝜑𝑁 ∈ Fin )
Assertion coe1fzgsumd ( 𝜑 → ( ( coe1 ‘ ( 𝑃 Σg ( 𝑥𝑁𝑀 ) ) ) ‘ 𝐾 ) = ( 𝑅 Σg ( 𝑥𝑁 ↦ ( ( coe1𝑀 ) ‘ 𝐾 ) ) ) )

Proof

Step Hyp Ref Expression
1 coe1fzgsumd.p 𝑃 = ( Poly1𝑅 )
2 coe1fzgsumd.b 𝐵 = ( Base ‘ 𝑃 )
3 coe1fzgsumd.r ( 𝜑𝑅 ∈ Ring )
4 coe1fzgsumd.k ( 𝜑𝐾 ∈ ℕ0 )
5 coe1fzgsumd.m ( 𝜑 → ∀ 𝑥𝑁 𝑀𝐵 )
6 coe1fzgsumd.n ( 𝜑𝑁 ∈ Fin )
7 raleq ( 𝑛 = ∅ → ( ∀ 𝑥𝑛 𝑀𝐵 ↔ ∀ 𝑥 ∈ ∅ 𝑀𝐵 ) )
8 7 anbi2d ( 𝑛 = ∅ → ( ( 𝜑 ∧ ∀ 𝑥𝑛 𝑀𝐵 ) ↔ ( 𝜑 ∧ ∀ 𝑥 ∈ ∅ 𝑀𝐵 ) ) )
9 mpteq1 ( 𝑛 = ∅ → ( 𝑥𝑛𝑀 ) = ( 𝑥 ∈ ∅ ↦ 𝑀 ) )
10 9 oveq2d ( 𝑛 = ∅ → ( 𝑃 Σg ( 𝑥𝑛𝑀 ) ) = ( 𝑃 Σg ( 𝑥 ∈ ∅ ↦ 𝑀 ) ) )
11 10 fveq2d ( 𝑛 = ∅ → ( coe1 ‘ ( 𝑃 Σg ( 𝑥𝑛𝑀 ) ) ) = ( coe1 ‘ ( 𝑃 Σg ( 𝑥 ∈ ∅ ↦ 𝑀 ) ) ) )
12 11 fveq1d ( 𝑛 = ∅ → ( ( coe1 ‘ ( 𝑃 Σg ( 𝑥𝑛𝑀 ) ) ) ‘ 𝐾 ) = ( ( coe1 ‘ ( 𝑃 Σg ( 𝑥 ∈ ∅ ↦ 𝑀 ) ) ) ‘ 𝐾 ) )
13 mpteq1 ( 𝑛 = ∅ → ( 𝑥𝑛 ↦ ( ( coe1𝑀 ) ‘ 𝐾 ) ) = ( 𝑥 ∈ ∅ ↦ ( ( coe1𝑀 ) ‘ 𝐾 ) ) )
14 13 oveq2d ( 𝑛 = ∅ → ( 𝑅 Σg ( 𝑥𝑛 ↦ ( ( coe1𝑀 ) ‘ 𝐾 ) ) ) = ( 𝑅 Σg ( 𝑥 ∈ ∅ ↦ ( ( coe1𝑀 ) ‘ 𝐾 ) ) ) )
15 12 14 eqeq12d ( 𝑛 = ∅ → ( ( ( coe1 ‘ ( 𝑃 Σg ( 𝑥𝑛𝑀 ) ) ) ‘ 𝐾 ) = ( 𝑅 Σg ( 𝑥𝑛 ↦ ( ( coe1𝑀 ) ‘ 𝐾 ) ) ) ↔ ( ( coe1 ‘ ( 𝑃 Σg ( 𝑥 ∈ ∅ ↦ 𝑀 ) ) ) ‘ 𝐾 ) = ( 𝑅 Σg ( 𝑥 ∈ ∅ ↦ ( ( coe1𝑀 ) ‘ 𝐾 ) ) ) ) )
16 8 15 imbi12d ( 𝑛 = ∅ → ( ( ( 𝜑 ∧ ∀ 𝑥𝑛 𝑀𝐵 ) → ( ( coe1 ‘ ( 𝑃 Σg ( 𝑥𝑛𝑀 ) ) ) ‘ 𝐾 ) = ( 𝑅 Σg ( 𝑥𝑛 ↦ ( ( coe1𝑀 ) ‘ 𝐾 ) ) ) ) ↔ ( ( 𝜑 ∧ ∀ 𝑥 ∈ ∅ 𝑀𝐵 ) → ( ( coe1 ‘ ( 𝑃 Σg ( 𝑥 ∈ ∅ ↦ 𝑀 ) ) ) ‘ 𝐾 ) = ( 𝑅 Σg ( 𝑥 ∈ ∅ ↦ ( ( coe1𝑀 ) ‘ 𝐾 ) ) ) ) ) )
17 raleq ( 𝑛 = 𝑚 → ( ∀ 𝑥𝑛 𝑀𝐵 ↔ ∀ 𝑥𝑚 𝑀𝐵 ) )
18 17 anbi2d ( 𝑛 = 𝑚 → ( ( 𝜑 ∧ ∀ 𝑥𝑛 𝑀𝐵 ) ↔ ( 𝜑 ∧ ∀ 𝑥𝑚 𝑀𝐵 ) ) )
19 mpteq1 ( 𝑛 = 𝑚 → ( 𝑥𝑛𝑀 ) = ( 𝑥𝑚𝑀 ) )
20 19 oveq2d ( 𝑛 = 𝑚 → ( 𝑃 Σg ( 𝑥𝑛𝑀 ) ) = ( 𝑃 Σg ( 𝑥𝑚𝑀 ) ) )
21 20 fveq2d ( 𝑛 = 𝑚 → ( coe1 ‘ ( 𝑃 Σg ( 𝑥𝑛𝑀 ) ) ) = ( coe1 ‘ ( 𝑃 Σg ( 𝑥𝑚𝑀 ) ) ) )
22 21 fveq1d ( 𝑛 = 𝑚 → ( ( coe1 ‘ ( 𝑃 Σg ( 𝑥𝑛𝑀 ) ) ) ‘ 𝐾 ) = ( ( coe1 ‘ ( 𝑃 Σg ( 𝑥𝑚𝑀 ) ) ) ‘ 𝐾 ) )
23 mpteq1 ( 𝑛 = 𝑚 → ( 𝑥𝑛 ↦ ( ( coe1𝑀 ) ‘ 𝐾 ) ) = ( 𝑥𝑚 ↦ ( ( coe1𝑀 ) ‘ 𝐾 ) ) )
24 23 oveq2d ( 𝑛 = 𝑚 → ( 𝑅 Σg ( 𝑥𝑛 ↦ ( ( coe1𝑀 ) ‘ 𝐾 ) ) ) = ( 𝑅 Σg ( 𝑥𝑚 ↦ ( ( coe1𝑀 ) ‘ 𝐾 ) ) ) )
25 22 24 eqeq12d ( 𝑛 = 𝑚 → ( ( ( coe1 ‘ ( 𝑃 Σg ( 𝑥𝑛𝑀 ) ) ) ‘ 𝐾 ) = ( 𝑅 Σg ( 𝑥𝑛 ↦ ( ( coe1𝑀 ) ‘ 𝐾 ) ) ) ↔ ( ( coe1 ‘ ( 𝑃 Σg ( 𝑥𝑚𝑀 ) ) ) ‘ 𝐾 ) = ( 𝑅 Σg ( 𝑥𝑚 ↦ ( ( coe1𝑀 ) ‘ 𝐾 ) ) ) ) )
26 18 25 imbi12d ( 𝑛 = 𝑚 → ( ( ( 𝜑 ∧ ∀ 𝑥𝑛 𝑀𝐵 ) → ( ( coe1 ‘ ( 𝑃 Σg ( 𝑥𝑛𝑀 ) ) ) ‘ 𝐾 ) = ( 𝑅 Σg ( 𝑥𝑛 ↦ ( ( coe1𝑀 ) ‘ 𝐾 ) ) ) ) ↔ ( ( 𝜑 ∧ ∀ 𝑥𝑚 𝑀𝐵 ) → ( ( coe1 ‘ ( 𝑃 Σg ( 𝑥𝑚𝑀 ) ) ) ‘ 𝐾 ) = ( 𝑅 Σg ( 𝑥𝑚 ↦ ( ( coe1𝑀 ) ‘ 𝐾 ) ) ) ) ) )
27 raleq ( 𝑛 = ( 𝑚 ∪ { 𝑎 } ) → ( ∀ 𝑥𝑛 𝑀𝐵 ↔ ∀ 𝑥 ∈ ( 𝑚 ∪ { 𝑎 } ) 𝑀𝐵 ) )
28 27 anbi2d ( 𝑛 = ( 𝑚 ∪ { 𝑎 } ) → ( ( 𝜑 ∧ ∀ 𝑥𝑛 𝑀𝐵 ) ↔ ( 𝜑 ∧ ∀ 𝑥 ∈ ( 𝑚 ∪ { 𝑎 } ) 𝑀𝐵 ) ) )
29 mpteq1 ( 𝑛 = ( 𝑚 ∪ { 𝑎 } ) → ( 𝑥𝑛𝑀 ) = ( 𝑥 ∈ ( 𝑚 ∪ { 𝑎 } ) ↦ 𝑀 ) )
30 29 oveq2d ( 𝑛 = ( 𝑚 ∪ { 𝑎 } ) → ( 𝑃 Σg ( 𝑥𝑛𝑀 ) ) = ( 𝑃 Σg ( 𝑥 ∈ ( 𝑚 ∪ { 𝑎 } ) ↦ 𝑀 ) ) )
31 30 fveq2d ( 𝑛 = ( 𝑚 ∪ { 𝑎 } ) → ( coe1 ‘ ( 𝑃 Σg ( 𝑥𝑛𝑀 ) ) ) = ( coe1 ‘ ( 𝑃 Σg ( 𝑥 ∈ ( 𝑚 ∪ { 𝑎 } ) ↦ 𝑀 ) ) ) )
32 31 fveq1d ( 𝑛 = ( 𝑚 ∪ { 𝑎 } ) → ( ( coe1 ‘ ( 𝑃 Σg ( 𝑥𝑛𝑀 ) ) ) ‘ 𝐾 ) = ( ( coe1 ‘ ( 𝑃 Σg ( 𝑥 ∈ ( 𝑚 ∪ { 𝑎 } ) ↦ 𝑀 ) ) ) ‘ 𝐾 ) )
33 mpteq1 ( 𝑛 = ( 𝑚 ∪ { 𝑎 } ) → ( 𝑥𝑛 ↦ ( ( coe1𝑀 ) ‘ 𝐾 ) ) = ( 𝑥 ∈ ( 𝑚 ∪ { 𝑎 } ) ↦ ( ( coe1𝑀 ) ‘ 𝐾 ) ) )
34 33 oveq2d ( 𝑛 = ( 𝑚 ∪ { 𝑎 } ) → ( 𝑅 Σg ( 𝑥𝑛 ↦ ( ( coe1𝑀 ) ‘ 𝐾 ) ) ) = ( 𝑅 Σg ( 𝑥 ∈ ( 𝑚 ∪ { 𝑎 } ) ↦ ( ( coe1𝑀 ) ‘ 𝐾 ) ) ) )
35 32 34 eqeq12d ( 𝑛 = ( 𝑚 ∪ { 𝑎 } ) → ( ( ( coe1 ‘ ( 𝑃 Σg ( 𝑥𝑛𝑀 ) ) ) ‘ 𝐾 ) = ( 𝑅 Σg ( 𝑥𝑛 ↦ ( ( coe1𝑀 ) ‘ 𝐾 ) ) ) ↔ ( ( coe1 ‘ ( 𝑃 Σg ( 𝑥 ∈ ( 𝑚 ∪ { 𝑎 } ) ↦ 𝑀 ) ) ) ‘ 𝐾 ) = ( 𝑅 Σg ( 𝑥 ∈ ( 𝑚 ∪ { 𝑎 } ) ↦ ( ( coe1𝑀 ) ‘ 𝐾 ) ) ) ) )
36 28 35 imbi12d ( 𝑛 = ( 𝑚 ∪ { 𝑎 } ) → ( ( ( 𝜑 ∧ ∀ 𝑥𝑛 𝑀𝐵 ) → ( ( coe1 ‘ ( 𝑃 Σg ( 𝑥𝑛𝑀 ) ) ) ‘ 𝐾 ) = ( 𝑅 Σg ( 𝑥𝑛 ↦ ( ( coe1𝑀 ) ‘ 𝐾 ) ) ) ) ↔ ( ( 𝜑 ∧ ∀ 𝑥 ∈ ( 𝑚 ∪ { 𝑎 } ) 𝑀𝐵 ) → ( ( coe1 ‘ ( 𝑃 Σg ( 𝑥 ∈ ( 𝑚 ∪ { 𝑎 } ) ↦ 𝑀 ) ) ) ‘ 𝐾 ) = ( 𝑅 Σg ( 𝑥 ∈ ( 𝑚 ∪ { 𝑎 } ) ↦ ( ( coe1𝑀 ) ‘ 𝐾 ) ) ) ) ) )
37 raleq ( 𝑛 = 𝑁 → ( ∀ 𝑥𝑛 𝑀𝐵 ↔ ∀ 𝑥𝑁 𝑀𝐵 ) )
38 37 anbi2d ( 𝑛 = 𝑁 → ( ( 𝜑 ∧ ∀ 𝑥𝑛 𝑀𝐵 ) ↔ ( 𝜑 ∧ ∀ 𝑥𝑁 𝑀𝐵 ) ) )
39 mpteq1 ( 𝑛 = 𝑁 → ( 𝑥𝑛𝑀 ) = ( 𝑥𝑁𝑀 ) )
40 39 oveq2d ( 𝑛 = 𝑁 → ( 𝑃 Σg ( 𝑥𝑛𝑀 ) ) = ( 𝑃 Σg ( 𝑥𝑁𝑀 ) ) )
41 40 fveq2d ( 𝑛 = 𝑁 → ( coe1 ‘ ( 𝑃 Σg ( 𝑥𝑛𝑀 ) ) ) = ( coe1 ‘ ( 𝑃 Σg ( 𝑥𝑁𝑀 ) ) ) )
42 41 fveq1d ( 𝑛 = 𝑁 → ( ( coe1 ‘ ( 𝑃 Σg ( 𝑥𝑛𝑀 ) ) ) ‘ 𝐾 ) = ( ( coe1 ‘ ( 𝑃 Σg ( 𝑥𝑁𝑀 ) ) ) ‘ 𝐾 ) )
43 mpteq1 ( 𝑛 = 𝑁 → ( 𝑥𝑛 ↦ ( ( coe1𝑀 ) ‘ 𝐾 ) ) = ( 𝑥𝑁 ↦ ( ( coe1𝑀 ) ‘ 𝐾 ) ) )
44 43 oveq2d ( 𝑛 = 𝑁 → ( 𝑅 Σg ( 𝑥𝑛 ↦ ( ( coe1𝑀 ) ‘ 𝐾 ) ) ) = ( 𝑅 Σg ( 𝑥𝑁 ↦ ( ( coe1𝑀 ) ‘ 𝐾 ) ) ) )
45 42 44 eqeq12d ( 𝑛 = 𝑁 → ( ( ( coe1 ‘ ( 𝑃 Σg ( 𝑥𝑛𝑀 ) ) ) ‘ 𝐾 ) = ( 𝑅 Σg ( 𝑥𝑛 ↦ ( ( coe1𝑀 ) ‘ 𝐾 ) ) ) ↔ ( ( coe1 ‘ ( 𝑃 Σg ( 𝑥𝑁𝑀 ) ) ) ‘ 𝐾 ) = ( 𝑅 Σg ( 𝑥𝑁 ↦ ( ( coe1𝑀 ) ‘ 𝐾 ) ) ) ) )
46 38 45 imbi12d ( 𝑛 = 𝑁 → ( ( ( 𝜑 ∧ ∀ 𝑥𝑛 𝑀𝐵 ) → ( ( coe1 ‘ ( 𝑃 Σg ( 𝑥𝑛𝑀 ) ) ) ‘ 𝐾 ) = ( 𝑅 Σg ( 𝑥𝑛 ↦ ( ( coe1𝑀 ) ‘ 𝐾 ) ) ) ) ↔ ( ( 𝜑 ∧ ∀ 𝑥𝑁 𝑀𝐵 ) → ( ( coe1 ‘ ( 𝑃 Σg ( 𝑥𝑁𝑀 ) ) ) ‘ 𝐾 ) = ( 𝑅 Σg ( 𝑥𝑁 ↦ ( ( coe1𝑀 ) ‘ 𝐾 ) ) ) ) ) )
47 mpt0 ( 𝑥 ∈ ∅ ↦ 𝑀 ) = ∅
48 47 oveq2i ( 𝑃 Σg ( 𝑥 ∈ ∅ ↦ 𝑀 ) ) = ( 𝑃 Σg ∅ )
49 eqid ( 0g𝑃 ) = ( 0g𝑃 )
50 49 gsum0 ( 𝑃 Σg ∅ ) = ( 0g𝑃 )
51 48 50 eqtri ( 𝑃 Σg ( 𝑥 ∈ ∅ ↦ 𝑀 ) ) = ( 0g𝑃 )
52 51 fveq2i ( coe1 ‘ ( 𝑃 Σg ( 𝑥 ∈ ∅ ↦ 𝑀 ) ) ) = ( coe1 ‘ ( 0g𝑃 ) )
53 52 a1i ( 𝜑 → ( coe1 ‘ ( 𝑃 Σg ( 𝑥 ∈ ∅ ↦ 𝑀 ) ) ) = ( coe1 ‘ ( 0g𝑃 ) ) )
54 53 fveq1d ( 𝜑 → ( ( coe1 ‘ ( 𝑃 Σg ( 𝑥 ∈ ∅ ↦ 𝑀 ) ) ) ‘ 𝐾 ) = ( ( coe1 ‘ ( 0g𝑃 ) ) ‘ 𝐾 ) )
55 eqid ( 0g𝑅 ) = ( 0g𝑅 )
56 1 49 55 coe1z ( 𝑅 ∈ Ring → ( coe1 ‘ ( 0g𝑃 ) ) = ( ℕ0 × { ( 0g𝑅 ) } ) )
57 3 56 syl ( 𝜑 → ( coe1 ‘ ( 0g𝑃 ) ) = ( ℕ0 × { ( 0g𝑅 ) } ) )
58 57 fveq1d ( 𝜑 → ( ( coe1 ‘ ( 0g𝑃 ) ) ‘ 𝐾 ) = ( ( ℕ0 × { ( 0g𝑅 ) } ) ‘ 𝐾 ) )
59 fvex ( 0g𝑅 ) ∈ V
60 fvconst2g ( ( ( 0g𝑅 ) ∈ V ∧ 𝐾 ∈ ℕ0 ) → ( ( ℕ0 × { ( 0g𝑅 ) } ) ‘ 𝐾 ) = ( 0g𝑅 ) )
61 59 4 60 sylancr ( 𝜑 → ( ( ℕ0 × { ( 0g𝑅 ) } ) ‘ 𝐾 ) = ( 0g𝑅 ) )
62 54 58 61 3eqtrd ( 𝜑 → ( ( coe1 ‘ ( 𝑃 Σg ( 𝑥 ∈ ∅ ↦ 𝑀 ) ) ) ‘ 𝐾 ) = ( 0g𝑅 ) )
63 mpt0 ( 𝑥 ∈ ∅ ↦ ( ( coe1𝑀 ) ‘ 𝐾 ) ) = ∅
64 63 oveq2i ( 𝑅 Σg ( 𝑥 ∈ ∅ ↦ ( ( coe1𝑀 ) ‘ 𝐾 ) ) ) = ( 𝑅 Σg ∅ )
65 55 gsum0 ( 𝑅 Σg ∅ ) = ( 0g𝑅 )
66 64 65 eqtri ( 𝑅 Σg ( 𝑥 ∈ ∅ ↦ ( ( coe1𝑀 ) ‘ 𝐾 ) ) ) = ( 0g𝑅 )
67 62 66 eqtr4di ( 𝜑 → ( ( coe1 ‘ ( 𝑃 Σg ( 𝑥 ∈ ∅ ↦ 𝑀 ) ) ) ‘ 𝐾 ) = ( 𝑅 Σg ( 𝑥 ∈ ∅ ↦ ( ( coe1𝑀 ) ‘ 𝐾 ) ) ) )
68 67 adantr ( ( 𝜑 ∧ ∀ 𝑥 ∈ ∅ 𝑀𝐵 ) → ( ( coe1 ‘ ( 𝑃 Σg ( 𝑥 ∈ ∅ ↦ 𝑀 ) ) ) ‘ 𝐾 ) = ( 𝑅 Σg ( 𝑥 ∈ ∅ ↦ ( ( coe1𝑀 ) ‘ 𝐾 ) ) ) )
69 1 2 3 4 coe1fzgsumdlem ( ( 𝑚 ∈ Fin ∧ ¬ 𝑎𝑚𝜑 ) → ( ( ∀ 𝑥𝑚 𝑀𝐵 → ( ( coe1 ‘ ( 𝑃 Σg ( 𝑥𝑚𝑀 ) ) ) ‘ 𝐾 ) = ( 𝑅 Σg ( 𝑥𝑚 ↦ ( ( coe1𝑀 ) ‘ 𝐾 ) ) ) ) → ( ∀ 𝑥 ∈ ( 𝑚 ∪ { 𝑎 } ) 𝑀𝐵 → ( ( coe1 ‘ ( 𝑃 Σg ( 𝑥 ∈ ( 𝑚 ∪ { 𝑎 } ) ↦ 𝑀 ) ) ) ‘ 𝐾 ) = ( 𝑅 Σg ( 𝑥 ∈ ( 𝑚 ∪ { 𝑎 } ) ↦ ( ( coe1𝑀 ) ‘ 𝐾 ) ) ) ) ) )
70 69 3expia ( ( 𝑚 ∈ Fin ∧ ¬ 𝑎𝑚 ) → ( 𝜑 → ( ( ∀ 𝑥𝑚 𝑀𝐵 → ( ( coe1 ‘ ( 𝑃 Σg ( 𝑥𝑚𝑀 ) ) ) ‘ 𝐾 ) = ( 𝑅 Σg ( 𝑥𝑚 ↦ ( ( coe1𝑀 ) ‘ 𝐾 ) ) ) ) → ( ∀ 𝑥 ∈ ( 𝑚 ∪ { 𝑎 } ) 𝑀𝐵 → ( ( coe1 ‘ ( 𝑃 Σg ( 𝑥 ∈ ( 𝑚 ∪ { 𝑎 } ) ↦ 𝑀 ) ) ) ‘ 𝐾 ) = ( 𝑅 Σg ( 𝑥 ∈ ( 𝑚 ∪ { 𝑎 } ) ↦ ( ( coe1𝑀 ) ‘ 𝐾 ) ) ) ) ) ) )
71 70 a2d ( ( 𝑚 ∈ Fin ∧ ¬ 𝑎𝑚 ) → ( ( 𝜑 → ( ∀ 𝑥𝑚 𝑀𝐵 → ( ( coe1 ‘ ( 𝑃 Σg ( 𝑥𝑚𝑀 ) ) ) ‘ 𝐾 ) = ( 𝑅 Σg ( 𝑥𝑚 ↦ ( ( coe1𝑀 ) ‘ 𝐾 ) ) ) ) ) → ( 𝜑 → ( ∀ 𝑥 ∈ ( 𝑚 ∪ { 𝑎 } ) 𝑀𝐵 → ( ( coe1 ‘ ( 𝑃 Σg ( 𝑥 ∈ ( 𝑚 ∪ { 𝑎 } ) ↦ 𝑀 ) ) ) ‘ 𝐾 ) = ( 𝑅 Σg ( 𝑥 ∈ ( 𝑚 ∪ { 𝑎 } ) ↦ ( ( coe1𝑀 ) ‘ 𝐾 ) ) ) ) ) ) )
72 impexp ( ( ( 𝜑 ∧ ∀ 𝑥𝑚 𝑀𝐵 ) → ( ( coe1 ‘ ( 𝑃 Σg ( 𝑥𝑚𝑀 ) ) ) ‘ 𝐾 ) = ( 𝑅 Σg ( 𝑥𝑚 ↦ ( ( coe1𝑀 ) ‘ 𝐾 ) ) ) ) ↔ ( 𝜑 → ( ∀ 𝑥𝑚 𝑀𝐵 → ( ( coe1 ‘ ( 𝑃 Σg ( 𝑥𝑚𝑀 ) ) ) ‘ 𝐾 ) = ( 𝑅 Σg ( 𝑥𝑚 ↦ ( ( coe1𝑀 ) ‘ 𝐾 ) ) ) ) ) )
73 impexp ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ ( 𝑚 ∪ { 𝑎 } ) 𝑀𝐵 ) → ( ( coe1 ‘ ( 𝑃 Σg ( 𝑥 ∈ ( 𝑚 ∪ { 𝑎 } ) ↦ 𝑀 ) ) ) ‘ 𝐾 ) = ( 𝑅 Σg ( 𝑥 ∈ ( 𝑚 ∪ { 𝑎 } ) ↦ ( ( coe1𝑀 ) ‘ 𝐾 ) ) ) ) ↔ ( 𝜑 → ( ∀ 𝑥 ∈ ( 𝑚 ∪ { 𝑎 } ) 𝑀𝐵 → ( ( coe1 ‘ ( 𝑃 Σg ( 𝑥 ∈ ( 𝑚 ∪ { 𝑎 } ) ↦ 𝑀 ) ) ) ‘ 𝐾 ) = ( 𝑅 Σg ( 𝑥 ∈ ( 𝑚 ∪ { 𝑎 } ) ↦ ( ( coe1𝑀 ) ‘ 𝐾 ) ) ) ) ) )
74 71 72 73 3imtr4g ( ( 𝑚 ∈ Fin ∧ ¬ 𝑎𝑚 ) → ( ( ( 𝜑 ∧ ∀ 𝑥𝑚 𝑀𝐵 ) → ( ( coe1 ‘ ( 𝑃 Σg ( 𝑥𝑚𝑀 ) ) ) ‘ 𝐾 ) = ( 𝑅 Σg ( 𝑥𝑚 ↦ ( ( coe1𝑀 ) ‘ 𝐾 ) ) ) ) → ( ( 𝜑 ∧ ∀ 𝑥 ∈ ( 𝑚 ∪ { 𝑎 } ) 𝑀𝐵 ) → ( ( coe1 ‘ ( 𝑃 Σg ( 𝑥 ∈ ( 𝑚 ∪ { 𝑎 } ) ↦ 𝑀 ) ) ) ‘ 𝐾 ) = ( 𝑅 Σg ( 𝑥 ∈ ( 𝑚 ∪ { 𝑎 } ) ↦ ( ( coe1𝑀 ) ‘ 𝐾 ) ) ) ) ) )
75 16 26 36 46 68 74 findcard2s ( 𝑁 ∈ Fin → ( ( 𝜑 ∧ ∀ 𝑥𝑁 𝑀𝐵 ) → ( ( coe1 ‘ ( 𝑃 Σg ( 𝑥𝑁𝑀 ) ) ) ‘ 𝐾 ) = ( 𝑅 Σg ( 𝑥𝑁 ↦ ( ( coe1𝑀 ) ‘ 𝐾 ) ) ) ) )
76 75 expd ( 𝑁 ∈ Fin → ( 𝜑 → ( ∀ 𝑥𝑁 𝑀𝐵 → ( ( coe1 ‘ ( 𝑃 Σg ( 𝑥𝑁𝑀 ) ) ) ‘ 𝐾 ) = ( 𝑅 Σg ( 𝑥𝑁 ↦ ( ( coe1𝑀 ) ‘ 𝐾 ) ) ) ) ) )
77 6 76 mpcom ( 𝜑 → ( ∀ 𝑥𝑁 𝑀𝐵 → ( ( coe1 ‘ ( 𝑃 Σg ( 𝑥𝑁𝑀 ) ) ) ‘ 𝐾 ) = ( 𝑅 Σg ( 𝑥𝑁 ↦ ( ( coe1𝑀 ) ‘ 𝐾 ) ) ) ) )
78 5 77 mpd ( 𝜑 → ( ( coe1 ‘ ( 𝑃 Σg ( 𝑥𝑁𝑀 ) ) ) ‘ 𝐾 ) = ( 𝑅 Σg ( 𝑥𝑁 ↦ ( ( coe1𝑀 ) ‘ 𝐾 ) ) ) )