This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem mplcoe5

Description: Decompose a monomial into a finite product of powers of variables. Instead of assuming that R is a commutative ring (as in mplcoe2 ), it is sufficient that R is a ring and all the variables of the multivariate polynomial commute. (Contributed by AV, 7-Oct-2019)

Ref Expression
Hypotheses mplcoe1.p ⊢ 𝑃 = ( 𝐼 mPoly 𝑅 )
mplcoe1.d ⊢ 𝐷 = { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin }
mplcoe1.z ⊢ 0 = ( 0g ‘ 𝑅 )
mplcoe1.o ⊢ 1 = ( 1r ‘ 𝑅 )
mplcoe1.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
mplcoe2.g ⊢ 𝐺 = ( mulGrp ‘ 𝑃 )
mplcoe2.m ⊢ ↑ = ( .g ‘ 𝐺 )
mplcoe2.v ⊢ 𝑉 = ( 𝐼 mVar 𝑅 )
mplcoe5.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
mplcoe5.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐷 )
mplcoe5.c ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐼 ∀ 𝑦 ∈ 𝐼 ( ( 𝑉 ‘ 𝑦 ) ( +g ‘ 𝐺 ) ( 𝑉 ‘ 𝑥 ) ) = ( ( 𝑉 ‘ 𝑥 ) ( +g ‘ 𝐺 ) ( 𝑉 ‘ 𝑦 ) ) )
Assertion mplcoe5 ( 𝜑 → ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑌 , 1 , 0 ) ) = ( 𝐺 Σg ( 𝑘 ∈ 𝐼 ↦ ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 mplcoe1.p ⊢ 𝑃 = ( 𝐼 mPoly 𝑅 )
2 mplcoe1.d ⊢ 𝐷 = { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin }
3 mplcoe1.z ⊢ 0 = ( 0g ‘ 𝑅 )
4 mplcoe1.o ⊢ 1 = ( 1r ‘ 𝑅 )
5 mplcoe1.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
6 mplcoe2.g ⊢ 𝐺 = ( mulGrp ‘ 𝑃 )
7 mplcoe2.m ⊢ ↑ = ( .g ‘ 𝐺 )
8 mplcoe2.v ⊢ 𝑉 = ( 𝐼 mVar 𝑅 )
9 mplcoe5.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
10 mplcoe5.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐷 )
11 mplcoe5.c ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐼 ∀ 𝑦 ∈ 𝐼 ( ( 𝑉 ‘ 𝑦 ) ( +g ‘ 𝐺 ) ( 𝑉 ‘ 𝑥 ) ) = ( ( 𝑉 ‘ 𝑥 ) ( +g ‘ 𝐺 ) ( 𝑉 ‘ 𝑦 ) ) )
12 2 psrbag ⊢ ( 𝐼 ∈ 𝑊 → ( 𝑌 ∈ 𝐷 ↔ ( 𝑌 : 𝐼 ⟶ ℕ0 ∧ ( ◡ 𝑌 “ ℕ ) ∈ Fin ) ) )
13 5 12 syl ⊢ ( 𝜑 → ( 𝑌 ∈ 𝐷 ↔ ( 𝑌 : 𝐼 ⟶ ℕ0 ∧ ( ◡ 𝑌 “ ℕ ) ∈ Fin ) ) )
14 10 13 mpbid ⊢ ( 𝜑 → ( 𝑌 : 𝐼 ⟶ ℕ0 ∧ ( ◡ 𝑌 “ ℕ ) ∈ Fin ) )
15 14 simpld ⊢ ( 𝜑 → 𝑌 : 𝐼 ⟶ ℕ0 )
16 15 feqmptd ⊢ ( 𝜑 → 𝑌 = ( 𝑖 ∈ 𝐼 ↦ ( 𝑌 ‘ 𝑖 ) ) )
17 iftrue ⊢ ( 𝑖 ∈ ( ◡ 𝑌 “ ℕ ) → if ( 𝑖 ∈ ( ◡ 𝑌 “ ℕ ) , ( 𝑌 ‘ 𝑖 ) , 0 ) = ( 𝑌 ‘ 𝑖 ) )
18 17 adantl ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) ∧ 𝑖 ∈ ( ◡ 𝑌 “ ℕ ) ) → if ( 𝑖 ∈ ( ◡ 𝑌 “ ℕ ) , ( 𝑌 ‘ 𝑖 ) , 0 ) = ( 𝑌 ‘ 𝑖 ) )
19 eldif ⊢ ( 𝑖 ∈ ( 𝐼 ∖ ( ◡ 𝑌 “ ℕ ) ) ↔ ( 𝑖 ∈ 𝐼 ∧ ¬ 𝑖 ∈ ( ◡ 𝑌 “ ℕ ) ) )
20 fcdmnn0supp ⊢ ( ( 𝐼 ∈ 𝑊 ∧ 𝑌 : 𝐼 ⟶ ℕ0 ) → ( 𝑌 supp 0 ) = ( ◡ 𝑌 “ ℕ ) )
21 5 15 20 syl2anc ⊢ ( 𝜑 → ( 𝑌 supp 0 ) = ( ◡ 𝑌 “ ℕ ) )
22 eqimss ⊢ ( ( 𝑌 supp 0 ) = ( ◡ 𝑌 “ ℕ ) → ( 𝑌 supp 0 ) ⊆ ( ◡ 𝑌 “ ℕ ) )
23 21 22 syl ⊢ ( 𝜑 → ( 𝑌 supp 0 ) ⊆ ( ◡ 𝑌 “ ℕ ) )
24 c0ex ⊢ 0 ∈ V
25 24 a1i ⊢ ( 𝜑 → 0 ∈ V )
26 15 23 5 25 suppssr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝐼 ∖ ( ◡ 𝑌 “ ℕ ) ) ) → ( 𝑌 ‘ 𝑖 ) = 0 )
27 26 ifeq2d ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝐼 ∖ ( ◡ 𝑌 “ ℕ ) ) ) → if ( 𝑖 ∈ ( ◡ 𝑌 “ ℕ ) , ( 𝑌 ‘ 𝑖 ) , ( 𝑌 ‘ 𝑖 ) ) = if ( 𝑖 ∈ ( ◡ 𝑌 “ ℕ ) , ( 𝑌 ‘ 𝑖 ) , 0 ) )
28 ifid ⊢ if ( 𝑖 ∈ ( ◡ 𝑌 “ ℕ ) , ( 𝑌 ‘ 𝑖 ) , ( 𝑌 ‘ 𝑖 ) ) = ( 𝑌 ‘ 𝑖 )
29 27 28 eqtr3di ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝐼 ∖ ( ◡ 𝑌 “ ℕ ) ) ) → if ( 𝑖 ∈ ( ◡ 𝑌 “ ℕ ) , ( 𝑌 ‘ 𝑖 ) , 0 ) = ( 𝑌 ‘ 𝑖 ) )
30 19 29 sylan2br ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ 𝐼 ∧ ¬ 𝑖 ∈ ( ◡ 𝑌 “ ℕ ) ) ) → if ( 𝑖 ∈ ( ◡ 𝑌 “ ℕ ) , ( 𝑌 ‘ 𝑖 ) , 0 ) = ( 𝑌 ‘ 𝑖 ) )
31 30 anassrs ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) ∧ ¬ 𝑖 ∈ ( ◡ 𝑌 “ ℕ ) ) → if ( 𝑖 ∈ ( ◡ 𝑌 “ ℕ ) , ( 𝑌 ‘ 𝑖 ) , 0 ) = ( 𝑌 ‘ 𝑖 ) )
32 18 31 pm2.61dan ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ) → if ( 𝑖 ∈ ( ◡ 𝑌 “ ℕ ) , ( 𝑌 ‘ 𝑖 ) , 0 ) = ( 𝑌 ‘ 𝑖 ) )
33 32 mpteq2dva ⊢ ( 𝜑 → ( 𝑖 ∈ 𝐼 ↦ if ( 𝑖 ∈ ( ◡ 𝑌 “ ℕ ) , ( 𝑌 ‘ 𝑖 ) , 0 ) ) = ( 𝑖 ∈ 𝐼 ↦ ( 𝑌 ‘ 𝑖 ) ) )
34 16 33 eqtr4d ⊢ ( 𝜑 → 𝑌 = ( 𝑖 ∈ 𝐼 ↦ if ( 𝑖 ∈ ( ◡ 𝑌 “ ℕ ) , ( 𝑌 ‘ 𝑖 ) , 0 ) ) )
35 34 eqeq2d ⊢ ( 𝜑 → ( 𝑦 = 𝑌 ↔ 𝑦 = ( 𝑖 ∈ 𝐼 ↦ if ( 𝑖 ∈ ( ◡ 𝑌 “ ℕ ) , ( 𝑌 ‘ 𝑖 ) , 0 ) ) ) )
36 35 ifbid ⊢ ( 𝜑 → if ( 𝑦 = 𝑌 , 1 , 0 ) = if ( 𝑦 = ( 𝑖 ∈ 𝐼 ↦ if ( 𝑖 ∈ ( ◡ 𝑌 “ ℕ ) , ( 𝑌 ‘ 𝑖 ) , 0 ) ) , 1 , 0 ) )
37 36 mpteq2dv ⊢ ( 𝜑 → ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑌 , 1 , 0 ) ) = ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = ( 𝑖 ∈ 𝐼 ↦ if ( 𝑖 ∈ ( ◡ 𝑌 “ ℕ ) , ( 𝑌 ‘ 𝑖 ) , 0 ) ) , 1 , 0 ) ) )
38 cnvimass ⊢ ( ◡ 𝑌 “ ℕ ) ⊆ dom 𝑌
39 38 15 fssdm ⊢ ( 𝜑 → ( ◡ 𝑌 “ ℕ ) ⊆ 𝐼 )
40 14 simprd ⊢ ( 𝜑 → ( ◡ 𝑌 “ ℕ ) ∈ Fin )
41 sseq1 ⊢ ( 𝑤 = ∅ → ( 𝑤 ⊆ 𝐼 ↔ ∅ ⊆ 𝐼 ) )
42 noel ⊢ ¬ 𝑖 ∈ ∅
43 eleq2 ⊢ ( 𝑤 = ∅ → ( 𝑖 ∈ 𝑤 ↔ 𝑖 ∈ ∅ ) )
44 42 43 mtbiri ⊢ ( 𝑤 = ∅ → ¬ 𝑖 ∈ 𝑤 )
45 44 iffalsed ⊢ ( 𝑤 = ∅ → if ( 𝑖 ∈ 𝑤 , ( 𝑌 ‘ 𝑖 ) , 0 ) = 0 )
46 45 mpteq2dv ⊢ ( 𝑤 = ∅ → ( 𝑖 ∈ 𝐼 ↦ if ( 𝑖 ∈ 𝑤 , ( 𝑌 ‘ 𝑖 ) , 0 ) ) = ( 𝑖 ∈ 𝐼 ↦ 0 ) )
47 fconstmpt ⊢ ( 𝐼 × { 0 } ) = ( 𝑖 ∈ 𝐼 ↦ 0 )
48 46 47 eqtr4di ⊢ ( 𝑤 = ∅ → ( 𝑖 ∈ 𝐼 ↦ if ( 𝑖 ∈ 𝑤 , ( 𝑌 ‘ 𝑖 ) , 0 ) ) = ( 𝐼 × { 0 } ) )
49 48 eqeq2d ⊢ ( 𝑤 = ∅ → ( 𝑦 = ( 𝑖 ∈ 𝐼 ↦ if ( 𝑖 ∈ 𝑤 , ( 𝑌 ‘ 𝑖 ) , 0 ) ) ↔ 𝑦 = ( 𝐼 × { 0 } ) ) )
50 49 ifbid ⊢ ( 𝑤 = ∅ → if ( 𝑦 = ( 𝑖 ∈ 𝐼 ↦ if ( 𝑖 ∈ 𝑤 , ( 𝑌 ‘ 𝑖 ) , 0 ) ) , 1 , 0 ) = if ( 𝑦 = ( 𝐼 × { 0 } ) , 1 , 0 ) )
51 50 mpteq2dv ⊢ ( 𝑤 = ∅ → ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = ( 𝑖 ∈ 𝐼 ↦ if ( 𝑖 ∈ 𝑤 , ( 𝑌 ‘ 𝑖 ) , 0 ) ) , 1 , 0 ) ) = ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = ( 𝐼 × { 0 } ) , 1 , 0 ) ) )
52 mpteq1 ⊢ ( 𝑤 = ∅ → ( 𝑘 ∈ 𝑤 ↦ ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ) = ( 𝑘 ∈ ∅ ↦ ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ) )
53 mpt0 ⊢ ( 𝑘 ∈ ∅ ↦ ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ) = ∅
54 52 53 eqtrdi ⊢ ( 𝑤 = ∅ → ( 𝑘 ∈ 𝑤 ↦ ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ) = ∅ )
55 54 oveq2d ⊢ ( 𝑤 = ∅ → ( 𝐺 Σg ( 𝑘 ∈ 𝑤 ↦ ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ) ) = ( 𝐺 Σg ∅ ) )
56 eqid ⊢ ( 1r ‘ 𝑃 ) = ( 1r ‘ 𝑃 )
57 6 56 ringidval ⊢ ( 1r ‘ 𝑃 ) = ( 0g ‘ 𝐺 )
58 57 gsum0 ⊢ ( 𝐺 Σg ∅ ) = ( 1r ‘ 𝑃 )
59 55 58 eqtrdi ⊢ ( 𝑤 = ∅ → ( 𝐺 Σg ( 𝑘 ∈ 𝑤 ↦ ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ) ) = ( 1r ‘ 𝑃 ) )
60 51 59 eqeq12d ⊢ ( 𝑤 = ∅ → ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = ( 𝑖 ∈ 𝐼 ↦ if ( 𝑖 ∈ 𝑤 , ( 𝑌 ‘ 𝑖 ) , 0 ) ) , 1 , 0 ) ) = ( 𝐺 Σg ( 𝑘 ∈ 𝑤 ↦ ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ) ) ↔ ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = ( 𝐼 × { 0 } ) , 1 , 0 ) ) = ( 1r ‘ 𝑃 ) ) )
61 41 60 imbi12d ⊢ ( 𝑤 = ∅ → ( ( 𝑤 ⊆ 𝐼 → ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = ( 𝑖 ∈ 𝐼 ↦ if ( 𝑖 ∈ 𝑤 , ( 𝑌 ‘ 𝑖 ) , 0 ) ) , 1 , 0 ) ) = ( 𝐺 Σg ( 𝑘 ∈ 𝑤 ↦ ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ) ) ) ↔ ( ∅ ⊆ 𝐼 → ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = ( 𝐼 × { 0 } ) , 1 , 0 ) ) = ( 1r ‘ 𝑃 ) ) ) )
62 61 imbi2d ⊢ ( 𝑤 = ∅ → ( ( 𝜑 → ( 𝑤 ⊆ 𝐼 → ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = ( 𝑖 ∈ 𝐼 ↦ if ( 𝑖 ∈ 𝑤 , ( 𝑌 ‘ 𝑖 ) , 0 ) ) , 1 , 0 ) ) = ( 𝐺 Σg ( 𝑘 ∈ 𝑤 ↦ ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ) ) ) ) ↔ ( 𝜑 → ( ∅ ⊆ 𝐼 → ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = ( 𝐼 × { 0 } ) , 1 , 0 ) ) = ( 1r ‘ 𝑃 ) ) ) ) )
63 sseq1 ⊢ ( 𝑤 = 𝑥 → ( 𝑤 ⊆ 𝐼 ↔ 𝑥 ⊆ 𝐼 ) )
64 eleq2 ⊢ ( 𝑤 = 𝑥 → ( 𝑖 ∈ 𝑤 ↔ 𝑖 ∈ 𝑥 ) )
65 64 ifbid ⊢ ( 𝑤 = 𝑥 → if ( 𝑖 ∈ 𝑤 , ( 𝑌 ‘ 𝑖 ) , 0 ) = if ( 𝑖 ∈ 𝑥 , ( 𝑌 ‘ 𝑖 ) , 0 ) )
66 65 mpteq2dv ⊢ ( 𝑤 = 𝑥 → ( 𝑖 ∈ 𝐼 ↦ if ( 𝑖 ∈ 𝑤 , ( 𝑌 ‘ 𝑖 ) , 0 ) ) = ( 𝑖 ∈ 𝐼 ↦ if ( 𝑖 ∈ 𝑥 , ( 𝑌 ‘ 𝑖 ) , 0 ) ) )
67 66 eqeq2d ⊢ ( 𝑤 = 𝑥 → ( 𝑦 = ( 𝑖 ∈ 𝐼 ↦ if ( 𝑖 ∈ 𝑤 , ( 𝑌 ‘ 𝑖 ) , 0 ) ) ↔ 𝑦 = ( 𝑖 ∈ 𝐼 ↦ if ( 𝑖 ∈ 𝑥 , ( 𝑌 ‘ 𝑖 ) , 0 ) ) ) )
68 67 ifbid ⊢ ( 𝑤 = 𝑥 → if ( 𝑦 = ( 𝑖 ∈ 𝐼 ↦ if ( 𝑖 ∈ 𝑤 , ( 𝑌 ‘ 𝑖 ) , 0 ) ) , 1 , 0 ) = if ( 𝑦 = ( 𝑖 ∈ 𝐼 ↦ if ( 𝑖 ∈ 𝑥 , ( 𝑌 ‘ 𝑖 ) , 0 ) ) , 1 , 0 ) )
69 68 mpteq2dv ⊢ ( 𝑤 = 𝑥 → ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = ( 𝑖 ∈ 𝐼 ↦ if ( 𝑖 ∈ 𝑤 , ( 𝑌 ‘ 𝑖 ) , 0 ) ) , 1 , 0 ) ) = ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = ( 𝑖 ∈ 𝐼 ↦ if ( 𝑖 ∈ 𝑥 , ( 𝑌 ‘ 𝑖 ) , 0 ) ) , 1 , 0 ) ) )
70 mpteq1 ⊢ ( 𝑤 = 𝑥 → ( 𝑘 ∈ 𝑤 ↦ ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ) = ( 𝑘 ∈ 𝑥 ↦ ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ) )
71 70 oveq2d ⊢ ( 𝑤 = 𝑥 → ( 𝐺 Σg ( 𝑘 ∈ 𝑤 ↦ ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ) ) = ( 𝐺 Σg ( 𝑘 ∈ 𝑥 ↦ ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ) ) )
72 69 71 eqeq12d ⊢ ( 𝑤 = 𝑥 → ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = ( 𝑖 ∈ 𝐼 ↦ if ( 𝑖 ∈ 𝑤 , ( 𝑌 ‘ 𝑖 ) , 0 ) ) , 1 , 0 ) ) = ( 𝐺 Σg ( 𝑘 ∈ 𝑤 ↦ ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ) ) ↔ ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = ( 𝑖 ∈ 𝐼 ↦ if ( 𝑖 ∈ 𝑥 , ( 𝑌 ‘ 𝑖 ) , 0 ) ) , 1 , 0 ) ) = ( 𝐺 Σg ( 𝑘 ∈ 𝑥 ↦ ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ) ) ) )
73 63 72 imbi12d ⊢ ( 𝑤 = 𝑥 → ( ( 𝑤 ⊆ 𝐼 → ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = ( 𝑖 ∈ 𝐼 ↦ if ( 𝑖 ∈ 𝑤 , ( 𝑌 ‘ 𝑖 ) , 0 ) ) , 1 , 0 ) ) = ( 𝐺 Σg ( 𝑘 ∈ 𝑤 ↦ ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ) ) ) ↔ ( 𝑥 ⊆ 𝐼 → ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = ( 𝑖 ∈ 𝐼 ↦ if ( 𝑖 ∈ 𝑥 , ( 𝑌 ‘ 𝑖 ) , 0 ) ) , 1 , 0 ) ) = ( 𝐺 Σg ( 𝑘 ∈ 𝑥 ↦ ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ) ) ) ) )
74 73 imbi2d ⊢ ( 𝑤 = 𝑥 → ( ( 𝜑 → ( 𝑤 ⊆ 𝐼 → ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = ( 𝑖 ∈ 𝐼 ↦ if ( 𝑖 ∈ 𝑤 , ( 𝑌 ‘ 𝑖 ) , 0 ) ) , 1 , 0 ) ) = ( 𝐺 Σg ( 𝑘 ∈ 𝑤 ↦ ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ) ) ) ) ↔ ( 𝜑 → ( 𝑥 ⊆ 𝐼 → ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = ( 𝑖 ∈ 𝐼 ↦ if ( 𝑖 ∈ 𝑥 , ( 𝑌 ‘ 𝑖 ) , 0 ) ) , 1 , 0 ) ) = ( 𝐺 Σg ( 𝑘 ∈ 𝑥 ↦ ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ) ) ) ) ) )
75 sseq1 ⊢ ( 𝑤 = ( 𝑥 ∪ { 𝑧 } ) → ( 𝑤 ⊆ 𝐼 ↔ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐼 ) )
76 eleq2 ⊢ ( 𝑤 = ( 𝑥 ∪ { 𝑧 } ) → ( 𝑖 ∈ 𝑤 ↔ 𝑖 ∈ ( 𝑥 ∪ { 𝑧 } ) ) )
77 76 ifbid ⊢ ( 𝑤 = ( 𝑥 ∪ { 𝑧 } ) → if ( 𝑖 ∈ 𝑤 , ( 𝑌 ‘ 𝑖 ) , 0 ) = if ( 𝑖 ∈ ( 𝑥 ∪ { 𝑧 } ) , ( 𝑌 ‘ 𝑖 ) , 0 ) )
78 77 mpteq2dv ⊢ ( 𝑤 = ( 𝑥 ∪ { 𝑧 } ) → ( 𝑖 ∈ 𝐼 ↦ if ( 𝑖 ∈ 𝑤 , ( 𝑌 ‘ 𝑖 ) , 0 ) ) = ( 𝑖 ∈ 𝐼 ↦ if ( 𝑖 ∈ ( 𝑥 ∪ { 𝑧 } ) , ( 𝑌 ‘ 𝑖 ) , 0 ) ) )
79 78 eqeq2d ⊢ ( 𝑤 = ( 𝑥 ∪ { 𝑧 } ) → ( 𝑦 = ( 𝑖 ∈ 𝐼 ↦ if ( 𝑖 ∈ 𝑤 , ( 𝑌 ‘ 𝑖 ) , 0 ) ) ↔ 𝑦 = ( 𝑖 ∈ 𝐼 ↦ if ( 𝑖 ∈ ( 𝑥 ∪ { 𝑧 } ) , ( 𝑌 ‘ 𝑖 ) , 0 ) ) ) )
80 79 ifbid ⊢ ( 𝑤 = ( 𝑥 ∪ { 𝑧 } ) → if ( 𝑦 = ( 𝑖 ∈ 𝐼 ↦ if ( 𝑖 ∈ 𝑤 , ( 𝑌 ‘ 𝑖 ) , 0 ) ) , 1 , 0 ) = if ( 𝑦 = ( 𝑖 ∈ 𝐼 ↦ if ( 𝑖 ∈ ( 𝑥 ∪ { 𝑧 } ) , ( 𝑌 ‘ 𝑖 ) , 0 ) ) , 1 , 0 ) )
81 80 mpteq2dv ⊢ ( 𝑤 = ( 𝑥 ∪ { 𝑧 } ) → ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = ( 𝑖 ∈ 𝐼 ↦ if ( 𝑖 ∈ 𝑤 , ( 𝑌 ‘ 𝑖 ) , 0 ) ) , 1 , 0 ) ) = ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = ( 𝑖 ∈ 𝐼 ↦ if ( 𝑖 ∈ ( 𝑥 ∪ { 𝑧 } ) , ( 𝑌 ‘ 𝑖 ) , 0 ) ) , 1 , 0 ) ) )
82 mpteq1 ⊢ ( 𝑤 = ( 𝑥 ∪ { 𝑧 } ) → ( 𝑘 ∈ 𝑤 ↦ ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ) = ( 𝑘 ∈ ( 𝑥 ∪ { 𝑧 } ) ↦ ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ) )
83 82 oveq2d ⊢ ( 𝑤 = ( 𝑥 ∪ { 𝑧 } ) → ( 𝐺 Σg ( 𝑘 ∈ 𝑤 ↦ ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ) ) = ( 𝐺 Σg ( 𝑘 ∈ ( 𝑥 ∪ { 𝑧 } ) ↦ ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ) ) )
84 81 83 eqeq12d ⊢ ( 𝑤 = ( 𝑥 ∪ { 𝑧 } ) → ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = ( 𝑖 ∈ 𝐼 ↦ if ( 𝑖 ∈ 𝑤 , ( 𝑌 ‘ 𝑖 ) , 0 ) ) , 1 , 0 ) ) = ( 𝐺 Σg ( 𝑘 ∈ 𝑤 ↦ ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ) ) ↔ ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = ( 𝑖 ∈ 𝐼 ↦ if ( 𝑖 ∈ ( 𝑥 ∪ { 𝑧 } ) , ( 𝑌 ‘ 𝑖 ) , 0 ) ) , 1 , 0 ) ) = ( 𝐺 Σg ( 𝑘 ∈ ( 𝑥 ∪ { 𝑧 } ) ↦ ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ) ) ) )
85 75 84 imbi12d ⊢ ( 𝑤 = ( 𝑥 ∪ { 𝑧 } ) → ( ( 𝑤 ⊆ 𝐼 → ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = ( 𝑖 ∈ 𝐼 ↦ if ( 𝑖 ∈ 𝑤 , ( 𝑌 ‘ 𝑖 ) , 0 ) ) , 1 , 0 ) ) = ( 𝐺 Σg ( 𝑘 ∈ 𝑤 ↦ ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ) ) ) ↔ ( ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐼 → ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = ( 𝑖 ∈ 𝐼 ↦ if ( 𝑖 ∈ ( 𝑥 ∪ { 𝑧 } ) , ( 𝑌 ‘ 𝑖 ) , 0 ) ) , 1 , 0 ) ) = ( 𝐺 Σg ( 𝑘 ∈ ( 𝑥 ∪ { 𝑧 } ) ↦ ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ) ) ) ) )
86 85 imbi2d ⊢ ( 𝑤 = ( 𝑥 ∪ { 𝑧 } ) → ( ( 𝜑 → ( 𝑤 ⊆ 𝐼 → ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = ( 𝑖 ∈ 𝐼 ↦ if ( 𝑖 ∈ 𝑤 , ( 𝑌 ‘ 𝑖 ) , 0 ) ) , 1 , 0 ) ) = ( 𝐺 Σg ( 𝑘 ∈ 𝑤 ↦ ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ) ) ) ) ↔ ( 𝜑 → ( ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐼 → ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = ( 𝑖 ∈ 𝐼 ↦ if ( 𝑖 ∈ ( 𝑥 ∪ { 𝑧 } ) , ( 𝑌 ‘ 𝑖 ) , 0 ) ) , 1 , 0 ) ) = ( 𝐺 Σg ( 𝑘 ∈ ( 𝑥 ∪ { 𝑧 } ) ↦ ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ) ) ) ) ) )
87 sseq1 ⊢ ( 𝑤 = ( ◡ 𝑌 “ ℕ ) → ( 𝑤 ⊆ 𝐼 ↔ ( ◡ 𝑌 “ ℕ ) ⊆ 𝐼 ) )
88 eleq2 ⊢ ( 𝑤 = ( ◡ 𝑌 “ ℕ ) → ( 𝑖 ∈ 𝑤 ↔ 𝑖 ∈ ( ◡ 𝑌 “ ℕ ) ) )
89 88 ifbid ⊢ ( 𝑤 = ( ◡ 𝑌 “ ℕ ) → if ( 𝑖 ∈ 𝑤 , ( 𝑌 ‘ 𝑖 ) , 0 ) = if ( 𝑖 ∈ ( ◡ 𝑌 “ ℕ ) , ( 𝑌 ‘ 𝑖 ) , 0 ) )
90 89 mpteq2dv ⊢ ( 𝑤 = ( ◡ 𝑌 “ ℕ ) → ( 𝑖 ∈ 𝐼 ↦ if ( 𝑖 ∈ 𝑤 , ( 𝑌 ‘ 𝑖 ) , 0 ) ) = ( 𝑖 ∈ 𝐼 ↦ if ( 𝑖 ∈ ( ◡ 𝑌 “ ℕ ) , ( 𝑌 ‘ 𝑖 ) , 0 ) ) )
91 90 eqeq2d ⊢ ( 𝑤 = ( ◡ 𝑌 “ ℕ ) → ( 𝑦 = ( 𝑖 ∈ 𝐼 ↦ if ( 𝑖 ∈ 𝑤 , ( 𝑌 ‘ 𝑖 ) , 0 ) ) ↔ 𝑦 = ( 𝑖 ∈ 𝐼 ↦ if ( 𝑖 ∈ ( ◡ 𝑌 “ ℕ ) , ( 𝑌 ‘ 𝑖 ) , 0 ) ) ) )
92 91 ifbid ⊢ ( 𝑤 = ( ◡ 𝑌 “ ℕ ) → if ( 𝑦 = ( 𝑖 ∈ 𝐼 ↦ if ( 𝑖 ∈ 𝑤 , ( 𝑌 ‘ 𝑖 ) , 0 ) ) , 1 , 0 ) = if ( 𝑦 = ( 𝑖 ∈ 𝐼 ↦ if ( 𝑖 ∈ ( ◡ 𝑌 “ ℕ ) , ( 𝑌 ‘ 𝑖 ) , 0 ) ) , 1 , 0 ) )
93 92 mpteq2dv ⊢ ( 𝑤 = ( ◡ 𝑌 “ ℕ ) → ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = ( 𝑖 ∈ 𝐼 ↦ if ( 𝑖 ∈ 𝑤 , ( 𝑌 ‘ 𝑖 ) , 0 ) ) , 1 , 0 ) ) = ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = ( 𝑖 ∈ 𝐼 ↦ if ( 𝑖 ∈ ( ◡ 𝑌 “ ℕ ) , ( 𝑌 ‘ 𝑖 ) , 0 ) ) , 1 , 0 ) ) )
94 mpteq1 ⊢ ( 𝑤 = ( ◡ 𝑌 “ ℕ ) → ( 𝑘 ∈ 𝑤 ↦ ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ) = ( 𝑘 ∈ ( ◡ 𝑌 “ ℕ ) ↦ ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ) )
95 94 oveq2d ⊢ ( 𝑤 = ( ◡ 𝑌 “ ℕ ) → ( 𝐺 Σg ( 𝑘 ∈ 𝑤 ↦ ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ) ) = ( 𝐺 Σg ( 𝑘 ∈ ( ◡ 𝑌 “ ℕ ) ↦ ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ) ) )
96 93 95 eqeq12d ⊢ ( 𝑤 = ( ◡ 𝑌 “ ℕ ) → ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = ( 𝑖 ∈ 𝐼 ↦ if ( 𝑖 ∈ 𝑤 , ( 𝑌 ‘ 𝑖 ) , 0 ) ) , 1 , 0 ) ) = ( 𝐺 Σg ( 𝑘 ∈ 𝑤 ↦ ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ) ) ↔ ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = ( 𝑖 ∈ 𝐼 ↦ if ( 𝑖 ∈ ( ◡ 𝑌 “ ℕ ) , ( 𝑌 ‘ 𝑖 ) , 0 ) ) , 1 , 0 ) ) = ( 𝐺 Σg ( 𝑘 ∈ ( ◡ 𝑌 “ ℕ ) ↦ ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ) ) ) )
97 87 96 imbi12d ⊢ ( 𝑤 = ( ◡ 𝑌 “ ℕ ) → ( ( 𝑤 ⊆ 𝐼 → ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = ( 𝑖 ∈ 𝐼 ↦ if ( 𝑖 ∈ 𝑤 , ( 𝑌 ‘ 𝑖 ) , 0 ) ) , 1 , 0 ) ) = ( 𝐺 Σg ( 𝑘 ∈ 𝑤 ↦ ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ) ) ) ↔ ( ( ◡ 𝑌 “ ℕ ) ⊆ 𝐼 → ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = ( 𝑖 ∈ 𝐼 ↦ if ( 𝑖 ∈ ( ◡ 𝑌 “ ℕ ) , ( 𝑌 ‘ 𝑖 ) , 0 ) ) , 1 , 0 ) ) = ( 𝐺 Σg ( 𝑘 ∈ ( ◡ 𝑌 “ ℕ ) ↦ ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ) ) ) ) )
98 97 imbi2d ⊢ ( 𝑤 = ( ◡ 𝑌 “ ℕ ) → ( ( 𝜑 → ( 𝑤 ⊆ 𝐼 → ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = ( 𝑖 ∈ 𝐼 ↦ if ( 𝑖 ∈ 𝑤 , ( 𝑌 ‘ 𝑖 ) , 0 ) ) , 1 , 0 ) ) = ( 𝐺 Σg ( 𝑘 ∈ 𝑤 ↦ ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ) ) ) ) ↔ ( 𝜑 → ( ( ◡ 𝑌 “ ℕ ) ⊆ 𝐼 → ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = ( 𝑖 ∈ 𝐼 ↦ if ( 𝑖 ∈ ( ◡ 𝑌 “ ℕ ) , ( 𝑌 ‘ 𝑖 ) , 0 ) ) , 1 , 0 ) ) = ( 𝐺 Σg ( 𝑘 ∈ ( ◡ 𝑌 “ ℕ ) ↦ ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ) ) ) ) ) )
99 1 2 3 4 56 5 9 mpl1 ⊢ ( 𝜑 → ( 1r ‘ 𝑃 ) = ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = ( 𝐼 × { 0 } ) , 1 , 0 ) ) )
100 99 56 eqtr3di ⊢ ( 𝜑 → ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = ( 𝐼 × { 0 } ) , 1 , 0 ) ) = ( 1r ‘ 𝑃 ) )
101 100 a1d ⊢ ( 𝜑 → ( ∅ ⊆ 𝐼 → ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = ( 𝐼 × { 0 } ) , 1 , 0 ) ) = ( 1r ‘ 𝑃 ) ) )
102 ssun1 ⊢ 𝑥 ⊆ ( 𝑥 ∪ { 𝑧 } )
103 sstr2 ⊢ ( 𝑥 ⊆ ( 𝑥 ∪ { 𝑧 } ) → ( ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐼 → 𝑥 ⊆ 𝐼 ) )
104 102 103 ax-mp ⊢ ( ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐼 → 𝑥 ⊆ 𝐼 )
105 104 imim1i ⊢ ( ( 𝑥 ⊆ 𝐼 → ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = ( 𝑖 ∈ 𝐼 ↦ if ( 𝑖 ∈ 𝑥 , ( 𝑌 ‘ 𝑖 ) , 0 ) ) , 1 , 0 ) ) = ( 𝐺 Σg ( 𝑘 ∈ 𝑥 ↦ ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ) ) ) → ( ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐼 → ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = ( 𝑖 ∈ 𝐼 ↦ if ( 𝑖 ∈ 𝑥 , ( 𝑌 ‘ 𝑖 ) , 0 ) ) , 1 , 0 ) ) = ( 𝐺 Σg ( 𝑘 ∈ 𝑥 ↦ ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ) ) ) )
106 oveq1 ⊢ ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = ( 𝑖 ∈ 𝐼 ↦ if ( 𝑖 ∈ 𝑥 , ( 𝑌 ‘ 𝑖 ) , 0 ) ) , 1 , 0 ) ) = ( 𝐺 Σg ( 𝑘 ∈ 𝑥 ↦ ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ) ) → ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = ( 𝑖 ∈ 𝐼 ↦ if ( 𝑖 ∈ 𝑥 , ( 𝑌 ‘ 𝑖 ) , 0 ) ) , 1 , 0 ) ) ( .r ‘ 𝑃 ) ( ( 𝑌 ‘ 𝑧 ) ↑ ( 𝑉 ‘ 𝑧 ) ) ) = ( ( 𝐺 Σg ( 𝑘 ∈ 𝑥 ↦ ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ) ) ( .r ‘ 𝑃 ) ( ( 𝑌 ‘ 𝑧 ) ↑ ( 𝑉 ‘ 𝑧 ) ) ) )
107 eqid ⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
108 5 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐼 ) ) → 𝐼 ∈ 𝑊 )
109 9 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐼 ) ) → 𝑅 ∈ Ring )
110 15 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐼 ) ) → 𝑌 : 𝐼 ⟶ ℕ0 )
111 110 ffvelcdmda ⊢ ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐼 ) ) ∧ 𝑖 ∈ 𝐼 ) → ( 𝑌 ‘ 𝑖 ) ∈ ℕ0 )
112 0nn0 ⊢ 0 ∈ ℕ0
113 ifcl ⊢ ( ( ( 𝑌 ‘ 𝑖 ) ∈ ℕ0 ∧ 0 ∈ ℕ0 ) → if ( 𝑖 ∈ 𝑥 , ( 𝑌 ‘ 𝑖 ) , 0 ) ∈ ℕ0 )
114 111 112 113 sylancl ⊢ ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐼 ) ) ∧ 𝑖 ∈ 𝐼 ) → if ( 𝑖 ∈ 𝑥 , ( 𝑌 ‘ 𝑖 ) , 0 ) ∈ ℕ0 )
115 114 fmpttd ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐼 ) ) → ( 𝑖 ∈ 𝐼 ↦ if ( 𝑖 ∈ 𝑥 , ( 𝑌 ‘ 𝑖 ) , 0 ) ) : 𝐼 ⟶ ℕ0 )
116 fcdmnn0supp ⊢ ( ( 𝐼 ∈ 𝑊 ∧ ( 𝑖 ∈ 𝐼 ↦ if ( 𝑖 ∈ 𝑥 , ( 𝑌 ‘ 𝑖 ) , 0 ) ) : 𝐼 ⟶ ℕ0 ) → ( ( 𝑖 ∈ 𝐼 ↦ if ( 𝑖 ∈ 𝑥 , ( 𝑌 ‘ 𝑖 ) , 0 ) ) supp 0 ) = ( ◡ ( 𝑖 ∈ 𝐼 ↦ if ( 𝑖 ∈ 𝑥 , ( 𝑌 ‘ 𝑖 ) , 0 ) ) “ ℕ ) )
117 108 115 116 syl2anc ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐼 ) ) → ( ( 𝑖 ∈ 𝐼 ↦ if ( 𝑖 ∈ 𝑥 , ( 𝑌 ‘ 𝑖 ) , 0 ) ) supp 0 ) = ( ◡ ( 𝑖 ∈ 𝐼 ↦ if ( 𝑖 ∈ 𝑥 , ( 𝑌 ‘ 𝑖 ) , 0 ) ) “ ℕ ) )
118 simprll ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐼 ) ) → 𝑥 ∈ Fin )
119 eldifn ⊢ ( 𝑖 ∈ ( 𝐼 ∖ 𝑥 ) → ¬ 𝑖 ∈ 𝑥 )
120 119 adantl ⊢ ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐼 ) ) ∧ 𝑖 ∈ ( 𝐼 ∖ 𝑥 ) ) → ¬ 𝑖 ∈ 𝑥 )
121 120 iffalsed ⊢ ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐼 ) ) ∧ 𝑖 ∈ ( 𝐼 ∖ 𝑥 ) ) → if ( 𝑖 ∈ 𝑥 , ( 𝑌 ‘ 𝑖 ) , 0 ) = 0 )
122 121 108 suppss2 ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐼 ) ) → ( ( 𝑖 ∈ 𝐼 ↦ if ( 𝑖 ∈ 𝑥 , ( 𝑌 ‘ 𝑖 ) , 0 ) ) supp 0 ) ⊆ 𝑥 )
123 118 122 ssfid ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐼 ) ) → ( ( 𝑖 ∈ 𝐼 ↦ if ( 𝑖 ∈ 𝑥 , ( 𝑌 ‘ 𝑖 ) , 0 ) ) supp 0 ) ∈ Fin )
124 117 123 eqeltrrd ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐼 ) ) → ( ◡ ( 𝑖 ∈ 𝐼 ↦ if ( 𝑖 ∈ 𝑥 , ( 𝑌 ‘ 𝑖 ) , 0 ) ) “ ℕ ) ∈ Fin )
125 2 psrbag ⊢ ( 𝐼 ∈ 𝑊 → ( ( 𝑖 ∈ 𝐼 ↦ if ( 𝑖 ∈ 𝑥 , ( 𝑌 ‘ 𝑖 ) , 0 ) ) ∈ 𝐷 ↔ ( ( 𝑖 ∈ 𝐼 ↦ if ( 𝑖 ∈ 𝑥 , ( 𝑌 ‘ 𝑖 ) , 0 ) ) : 𝐼 ⟶ ℕ0 ∧ ( ◡ ( 𝑖 ∈ 𝐼 ↦ if ( 𝑖 ∈ 𝑥 , ( 𝑌 ‘ 𝑖 ) , 0 ) ) “ ℕ ) ∈ Fin ) ) )
126 108 125 syl ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐼 ) ) → ( ( 𝑖 ∈ 𝐼 ↦ if ( 𝑖 ∈ 𝑥 , ( 𝑌 ‘ 𝑖 ) , 0 ) ) ∈ 𝐷 ↔ ( ( 𝑖 ∈ 𝐼 ↦ if ( 𝑖 ∈ 𝑥 , ( 𝑌 ‘ 𝑖 ) , 0 ) ) : 𝐼 ⟶ ℕ0 ∧ ( ◡ ( 𝑖 ∈ 𝐼 ↦ if ( 𝑖 ∈ 𝑥 , ( 𝑌 ‘ 𝑖 ) , 0 ) ) “ ℕ ) ∈ Fin ) ) )
127 115 124 126 mpbir2and ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐼 ) ) → ( 𝑖 ∈ 𝐼 ↦ if ( 𝑖 ∈ 𝑥 , ( 𝑌 ‘ 𝑖 ) , 0 ) ) ∈ 𝐷 )
128 eqid ⊢ ( .r ‘ 𝑃 ) = ( .r ‘ 𝑃 )
129 ssun2 ⊢ { 𝑧 } ⊆ ( 𝑥 ∪ { 𝑧 } )
130 simprr ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐼 ) ) → ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐼 )
131 129 130 sstrid ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐼 ) ) → { 𝑧 } ⊆ 𝐼 )
132 vex ⊢ 𝑧 ∈ V
133 132 snss ⊢ ( 𝑧 ∈ 𝐼 ↔ { 𝑧 } ⊆ 𝐼 )
134 131 133 sylibr ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐼 ) ) → 𝑧 ∈ 𝐼 )
135 110 134 ffvelcdmd ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐼 ) ) → ( 𝑌 ‘ 𝑧 ) ∈ ℕ0 )
136 2 snifpsrbag ⊢ ( ( 𝐼 ∈ 𝑊 ∧ ( 𝑌 ‘ 𝑧 ) ∈ ℕ0 ) → ( 𝑖 ∈ 𝐼 ↦ if ( 𝑖 = 𝑧 , ( 𝑌 ‘ 𝑧 ) , 0 ) ) ∈ 𝐷 )
137 108 135 136 syl2anc ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐼 ) ) → ( 𝑖 ∈ 𝐼 ↦ if ( 𝑖 = 𝑧 , ( 𝑌 ‘ 𝑧 ) , 0 ) ) ∈ 𝐷 )
138 1 107 3 4 2 108 109 127 128 137 mplmonmul ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐼 ) ) → ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = ( 𝑖 ∈ 𝐼 ↦ if ( 𝑖 ∈ 𝑥 , ( 𝑌 ‘ 𝑖 ) , 0 ) ) , 1 , 0 ) ) ( .r ‘ 𝑃 ) ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = ( 𝑖 ∈ 𝐼 ↦ if ( 𝑖 = 𝑧 , ( 𝑌 ‘ 𝑧 ) , 0 ) ) , 1 , 0 ) ) ) = ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = ( ( 𝑖 ∈ 𝐼 ↦ if ( 𝑖 ∈ 𝑥 , ( 𝑌 ‘ 𝑖 ) , 0 ) ) ∘f + ( 𝑖 ∈ 𝐼 ↦ if ( 𝑖 = 𝑧 , ( 𝑌 ‘ 𝑧 ) , 0 ) ) ) , 1 , 0 ) ) )
139 1 2 3 4 108 6 7 8 109 134 135 mplcoe3 ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐼 ) ) → ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = ( 𝑖 ∈ 𝐼 ↦ if ( 𝑖 = 𝑧 , ( 𝑌 ‘ 𝑧 ) , 0 ) ) , 1 , 0 ) ) = ( ( 𝑌 ‘ 𝑧 ) ↑ ( 𝑉 ‘ 𝑧 ) ) )
140 139 oveq2d ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐼 ) ) → ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = ( 𝑖 ∈ 𝐼 ↦ if ( 𝑖 ∈ 𝑥 , ( 𝑌 ‘ 𝑖 ) , 0 ) ) , 1 , 0 ) ) ( .r ‘ 𝑃 ) ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = ( 𝑖 ∈ 𝐼 ↦ if ( 𝑖 = 𝑧 , ( 𝑌 ‘ 𝑧 ) , 0 ) ) , 1 , 0 ) ) ) = ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = ( 𝑖 ∈ 𝐼 ↦ if ( 𝑖 ∈ 𝑥 , ( 𝑌 ‘ 𝑖 ) , 0 ) ) , 1 , 0 ) ) ( .r ‘ 𝑃 ) ( ( 𝑌 ‘ 𝑧 ) ↑ ( 𝑉 ‘ 𝑧 ) ) ) )
141 135 adantr ⊢ ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐼 ) ) ∧ 𝑖 ∈ 𝐼 ) → ( 𝑌 ‘ 𝑧 ) ∈ ℕ0 )
142 ifcl ⊢ ( ( ( 𝑌 ‘ 𝑧 ) ∈ ℕ0 ∧ 0 ∈ ℕ0 ) → if ( 𝑖 = 𝑧 , ( 𝑌 ‘ 𝑧 ) , 0 ) ∈ ℕ0 )
143 141 112 142 sylancl ⊢ ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐼 ) ) ∧ 𝑖 ∈ 𝐼 ) → if ( 𝑖 = 𝑧 , ( 𝑌 ‘ 𝑧 ) , 0 ) ∈ ℕ0 )
144 eqidd ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐼 ) ) → ( 𝑖 ∈ 𝐼 ↦ if ( 𝑖 ∈ 𝑥 , ( 𝑌 ‘ 𝑖 ) , 0 ) ) = ( 𝑖 ∈ 𝐼 ↦ if ( 𝑖 ∈ 𝑥 , ( 𝑌 ‘ 𝑖 ) , 0 ) ) )
145 eqidd ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐼 ) ) → ( 𝑖 ∈ 𝐼 ↦ if ( 𝑖 = 𝑧 , ( 𝑌 ‘ 𝑧 ) , 0 ) ) = ( 𝑖 ∈ 𝐼 ↦ if ( 𝑖 = 𝑧 , ( 𝑌 ‘ 𝑧 ) , 0 ) ) )
146 108 114 143 144 145 offval2 ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐼 ) ) → ( ( 𝑖 ∈ 𝐼 ↦ if ( 𝑖 ∈ 𝑥 , ( 𝑌 ‘ 𝑖 ) , 0 ) ) ∘f + ( 𝑖 ∈ 𝐼 ↦ if ( 𝑖 = 𝑧 , ( 𝑌 ‘ 𝑧 ) , 0 ) ) ) = ( 𝑖 ∈ 𝐼 ↦ ( if ( 𝑖 ∈ 𝑥 , ( 𝑌 ‘ 𝑖 ) , 0 ) + if ( 𝑖 = 𝑧 , ( 𝑌 ‘ 𝑧 ) , 0 ) ) ) )
147 111 adantr ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐼 ) ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝑖 ∈ { 𝑧 } ) → ( 𝑌 ‘ 𝑖 ) ∈ ℕ0 )
148 147 nn0cnd ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐼 ) ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝑖 ∈ { 𝑧 } ) → ( 𝑌 ‘ 𝑖 ) ∈ ℂ )
149 148 addlidd ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐼 ) ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝑖 ∈ { 𝑧 } ) → ( 0 + ( 𝑌 ‘ 𝑖 ) ) = ( 𝑌 ‘ 𝑖 ) )
150 elsni ⊢ ( 𝑖 ∈ { 𝑧 } → 𝑖 = 𝑧 )
151 150 adantl ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐼 ) ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝑖 ∈ { 𝑧 } ) → 𝑖 = 𝑧 )
152 simprlr ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐼 ) ) → ¬ 𝑧 ∈ 𝑥 )
153 152 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐼 ) ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝑖 ∈ { 𝑧 } ) → ¬ 𝑧 ∈ 𝑥 )
154 151 153 eqneltrd ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐼 ) ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝑖 ∈ { 𝑧 } ) → ¬ 𝑖 ∈ 𝑥 )
155 154 iffalsed ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐼 ) ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝑖 ∈ { 𝑧 } ) → if ( 𝑖 ∈ 𝑥 , ( 𝑌 ‘ 𝑖 ) , 0 ) = 0 )
156 151 iftrued ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐼 ) ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝑖 ∈ { 𝑧 } ) → if ( 𝑖 = 𝑧 , ( 𝑌 ‘ 𝑧 ) , 0 ) = ( 𝑌 ‘ 𝑧 ) )
157 151 fveq2d ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐼 ) ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝑖 ∈ { 𝑧 } ) → ( 𝑌 ‘ 𝑖 ) = ( 𝑌 ‘ 𝑧 ) )
158 156 157 eqtr4d ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐼 ) ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝑖 ∈ { 𝑧 } ) → if ( 𝑖 = 𝑧 , ( 𝑌 ‘ 𝑧 ) , 0 ) = ( 𝑌 ‘ 𝑖 ) )
159 155 158 oveq12d ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐼 ) ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝑖 ∈ { 𝑧 } ) → ( if ( 𝑖 ∈ 𝑥 , ( 𝑌 ‘ 𝑖 ) , 0 ) + if ( 𝑖 = 𝑧 , ( 𝑌 ‘ 𝑧 ) , 0 ) ) = ( 0 + ( 𝑌 ‘ 𝑖 ) ) )
160 simpr ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐼 ) ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝑖 ∈ { 𝑧 } ) → 𝑖 ∈ { 𝑧 } )
161 129 160 sselid ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐼 ) ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝑖 ∈ { 𝑧 } ) → 𝑖 ∈ ( 𝑥 ∪ { 𝑧 } ) )
162 161 iftrued ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐼 ) ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝑖 ∈ { 𝑧 } ) → if ( 𝑖 ∈ ( 𝑥 ∪ { 𝑧 } ) , ( 𝑌 ‘ 𝑖 ) , 0 ) = ( 𝑌 ‘ 𝑖 ) )
163 149 159 162 3eqtr4d ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐼 ) ) ∧ 𝑖 ∈ 𝐼 ) ∧ 𝑖 ∈ { 𝑧 } ) → ( if ( 𝑖 ∈ 𝑥 , ( 𝑌 ‘ 𝑖 ) , 0 ) + if ( 𝑖 = 𝑧 , ( 𝑌 ‘ 𝑧 ) , 0 ) ) = if ( 𝑖 ∈ ( 𝑥 ∪ { 𝑧 } ) , ( 𝑌 ‘ 𝑖 ) , 0 ) )
164 114 adantr ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐼 ) ) ∧ 𝑖 ∈ 𝐼 ) ∧ ¬ 𝑖 ∈ { 𝑧 } ) → if ( 𝑖 ∈ 𝑥 , ( 𝑌 ‘ 𝑖 ) , 0 ) ∈ ℕ0 )
165 164 nn0cnd ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐼 ) ) ∧ 𝑖 ∈ 𝐼 ) ∧ ¬ 𝑖 ∈ { 𝑧 } ) → if ( 𝑖 ∈ 𝑥 , ( 𝑌 ‘ 𝑖 ) , 0 ) ∈ ℂ )
166 165 addridd ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐼 ) ) ∧ 𝑖 ∈ 𝐼 ) ∧ ¬ 𝑖 ∈ { 𝑧 } ) → ( if ( 𝑖 ∈ 𝑥 , ( 𝑌 ‘ 𝑖 ) , 0 ) + 0 ) = if ( 𝑖 ∈ 𝑥 , ( 𝑌 ‘ 𝑖 ) , 0 ) )
167 simpr ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐼 ) ) ∧ 𝑖 ∈ 𝐼 ) ∧ ¬ 𝑖 ∈ { 𝑧 } ) → ¬ 𝑖 ∈ { 𝑧 } )
168 velsn ⊢ ( 𝑖 ∈ { 𝑧 } ↔ 𝑖 = 𝑧 )
169 167 168 sylnib ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐼 ) ) ∧ 𝑖 ∈ 𝐼 ) ∧ ¬ 𝑖 ∈ { 𝑧 } ) → ¬ 𝑖 = 𝑧 )
170 169 iffalsed ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐼 ) ) ∧ 𝑖 ∈ 𝐼 ) ∧ ¬ 𝑖 ∈ { 𝑧 } ) → if ( 𝑖 = 𝑧 , ( 𝑌 ‘ 𝑧 ) , 0 ) = 0 )
171 170 oveq2d ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐼 ) ) ∧ 𝑖 ∈ 𝐼 ) ∧ ¬ 𝑖 ∈ { 𝑧 } ) → ( if ( 𝑖 ∈ 𝑥 , ( 𝑌 ‘ 𝑖 ) , 0 ) + if ( 𝑖 = 𝑧 , ( 𝑌 ‘ 𝑧 ) , 0 ) ) = ( if ( 𝑖 ∈ 𝑥 , ( 𝑌 ‘ 𝑖 ) , 0 ) + 0 ) )
172 elun ⊢ ( 𝑖 ∈ ( 𝑥 ∪ { 𝑧 } ) ↔ ( 𝑖 ∈ 𝑥 ∨ 𝑖 ∈ { 𝑧 } ) )
173 orcom ⊢ ( ( 𝑖 ∈ 𝑥 ∨ 𝑖 ∈ { 𝑧 } ) ↔ ( 𝑖 ∈ { 𝑧 } ∨ 𝑖 ∈ 𝑥 ) )
174 172 173 bitri ⊢ ( 𝑖 ∈ ( 𝑥 ∪ { 𝑧 } ) ↔ ( 𝑖 ∈ { 𝑧 } ∨ 𝑖 ∈ 𝑥 ) )
175 biorf ⊢ ( ¬ 𝑖 ∈ { 𝑧 } → ( 𝑖 ∈ 𝑥 ↔ ( 𝑖 ∈ { 𝑧 } ∨ 𝑖 ∈ 𝑥 ) ) )
176 174 175 bitr4id ⊢ ( ¬ 𝑖 ∈ { 𝑧 } → ( 𝑖 ∈ ( 𝑥 ∪ { 𝑧 } ) ↔ 𝑖 ∈ 𝑥 ) )
177 176 adantl ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐼 ) ) ∧ 𝑖 ∈ 𝐼 ) ∧ ¬ 𝑖 ∈ { 𝑧 } ) → ( 𝑖 ∈ ( 𝑥 ∪ { 𝑧 } ) ↔ 𝑖 ∈ 𝑥 ) )
178 177 ifbid ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐼 ) ) ∧ 𝑖 ∈ 𝐼 ) ∧ ¬ 𝑖 ∈ { 𝑧 } ) → if ( 𝑖 ∈ ( 𝑥 ∪ { 𝑧 } ) , ( 𝑌 ‘ 𝑖 ) , 0 ) = if ( 𝑖 ∈ 𝑥 , ( 𝑌 ‘ 𝑖 ) , 0 ) )
179 166 171 178 3eqtr4d ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐼 ) ) ∧ 𝑖 ∈ 𝐼 ) ∧ ¬ 𝑖 ∈ { 𝑧 } ) → ( if ( 𝑖 ∈ 𝑥 , ( 𝑌 ‘ 𝑖 ) , 0 ) + if ( 𝑖 = 𝑧 , ( 𝑌 ‘ 𝑧 ) , 0 ) ) = if ( 𝑖 ∈ ( 𝑥 ∪ { 𝑧 } ) , ( 𝑌 ‘ 𝑖 ) , 0 ) )
180 163 179 pm2.61dan ⊢ ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐼 ) ) ∧ 𝑖 ∈ 𝐼 ) → ( if ( 𝑖 ∈ 𝑥 , ( 𝑌 ‘ 𝑖 ) , 0 ) + if ( 𝑖 = 𝑧 , ( 𝑌 ‘ 𝑧 ) , 0 ) ) = if ( 𝑖 ∈ ( 𝑥 ∪ { 𝑧 } ) , ( 𝑌 ‘ 𝑖 ) , 0 ) )
181 180 mpteq2dva ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐼 ) ) → ( 𝑖 ∈ 𝐼 ↦ ( if ( 𝑖 ∈ 𝑥 , ( 𝑌 ‘ 𝑖 ) , 0 ) + if ( 𝑖 = 𝑧 , ( 𝑌 ‘ 𝑧 ) , 0 ) ) ) = ( 𝑖 ∈ 𝐼 ↦ if ( 𝑖 ∈ ( 𝑥 ∪ { 𝑧 } ) , ( 𝑌 ‘ 𝑖 ) , 0 ) ) )
182 146 181 eqtrd ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐼 ) ) → ( ( 𝑖 ∈ 𝐼 ↦ if ( 𝑖 ∈ 𝑥 , ( 𝑌 ‘ 𝑖 ) , 0 ) ) ∘f + ( 𝑖 ∈ 𝐼 ↦ if ( 𝑖 = 𝑧 , ( 𝑌 ‘ 𝑧 ) , 0 ) ) ) = ( 𝑖 ∈ 𝐼 ↦ if ( 𝑖 ∈ ( 𝑥 ∪ { 𝑧 } ) , ( 𝑌 ‘ 𝑖 ) , 0 ) ) )
183 182 eqeq2d ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐼 ) ) → ( 𝑦 = ( ( 𝑖 ∈ 𝐼 ↦ if ( 𝑖 ∈ 𝑥 , ( 𝑌 ‘ 𝑖 ) , 0 ) ) ∘f + ( 𝑖 ∈ 𝐼 ↦ if ( 𝑖 = 𝑧 , ( 𝑌 ‘ 𝑧 ) , 0 ) ) ) ↔ 𝑦 = ( 𝑖 ∈ 𝐼 ↦ if ( 𝑖 ∈ ( 𝑥 ∪ { 𝑧 } ) , ( 𝑌 ‘ 𝑖 ) , 0 ) ) ) )
184 183 ifbid ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐼 ) ) → if ( 𝑦 = ( ( 𝑖 ∈ 𝐼 ↦ if ( 𝑖 ∈ 𝑥 , ( 𝑌 ‘ 𝑖 ) , 0 ) ) ∘f + ( 𝑖 ∈ 𝐼 ↦ if ( 𝑖 = 𝑧 , ( 𝑌 ‘ 𝑧 ) , 0 ) ) ) , 1 , 0 ) = if ( 𝑦 = ( 𝑖 ∈ 𝐼 ↦ if ( 𝑖 ∈ ( 𝑥 ∪ { 𝑧 } ) , ( 𝑌 ‘ 𝑖 ) , 0 ) ) , 1 , 0 ) )
185 184 mpteq2dv ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐼 ) ) → ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = ( ( 𝑖 ∈ 𝐼 ↦ if ( 𝑖 ∈ 𝑥 , ( 𝑌 ‘ 𝑖 ) , 0 ) ) ∘f + ( 𝑖 ∈ 𝐼 ↦ if ( 𝑖 = 𝑧 , ( 𝑌 ‘ 𝑧 ) , 0 ) ) ) , 1 , 0 ) ) = ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = ( 𝑖 ∈ 𝐼 ↦ if ( 𝑖 ∈ ( 𝑥 ∪ { 𝑧 } ) , ( 𝑌 ‘ 𝑖 ) , 0 ) ) , 1 , 0 ) ) )
186 138 140 185 3eqtr3rd ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐼 ) ) → ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = ( 𝑖 ∈ 𝐼 ↦ if ( 𝑖 ∈ ( 𝑥 ∪ { 𝑧 } ) , ( 𝑌 ‘ 𝑖 ) , 0 ) ) , 1 , 0 ) ) = ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = ( 𝑖 ∈ 𝐼 ↦ if ( 𝑖 ∈ 𝑥 , ( 𝑌 ‘ 𝑖 ) , 0 ) ) , 1 , 0 ) ) ( .r ‘ 𝑃 ) ( ( 𝑌 ‘ 𝑧 ) ↑ ( 𝑉 ‘ 𝑧 ) ) ) )
187 6 107 mgpbas ⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝐺 )
188 6 128 mgpplusg ⊢ ( .r ‘ 𝑃 ) = ( +g ‘ 𝐺 )
189 eqid ⊢ ( Cntz ‘ 𝐺 ) = ( Cntz ‘ 𝐺 )
190 eqid ⊢ ( 𝑘 ∈ ( 𝑥 ∪ { 𝑧 } ) ↦ ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ) = ( 𝑘 ∈ ( 𝑥 ∪ { 𝑧 } ) ↦ ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) )
191 1 5 9 mplringd ⊢ ( 𝜑 → 𝑃 ∈ Ring )
192 6 ringmgp ⊢ ( 𝑃 ∈ Ring → 𝐺 ∈ Mnd )
193 191 192 syl ⊢ ( 𝜑 → 𝐺 ∈ Mnd )
194 193 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐼 ) ) → 𝐺 ∈ Mnd )
195 10 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐼 ) ) → 𝑌 ∈ 𝐷 )
196 fveq2 ⊢ ( 𝑥 = 𝑎 → ( 𝑉 ‘ 𝑥 ) = ( 𝑉 ‘ 𝑎 ) )
197 196 oveq2d ⊢ ( 𝑥 = 𝑎 → ( ( 𝑉 ‘ 𝑦 ) ( +g ‘ 𝐺 ) ( 𝑉 ‘ 𝑥 ) ) = ( ( 𝑉 ‘ 𝑦 ) ( +g ‘ 𝐺 ) ( 𝑉 ‘ 𝑎 ) ) )
198 196 oveq1d ⊢ ( 𝑥 = 𝑎 → ( ( 𝑉 ‘ 𝑥 ) ( +g ‘ 𝐺 ) ( 𝑉 ‘ 𝑦 ) ) = ( ( 𝑉 ‘ 𝑎 ) ( +g ‘ 𝐺 ) ( 𝑉 ‘ 𝑦 ) ) )
199 197 198 eqeq12d ⊢ ( 𝑥 = 𝑎 → ( ( ( 𝑉 ‘ 𝑦 ) ( +g ‘ 𝐺 ) ( 𝑉 ‘ 𝑥 ) ) = ( ( 𝑉 ‘ 𝑥 ) ( +g ‘ 𝐺 ) ( 𝑉 ‘ 𝑦 ) ) ↔ ( ( 𝑉 ‘ 𝑦 ) ( +g ‘ 𝐺 ) ( 𝑉 ‘ 𝑎 ) ) = ( ( 𝑉 ‘ 𝑎 ) ( +g ‘ 𝐺 ) ( 𝑉 ‘ 𝑦 ) ) ) )
200 fveq2 ⊢ ( 𝑦 = 𝑏 → ( 𝑉 ‘ 𝑦 ) = ( 𝑉 ‘ 𝑏 ) )
201 200 oveq1d ⊢ ( 𝑦 = 𝑏 → ( ( 𝑉 ‘ 𝑦 ) ( +g ‘ 𝐺 ) ( 𝑉 ‘ 𝑎 ) ) = ( ( 𝑉 ‘ 𝑏 ) ( +g ‘ 𝐺 ) ( 𝑉 ‘ 𝑎 ) ) )
202 200 oveq2d ⊢ ( 𝑦 = 𝑏 → ( ( 𝑉 ‘ 𝑎 ) ( +g ‘ 𝐺 ) ( 𝑉 ‘ 𝑦 ) ) = ( ( 𝑉 ‘ 𝑎 ) ( +g ‘ 𝐺 ) ( 𝑉 ‘ 𝑏 ) ) )
203 201 202 eqeq12d ⊢ ( 𝑦 = 𝑏 → ( ( ( 𝑉 ‘ 𝑦 ) ( +g ‘ 𝐺 ) ( 𝑉 ‘ 𝑎 ) ) = ( ( 𝑉 ‘ 𝑎 ) ( +g ‘ 𝐺 ) ( 𝑉 ‘ 𝑦 ) ) ↔ ( ( 𝑉 ‘ 𝑏 ) ( +g ‘ 𝐺 ) ( 𝑉 ‘ 𝑎 ) ) = ( ( 𝑉 ‘ 𝑎 ) ( +g ‘ 𝐺 ) ( 𝑉 ‘ 𝑏 ) ) ) )
204 199 203 cbvral2vw ⊢ ( ∀ 𝑥 ∈ 𝐼 ∀ 𝑦 ∈ 𝐼 ( ( 𝑉 ‘ 𝑦 ) ( +g ‘ 𝐺 ) ( 𝑉 ‘ 𝑥 ) ) = ( ( 𝑉 ‘ 𝑥 ) ( +g ‘ 𝐺 ) ( 𝑉 ‘ 𝑦 ) ) ↔ ∀ 𝑎 ∈ 𝐼 ∀ 𝑏 ∈ 𝐼 ( ( 𝑉 ‘ 𝑏 ) ( +g ‘ 𝐺 ) ( 𝑉 ‘ 𝑎 ) ) = ( ( 𝑉 ‘ 𝑎 ) ( +g ‘ 𝐺 ) ( 𝑉 ‘ 𝑏 ) ) )
205 11 204 sylib ⊢ ( 𝜑 → ∀ 𝑎 ∈ 𝐼 ∀ 𝑏 ∈ 𝐼 ( ( 𝑉 ‘ 𝑏 ) ( +g ‘ 𝐺 ) ( 𝑉 ‘ 𝑎 ) ) = ( ( 𝑉 ‘ 𝑎 ) ( +g ‘ 𝐺 ) ( 𝑉 ‘ 𝑏 ) ) )
206 205 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐼 ) ) → ∀ 𝑎 ∈ 𝐼 ∀ 𝑏 ∈ 𝐼 ( ( 𝑉 ‘ 𝑏 ) ( +g ‘ 𝐺 ) ( 𝑉 ‘ 𝑎 ) ) = ( ( 𝑉 ‘ 𝑎 ) ( +g ‘ 𝐺 ) ( 𝑉 ‘ 𝑏 ) ) )
207 1 2 3 4 108 6 7 8 109 195 206 130 mplcoe5lem ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐼 ) ) → ran ( 𝑘 ∈ ( 𝑥 ∪ { 𝑧 } ) ↦ ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ) ⊆ ( ( Cntz ‘ 𝐺 ) ‘ ran ( 𝑘 ∈ ( 𝑥 ∪ { 𝑧 } ) ↦ ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ) ) )
208 102 130 sstrid ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐼 ) ) → 𝑥 ⊆ 𝐼 )
209 208 sselda ⊢ ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐼 ) ) ∧ 𝑘 ∈ 𝑥 ) → 𝑘 ∈ 𝐼 )
210 193 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) → 𝐺 ∈ Mnd )
211 15 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) → ( 𝑌 ‘ 𝑘 ) ∈ ℕ0 )
212 5 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) → 𝐼 ∈ 𝑊 )
213 9 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) → 𝑅 ∈ Ring )
214 simpr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) → 𝑘 ∈ 𝐼 )
215 1 8 107 212 213 214 mvrcl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) → ( 𝑉 ‘ 𝑘 ) ∈ ( Base ‘ 𝑃 ) )
216 187 7 210 211 215 mulgnn0cld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) → ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ∈ ( Base ‘ 𝑃 ) )
217 216 adantlr ⊢ ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐼 ) ) ∧ 𝑘 ∈ 𝐼 ) → ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ∈ ( Base ‘ 𝑃 ) )
218 209 217 syldan ⊢ ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐼 ) ) ∧ 𝑘 ∈ 𝑥 ) → ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ∈ ( Base ‘ 𝑃 ) )
219 1 8 107 108 109 134 mvrcl ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐼 ) ) → ( 𝑉 ‘ 𝑧 ) ∈ ( Base ‘ 𝑃 ) )
220 187 7 194 135 219 mulgnn0cld ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐼 ) ) → ( ( 𝑌 ‘ 𝑧 ) ↑ ( 𝑉 ‘ 𝑧 ) ) ∈ ( Base ‘ 𝑃 ) )
221 fveq2 ⊢ ( 𝑘 = 𝑧 → ( 𝑌 ‘ 𝑘 ) = ( 𝑌 ‘ 𝑧 ) )
222 fveq2 ⊢ ( 𝑘 = 𝑧 → ( 𝑉 ‘ 𝑘 ) = ( 𝑉 ‘ 𝑧 ) )
223 221 222 oveq12d ⊢ ( 𝑘 = 𝑧 → ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) = ( ( 𝑌 ‘ 𝑧 ) ↑ ( 𝑉 ‘ 𝑧 ) ) )
224 223 adantl ⊢ ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐼 ) ) ∧ 𝑘 = 𝑧 ) → ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) = ( ( 𝑌 ‘ 𝑧 ) ↑ ( 𝑉 ‘ 𝑧 ) ) )
225 187 188 189 190 194 118 207 218 134 152 220 224 gsumzunsnd ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐼 ) ) → ( 𝐺 Σg ( 𝑘 ∈ ( 𝑥 ∪ { 𝑧 } ) ↦ ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ) ) = ( ( 𝐺 Σg ( 𝑘 ∈ 𝑥 ↦ ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ) ) ( .r ‘ 𝑃 ) ( ( 𝑌 ‘ 𝑧 ) ↑ ( 𝑉 ‘ 𝑧 ) ) ) )
226 186 225 eqeq12d ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐼 ) ) → ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = ( 𝑖 ∈ 𝐼 ↦ if ( 𝑖 ∈ ( 𝑥 ∪ { 𝑧 } ) , ( 𝑌 ‘ 𝑖 ) , 0 ) ) , 1 , 0 ) ) = ( 𝐺 Σg ( 𝑘 ∈ ( 𝑥 ∪ { 𝑧 } ) ↦ ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ) ) ↔ ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = ( 𝑖 ∈ 𝐼 ↦ if ( 𝑖 ∈ 𝑥 , ( 𝑌 ‘ 𝑖 ) , 0 ) ) , 1 , 0 ) ) ( .r ‘ 𝑃 ) ( ( 𝑌 ‘ 𝑧 ) ↑ ( 𝑉 ‘ 𝑧 ) ) ) = ( ( 𝐺 Σg ( 𝑘 ∈ 𝑥 ↦ ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ) ) ( .r ‘ 𝑃 ) ( ( 𝑌 ‘ 𝑧 ) ↑ ( 𝑉 ‘ 𝑧 ) ) ) ) )
227 106 226 imbitrrid ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐼 ) ) → ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = ( 𝑖 ∈ 𝐼 ↦ if ( 𝑖 ∈ 𝑥 , ( 𝑌 ‘ 𝑖 ) , 0 ) ) , 1 , 0 ) ) = ( 𝐺 Σg ( 𝑘 ∈ 𝑥 ↦ ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ) ) → ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = ( 𝑖 ∈ 𝐼 ↦ if ( 𝑖 ∈ ( 𝑥 ∪ { 𝑧 } ) , ( 𝑌 ‘ 𝑖 ) , 0 ) ) , 1 , 0 ) ) = ( 𝐺 Σg ( 𝑘 ∈ ( 𝑥 ∪ { 𝑧 } ) ↦ ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ) ) ) )
228 227 expr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ) → ( ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐼 → ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = ( 𝑖 ∈ 𝐼 ↦ if ( 𝑖 ∈ 𝑥 , ( 𝑌 ‘ 𝑖 ) , 0 ) ) , 1 , 0 ) ) = ( 𝐺 Σg ( 𝑘 ∈ 𝑥 ↦ ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ) ) → ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = ( 𝑖 ∈ 𝐼 ↦ if ( 𝑖 ∈ ( 𝑥 ∪ { 𝑧 } ) , ( 𝑌 ‘ 𝑖 ) , 0 ) ) , 1 , 0 ) ) = ( 𝐺 Σg ( 𝑘 ∈ ( 𝑥 ∪ { 𝑧 } ) ↦ ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ) ) ) ) )
229 228 a2d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ) → ( ( ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐼 → ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = ( 𝑖 ∈ 𝐼 ↦ if ( 𝑖 ∈ 𝑥 , ( 𝑌 ‘ 𝑖 ) , 0 ) ) , 1 , 0 ) ) = ( 𝐺 Σg ( 𝑘 ∈ 𝑥 ↦ ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ) ) ) → ( ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐼 → ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = ( 𝑖 ∈ 𝐼 ↦ if ( 𝑖 ∈ ( 𝑥 ∪ { 𝑧 } ) , ( 𝑌 ‘ 𝑖 ) , 0 ) ) , 1 , 0 ) ) = ( 𝐺 Σg ( 𝑘 ∈ ( 𝑥 ∪ { 𝑧 } ) ↦ ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ) ) ) ) )
230 105 229 syl5 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ) → ( ( 𝑥 ⊆ 𝐼 → ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = ( 𝑖 ∈ 𝐼 ↦ if ( 𝑖 ∈ 𝑥 , ( 𝑌 ‘ 𝑖 ) , 0 ) ) , 1 , 0 ) ) = ( 𝐺 Σg ( 𝑘 ∈ 𝑥 ↦ ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ) ) ) → ( ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐼 → ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = ( 𝑖 ∈ 𝐼 ↦ if ( 𝑖 ∈ ( 𝑥 ∪ { 𝑧 } ) , ( 𝑌 ‘ 𝑖 ) , 0 ) ) , 1 , 0 ) ) = ( 𝐺 Σg ( 𝑘 ∈ ( 𝑥 ∪ { 𝑧 } ) ↦ ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ) ) ) ) )
231 230 expcom ⊢ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) → ( 𝜑 → ( ( 𝑥 ⊆ 𝐼 → ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = ( 𝑖 ∈ 𝐼 ↦ if ( 𝑖 ∈ 𝑥 , ( 𝑌 ‘ 𝑖 ) , 0 ) ) , 1 , 0 ) ) = ( 𝐺 Σg ( 𝑘 ∈ 𝑥 ↦ ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ) ) ) → ( ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐼 → ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = ( 𝑖 ∈ 𝐼 ↦ if ( 𝑖 ∈ ( 𝑥 ∪ { 𝑧 } ) , ( 𝑌 ‘ 𝑖 ) , 0 ) ) , 1 , 0 ) ) = ( 𝐺 Σg ( 𝑘 ∈ ( 𝑥 ∪ { 𝑧 } ) ↦ ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ) ) ) ) ) )
232 231 a2d ⊢ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) → ( ( 𝜑 → ( 𝑥 ⊆ 𝐼 → ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = ( 𝑖 ∈ 𝐼 ↦ if ( 𝑖 ∈ 𝑥 , ( 𝑌 ‘ 𝑖 ) , 0 ) ) , 1 , 0 ) ) = ( 𝐺 Σg ( 𝑘 ∈ 𝑥 ↦ ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ) ) ) ) → ( 𝜑 → ( ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐼 → ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = ( 𝑖 ∈ 𝐼 ↦ if ( 𝑖 ∈ ( 𝑥 ∪ { 𝑧 } ) , ( 𝑌 ‘ 𝑖 ) , 0 ) ) , 1 , 0 ) ) = ( 𝐺 Σg ( 𝑘 ∈ ( 𝑥 ∪ { 𝑧 } ) ↦ ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ) ) ) ) ) )
233 62 74 86 98 101 232 findcard2s ⊢ ( ( ◡ 𝑌 “ ℕ ) ∈ Fin → ( 𝜑 → ( ( ◡ 𝑌 “ ℕ ) ⊆ 𝐼 → ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = ( 𝑖 ∈ 𝐼 ↦ if ( 𝑖 ∈ ( ◡ 𝑌 “ ℕ ) , ( 𝑌 ‘ 𝑖 ) , 0 ) ) , 1 , 0 ) ) = ( 𝐺 Σg ( 𝑘 ∈ ( ◡ 𝑌 “ ℕ ) ↦ ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ) ) ) ) )
234 40 233 mpcom ⊢ ( 𝜑 → ( ( ◡ 𝑌 “ ℕ ) ⊆ 𝐼 → ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = ( 𝑖 ∈ 𝐼 ↦ if ( 𝑖 ∈ ( ◡ 𝑌 “ ℕ ) , ( 𝑌 ‘ 𝑖 ) , 0 ) ) , 1 , 0 ) ) = ( 𝐺 Σg ( 𝑘 ∈ ( ◡ 𝑌 “ ℕ ) ↦ ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ) ) ) )
235 39 234 mpd ⊢ ( 𝜑 → ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = ( 𝑖 ∈ 𝐼 ↦ if ( 𝑖 ∈ ( ◡ 𝑌 “ ℕ ) , ( 𝑌 ‘ 𝑖 ) , 0 ) ) , 1 , 0 ) ) = ( 𝐺 Σg ( 𝑘 ∈ ( ◡ 𝑌 “ ℕ ) ↦ ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ) ) )
236 39 resmptd ⊢ ( 𝜑 → ( ( 𝑘 ∈ 𝐼 ↦ ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ) ↾ ( ◡ 𝑌 “ ℕ ) ) = ( 𝑘 ∈ ( ◡ 𝑌 “ ℕ ) ↦ ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ) )
237 236 oveq2d ⊢ ( 𝜑 → ( 𝐺 Σg ( ( 𝑘 ∈ 𝐼 ↦ ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ) ↾ ( ◡ 𝑌 “ ℕ ) ) ) = ( 𝐺 Σg ( 𝑘 ∈ ( ◡ 𝑌 “ ℕ ) ↦ ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ) ) )
238 216 fmpttd ⊢ ( 𝜑 → ( 𝑘 ∈ 𝐼 ↦ ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ) : 𝐼 ⟶ ( Base ‘ 𝑃 ) )
239 ssidd ⊢ ( 𝜑 → 𝐼 ⊆ 𝐼 )
240 1 2 3 4 5 6 7 8 9 10 11 239 mplcoe5lem ⊢ ( 𝜑 → ran ( 𝑘 ∈ 𝐼 ↦ ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ) ⊆ ( ( Cntz ‘ 𝐺 ) ‘ ran ( 𝑘 ∈ 𝐼 ↦ ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ) ) )
241 15 23 5 25 suppssr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐼 ∖ ( ◡ 𝑌 “ ℕ ) ) ) → ( 𝑌 ‘ 𝑘 ) = 0 )
242 241 oveq1d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐼 ∖ ( ◡ 𝑌 “ ℕ ) ) ) → ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) = ( 0 ↑ ( 𝑉 ‘ 𝑘 ) ) )
243 eldifi ⊢ ( 𝑘 ∈ ( 𝐼 ∖ ( ◡ 𝑌 “ ℕ ) ) → 𝑘 ∈ 𝐼 )
244 243 215 sylan2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐼 ∖ ( ◡ 𝑌 “ ℕ ) ) ) → ( 𝑉 ‘ 𝑘 ) ∈ ( Base ‘ 𝑃 ) )
245 187 57 7 mulg0 ⊢ ( ( 𝑉 ‘ 𝑘 ) ∈ ( Base ‘ 𝑃 ) → ( 0 ↑ ( 𝑉 ‘ 𝑘 ) ) = ( 1r ‘ 𝑃 ) )
246 244 245 syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐼 ∖ ( ◡ 𝑌 “ ℕ ) ) ) → ( 0 ↑ ( 𝑉 ‘ 𝑘 ) ) = ( 1r ‘ 𝑃 ) )
247 242 246 eqtrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐼 ∖ ( ◡ 𝑌 “ ℕ ) ) ) → ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) = ( 1r ‘ 𝑃 ) )
248 247 5 suppss2 ⊢ ( 𝜑 → ( ( 𝑘 ∈ 𝐼 ↦ ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ) supp ( 1r ‘ 𝑃 ) ) ⊆ ( ◡ 𝑌 “ ℕ ) )
249 5 mptexd ⊢ ( 𝜑 → ( 𝑘 ∈ 𝐼 ↦ ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ) ∈ V )
250 funmpt ⊢ Fun ( 𝑘 ∈ 𝐼 ↦ ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) )
251 250 a1i ⊢ ( 𝜑 → Fun ( 𝑘 ∈ 𝐼 ↦ ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ) )
252 fvexd ⊢ ( 𝜑 → ( 1r ‘ 𝑃 ) ∈ V )
253 suppssfifsupp ⊢ ( ( ( ( 𝑘 ∈ 𝐼 ↦ ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ) ∈ V ∧ Fun ( 𝑘 ∈ 𝐼 ↦ ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ) ∧ ( 1r ‘ 𝑃 ) ∈ V ) ∧ ( ( ◡ 𝑌 “ ℕ ) ∈ Fin ∧ ( ( 𝑘 ∈ 𝐼 ↦ ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ) supp ( 1r ‘ 𝑃 ) ) ⊆ ( ◡ 𝑌 “ ℕ ) ) ) → ( 𝑘 ∈ 𝐼 ↦ ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ) finSupp ( 1r ‘ 𝑃 ) )
254 249 251 252 40 248 253 syl32anc ⊢ ( 𝜑 → ( 𝑘 ∈ 𝐼 ↦ ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ) finSupp ( 1r ‘ 𝑃 ) )
255 187 57 189 193 5 238 240 248 254 gsumzres ⊢ ( 𝜑 → ( 𝐺 Σg ( ( 𝑘 ∈ 𝐼 ↦ ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ) ↾ ( ◡ 𝑌 “ ℕ ) ) ) = ( 𝐺 Σg ( 𝑘 ∈ 𝐼 ↦ ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ) ) )
256 235 237 255 3eqtr2d ⊢ ( 𝜑 → ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = ( 𝑖 ∈ 𝐼 ↦ if ( 𝑖 ∈ ( ◡ 𝑌 “ ℕ ) , ( 𝑌 ‘ 𝑖 ) , 0 ) ) , 1 , 0 ) ) = ( 𝐺 Σg ( 𝑘 ∈ 𝐼 ↦ ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ) ) )
257 37 256 eqtrd ⊢ ( 𝜑 → ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑌 , 1 , 0 ) ) = ( 𝐺 Σg ( 𝑘 ∈ 𝐼 ↦ ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ) ) )