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