evl1gsumdlem

Description: Lemma for evl1gsumd (induction step). (Contributed by AV, 17-Sep-2019)

	Ref	Expression
Hypotheses	evl1gsumd.q	⊢ 𝑂 = ( eval₁ ‘ 𝑅 )
	evl1gsumd.p	⊢ 𝑃 = ( Poly₁ ‘ 𝑅 )
	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	⊢ 𝑂 = ( eval₁ ‘ 𝑅 )
2		evl1gsumd.p	⊢ 𝑃 = ( Poly₁ ‘ 𝑅 )
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	eqtrid	⊢ ( ( ( ( 𝑚 ∈ 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	eqtrid	⊢ ( ( ( ( 𝑚 ∈ 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	biimtrid	⊢ ( ( ( 𝑚 ∈ Fin ∧ ¬ 𝑎 ∈ 𝑚 ∧ 𝜑 ) ∧ ( ∀ 𝑥 ∈ 𝑚 𝑀 ∈ 𝑈 → ( ( 𝑂 ‘ ( 𝑃 Σ_g ( 𝑥 ∈ 𝑚 ↦ 𝑀 ) ) ) ‘ 𝑌 ) = ( 𝑅 Σ_g ( 𝑥 ∈ 𝑚 ↦ ( ( 𝑂 ‘ 𝑀 ) ‘ 𝑌 ) ) ) ) ) → ( ∀ 𝑥 ∈ ( 𝑚 ∪ { 𝑎 } ) 𝑀 ∈ 𝑈 → ( ( 𝑂 ‘ ( 𝑃 Σ_g ( 𝑥 ∈ ( 𝑚 ∪ { 𝑎 } ) ↦ 𝑀 ) ) ) ‘ 𝑌 ) = ( 𝑅 Σ_g ( 𝑥 ∈ ( 𝑚 ∪ { 𝑎 } ) ↦ ( ( 𝑂 ‘ 𝑀 ) ‘ 𝑌 ) ) ) ) )
107	106	ex	⊢ ( ( 𝑚 ∈ Fin ∧ ¬ 𝑎 ∈ 𝑚 ∧ 𝜑 ) → ( ( ∀ 𝑥 ∈ 𝑚 𝑀 ∈ 𝑈 → ( ( 𝑂 ‘ ( 𝑃 Σ_g ( 𝑥 ∈ 𝑚 ↦ 𝑀 ) ) ) ‘ 𝑌 ) = ( 𝑅 Σ_g ( 𝑥 ∈ 𝑚 ↦ ( ( 𝑂 ‘ 𝑀 ) ‘ 𝑌 ) ) ) ) → ( ∀ 𝑥 ∈ ( 𝑚 ∪ { 𝑎 } ) 𝑀 ∈ 𝑈 → ( ( 𝑂 ‘ ( 𝑃 Σ_g ( 𝑥 ∈ ( 𝑚 ∪ { 𝑎 } ) ↦ 𝑀 ) ) ) ‘ 𝑌 ) = ( 𝑅 Σ_g ( 𝑥 ∈ ( 𝑚 ∪ { 𝑎 } ) ↦ ( ( 𝑂 ‘ 𝑀 ) ‘ 𝑌 ) ) ) ) ) )

Metamath Proof Explorer

Theorem evl1gsumdlem

Proof