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 ( 𝑥 ∈ ( 𝑚 ∪ { 𝑎 } ) ↦ ( ( 𝑂 ‘ 𝑀 ) ‘ 𝑌 ) ) ) ) ) )