# Metamath Proof Explorer

## Theorem evl1gsumdlem

Description: Lemma for evl1gsumd (induction step). (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 ( 𝜑𝑌𝐵 )
Assertion evl1gsumdlem ( ( 𝑚 ∈ Fin ∧ ¬ 𝑎𝑚𝜑 ) → ( ( ∀ 𝑥𝑚 𝑀𝑈 → ( ( 𝑂 ‘ ( 𝑃 Σg ( 𝑥𝑚𝑀 ) ) ) ‘ 𝑌 ) = ( 𝑅 Σg ( 𝑥𝑚 ↦ ( ( 𝑂𝑀 ) ‘ 𝑌 ) ) ) ) → ( ∀ 𝑥 ∈ ( 𝑚 ∪ { 𝑎 } ) 𝑀𝑈 → ( ( 𝑂 ‘ ( 𝑃 Σ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 ralunb ( ∀ 𝑥 ∈ ( 𝑚 ∪ { 𝑎 } ) 𝑀𝑈 ↔ ( ∀ 𝑥𝑚 𝑀𝑈 ∧ ∀ 𝑥 ∈ { 𝑎 } 𝑀𝑈 ) )
8 nfcv 𝑦 𝑀
9 nfcsb1v 𝑥 𝑦 / 𝑥 𝑀
10 csbeq1a ( 𝑥 = 𝑦𝑀 = 𝑦 / 𝑥 𝑀 )
11 8 9 10 cbvmpt ( 𝑥 ∈ ( 𝑚 ∪ { 𝑎 } ) ↦ 𝑀 ) = ( 𝑦 ∈ ( 𝑚 ∪ { 𝑎 } ) ↦ 𝑦 / 𝑥 𝑀 )
12 11 oveq2i ( 𝑃 Σg ( 𝑥 ∈ ( 𝑚 ∪ { 𝑎 } ) ↦ 𝑀 ) ) = ( 𝑃 Σg ( 𝑦 ∈ ( 𝑚 ∪ { 𝑎 } ) ↦ 𝑦 / 𝑥 𝑀 ) )
13 eqid ( +g𝑃 ) = ( +g𝑃 )
14 crngring ( 𝑅 ∈ CRing → 𝑅 ∈ Ring )
15 5 14 syl ( 𝜑𝑅 ∈ Ring )
16 2 ply1ring ( 𝑅 ∈ Ring → 𝑃 ∈ Ring )
17 15 16 syl ( 𝜑𝑃 ∈ Ring )
18 ringcmn ( 𝑃 ∈ Ring → 𝑃 ∈ CMnd )
19 17 18 syl ( 𝜑𝑃 ∈ CMnd )
20 19 3ad2ant3 ( ( 𝑚 ∈ Fin ∧ ¬ 𝑎𝑚𝜑 ) → 𝑃 ∈ CMnd )
21 20 ad2antrr ( ( ( ( 𝑚 ∈ Fin ∧ ¬ 𝑎𝑚𝜑 ) ∧ ∀ 𝑥𝑚 𝑀𝑈 ) ∧ ∀ 𝑥 ∈ { 𝑎 } 𝑀𝑈 ) → 𝑃 ∈ CMnd )
22 simpll1 ( ( ( ( 𝑚 ∈ Fin ∧ ¬ 𝑎𝑚𝜑 ) ∧ ∀ 𝑥𝑚 𝑀𝑈 ) ∧ ∀ 𝑥 ∈ { 𝑎 } 𝑀𝑈 ) → 𝑚 ∈ Fin )
23 rspcsbela ( ( 𝑦𝑚 ∧ ∀ 𝑥𝑚 𝑀𝑈 ) → 𝑦 / 𝑥 𝑀𝑈 )
24 23 expcom ( ∀ 𝑥𝑚 𝑀𝑈 → ( 𝑦𝑚 𝑦 / 𝑥 𝑀𝑈 ) )
25 24 adantl ( ( ( 𝑚 ∈ Fin ∧ ¬ 𝑎𝑚𝜑 ) ∧ ∀ 𝑥𝑚 𝑀𝑈 ) → ( 𝑦𝑚 𝑦 / 𝑥 𝑀𝑈 ) )
26 25 adantr ( ( ( ( 𝑚 ∈ Fin ∧ ¬ 𝑎𝑚𝜑 ) ∧ ∀ 𝑥𝑚 𝑀𝑈 ) ∧ ∀ 𝑥 ∈ { 𝑎 } 𝑀𝑈 ) → ( 𝑦𝑚 𝑦 / 𝑥 𝑀𝑈 ) )
27 26 imp ( ( ( ( ( 𝑚 ∈ Fin ∧ ¬ 𝑎𝑚𝜑 ) ∧ ∀ 𝑥𝑚 𝑀𝑈 ) ∧ ∀ 𝑥 ∈ { 𝑎 } 𝑀𝑈 ) ∧ 𝑦𝑚 ) → 𝑦 / 𝑥 𝑀𝑈 )
28 vex 𝑎 ∈ V
29 28 a1i ( ( ( ( 𝑚 ∈ Fin ∧ ¬ 𝑎𝑚𝜑 ) ∧ ∀ 𝑥𝑚 𝑀𝑈 ) ∧ ∀ 𝑥 ∈ { 𝑎 } 𝑀𝑈 ) → 𝑎 ∈ V )
30 simpll2 ( ( ( ( 𝑚 ∈ Fin ∧ ¬ 𝑎𝑚𝜑 ) ∧ ∀ 𝑥𝑚 𝑀𝑈 ) ∧ ∀ 𝑥 ∈ { 𝑎 } 𝑀𝑈 ) → ¬ 𝑎𝑚 )
31 vsnid 𝑎 ∈ { 𝑎 }
32 rspcsbela ( ( 𝑎 ∈ { 𝑎 } ∧ ∀ 𝑥 ∈ { 𝑎 } 𝑀𝑈 ) → 𝑎 / 𝑥 𝑀𝑈 )
33 31 32 mpan ( ∀ 𝑥 ∈ { 𝑎 } 𝑀𝑈 𝑎 / 𝑥 𝑀𝑈 )
34 33 adantl ( ( ( ( 𝑚 ∈ Fin ∧ ¬ 𝑎𝑚𝜑 ) ∧ ∀ 𝑥𝑚 𝑀𝑈 ) ∧ ∀ 𝑥 ∈ { 𝑎 } 𝑀𝑈 ) → 𝑎 / 𝑥 𝑀𝑈 )
35 csbeq1 ( 𝑦 = 𝑎 𝑦 / 𝑥 𝑀 = 𝑎 / 𝑥 𝑀 )
36 4 13 21 22 27 29 30 34 35 gsumunsn ( ( ( ( 𝑚 ∈ Fin ∧ ¬ 𝑎𝑚𝜑 ) ∧ ∀ 𝑥𝑚 𝑀𝑈 ) ∧ ∀ 𝑥 ∈ { 𝑎 } 𝑀𝑈 ) → ( 𝑃 Σg ( 𝑦 ∈ ( 𝑚 ∪ { 𝑎 } ) ↦ 𝑦 / 𝑥 𝑀 ) ) = ( ( 𝑃 Σg ( 𝑦𝑚 𝑦 / 𝑥 𝑀 ) ) ( +g𝑃 ) 𝑎 / 𝑥 𝑀 ) )
37 12 36 syl5eq ( ( ( ( 𝑚 ∈ Fin ∧ ¬ 𝑎𝑚𝜑 ) ∧ ∀ 𝑥𝑚 𝑀𝑈 ) ∧ ∀ 𝑥 ∈ { 𝑎 } 𝑀𝑈 ) → ( 𝑃 Σg ( 𝑥 ∈ ( 𝑚 ∪ { 𝑎 } ) ↦ 𝑀 ) ) = ( ( 𝑃 Σg ( 𝑦𝑚 𝑦 / 𝑥 𝑀 ) ) ( +g𝑃 ) 𝑎 / 𝑥 𝑀 ) )
38 8 9 10 cbvmpt ( 𝑥𝑚𝑀 ) = ( 𝑦𝑚 𝑦 / 𝑥 𝑀 )
39 38 eqcomi ( 𝑦𝑚 𝑦 / 𝑥 𝑀 ) = ( 𝑥𝑚𝑀 )
40 39 oveq2i ( 𝑃 Σg ( 𝑦𝑚 𝑦 / 𝑥 𝑀 ) ) = ( 𝑃 Σg ( 𝑥𝑚𝑀 ) )
41 40 oveq1i ( ( 𝑃 Σg ( 𝑦𝑚 𝑦 / 𝑥 𝑀 ) ) ( +g𝑃 ) 𝑎 / 𝑥 𝑀 ) = ( ( 𝑃 Σg ( 𝑥𝑚𝑀 ) ) ( +g𝑃 ) 𝑎 / 𝑥 𝑀 )
42 37 41 eqtrdi ( ( ( ( 𝑚 ∈ Fin ∧ ¬ 𝑎𝑚𝜑 ) ∧ ∀ 𝑥𝑚 𝑀𝑈 ) ∧ ∀ 𝑥 ∈ { 𝑎 } 𝑀𝑈 ) → ( 𝑃 Σg ( 𝑥 ∈ ( 𝑚 ∪ { 𝑎 } ) ↦ 𝑀 ) ) = ( ( 𝑃 Σg ( 𝑥𝑚𝑀 ) ) ( +g𝑃 ) 𝑎 / 𝑥 𝑀 ) )
43 42 fveq2d ( ( ( ( 𝑚 ∈ Fin ∧ ¬ 𝑎𝑚𝜑 ) ∧ ∀ 𝑥𝑚 𝑀𝑈 ) ∧ ∀ 𝑥 ∈ { 𝑎 } 𝑀𝑈 ) → ( 𝑂 ‘ ( 𝑃 Σg ( 𝑥 ∈ ( 𝑚 ∪ { 𝑎 } ) ↦ 𝑀 ) ) ) = ( 𝑂 ‘ ( ( 𝑃 Σg ( 𝑥𝑚𝑀 ) ) ( +g𝑃 ) 𝑎 / 𝑥 𝑀 ) ) )
44 43 fveq1d ( ( ( ( 𝑚 ∈ Fin ∧ ¬ 𝑎𝑚𝜑 ) ∧ ∀ 𝑥𝑚 𝑀𝑈 ) ∧ ∀ 𝑥 ∈ { 𝑎 } 𝑀𝑈 ) → ( ( 𝑂 ‘ ( 𝑃 Σg ( 𝑥 ∈ ( 𝑚 ∪ { 𝑎 } ) ↦ 𝑀 ) ) ) ‘ 𝑌 ) = ( ( 𝑂 ‘ ( ( 𝑃 Σg ( 𝑥𝑚𝑀 ) ) ( +g𝑃 ) 𝑎 / 𝑥 𝑀 ) ) ‘ 𝑌 ) )
45 5 3ad2ant3 ( ( 𝑚 ∈ Fin ∧ ¬ 𝑎𝑚𝜑 ) → 𝑅 ∈ CRing )
46 45 ad2antrr ( ( ( ( 𝑚 ∈ Fin ∧ ¬ 𝑎𝑚𝜑 ) ∧ ∀ 𝑥𝑚 𝑀𝑈 ) ∧ ∀ 𝑥 ∈ { 𝑎 } 𝑀𝑈 ) → 𝑅 ∈ CRing )
47 6 3ad2ant3 ( ( 𝑚 ∈ Fin ∧ ¬ 𝑎𝑚𝜑 ) → 𝑌𝐵 )
48 47 ad2antrr ( ( ( ( 𝑚 ∈ Fin ∧ ¬ 𝑎𝑚𝜑 ) ∧ ∀ 𝑥𝑚 𝑀𝑈 ) ∧ ∀ 𝑥 ∈ { 𝑎 } 𝑀𝑈 ) → 𝑌𝐵 )
49 simplr ( ( ( ( 𝑚 ∈ Fin ∧ ¬ 𝑎𝑚𝜑 ) ∧ ∀ 𝑥𝑚 𝑀𝑈 ) ∧ ∀ 𝑥 ∈ { 𝑎 } 𝑀𝑈 ) → ∀ 𝑥𝑚 𝑀𝑈 )
50 4 21 22 49 gsummptcl ( ( ( ( 𝑚 ∈ Fin ∧ ¬ 𝑎𝑚𝜑 ) ∧ ∀ 𝑥𝑚 𝑀𝑈 ) ∧ ∀ 𝑥 ∈ { 𝑎 } 𝑀𝑈 ) → ( 𝑃 Σg ( 𝑥𝑚𝑀 ) ) ∈ 𝑈 )
51 eqidd ( ( ( ( 𝑚 ∈ Fin ∧ ¬ 𝑎𝑚𝜑 ) ∧ ∀ 𝑥𝑚 𝑀𝑈 ) ∧ ∀ 𝑥 ∈ { 𝑎 } 𝑀𝑈 ) → ( ( 𝑂 ‘ ( 𝑃 Σg ( 𝑥𝑚𝑀 ) ) ) ‘ 𝑌 ) = ( ( 𝑂 ‘ ( 𝑃 Σg ( 𝑥𝑚𝑀 ) ) ) ‘ 𝑌 ) )
52 50 51 jca ( ( ( ( 𝑚 ∈ Fin ∧ ¬ 𝑎𝑚𝜑 ) ∧ ∀ 𝑥𝑚 𝑀𝑈 ) ∧ ∀ 𝑥 ∈ { 𝑎 } 𝑀𝑈 ) → ( ( 𝑃 Σg ( 𝑥𝑚𝑀 ) ) ∈ 𝑈 ∧ ( ( 𝑂 ‘ ( 𝑃 Σg ( 𝑥𝑚𝑀 ) ) ) ‘ 𝑌 ) = ( ( 𝑂 ‘ ( 𝑃 Σg ( 𝑥𝑚𝑀 ) ) ) ‘ 𝑌 ) ) )
53 eqidd ( ( ( ( 𝑚 ∈ Fin ∧ ¬ 𝑎𝑚𝜑 ) ∧ ∀ 𝑥𝑚 𝑀𝑈 ) ∧ ∀ 𝑥 ∈ { 𝑎 } 𝑀𝑈 ) → ( ( 𝑂 𝑎 / 𝑥 𝑀 ) ‘ 𝑌 ) = ( ( 𝑂 𝑎 / 𝑥 𝑀 ) ‘ 𝑌 ) )
54 34 53 jca ( ( ( ( 𝑚 ∈ Fin ∧ ¬ 𝑎𝑚𝜑 ) ∧ ∀ 𝑥𝑚 𝑀𝑈 ) ∧ ∀ 𝑥 ∈ { 𝑎 } 𝑀𝑈 ) → ( 𝑎 / 𝑥 𝑀𝑈 ∧ ( ( 𝑂 𝑎 / 𝑥 𝑀 ) ‘ 𝑌 ) = ( ( 𝑂 𝑎 / 𝑥 𝑀 ) ‘ 𝑌 ) ) )
55 eqid ( +g𝑅 ) = ( +g𝑅 )
56 1 2 3 4 46 48 52 54 13 55 evl1addd ( ( ( ( 𝑚 ∈ Fin ∧ ¬ 𝑎𝑚𝜑 ) ∧ ∀ 𝑥𝑚 𝑀𝑈 ) ∧ ∀ 𝑥 ∈ { 𝑎 } 𝑀𝑈 ) → ( ( ( 𝑃 Σg ( 𝑥𝑚𝑀 ) ) ( +g𝑃 ) 𝑎 / 𝑥 𝑀 ) ∈ 𝑈 ∧ ( ( 𝑂 ‘ ( ( 𝑃 Σg ( 𝑥𝑚𝑀 ) ) ( +g𝑃 ) 𝑎 / 𝑥 𝑀 ) ) ‘ 𝑌 ) = ( ( ( 𝑂 ‘ ( 𝑃 Σg ( 𝑥𝑚𝑀 ) ) ) ‘ 𝑌 ) ( +g𝑅 ) ( ( 𝑂 𝑎 / 𝑥 𝑀 ) ‘ 𝑌 ) ) ) )
57 56 simprd ( ( ( ( 𝑚 ∈ Fin ∧ ¬ 𝑎𝑚𝜑 ) ∧ ∀ 𝑥𝑚 𝑀𝑈 ) ∧ ∀ 𝑥 ∈ { 𝑎 } 𝑀𝑈 ) → ( ( 𝑂 ‘ ( ( 𝑃 Σg ( 𝑥𝑚𝑀 ) ) ( +g𝑃 ) 𝑎 / 𝑥 𝑀 ) ) ‘ 𝑌 ) = ( ( ( 𝑂 ‘ ( 𝑃 Σg ( 𝑥𝑚𝑀 ) ) ) ‘ 𝑌 ) ( +g𝑅 ) ( ( 𝑂 𝑎 / 𝑥 𝑀 ) ‘ 𝑌 ) ) )
58 44 57 eqtrd ( ( ( ( 𝑚 ∈ Fin ∧ ¬ 𝑎𝑚𝜑 ) ∧ ∀ 𝑥𝑚 𝑀𝑈 ) ∧ ∀ 𝑥 ∈ { 𝑎 } 𝑀𝑈 ) → ( ( 𝑂 ‘ ( 𝑃 Σg ( 𝑥 ∈ ( 𝑚 ∪ { 𝑎 } ) ↦ 𝑀 ) ) ) ‘ 𝑌 ) = ( ( ( 𝑂 ‘ ( 𝑃 Σg ( 𝑥𝑚𝑀 ) ) ) ‘ 𝑌 ) ( +g𝑅 ) ( ( 𝑂 𝑎 / 𝑥 𝑀 ) ‘ 𝑌 ) ) )
59 oveq1 ( ( ( 𝑂 ‘ ( 𝑃 Σg ( 𝑥𝑚𝑀 ) ) ) ‘ 𝑌 ) = ( 𝑅 Σg ( 𝑥𝑚 ↦ ( ( 𝑂𝑀 ) ‘ 𝑌 ) ) ) → ( ( ( 𝑂 ‘ ( 𝑃 Σg ( 𝑥𝑚𝑀 ) ) ) ‘ 𝑌 ) ( +g𝑅 ) ( ( 𝑂 𝑎 / 𝑥 𝑀 ) ‘ 𝑌 ) ) = ( ( 𝑅 Σg ( 𝑥𝑚 ↦ ( ( 𝑂𝑀 ) ‘ 𝑌 ) ) ) ( +g𝑅 ) ( ( 𝑂 𝑎 / 𝑥 𝑀 ) ‘ 𝑌 ) ) )
60 58 59 sylan9eq ( ( ( ( ( 𝑚 ∈ Fin ∧ ¬ 𝑎𝑚𝜑 ) ∧ ∀ 𝑥𝑚 𝑀𝑈 ) ∧ ∀ 𝑥 ∈ { 𝑎 } 𝑀𝑈 ) ∧ ( ( 𝑂 ‘ ( 𝑃 Σg ( 𝑥𝑚𝑀 ) ) ) ‘ 𝑌 ) = ( 𝑅 Σg ( 𝑥𝑚 ↦ ( ( 𝑂𝑀 ) ‘ 𝑌 ) ) ) ) → ( ( 𝑂 ‘ ( 𝑃 Σg ( 𝑥 ∈ ( 𝑚 ∪ { 𝑎 } ) ↦ 𝑀 ) ) ) ‘ 𝑌 ) = ( ( 𝑅 Σg ( 𝑥𝑚 ↦ ( ( 𝑂𝑀 ) ‘ 𝑌 ) ) ) ( +g𝑅 ) ( ( 𝑂 𝑎 / 𝑥 𝑀 ) ‘ 𝑌 ) ) )
61 nfcv 𝑦 ( ( 𝑂𝑀 ) ‘ 𝑌 )
62 nfcsb1v 𝑥 𝑦 / 𝑥 ( ( 𝑂𝑀 ) ‘ 𝑌 )
63 csbeq1a ( 𝑥 = 𝑦 → ( ( 𝑂𝑀 ) ‘ 𝑌 ) = 𝑦 / 𝑥 ( ( 𝑂𝑀 ) ‘ 𝑌 ) )
64 61 62 63 cbvmpt ( 𝑥 ∈ ( 𝑚 ∪ { 𝑎 } ) ↦ ( ( 𝑂𝑀 ) ‘ 𝑌 ) ) = ( 𝑦 ∈ ( 𝑚 ∪ { 𝑎 } ) ↦ 𝑦 / 𝑥 ( ( 𝑂𝑀 ) ‘ 𝑌 ) )
65 64 oveq2i ( 𝑅 Σg ( 𝑥 ∈ ( 𝑚 ∪ { 𝑎 } ) ↦ ( ( 𝑂𝑀 ) ‘ 𝑌 ) ) ) = ( 𝑅 Σg ( 𝑦 ∈ ( 𝑚 ∪ { 𝑎 } ) ↦ 𝑦 / 𝑥 ( ( 𝑂𝑀 ) ‘ 𝑌 ) ) )
66 ringcmn ( 𝑅 ∈ Ring → 𝑅 ∈ CMnd )
67 15 66 syl ( 𝜑𝑅 ∈ CMnd )
68 67 3ad2ant3 ( ( 𝑚 ∈ Fin ∧ ¬ 𝑎𝑚𝜑 ) → 𝑅 ∈ CMnd )
69 68 ad2antrr ( ( ( ( 𝑚 ∈ Fin ∧ ¬ 𝑎𝑚𝜑 ) ∧ ∀ 𝑥𝑚 𝑀𝑈 ) ∧ ∀ 𝑥 ∈ { 𝑎 } 𝑀𝑈 ) → 𝑅 ∈ CMnd )
70 csbfv12 𝑦 / 𝑥 ( ( 𝑂𝑀 ) ‘ 𝑌 ) = ( 𝑦 / 𝑥 ( 𝑂𝑀 ) ‘ 𝑦 / 𝑥 𝑌 )
71 csbfv2g ( 𝑦 ∈ V → 𝑦 / 𝑥 ( 𝑂𝑀 ) = ( 𝑂 𝑦 / 𝑥 𝑀 ) )
72 71 elv 𝑦 / 𝑥 ( 𝑂𝑀 ) = ( 𝑂 𝑦 / 𝑥 𝑀 )
73 csbconstg ( 𝑦 ∈ V → 𝑦 / 𝑥 𝑌 = 𝑌 )
74 73 elv 𝑦 / 𝑥 𝑌 = 𝑌
75 72 74 fveq12i ( 𝑦 / 𝑥 ( 𝑂𝑀 ) ‘ 𝑦 / 𝑥 𝑌 ) = ( ( 𝑂 𝑦 / 𝑥 𝑀 ) ‘ 𝑌 )
76 70 75 eqtri 𝑦 / 𝑥 ( ( 𝑂𝑀 ) ‘ 𝑌 ) = ( ( 𝑂 𝑦 / 𝑥 𝑀 ) ‘ 𝑌 )
77 46 adantr ( ( ( ( ( 𝑚 ∈ Fin ∧ ¬ 𝑎𝑚𝜑 ) ∧ ∀ 𝑥𝑚 𝑀𝑈 ) ∧ ∀ 𝑥 ∈ { 𝑎 } 𝑀𝑈 ) ∧ 𝑦𝑚 ) → 𝑅 ∈ CRing )
78 48 adantr ( ( ( ( ( 𝑚 ∈ Fin ∧ ¬ 𝑎𝑚𝜑 ) ∧ ∀ 𝑥𝑚 𝑀𝑈 ) ∧ ∀ 𝑥 ∈ { 𝑎 } 𝑀𝑈 ) ∧ 𝑦𝑚 ) → 𝑌𝐵 )
79 1 2 3 4 77 78 27 fveval1fvcl ( ( ( ( ( 𝑚 ∈ Fin ∧ ¬ 𝑎𝑚𝜑 ) ∧ ∀ 𝑥𝑚 𝑀𝑈 ) ∧ ∀ 𝑥 ∈ { 𝑎 } 𝑀𝑈 ) ∧ 𝑦𝑚 ) → ( ( 𝑂 𝑦 / 𝑥 𝑀 ) ‘ 𝑌 ) ∈ 𝐵 )
80 76 79 eqeltrid ( ( ( ( ( 𝑚 ∈ Fin ∧ ¬ 𝑎𝑚𝜑 ) ∧ ∀ 𝑥𝑚 𝑀𝑈 ) ∧ ∀ 𝑥 ∈ { 𝑎 } 𝑀𝑈 ) ∧ 𝑦𝑚 ) → 𝑦 / 𝑥 ( ( 𝑂𝑀 ) ‘ 𝑌 ) ∈ 𝐵 )
81 1 2 3 4 46 48 34 fveval1fvcl ( ( ( ( 𝑚 ∈ Fin ∧ ¬ 𝑎𝑚𝜑 ) ∧ ∀ 𝑥𝑚 𝑀𝑈 ) ∧ ∀ 𝑥 ∈ { 𝑎 } 𝑀𝑈 ) → ( ( 𝑂 𝑎 / 𝑥 𝑀 ) ‘ 𝑌 ) ∈ 𝐵 )
82 nfcv 𝑥 𝑎
83 nfcv 𝑥 𝑂
84 nfcsb1v 𝑥 𝑎 / 𝑥 𝑀
85 83 84 nffv 𝑥 ( 𝑂 𝑎 / 𝑥 𝑀 )
86 nfcv 𝑥 𝑌
87 85 86 nffv 𝑥 ( ( 𝑂 𝑎 / 𝑥 𝑀 ) ‘ 𝑌 )
88 csbeq1a ( 𝑥 = 𝑎𝑀 = 𝑎 / 𝑥 𝑀 )
89 88 fveq2d ( 𝑥 = 𝑎 → ( 𝑂𝑀 ) = ( 𝑂 𝑎 / 𝑥 𝑀 ) )
90 89 fveq1d ( 𝑥 = 𝑎 → ( ( 𝑂𝑀 ) ‘ 𝑌 ) = ( ( 𝑂 𝑎 / 𝑥 𝑀 ) ‘ 𝑌 ) )
91 82 87 90 csbhypf ( 𝑦 = 𝑎 𝑦 / 𝑥 ( ( 𝑂𝑀 ) ‘ 𝑌 ) = ( ( 𝑂 𝑎 / 𝑥 𝑀 ) ‘ 𝑌 ) )
92 3 55 69 22 80 29 30 81 91 gsumunsn ( ( ( ( 𝑚 ∈ Fin ∧ ¬ 𝑎𝑚𝜑 ) ∧ ∀ 𝑥𝑚 𝑀𝑈 ) ∧ ∀ 𝑥 ∈ { 𝑎 } 𝑀𝑈 ) → ( 𝑅 Σg ( 𝑦 ∈ ( 𝑚 ∪ { 𝑎 } ) ↦ 𝑦 / 𝑥 ( ( 𝑂𝑀 ) ‘ 𝑌 ) ) ) = ( ( 𝑅 Σg ( 𝑦𝑚 𝑦 / 𝑥 ( ( 𝑂𝑀 ) ‘ 𝑌 ) ) ) ( +g𝑅 ) ( ( 𝑂 𝑎 / 𝑥 𝑀 ) ‘ 𝑌 ) ) )
93 65 92 syl5eq ( ( ( ( 𝑚 ∈ Fin ∧ ¬ 𝑎𝑚𝜑 ) ∧ ∀ 𝑥𝑚 𝑀𝑈 ) ∧ ∀ 𝑥 ∈ { 𝑎 } 𝑀𝑈 ) → ( 𝑅 Σg ( 𝑥 ∈ ( 𝑚 ∪ { 𝑎 } ) ↦ ( ( 𝑂𝑀 ) ‘ 𝑌 ) ) ) = ( ( 𝑅 Σg ( 𝑦𝑚 𝑦 / 𝑥 ( ( 𝑂𝑀 ) ‘ 𝑌 ) ) ) ( +g𝑅 ) ( ( 𝑂 𝑎 / 𝑥 𝑀 ) ‘ 𝑌 ) ) )
94 61 62 63 cbvmpt ( 𝑥𝑚 ↦ ( ( 𝑂𝑀 ) ‘ 𝑌 ) ) = ( 𝑦𝑚 𝑦 / 𝑥 ( ( 𝑂𝑀 ) ‘ 𝑌 ) )
95 94 eqcomi ( 𝑦𝑚 𝑦 / 𝑥 ( ( 𝑂𝑀 ) ‘ 𝑌 ) ) = ( 𝑥𝑚 ↦ ( ( 𝑂𝑀 ) ‘ 𝑌 ) )
96 95 oveq2i ( 𝑅 Σg ( 𝑦𝑚 𝑦 / 𝑥 ( ( 𝑂𝑀 ) ‘ 𝑌 ) ) ) = ( 𝑅 Σg ( 𝑥𝑚 ↦ ( ( 𝑂𝑀 ) ‘ 𝑌 ) ) )
97 96 oveq1i ( ( 𝑅 Σg ( 𝑦𝑚 𝑦 / 𝑥 ( ( 𝑂𝑀 ) ‘ 𝑌 ) ) ) ( +g𝑅 ) ( ( 𝑂 𝑎 / 𝑥 𝑀 ) ‘ 𝑌 ) ) = ( ( 𝑅 Σg ( 𝑥𝑚 ↦ ( ( 𝑂𝑀 ) ‘ 𝑌 ) ) ) ( +g𝑅 ) ( ( 𝑂 𝑎 / 𝑥 𝑀 ) ‘ 𝑌 ) )
98 93 97 eqtr2di ( ( ( ( 𝑚 ∈ Fin ∧ ¬ 𝑎𝑚𝜑 ) ∧ ∀ 𝑥𝑚 𝑀𝑈 ) ∧ ∀ 𝑥 ∈ { 𝑎 } 𝑀𝑈 ) → ( ( 𝑅 Σg ( 𝑥𝑚 ↦ ( ( 𝑂𝑀 ) ‘ 𝑌 ) ) ) ( +g𝑅 ) ( ( 𝑂 𝑎 / 𝑥 𝑀 ) ‘ 𝑌 ) ) = ( 𝑅 Σg ( 𝑥 ∈ ( 𝑚 ∪ { 𝑎 } ) ↦ ( ( 𝑂𝑀 ) ‘ 𝑌 ) ) ) )
99 98 adantr ( ( ( ( ( 𝑚 ∈ Fin ∧ ¬ 𝑎𝑚𝜑 ) ∧ ∀ 𝑥𝑚 𝑀𝑈 ) ∧ ∀ 𝑥 ∈ { 𝑎 } 𝑀𝑈 ) ∧ ( ( 𝑂 ‘ ( 𝑃 Σg ( 𝑥𝑚𝑀 ) ) ) ‘ 𝑌 ) = ( 𝑅 Σg ( 𝑥𝑚 ↦ ( ( 𝑂𝑀 ) ‘ 𝑌 ) ) ) ) → ( ( 𝑅 Σg ( 𝑥𝑚 ↦ ( ( 𝑂𝑀 ) ‘ 𝑌 ) ) ) ( +g𝑅 ) ( ( 𝑂 𝑎 / 𝑥 𝑀 ) ‘ 𝑌 ) ) = ( 𝑅 Σg ( 𝑥 ∈ ( 𝑚 ∪ { 𝑎 } ) ↦ ( ( 𝑂𝑀 ) ‘ 𝑌 ) ) ) )
100 60 99 eqtrd ( ( ( ( ( 𝑚 ∈ Fin ∧ ¬ 𝑎𝑚𝜑 ) ∧ ∀ 𝑥𝑚 𝑀𝑈 ) ∧ ∀ 𝑥 ∈ { 𝑎 } 𝑀𝑈 ) ∧ ( ( 𝑂 ‘ ( 𝑃 Σg ( 𝑥𝑚𝑀 ) ) ) ‘ 𝑌 ) = ( 𝑅 Σg ( 𝑥𝑚 ↦ ( ( 𝑂𝑀 ) ‘ 𝑌 ) ) ) ) → ( ( 𝑂 ‘ ( 𝑃 Σg ( 𝑥 ∈ ( 𝑚 ∪ { 𝑎 } ) ↦ 𝑀 ) ) ) ‘ 𝑌 ) = ( 𝑅 Σg ( 𝑥 ∈ ( 𝑚 ∪ { 𝑎 } ) ↦ ( ( 𝑂𝑀 ) ‘ 𝑌 ) ) ) )
101 100 exp31 ( ( ( 𝑚 ∈ Fin ∧ ¬ 𝑎𝑚𝜑 ) ∧ ∀ 𝑥𝑚 𝑀𝑈 ) → ( ∀ 𝑥 ∈ { 𝑎 } 𝑀𝑈 → ( ( ( 𝑂 ‘ ( 𝑃 Σg ( 𝑥𝑚𝑀 ) ) ) ‘ 𝑌 ) = ( 𝑅 Σg ( 𝑥𝑚 ↦ ( ( 𝑂𝑀 ) ‘ 𝑌 ) ) ) → ( ( 𝑂 ‘ ( 𝑃 Σg ( 𝑥 ∈ ( 𝑚 ∪ { 𝑎 } ) ↦ 𝑀 ) ) ) ‘ 𝑌 ) = ( 𝑅 Σg ( 𝑥 ∈ ( 𝑚 ∪ { 𝑎 } ) ↦ ( ( 𝑂𝑀 ) ‘ 𝑌 ) ) ) ) ) )
102 101 com23 ( ( ( 𝑚 ∈ Fin ∧ ¬ 𝑎𝑚𝜑 ) ∧ ∀ 𝑥𝑚 𝑀𝑈 ) → ( ( ( 𝑂 ‘ ( 𝑃 Σg ( 𝑥𝑚𝑀 ) ) ) ‘ 𝑌 ) = ( 𝑅 Σg ( 𝑥𝑚 ↦ ( ( 𝑂𝑀 ) ‘ 𝑌 ) ) ) → ( ∀ 𝑥 ∈ { 𝑎 } 𝑀𝑈 → ( ( 𝑂 ‘ ( 𝑃 Σg ( 𝑥 ∈ ( 𝑚 ∪ { 𝑎 } ) ↦ 𝑀 ) ) ) ‘ 𝑌 ) = ( 𝑅 Σg ( 𝑥 ∈ ( 𝑚 ∪ { 𝑎 } ) ↦ ( ( 𝑂𝑀 ) ‘ 𝑌 ) ) ) ) ) )
103 102 ex ( ( 𝑚 ∈ Fin ∧ ¬ 𝑎𝑚𝜑 ) → ( ∀ 𝑥𝑚 𝑀𝑈 → ( ( ( 𝑂 ‘ ( 𝑃 Σg ( 𝑥𝑚𝑀 ) ) ) ‘ 𝑌 ) = ( 𝑅 Σg ( 𝑥𝑚 ↦ ( ( 𝑂𝑀 ) ‘ 𝑌 ) ) ) → ( ∀ 𝑥 ∈ { 𝑎 } 𝑀𝑈 → ( ( 𝑂 ‘ ( 𝑃 Σg ( 𝑥 ∈ ( 𝑚 ∪ { 𝑎 } ) ↦ 𝑀 ) ) ) ‘ 𝑌 ) = ( 𝑅 Σg ( 𝑥 ∈ ( 𝑚 ∪ { 𝑎 } ) ↦ ( ( 𝑂𝑀 ) ‘ 𝑌 ) ) ) ) ) ) )
104 103 a2d ( ( 𝑚 ∈ Fin ∧ ¬ 𝑎𝑚𝜑 ) → ( ( ∀ 𝑥𝑚 𝑀𝑈 → ( ( 𝑂 ‘ ( 𝑃 Σg ( 𝑥𝑚𝑀 ) ) ) ‘ 𝑌 ) = ( 𝑅 Σg ( 𝑥𝑚 ↦ ( ( 𝑂𝑀 ) ‘ 𝑌 ) ) ) ) → ( ∀ 𝑥𝑚 𝑀𝑈 → ( ∀ 𝑥 ∈ { 𝑎 } 𝑀𝑈 → ( ( 𝑂 ‘ ( 𝑃 Σg ( 𝑥 ∈ ( 𝑚 ∪ { 𝑎 } ) ↦ 𝑀 ) ) ) ‘ 𝑌 ) = ( 𝑅 Σg ( 𝑥 ∈ ( 𝑚 ∪ { 𝑎 } ) ↦ ( ( 𝑂𝑀 ) ‘ 𝑌 ) ) ) ) ) ) )
105 104 imp4b ( ( ( 𝑚 ∈ Fin ∧ ¬ 𝑎𝑚𝜑 ) ∧ ( ∀ 𝑥𝑚 𝑀𝑈 → ( ( 𝑂 ‘ ( 𝑃 Σg ( 𝑥𝑚𝑀 ) ) ) ‘ 𝑌 ) = ( 𝑅 Σg ( 𝑥𝑚 ↦ ( ( 𝑂𝑀 ) ‘ 𝑌 ) ) ) ) ) → ( ( ∀ 𝑥𝑚 𝑀𝑈 ∧ ∀ 𝑥 ∈ { 𝑎 } 𝑀𝑈 ) → ( ( 𝑂 ‘ ( 𝑃 Σg ( 𝑥 ∈ ( 𝑚 ∪ { 𝑎 } ) ↦ 𝑀 ) ) ) ‘ 𝑌 ) = ( 𝑅 Σg ( 𝑥 ∈ ( 𝑚 ∪ { 𝑎 } ) ↦ ( ( 𝑂𝑀 ) ‘ 𝑌 ) ) ) ) )
106 7 105 syl5bi ( ( ( 𝑚 ∈ Fin ∧ ¬ 𝑎𝑚𝜑 ) ∧ ( ∀ 𝑥𝑚 𝑀𝑈 → ( ( 𝑂 ‘ ( 𝑃 Σg ( 𝑥𝑚𝑀 ) ) ) ‘ 𝑌 ) = ( 𝑅 Σg ( 𝑥𝑚 ↦ ( ( 𝑂𝑀 ) ‘ 𝑌 ) ) ) ) ) → ( ∀ 𝑥 ∈ ( 𝑚 ∪ { 𝑎 } ) 𝑀𝑈 → ( ( 𝑂 ‘ ( 𝑃 Σg ( 𝑥 ∈ ( 𝑚 ∪ { 𝑎 } ) ↦ 𝑀 ) ) ) ‘ 𝑌 ) = ( 𝑅 Σg ( 𝑥 ∈ ( 𝑚 ∪ { 𝑎 } ) ↦ ( ( 𝑂𝑀 ) ‘ 𝑌 ) ) ) ) )
107 106 ex ( ( 𝑚 ∈ Fin ∧ ¬ 𝑎𝑚𝜑 ) → ( ( ∀ 𝑥𝑚 𝑀𝑈 → ( ( 𝑂 ‘ ( 𝑃 Σg ( 𝑥𝑚𝑀 ) ) ) ‘ 𝑌 ) = ( 𝑅 Σg ( 𝑥𝑚 ↦ ( ( 𝑂𝑀 ) ‘ 𝑌 ) ) ) ) → ( ∀ 𝑥 ∈ ( 𝑚 ∪ { 𝑎 } ) 𝑀𝑈 → ( ( 𝑂 ‘ ( 𝑃 Σg ( 𝑥 ∈ ( 𝑚 ∪ { 𝑎 } ) ↦ 𝑀 ) ) ) ‘ 𝑌 ) = ( 𝑅 Σg ( 𝑥 ∈ ( 𝑚 ∪ { 𝑎 } ) ↦ ( ( 𝑂𝑀 ) ‘ 𝑌 ) ) ) ) ) )