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 frnnn0supp ⊢ ( ( 𝐼 ∈ 𝑊 ∧ 𝑌 : 𝐼 ⟶ ℕ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 ffvelrnda ⊢ ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ 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 frnnn0supp ⊢ ( ( 𝐼 ∈ 𝑊 ∧ ( 𝑖 ∈ 𝐼 ↦ 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 ffvelrnd ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 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 addid2d ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ 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 addid1d ⊢ ( ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ 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 mplring ⊢ ( ( 𝐼 ∈ 𝑊 ∧ 𝑅 ∈ Ring ) → 𝑃 ∈ Ring )
192 5 9 191 syl2anc ⊢ ( 𝜑 → 𝑃 ∈ Ring )
193 6 ringmgp ⊢ ( 𝑃 ∈ Ring → 𝐺 ∈ Mnd )
194 192 193 syl ⊢ ( 𝜑 → 𝐺 ∈ Mnd )
195 194 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐼 ) ) → 𝐺 ∈ Mnd )
196 10 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐼 ) ) → 𝑌 ∈ 𝐷 )
197 fveq2 ⊢ ( 𝑥 = 𝑎 → ( 𝑉 ‘ 𝑥 ) = ( 𝑉 ‘ 𝑎 ) )
198 197 oveq2d ⊢ ( 𝑥 = 𝑎 → ( ( 𝑉 ‘ 𝑦 ) ( +g ‘ 𝐺 ) ( 𝑉 ‘ 𝑥 ) ) = ( ( 𝑉 ‘ 𝑦 ) ( +g ‘ 𝐺 ) ( 𝑉 ‘ 𝑎 ) ) )
199 197 oveq1d ⊢ ( 𝑥 = 𝑎 → ( ( 𝑉 ‘ 𝑥 ) ( +g ‘ 𝐺 ) ( 𝑉 ‘ 𝑦 ) ) = ( ( 𝑉 ‘ 𝑎 ) ( +g ‘ 𝐺 ) ( 𝑉 ‘ 𝑦 ) ) )
200 198 199 eqeq12d ⊢ ( 𝑥 = 𝑎 → ( ( ( 𝑉 ‘ 𝑦 ) ( +g ‘ 𝐺 ) ( 𝑉 ‘ 𝑥 ) ) = ( ( 𝑉 ‘ 𝑥 ) ( +g ‘ 𝐺 ) ( 𝑉 ‘ 𝑦 ) ) ↔ ( ( 𝑉 ‘ 𝑦 ) ( +g ‘ 𝐺 ) ( 𝑉 ‘ 𝑎 ) ) = ( ( 𝑉 ‘ 𝑎 ) ( +g ‘ 𝐺 ) ( 𝑉 ‘ 𝑦 ) ) ) )
201 fveq2 ⊢ ( 𝑦 = 𝑏 → ( 𝑉 ‘ 𝑦 ) = ( 𝑉 ‘ 𝑏 ) )
202 201 oveq1d ⊢ ( 𝑦 = 𝑏 → ( ( 𝑉 ‘ 𝑦 ) ( +g ‘ 𝐺 ) ( 𝑉 ‘ 𝑎 ) ) = ( ( 𝑉 ‘ 𝑏 ) ( +g ‘ 𝐺 ) ( 𝑉 ‘ 𝑎 ) ) )
203 201 oveq2d ⊢ ( 𝑦 = 𝑏 → ( ( 𝑉 ‘ 𝑎 ) ( +g ‘ 𝐺 ) ( 𝑉 ‘ 𝑦 ) ) = ( ( 𝑉 ‘ 𝑎 ) ( +g ‘ 𝐺 ) ( 𝑉 ‘ 𝑏 ) ) )
204 202 203 eqeq12d ⊢ ( 𝑦 = 𝑏 → ( ( ( 𝑉 ‘ 𝑦 ) ( +g ‘ 𝐺 ) ( 𝑉 ‘ 𝑎 ) ) = ( ( 𝑉 ‘ 𝑎 ) ( +g ‘ 𝐺 ) ( 𝑉 ‘ 𝑦 ) ) ↔ ( ( 𝑉 ‘ 𝑏 ) ( +g ‘ 𝐺 ) ( 𝑉 ‘ 𝑎 ) ) = ( ( 𝑉 ‘ 𝑎 ) ( +g ‘ 𝐺 ) ( 𝑉 ‘ 𝑏 ) ) ) )
205 200 204 cbvral2vw ⊢ ( ∀ 𝑥 ∈ 𝐼 ∀ 𝑦 ∈ 𝐼 ( ( 𝑉 ‘ 𝑦 ) ( +g ‘ 𝐺 ) ( 𝑉 ‘ 𝑥 ) ) = ( ( 𝑉 ‘ 𝑥 ) ( +g ‘ 𝐺 ) ( 𝑉 ‘ 𝑦 ) ) ↔ ∀ 𝑎 ∈ 𝐼 ∀ 𝑏 ∈ 𝐼 ( ( 𝑉 ‘ 𝑏 ) ( +g ‘ 𝐺 ) ( 𝑉 ‘ 𝑎 ) ) = ( ( 𝑉 ‘ 𝑎 ) ( +g ‘ 𝐺 ) ( 𝑉 ‘ 𝑏 ) ) )
206 11 205 sylib ⊢ ( 𝜑 → ∀ 𝑎 ∈ 𝐼 ∀ 𝑏 ∈ 𝐼 ( ( 𝑉 ‘ 𝑏 ) ( +g ‘ 𝐺 ) ( 𝑉 ‘ 𝑎 ) ) = ( ( 𝑉 ‘ 𝑎 ) ( +g ‘ 𝐺 ) ( 𝑉 ‘ 𝑏 ) ) )
207 206 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐼 ) ) → ∀ 𝑎 ∈ 𝐼 ∀ 𝑏 ∈ 𝐼 ( ( 𝑉 ‘ 𝑏 ) ( +g ‘ 𝐺 ) ( 𝑉 ‘ 𝑎 ) ) = ( ( 𝑉 ‘ 𝑎 ) ( +g ‘ 𝐺 ) ( 𝑉 ‘ 𝑏 ) ) )
208 1 2 3 4 108 6 7 8 109 196 207 130 mplcoe5lem ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐼 ) ) → ran ( 𝑘 ∈ ( 𝑥 ∪ { 𝑧 } ) ↦ ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ) ⊆ ( ( Cntz ‘ 𝐺 ) ‘ ran ( 𝑘 ∈ ( 𝑥 ∪ { 𝑧 } ) ↦ ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ) ) )
209 102 130 sstrid ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐼 ) ) → 𝑥 ⊆ 𝐼 )
210 209 sselda ⊢ ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐼 ) ) ∧ 𝑘 ∈ 𝑥 ) → 𝑘 ∈ 𝐼 )
211 194 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) → 𝐺 ∈ Mnd )
212 15 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) → ( 𝑌 ‘ 𝑘 ) ∈ ℕ0 )
213 5 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) → 𝐼 ∈ 𝑊 )
214 9 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) → 𝑅 ∈ Ring )
215 simpr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) → 𝑘 ∈ 𝐼 )
216 1 8 107 213 214 215 mvrcl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) → ( 𝑉 ‘ 𝑘 ) ∈ ( Base ‘ 𝑃 ) )
217 187 7 mulgnn0cl ⊢ ( ( 𝐺 ∈ Mnd ∧ ( 𝑌 ‘ 𝑘 ) ∈ ℕ0 ∧ ( 𝑉 ‘ 𝑘 ) ∈ ( Base ‘ 𝑃 ) ) → ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ∈ ( Base ‘ 𝑃 ) )
218 211 212 216 217 syl3anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐼 ) → ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ∈ ( Base ‘ 𝑃 ) )
219 218 adantlr ⊢ ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐼 ) ) ∧ 𝑘 ∈ 𝐼 ) → ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ∈ ( Base ‘ 𝑃 ) )
220 210 219 syldan ⊢ ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐼 ) ) ∧ 𝑘 ∈ 𝑥 ) → ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ∈ ( Base ‘ 𝑃 ) )
221 1 8 107 108 109 134 mvrcl ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐼 ) ) → ( 𝑉 ‘ 𝑧 ) ∈ ( Base ‘ 𝑃 ) )
222 187 7 mulgnn0cl ⊢ ( ( 𝐺 ∈ Mnd ∧ ( 𝑌 ‘ 𝑧 ) ∈ ℕ0 ∧ ( 𝑉 ‘ 𝑧 ) ∈ ( Base ‘ 𝑃 ) ) → ( ( 𝑌 ‘ 𝑧 ) ↑ ( 𝑉 ‘ 𝑧 ) ) ∈ ( Base ‘ 𝑃 ) )
223 195 135 221 222 syl3anc ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐼 ) ) → ( ( 𝑌 ‘ 𝑧 ) ↑ ( 𝑉 ‘ 𝑧 ) ) ∈ ( Base ‘ 𝑃 ) )
224 fveq2 ⊢ ( 𝑘 = 𝑧 → ( 𝑌 ‘ 𝑘 ) = ( 𝑌 ‘ 𝑧 ) )
225 fveq2 ⊢ ( 𝑘 = 𝑧 → ( 𝑉 ‘ 𝑘 ) = ( 𝑉 ‘ 𝑧 ) )
226 224 225 oveq12d ⊢ ( 𝑘 = 𝑧 → ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) = ( ( 𝑌 ‘ 𝑧 ) ↑ ( 𝑉 ‘ 𝑧 ) ) )
227 226 adantl ⊢ ( ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐼 ) ) ∧ 𝑘 = 𝑧 ) → ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) = ( ( 𝑌 ‘ 𝑧 ) ↑ ( 𝑉 ‘ 𝑧 ) ) )
228 187 188 189 190 195 118 208 220 134 152 223 227 gsumzunsnd ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐼 ) ) → ( 𝐺 Σg ( 𝑘 ∈ ( 𝑥 ∪ { 𝑧 } ) ↦ ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ) ) = ( ( 𝐺 Σg ( 𝑘 ∈ 𝑥 ↦ ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ) ) ( .r ‘ 𝑃 ) ( ( 𝑌 ‘ 𝑧 ) ↑ ( 𝑉 ‘ 𝑧 ) ) ) )
229 186 228 eqeq12d ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐼 ) ) → ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = ( 𝑖 ∈ 𝐼 ↦ if ( 𝑖 ∈ ( 𝑥 ∪ { 𝑧 } ) , ( 𝑌 ‘ 𝑖 ) , 0 ) ) , 1 , 0 ) ) = ( 𝐺 Σg ( 𝑘 ∈ ( 𝑥 ∪ { 𝑧 } ) ↦ ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ) ) ↔ ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = ( 𝑖 ∈ 𝐼 ↦ if ( 𝑖 ∈ 𝑥 , ( 𝑌 ‘ 𝑖 ) , 0 ) ) , 1 , 0 ) ) ( .r ‘ 𝑃 ) ( ( 𝑌 ‘ 𝑧 ) ↑ ( 𝑉 ‘ 𝑧 ) ) ) = ( ( 𝐺 Σg ( 𝑘 ∈ 𝑥 ↦ ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ) ) ( .r ‘ 𝑃 ) ( ( 𝑌 ‘ 𝑧 ) ↑ ( 𝑉 ‘ 𝑧 ) ) ) ) )
230 106 229 syl5ibr ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ∧ ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐼 ) ) → ( ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = ( 𝑖 ∈ 𝐼 ↦ if ( 𝑖 ∈ 𝑥 , ( 𝑌 ‘ 𝑖 ) , 0 ) ) , 1 , 0 ) ) = ( 𝐺 Σg ( 𝑘 ∈ 𝑥 ↦ ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ) ) → ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = ( 𝑖 ∈ 𝐼 ↦ if ( 𝑖 ∈ ( 𝑥 ∪ { 𝑧 } ) , ( 𝑌 ‘ 𝑖 ) , 0 ) ) , 1 , 0 ) ) = ( 𝐺 Σg ( 𝑘 ∈ ( 𝑥 ∪ { 𝑧 } ) ↦ ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ) ) ) )
231 230 expr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 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 105 232 syl5 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) ) → ( ( 𝑥 ⊆ 𝐼 → ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = ( 𝑖 ∈ 𝐼 ↦ if ( 𝑖 ∈ 𝑥 , ( 𝑌 ‘ 𝑖 ) , 0 ) ) , 1 , 0 ) ) = ( 𝐺 Σg ( 𝑘 ∈ 𝑥 ↦ ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ) ) ) → ( ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐼 → ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = ( 𝑖 ∈ 𝐼 ↦ if ( 𝑖 ∈ ( 𝑥 ∪ { 𝑧 } ) , ( 𝑌 ‘ 𝑖 ) , 0 ) ) , 1 , 0 ) ) = ( 𝐺 Σg ( 𝑘 ∈ ( 𝑥 ∪ { 𝑧 } ) ↦ ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ) ) ) ) )
234 233 expcom ⊢ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) → ( 𝜑 → ( ( 𝑥 ⊆ 𝐼 → ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = ( 𝑖 ∈ 𝐼 ↦ if ( 𝑖 ∈ 𝑥 , ( 𝑌 ‘ 𝑖 ) , 0 ) ) , 1 , 0 ) ) = ( 𝐺 Σg ( 𝑘 ∈ 𝑥 ↦ ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ) ) ) → ( ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐼 → ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = ( 𝑖 ∈ 𝐼 ↦ if ( 𝑖 ∈ ( 𝑥 ∪ { 𝑧 } ) , ( 𝑌 ‘ 𝑖 ) , 0 ) ) , 1 , 0 ) ) = ( 𝐺 Σg ( 𝑘 ∈ ( 𝑥 ∪ { 𝑧 } ) ↦ ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ) ) ) ) ) )
235 234 a2d ⊢ ( ( 𝑥 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑥 ) → ( ( 𝜑 → ( 𝑥 ⊆ 𝐼 → ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = ( 𝑖 ∈ 𝐼 ↦ if ( 𝑖 ∈ 𝑥 , ( 𝑌 ‘ 𝑖 ) , 0 ) ) , 1 , 0 ) ) = ( 𝐺 Σg ( 𝑘 ∈ 𝑥 ↦ ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ) ) ) ) → ( 𝜑 → ( ( 𝑥 ∪ { 𝑧 } ) ⊆ 𝐼 → ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = ( 𝑖 ∈ 𝐼 ↦ if ( 𝑖 ∈ ( 𝑥 ∪ { 𝑧 } ) , ( 𝑌 ‘ 𝑖 ) , 0 ) ) , 1 , 0 ) ) = ( 𝐺 Σg ( 𝑘 ∈ ( 𝑥 ∪ { 𝑧 } ) ↦ ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ) ) ) ) ) )
236 62 74 86 98 101 235 findcard2s ⊢ ( ( ◡ 𝑌 “ ℕ ) ∈ Fin → ( 𝜑 → ( ( ◡ 𝑌 “ ℕ ) ⊆ 𝐼 → ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = ( 𝑖 ∈ 𝐼 ↦ if ( 𝑖 ∈ ( ◡ 𝑌 “ ℕ ) , ( 𝑌 ‘ 𝑖 ) , 0 ) ) , 1 , 0 ) ) = ( 𝐺 Σg ( 𝑘 ∈ ( ◡ 𝑌 “ ℕ ) ↦ ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ) ) ) ) )
237 40 236 mpcom ⊢ ( 𝜑 → ( ( ◡ 𝑌 “ ℕ ) ⊆ 𝐼 → ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = ( 𝑖 ∈ 𝐼 ↦ if ( 𝑖 ∈ ( ◡ 𝑌 “ ℕ ) , ( 𝑌 ‘ 𝑖 ) , 0 ) ) , 1 , 0 ) ) = ( 𝐺 Σg ( 𝑘 ∈ ( ◡ 𝑌 “ ℕ ) ↦ ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ) ) ) )
238 39 237 mpd ⊢ ( 𝜑 → ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = ( 𝑖 ∈ 𝐼 ↦ if ( 𝑖 ∈ ( ◡ 𝑌 “ ℕ ) , ( 𝑌 ‘ 𝑖 ) , 0 ) ) , 1 , 0 ) ) = ( 𝐺 Σg ( 𝑘 ∈ ( ◡ 𝑌 “ ℕ ) ↦ ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ) ) )
239 39 resmptd ⊢ ( 𝜑 → ( ( 𝑘 ∈ 𝐼 ↦ ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ) ↾ ( ◡ 𝑌 “ ℕ ) ) = ( 𝑘 ∈ ( ◡ 𝑌 “ ℕ ) ↦ ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ) )
240 239 oveq2d ⊢ ( 𝜑 → ( 𝐺 Σg ( ( 𝑘 ∈ 𝐼 ↦ ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ) ↾ ( ◡ 𝑌 “ ℕ ) ) ) = ( 𝐺 Σg ( 𝑘 ∈ ( ◡ 𝑌 “ ℕ ) ↦ ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ) ) )
241 218 fmpttd ⊢ ( 𝜑 → ( 𝑘 ∈ 𝐼 ↦ ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ) : 𝐼 ⟶ ( Base ‘ 𝑃 ) )
242 ssidd ⊢ ( 𝜑 → 𝐼 ⊆ 𝐼 )
243 1 2 3 4 5 6 7 8 9 10 11 242 mplcoe5lem ⊢ ( 𝜑 → ran ( 𝑘 ∈ 𝐼 ↦ ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ) ⊆ ( ( Cntz ‘ 𝐺 ) ‘ ran ( 𝑘 ∈ 𝐼 ↦ ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ) ) )
244 15 23 5 25 suppssr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐼 ∖ ( ◡ 𝑌 “ ℕ ) ) ) → ( 𝑌 ‘ 𝑘 ) = 0 )
245 244 oveq1d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐼 ∖ ( ◡ 𝑌 “ ℕ ) ) ) → ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) = ( 0 ↑ ( 𝑉 ‘ 𝑘 ) ) )
246 eldifi ⊢ ( 𝑘 ∈ ( 𝐼 ∖ ( ◡ 𝑌 “ ℕ ) ) → 𝑘 ∈ 𝐼 )
247 246 216 sylan2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐼 ∖ ( ◡ 𝑌 “ ℕ ) ) ) → ( 𝑉 ‘ 𝑘 ) ∈ ( Base ‘ 𝑃 ) )
248 187 57 7 mulg0 ⊢ ( ( 𝑉 ‘ 𝑘 ) ∈ ( Base ‘ 𝑃 ) → ( 0 ↑ ( 𝑉 ‘ 𝑘 ) ) = ( 1r ‘ 𝑃 ) )
249 247 248 syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐼 ∖ ( ◡ 𝑌 “ ℕ ) ) ) → ( 0 ↑ ( 𝑉 ‘ 𝑘 ) ) = ( 1r ‘ 𝑃 ) )
250 245 249 eqtrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐼 ∖ ( ◡ 𝑌 “ ℕ ) ) ) → ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) = ( 1r ‘ 𝑃 ) )
251 250 5 suppss2 ⊢ ( 𝜑 → ( ( 𝑘 ∈ 𝐼 ↦ ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ) supp ( 1r ‘ 𝑃 ) ) ⊆ ( ◡ 𝑌 “ ℕ ) )
252 5 mptexd ⊢ ( 𝜑 → ( 𝑘 ∈ 𝐼 ↦ ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ) ∈ V )
253 funmpt ⊢ Fun ( 𝑘 ∈ 𝐼 ↦ ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) )
254 253 a1i ⊢ ( 𝜑 → Fun ( 𝑘 ∈ 𝐼 ↦ ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ) )
255 fvexd ⊢ ( 𝜑 → ( 1r ‘ 𝑃 ) ∈ V )
256 suppssfifsupp ⊢ ( ( ( ( 𝑘 ∈ 𝐼 ↦ ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ) ∈ V ∧ Fun ( 𝑘 ∈ 𝐼 ↦ ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ) ∧ ( 1r ‘ 𝑃 ) ∈ V ) ∧ ( ( ◡ 𝑌 “ ℕ ) ∈ Fin ∧ ( ( 𝑘 ∈ 𝐼 ↦ ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ) supp ( 1r ‘ 𝑃 ) ) ⊆ ( ◡ 𝑌 “ ℕ ) ) ) → ( 𝑘 ∈ 𝐼 ↦ ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ) finSupp ( 1r ‘ 𝑃 ) )
257 252 254 255 40 251 256 syl32anc ⊢ ( 𝜑 → ( 𝑘 ∈ 𝐼 ↦ ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ) finSupp ( 1r ‘ 𝑃 ) )
258 187 57 189 194 5 241 243 251 257 gsumzres ⊢ ( 𝜑 → ( 𝐺 Σg ( ( 𝑘 ∈ 𝐼 ↦ ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ) ↾ ( ◡ 𝑌 “ ℕ ) ) ) = ( 𝐺 Σg ( 𝑘 ∈ 𝐼 ↦ ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ) ) )
259 238 240 258 3eqtr2d ⊢ ( 𝜑 → ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = ( 𝑖 ∈ 𝐼 ↦ if ( 𝑖 ∈ ( ◡ 𝑌 “ ℕ ) , ( 𝑌 ‘ 𝑖 ) , 0 ) ) , 1 , 0 ) ) = ( 𝐺 Σg ( 𝑘 ∈ 𝐼 ↦ ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ) ) )
260 37 259 eqtrd ⊢ ( 𝜑 → ( 𝑦 ∈ 𝐷 ↦ if ( 𝑦 = 𝑌 , 1 , 0 ) ) = ( 𝐺 Σg ( 𝑘 ∈ 𝐼 ↦ ( ( 𝑌 ‘ 𝑘 ) ↑ ( 𝑉 ‘ 𝑘 ) ) ) ) )