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 ( 𝑥 ∈ 𝑁 ↦ ( ( 𝑂 ‘ 𝑀 ) ‘ 𝑌 ) ) ) )