Metamath Proof Explorer

Theorem pmatcollpw3lem

Description: Lemma for pmatcollpw3 and pmatcollpw3fi : Write a polynomial matrix (over a commutative ring) as a sum of products of variable powers and constant matrices with scalar entries. (Contributed by AV, 8-Dec-2019)

Ref Expression
Hypotheses pmatcollpw.p ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
pmatcollpw.c ⊢ 𝐶 = ( 𝑁 Mat 𝑃 )
pmatcollpw.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
pmatcollpw.m ⊢ ∗ = ( ·𝑠 ‘ 𝐶 )
pmatcollpw.e ⊢ ↑ = ( .g ‘ ( mulGrp ‘ 𝑃 ) )
pmatcollpw.x ⊢ 𝑋 = ( var1 ‘ 𝑅 )
pmatcollpw.t ⊢ 𝑇 = ( 𝑁 matToPolyMat 𝑅 )
pmatcollpw3.a ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
pmatcollpw3.d ⊢ 𝐷 = ( Base ‘ 𝐴 )
Assertion pmatcollpw3lem ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝐼 ⊆ ℕ0 ∧ 𝐼 ≠ ∅ ) ) → ( 𝑀 = ( 𝐶 Σg ( 𝑛 ∈ 𝐼 ↦ ( ( 𝑛 ↑ 𝑋 ) ∗ ( 𝑇 ‘ ( 𝑀 decompPMat 𝑛 ) ) ) ) ) → ∃ 𝑓 ∈ ( 𝐷 ↑m 𝐼 ) 𝑀 = ( 𝐶 Σg ( 𝑛 ∈ 𝐼 ↦ ( ( 𝑛 ↑ 𝑋 ) ∗ ( 𝑇 ‘ ( 𝑓 ‘ 𝑛 ) ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 pmatcollpw.p ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
2 pmatcollpw.c ⊢ 𝐶 = ( 𝑁 Mat 𝑃 )
3 pmatcollpw.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
4 pmatcollpw.m ⊢ ∗ = ( ·𝑠 ‘ 𝐶 )
5 pmatcollpw.e ⊢ ↑ = ( .g ‘ ( mulGrp ‘ 𝑃 ) )
6 pmatcollpw.x ⊢ 𝑋 = ( var1 ‘ 𝑅 )
7 pmatcollpw.t ⊢ 𝑇 = ( 𝑁 matToPolyMat 𝑅 )
8 pmatcollpw3.a ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
9 pmatcollpw3.d ⊢ 𝐷 = ( Base ‘ 𝐴 )
10 dmeq ⊢ ( 𝑥 = 𝑦 → dom 𝑥 = dom 𝑦 )
11 10 dmeqd ⊢ ( 𝑥 = 𝑦 → dom dom 𝑥 = dom dom 𝑦 )
12 oveq ⊢ ( 𝑥 = 𝑦 → ( 𝑖 𝑥 𝑗 ) = ( 𝑖 𝑦 𝑗 ) )
13 12 fveq2d ⊢ ( 𝑥 = 𝑦 → ( coe1 ‘ ( 𝑖 𝑥 𝑗 ) ) = ( coe1 ‘ ( 𝑖 𝑦 𝑗 ) ) )
14 13 fveq1d ⊢ ( 𝑥 = 𝑦 → ( ( coe1 ‘ ( 𝑖 𝑥 𝑗 ) ) ‘ 𝑘 ) = ( ( coe1 ‘ ( 𝑖 𝑦 𝑗 ) ) ‘ 𝑘 ) )
15 11 11 14 mpoeq123dv ⊢ ( 𝑥 = 𝑦 → ( 𝑖 ∈ dom dom 𝑥 , 𝑗 ∈ dom dom 𝑥 ↦ ( ( coe1 ‘ ( 𝑖 𝑥 𝑗 ) ) ‘ 𝑘 ) ) = ( 𝑖 ∈ dom dom 𝑦 , 𝑗 ∈ dom dom 𝑦 ↦ ( ( coe1 ‘ ( 𝑖 𝑦 𝑗 ) ) ‘ 𝑘 ) ) )
16 fveq2 ⊢ ( 𝑘 = 𝑙 → ( ( coe1 ‘ ( 𝑖 𝑦 𝑗 ) ) ‘ 𝑘 ) = ( ( coe1 ‘ ( 𝑖 𝑦 𝑗 ) ) ‘ 𝑙 ) )
17 16 mpoeq3dv ⊢ ( 𝑘 = 𝑙 → ( 𝑖 ∈ dom dom 𝑦 , 𝑗 ∈ dom dom 𝑦 ↦ ( ( coe1 ‘ ( 𝑖 𝑦 𝑗 ) ) ‘ 𝑘 ) ) = ( 𝑖 ∈ dom dom 𝑦 , 𝑗 ∈ dom dom 𝑦 ↦ ( ( coe1 ‘ ( 𝑖 𝑦 𝑗 ) ) ‘ 𝑙 ) ) )
18 15 17 cbvmpov ⊢ ( 𝑥 ∈ 𝐵 , 𝑘 ∈ 𝐼 ↦ ( 𝑖 ∈ dom dom 𝑥 , 𝑗 ∈ dom dom 𝑥 ↦ ( ( coe1 ‘ ( 𝑖 𝑥 𝑗 ) ) ‘ 𝑘 ) ) ) = ( 𝑦 ∈ 𝐵 , 𝑙 ∈ 𝐼 ↦ ( 𝑖 ∈ dom dom 𝑦 , 𝑗 ∈ dom dom 𝑦 ↦ ( ( coe1 ‘ ( 𝑖 𝑦 𝑗 ) ) ‘ 𝑙 ) ) )
19 dmexg ⊢ ( 𝑦 ∈ 𝐵 → dom 𝑦 ∈ V )
20 19 dmexd ⊢ ( 𝑦 ∈ 𝐵 → dom dom 𝑦 ∈ V )
21 20 20 jca ⊢ ( 𝑦 ∈ 𝐵 → ( dom dom 𝑦 ∈ V ∧ dom dom 𝑦 ∈ V ) )
22 21 ad2antrl ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝐼 ⊆ ℕ0 ∧ 𝐼 ≠ ∅ ) ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑙 ∈ 𝐼 ) ) → ( dom dom 𝑦 ∈ V ∧ dom dom 𝑦 ∈ V ) )
23 mpoexga ⊢ ( ( dom dom 𝑦 ∈ V ∧ dom dom 𝑦 ∈ V ) → ( 𝑖 ∈ dom dom 𝑦 , 𝑗 ∈ dom dom 𝑦 ↦ ( ( coe1 ‘ ( 𝑖 𝑦 𝑗 ) ) ‘ 𝑙 ) ) ∈ V )
24 22 23 syl ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝐼 ⊆ ℕ0 ∧ 𝐼 ≠ ∅ ) ) ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑙 ∈ 𝐼 ) ) → ( 𝑖 ∈ dom dom 𝑦 , 𝑗 ∈ dom dom 𝑦 ↦ ( ( coe1 ‘ ( 𝑖 𝑦 𝑗 ) ) ‘ 𝑙 ) ) ∈ V )
25 24 ralrimivva ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝐼 ⊆ ℕ0 ∧ 𝐼 ≠ ∅ ) ) → ∀ 𝑦 ∈ 𝐵 ∀ 𝑙 ∈ 𝐼 ( 𝑖 ∈ dom dom 𝑦 , 𝑗 ∈ dom dom 𝑦 ↦ ( ( coe1 ‘ ( 𝑖 𝑦 𝑗 ) ) ‘ 𝑙 ) ) ∈ V )
26 simprr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝐼 ⊆ ℕ0 ∧ 𝐼 ≠ ∅ ) ) → 𝐼 ≠ ∅ )
27 nn0ex ⊢ ℕ0 ∈ V
28 27 ssex ⊢ ( 𝐼 ⊆ ℕ0 → 𝐼 ∈ V )
29 28 ad2antrl ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝐼 ⊆ ℕ0 ∧ 𝐼 ≠ ∅ ) ) → 𝐼 ∈ V )
30 simp3 ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → 𝑀 ∈ 𝐵 )
31 30 adantr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝐼 ⊆ ℕ0 ∧ 𝐼 ≠ ∅ ) ) → 𝑀 ∈ 𝐵 )
32 18 25 26 29 31 mpocurryvald ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝐼 ⊆ ℕ0 ∧ 𝐼 ≠ ∅ ) ) → ( curry ( 𝑥 ∈ 𝐵 , 𝑘 ∈ 𝐼 ↦ ( 𝑖 ∈ dom dom 𝑥 , 𝑗 ∈ dom dom 𝑥 ↦ ( ( coe1 ‘ ( 𝑖 𝑥 𝑗 ) ) ‘ 𝑘 ) ) ) ‘ 𝑀 ) = ( 𝑙 ∈ 𝐼 ↦ ⦋ 𝑀 / 𝑦 ⦌ ( 𝑖 ∈ dom dom 𝑦 , 𝑗 ∈ dom dom 𝑦 ↦ ( ( coe1 ‘ ( 𝑖 𝑦 𝑗 ) ) ‘ 𝑙 ) ) ) )
33 fveq2 ⊢ ( 𝑙 = 𝑘 → ( ( coe1 ‘ ( 𝑖 𝑦 𝑗 ) ) ‘ 𝑙 ) = ( ( coe1 ‘ ( 𝑖 𝑦 𝑗 ) ) ‘ 𝑘 ) )
34 33 mpoeq3dv ⊢ ( 𝑙 = 𝑘 → ( 𝑖 ∈ dom dom 𝑦 , 𝑗 ∈ dom dom 𝑦 ↦ ( ( coe1 ‘ ( 𝑖 𝑦 𝑗 ) ) ‘ 𝑙 ) ) = ( 𝑖 ∈ dom dom 𝑦 , 𝑗 ∈ dom dom 𝑦 ↦ ( ( coe1 ‘ ( 𝑖 𝑦 𝑗 ) ) ‘ 𝑘 ) ) )
35 34 csbeq2dv ⊢ ( 𝑙 = 𝑘 → ⦋ 𝑀 / 𝑦 ⦌ ( 𝑖 ∈ dom dom 𝑦 , 𝑗 ∈ dom dom 𝑦 ↦ ( ( coe1 ‘ ( 𝑖 𝑦 𝑗 ) ) ‘ 𝑙 ) ) = ⦋ 𝑀 / 𝑦 ⦌ ( 𝑖 ∈ dom dom 𝑦 , 𝑗 ∈ dom dom 𝑦 ↦ ( ( coe1 ‘ ( 𝑖 𝑦 𝑗 ) ) ‘ 𝑘 ) ) )
36 eqcom ⊢ ( 𝑥 = 𝑦 ↔ 𝑦 = 𝑥 )
37 eqcom ⊢ ( ( 𝑖 ∈ dom dom 𝑥 , 𝑗 ∈ dom dom 𝑥 ↦ ( ( coe1 ‘ ( 𝑖 𝑥 𝑗 ) ) ‘ 𝑘 ) ) = ( 𝑖 ∈ dom dom 𝑦 , 𝑗 ∈ dom dom 𝑦 ↦ ( ( coe1 ‘ ( 𝑖 𝑦 𝑗 ) ) ‘ 𝑘 ) ) ↔ ( 𝑖 ∈ dom dom 𝑦 , 𝑗 ∈ dom dom 𝑦 ↦ ( ( coe1 ‘ ( 𝑖 𝑦 𝑗 ) ) ‘ 𝑘 ) ) = ( 𝑖 ∈ dom dom 𝑥 , 𝑗 ∈ dom dom 𝑥 ↦ ( ( coe1 ‘ ( 𝑖 𝑥 𝑗 ) ) ‘ 𝑘 ) ) )
38 15 36 37 3imtr3i ⊢ ( 𝑦 = 𝑥 → ( 𝑖 ∈ dom dom 𝑦 , 𝑗 ∈ dom dom 𝑦 ↦ ( ( coe1 ‘ ( 𝑖 𝑦 𝑗 ) ) ‘ 𝑘 ) ) = ( 𝑖 ∈ dom dom 𝑥 , 𝑗 ∈ dom dom 𝑥 ↦ ( ( coe1 ‘ ( 𝑖 𝑥 𝑗 ) ) ‘ 𝑘 ) ) )
39 38 cbvcsbv ⊢ ⦋ 𝑀 / 𝑦 ⦌ ( 𝑖 ∈ dom dom 𝑦 , 𝑗 ∈ dom dom 𝑦 ↦ ( ( coe1 ‘ ( 𝑖 𝑦 𝑗 ) ) ‘ 𝑘 ) ) = ⦋ 𝑀 / 𝑥 ⦌ ( 𝑖 ∈ dom dom 𝑥 , 𝑗 ∈ dom dom 𝑥 ↦ ( ( coe1 ‘ ( 𝑖 𝑥 𝑗 ) ) ‘ 𝑘 ) )
40 35 39 eqtrdi ⊢ ( 𝑙 = 𝑘 → ⦋ 𝑀 / 𝑦 ⦌ ( 𝑖 ∈ dom dom 𝑦 , 𝑗 ∈ dom dom 𝑦 ↦ ( ( coe1 ‘ ( 𝑖 𝑦 𝑗 ) ) ‘ 𝑙 ) ) = ⦋ 𝑀 / 𝑥 ⦌ ( 𝑖 ∈ dom dom 𝑥 , 𝑗 ∈ dom dom 𝑥 ↦ ( ( coe1 ‘ ( 𝑖 𝑥 𝑗 ) ) ‘ 𝑘 ) ) )
41 40 cbvmptv ⊢ ( 𝑙 ∈ 𝐼 ↦ ⦋ 𝑀 / 𝑦 ⦌ ( 𝑖 ∈ dom dom 𝑦 , 𝑗 ∈ dom dom 𝑦 ↦ ( ( coe1 ‘ ( 𝑖 𝑦 𝑗 ) ) ‘ 𝑙 ) ) ) = ( 𝑘 ∈ 𝐼 ↦ ⦋ 𝑀 / 𝑥 ⦌ ( 𝑖 ∈ dom dom 𝑥 , 𝑗 ∈ dom dom 𝑥 ↦ ( ( coe1 ‘ ( 𝑖 𝑥 𝑗 ) ) ‘ 𝑘 ) ) )
42 32 41 eqtrdi ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝐼 ⊆ ℕ0 ∧ 𝐼 ≠ ∅ ) ) → ( curry ( 𝑥 ∈ 𝐵 , 𝑘 ∈ 𝐼 ↦ ( 𝑖 ∈ dom dom 𝑥 , 𝑗 ∈ dom dom 𝑥 ↦ ( ( coe1 ‘ ( 𝑖 𝑥 𝑗 ) ) ‘ 𝑘 ) ) ) ‘ 𝑀 ) = ( 𝑘 ∈ 𝐼 ↦ ⦋ 𝑀 / 𝑥 ⦌ ( 𝑖 ∈ dom dom 𝑥 , 𝑗 ∈ dom dom 𝑥 ↦ ( ( coe1 ‘ ( 𝑖 𝑥 𝑗 ) ) ‘ 𝑘 ) ) ) )
43 dmeq ⊢ ( 𝑥 = 𝑀 → dom 𝑥 = dom 𝑀 )
44 43 dmeqd ⊢ ( 𝑥 = 𝑀 → dom dom 𝑥 = dom dom 𝑀 )
45 oveq ⊢ ( 𝑥 = 𝑀 → ( 𝑖 𝑥 𝑗 ) = ( 𝑖 𝑀 𝑗 ) )
46 45 fveq2d ⊢ ( 𝑥 = 𝑀 → ( coe1 ‘ ( 𝑖 𝑥 𝑗 ) ) = ( coe1 ‘ ( 𝑖 𝑀 𝑗 ) ) )
47 46 fveq1d ⊢ ( 𝑥 = 𝑀 → ( ( coe1 ‘ ( 𝑖 𝑥 𝑗 ) ) ‘ 𝑘 ) = ( ( coe1 ‘ ( 𝑖 𝑀 𝑗 ) ) ‘ 𝑘 ) )
48 44 44 47 mpoeq123dv ⊢ ( 𝑥 = 𝑀 → ( 𝑖 ∈ dom dom 𝑥 , 𝑗 ∈ dom dom 𝑥 ↦ ( ( coe1 ‘ ( 𝑖 𝑥 𝑗 ) ) ‘ 𝑘 ) ) = ( 𝑖 ∈ dom dom 𝑀 , 𝑗 ∈ dom dom 𝑀 ↦ ( ( coe1 ‘ ( 𝑖 𝑀 𝑗 ) ) ‘ 𝑘 ) ) )
49 48 adantl ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑥 = 𝑀 ) → ( 𝑖 ∈ dom dom 𝑥 , 𝑗 ∈ dom dom 𝑥 ↦ ( ( coe1 ‘ ( 𝑖 𝑥 𝑗 ) ) ‘ 𝑘 ) ) = ( 𝑖 ∈ dom dom 𝑀 , 𝑗 ∈ dom dom 𝑀 ↦ ( ( coe1 ‘ ( 𝑖 𝑀 𝑗 ) ) ‘ 𝑘 ) ) )
50 30 49 csbied ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ⦋ 𝑀 / 𝑥 ⦌ ( 𝑖 ∈ dom dom 𝑥 , 𝑗 ∈ dom dom 𝑥 ↦ ( ( coe1 ‘ ( 𝑖 𝑥 𝑗 ) ) ‘ 𝑘 ) ) = ( 𝑖 ∈ dom dom 𝑀 , 𝑗 ∈ dom dom 𝑀 ↦ ( ( coe1 ‘ ( 𝑖 𝑀 𝑗 ) ) ‘ 𝑘 ) ) )
51 eqid ⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
52 2 51 3 matbas2i ⊢ ( 𝑀 ∈ 𝐵 → 𝑀 ∈ ( ( Base ‘ 𝑃 ) ↑m ( 𝑁 × 𝑁 ) ) )
53 elmapi ⊢ ( 𝑀 ∈ ( ( Base ‘ 𝑃 ) ↑m ( 𝑁 × 𝑁 ) ) → 𝑀 : ( 𝑁 × 𝑁 ) ⟶ ( Base ‘ 𝑃 ) )
54 fdm ⊢ ( 𝑀 : ( 𝑁 × 𝑁 ) ⟶ ( Base ‘ 𝑃 ) → dom 𝑀 = ( 𝑁 × 𝑁 ) )
55 54 dmeqd ⊢ ( 𝑀 : ( 𝑁 × 𝑁 ) ⟶ ( Base ‘ 𝑃 ) → dom dom 𝑀 = dom ( 𝑁 × 𝑁 ) )
56 dmxpid ⊢ dom ( 𝑁 × 𝑁 ) = 𝑁
57 55 56 eqtr2di ⊢ ( 𝑀 : ( 𝑁 × 𝑁 ) ⟶ ( Base ‘ 𝑃 ) → 𝑁 = dom dom 𝑀 )
58 52 53 57 3syl ⊢ ( 𝑀 ∈ 𝐵 → 𝑁 = dom dom 𝑀 )
59 58 3ad2ant3 ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → 𝑁 = dom dom 𝑀 )
60 59 adantr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑚 = 𝑀 ) → 𝑁 = dom dom 𝑀 )
61 simpr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑚 = 𝑀 ) → 𝑚 = 𝑀 )
62 61 oveqd ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑚 = 𝑀 ) → ( 𝑖 𝑚 𝑗 ) = ( 𝑖 𝑀 𝑗 ) )
63 62 fveq2d ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑚 = 𝑀 ) → ( coe1 ‘ ( 𝑖 𝑚 𝑗 ) ) = ( coe1 ‘ ( 𝑖 𝑀 𝑗 ) ) )
64 63 fveq1d ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑚 = 𝑀 ) → ( ( coe1 ‘ ( 𝑖 𝑚 𝑗 ) ) ‘ 𝑘 ) = ( ( coe1 ‘ ( 𝑖 𝑀 𝑗 ) ) ‘ 𝑘 ) )
65 60 60 64 mpoeq123dv ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑚 = 𝑀 ) → ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑚 𝑗 ) ) ‘ 𝑘 ) ) = ( 𝑖 ∈ dom dom 𝑀 , 𝑗 ∈ dom dom 𝑀 ↦ ( ( coe1 ‘ ( 𝑖 𝑀 𝑗 ) ) ‘ 𝑘 ) ) )
66 30 65 csbied ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ⦋ 𝑀 / 𝑚 ⦌ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑚 𝑗 ) ) ‘ 𝑘 ) ) = ( 𝑖 ∈ dom dom 𝑀 , 𝑗 ∈ dom dom 𝑀 ↦ ( ( coe1 ‘ ( 𝑖 𝑀 𝑗 ) ) ‘ 𝑘 ) ) )
67 50 66 eqtr4d ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ⦋ 𝑀 / 𝑥 ⦌ ( 𝑖 ∈ dom dom 𝑥 , 𝑗 ∈ dom dom 𝑥 ↦ ( ( coe1 ‘ ( 𝑖 𝑥 𝑗 ) ) ‘ 𝑘 ) ) = ⦋ 𝑀 / 𝑚 ⦌ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑚 𝑗 ) ) ‘ 𝑘 ) ) )
68 67 adantr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝐼 ⊆ ℕ0 ∧ 𝐼 ≠ ∅ ) ) → ⦋ 𝑀 / 𝑥 ⦌ ( 𝑖 ∈ dom dom 𝑥 , 𝑗 ∈ dom dom 𝑥 ↦ ( ( coe1 ‘ ( 𝑖 𝑥 𝑗 ) ) ‘ 𝑘 ) ) = ⦋ 𝑀 / 𝑚 ⦌ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑚 𝑗 ) ) ‘ 𝑘 ) ) )
69 68 mpteq2dv ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝐼 ⊆ ℕ0 ∧ 𝐼 ≠ ∅ ) ) → ( 𝑘 ∈ 𝐼 ↦ ⦋ 𝑀 / 𝑥 ⦌ ( 𝑖 ∈ dom dom 𝑥 , 𝑗 ∈ dom dom 𝑥 ↦ ( ( coe1 ‘ ( 𝑖 𝑥 𝑗 ) ) ‘ 𝑘 ) ) ) = ( 𝑘 ∈ 𝐼 ↦ ⦋ 𝑀 / 𝑚 ⦌ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑚 𝑗 ) ) ‘ 𝑘 ) ) ) )
70 42 69 eqtrd ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝐼 ⊆ ℕ0 ∧ 𝐼 ≠ ∅ ) ) → ( curry ( 𝑥 ∈ 𝐵 , 𝑘 ∈ 𝐼 ↦ ( 𝑖 ∈ dom dom 𝑥 , 𝑗 ∈ dom dom 𝑥 ↦ ( ( coe1 ‘ ( 𝑖 𝑥 𝑗 ) ) ‘ 𝑘 ) ) ) ‘ 𝑀 ) = ( 𝑘 ∈ 𝐼 ↦ ⦋ 𝑀 / 𝑚 ⦌ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑚 𝑗 ) ) ‘ 𝑘 ) ) ) )
71 oveq ⊢ ( 𝑚 = 𝑀 → ( 𝑖 𝑚 𝑗 ) = ( 𝑖 𝑀 𝑗 ) )
72 71 adantl ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑚 = 𝑀 ) → ( 𝑖 𝑚 𝑗 ) = ( 𝑖 𝑀 𝑗 ) )
73 72 fveq2d ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑚 = 𝑀 ) → ( coe1 ‘ ( 𝑖 𝑚 𝑗 ) ) = ( coe1 ‘ ( 𝑖 𝑀 𝑗 ) ) )
74 73 fveq1d ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑚 = 𝑀 ) → ( ( coe1 ‘ ( 𝑖 𝑚 𝑗 ) ) ‘ 𝑘 ) = ( ( coe1 ‘ ( 𝑖 𝑀 𝑗 ) ) ‘ 𝑘 ) )
75 74 mpoeq3dv ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑚 = 𝑀 ) → ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑚 𝑗 ) ) ‘ 𝑘 ) ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑀 𝑗 ) ) ‘ 𝑘 ) ) )
76 30 75 csbied ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ⦋ 𝑀 / 𝑚 ⦌ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑚 𝑗 ) ) ‘ 𝑘 ) ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑀 𝑗 ) ) ‘ 𝑘 ) ) )
77 76 ad2antrr ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝐼 ⊆ ℕ0 ∧ 𝐼 ≠ ∅ ) ) ∧ 𝑘 ∈ 𝐼 ) → ⦋ 𝑀 / 𝑚 ⦌ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑚 𝑗 ) ) ‘ 𝑘 ) ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑀 𝑗 ) ) ‘ 𝑘 ) ) )
78 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
79 simpll1 ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝐼 ⊆ ℕ0 ∧ 𝐼 ≠ ∅ ) ) ∧ 𝑘 ∈ 𝐼 ) → 𝑁 ∈ Fin )
80 simpll2 ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝐼 ⊆ ℕ0 ∧ 𝐼 ≠ ∅ ) ) ∧ 𝑘 ∈ 𝐼 ) → 𝑅 ∈ CRing )
81 simp2 ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝐼 ⊆ ℕ0 ∧ 𝐼 ≠ ∅ ) ) ∧ 𝑘 ∈ 𝐼 ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → 𝑖 ∈ 𝑁 )
82 simp3 ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝐼 ⊆ ℕ0 ∧ 𝐼 ≠ ∅ ) ) ∧ 𝑘 ∈ 𝐼 ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → 𝑗 ∈ 𝑁 )
83 31 adantr ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝐼 ⊆ ℕ0 ∧ 𝐼 ≠ ∅ ) ) ∧ 𝑘 ∈ 𝐼 ) → 𝑀 ∈ 𝐵 )
84 83 3ad2ant1 ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝐼 ⊆ ℕ0 ∧ 𝐼 ≠ ∅ ) ) ∧ 𝑘 ∈ 𝐼 ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → 𝑀 ∈ 𝐵 )
85 2 51 3 81 82 84 matecld ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝐼 ⊆ ℕ0 ∧ 𝐼 ≠ ∅ ) ) ∧ 𝑘 ∈ 𝐼 ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ( 𝑖 𝑀 𝑗 ) ∈ ( Base ‘ 𝑃 ) )
86 ssel ⊢ ( 𝐼 ⊆ ℕ0 → ( 𝑘 ∈ 𝐼 → 𝑘 ∈ ℕ0 ) )
87 86 ad2antrl ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝐼 ⊆ ℕ0 ∧ 𝐼 ≠ ∅ ) ) → ( 𝑘 ∈ 𝐼 → 𝑘 ∈ ℕ0 ) )
88 87 imp ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝐼 ⊆ ℕ0 ∧ 𝐼 ≠ ∅ ) ) ∧ 𝑘 ∈ 𝐼 ) → 𝑘 ∈ ℕ0 )
89 88 3ad2ant1 ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝐼 ⊆ ℕ0 ∧ 𝐼 ≠ ∅ ) ) ∧ 𝑘 ∈ 𝐼 ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → 𝑘 ∈ ℕ0 )
90 eqid ⊢ ( coe1 ‘ ( 𝑖 𝑀 𝑗 ) ) = ( coe1 ‘ ( 𝑖 𝑀 𝑗 ) )
91 90 51 1 78 coe1fvalcl ⊢ ( ( ( 𝑖 𝑀 𝑗 ) ∈ ( Base ‘ 𝑃 ) ∧ 𝑘 ∈ ℕ0 ) → ( ( coe1 ‘ ( 𝑖 𝑀 𝑗 ) ) ‘ 𝑘 ) ∈ ( Base ‘ 𝑅 ) )
92 85 89 91 syl2anc ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝐼 ⊆ ℕ0 ∧ 𝐼 ≠ ∅ ) ) ∧ 𝑘 ∈ 𝐼 ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ( ( coe1 ‘ ( 𝑖 𝑀 𝑗 ) ) ‘ 𝑘 ) ∈ ( Base ‘ 𝑅 ) )
93 8 78 9 79 80 92 matbas2d ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝐼 ⊆ ℕ0 ∧ 𝐼 ≠ ∅ ) ) ∧ 𝑘 ∈ 𝐼 ) → ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑀 𝑗 ) ) ‘ 𝑘 ) ) ∈ 𝐷 )
94 77 93 eqeltrd ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝐼 ⊆ ℕ0 ∧ 𝐼 ≠ ∅ ) ) ∧ 𝑘 ∈ 𝐼 ) → ⦋ 𝑀 / 𝑚 ⦌ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑚 𝑗 ) ) ‘ 𝑘 ) ) ∈ 𝐷 )
95 94 fmpttd ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝐼 ⊆ ℕ0 ∧ 𝐼 ≠ ∅ ) ) → ( 𝑘 ∈ 𝐼 ↦ ⦋ 𝑀 / 𝑚 ⦌ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑚 𝑗 ) ) ‘ 𝑘 ) ) ) : 𝐼 ⟶ 𝐷 )
96 9 fvexi ⊢ 𝐷 ∈ V
97 96 a1i ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → 𝐷 ∈ V )
98 28 adantr ⊢ ( ( 𝐼 ⊆ ℕ0 ∧ 𝐼 ≠ ∅ ) → 𝐼 ∈ V )
99 elmapg ⊢ ( ( 𝐷 ∈ V ∧ 𝐼 ∈ V ) → ( ( 𝑘 ∈ 𝐼 ↦ ⦋ 𝑀 / 𝑚 ⦌ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑚 𝑗 ) ) ‘ 𝑘 ) ) ) ∈ ( 𝐷 ↑m 𝐼 ) ↔ ( 𝑘 ∈ 𝐼 ↦ ⦋ 𝑀 / 𝑚 ⦌ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑚 𝑗 ) ) ‘ 𝑘 ) ) ) : 𝐼 ⟶ 𝐷 ) )
100 97 98 99 syl2an ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝐼 ⊆ ℕ0 ∧ 𝐼 ≠ ∅ ) ) → ( ( 𝑘 ∈ 𝐼 ↦ ⦋ 𝑀 / 𝑚 ⦌ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑚 𝑗 ) ) ‘ 𝑘 ) ) ) ∈ ( 𝐷 ↑m 𝐼 ) ↔ ( 𝑘 ∈ 𝐼 ↦ ⦋ 𝑀 / 𝑚 ⦌ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑚 𝑗 ) ) ‘ 𝑘 ) ) ) : 𝐼 ⟶ 𝐷 ) )
101 95 100 mpbird ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝐼 ⊆ ℕ0 ∧ 𝐼 ≠ ∅ ) ) → ( 𝑘 ∈ 𝐼 ↦ ⦋ 𝑀 / 𝑚 ⦌ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( coe1 ‘ ( 𝑖 𝑚 𝑗 ) ) ‘ 𝑘 ) ) ) ∈ ( 𝐷 ↑m 𝐼 ) )
102 70 101 eqeltrd ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝐼 ⊆ ℕ0 ∧ 𝐼 ≠ ∅ ) ) → ( curry ( 𝑥 ∈ 𝐵 , 𝑘 ∈ 𝐼 ↦ ( 𝑖 ∈ dom dom 𝑥 , 𝑗 ∈ dom dom 𝑥 ↦ ( ( coe1 ‘ ( 𝑖 𝑥 𝑗 ) ) ‘ 𝑘 ) ) ) ‘ 𝑀 ) ∈ ( 𝐷 ↑m 𝐼 ) )
103 fveq1 ⊢ ( 𝑓 = ( curry ( 𝑥 ∈ 𝐵 , 𝑘 ∈ 𝐼 ↦ ( 𝑖 ∈ dom dom 𝑥 , 𝑗 ∈ dom dom 𝑥 ↦ ( ( coe1 ‘ ( 𝑖 𝑥 𝑗 ) ) ‘ 𝑘 ) ) ) ‘ 𝑀 ) → ( 𝑓 ‘ 𝑛 ) = ( ( curry ( 𝑥 ∈ 𝐵 , 𝑘 ∈ 𝐼 ↦ ( 𝑖 ∈ dom dom 𝑥 , 𝑗 ∈ dom dom 𝑥 ↦ ( ( coe1 ‘ ( 𝑖 𝑥 𝑗 ) ) ‘ 𝑘 ) ) ) ‘ 𝑀 ) ‘ 𝑛 ) )
104 103 adantl ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝐼 ⊆ ℕ0 ∧ 𝐼 ≠ ∅ ) ) ∧ 𝑓 = ( curry ( 𝑥 ∈ 𝐵 , 𝑘 ∈ 𝐼 ↦ ( 𝑖 ∈ dom dom 𝑥 , 𝑗 ∈ dom dom 𝑥 ↦ ( ( coe1 ‘ ( 𝑖 𝑥 𝑗 ) ) ‘ 𝑘 ) ) ) ‘ 𝑀 ) ) → ( 𝑓 ‘ 𝑛 ) = ( ( curry ( 𝑥 ∈ 𝐵 , 𝑘 ∈ 𝐼 ↦ ( 𝑖 ∈ dom dom 𝑥 , 𝑗 ∈ dom dom 𝑥 ↦ ( ( coe1 ‘ ( 𝑖 𝑥 𝑗 ) ) ‘ 𝑘 ) ) ) ‘ 𝑀 ) ‘ 𝑛 ) )
105 104 adantr ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝐼 ⊆ ℕ0 ∧ 𝐼 ≠ ∅ ) ) ∧ 𝑓 = ( curry ( 𝑥 ∈ 𝐵 , 𝑘 ∈ 𝐼 ↦ ( 𝑖 ∈ dom dom 𝑥 , 𝑗 ∈ dom dom 𝑥 ↦ ( ( coe1 ‘ ( 𝑖 𝑥 𝑗 ) ) ‘ 𝑘 ) ) ) ‘ 𝑀 ) ) ∧ 𝑛 ∈ 𝐼 ) → ( 𝑓 ‘ 𝑛 ) = ( ( curry ( 𝑥 ∈ 𝐵 , 𝑘 ∈ 𝐼 ↦ ( 𝑖 ∈ dom dom 𝑥 , 𝑗 ∈ dom dom 𝑥 ↦ ( ( coe1 ‘ ( 𝑖 𝑥 𝑗 ) ) ‘ 𝑘 ) ) ) ‘ 𝑀 ) ‘ 𝑛 ) )
106 eqid ⊢ ( 𝑥 ∈ 𝐵 , 𝑘 ∈ 𝐼 ↦ ( 𝑖 ∈ dom dom 𝑥 , 𝑗 ∈ dom dom 𝑥 ↦ ( ( coe1 ‘ ( 𝑖 𝑥 𝑗 ) ) ‘ 𝑘 ) ) ) = ( 𝑥 ∈ 𝐵 , 𝑘 ∈ 𝐼 ↦ ( 𝑖 ∈ dom dom 𝑥 , 𝑗 ∈ dom dom 𝑥 ↦ ( ( coe1 ‘ ( 𝑖 𝑥 𝑗 ) ) ‘ 𝑘 ) ) )
107 dmexg ⊢ ( 𝑥 ∈ 𝐵 → dom 𝑥 ∈ V )
108 107 dmexd ⊢ ( 𝑥 ∈ 𝐵 → dom dom 𝑥 ∈ V )
109 108 108 jca ⊢ ( 𝑥 ∈ 𝐵 → ( dom dom 𝑥 ∈ V ∧ dom dom 𝑥 ∈ V ) )
110 109 ad2antrl ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝐼 ⊆ ℕ0 ∧ 𝐼 ≠ ∅ ) ) ∧ 𝑛 ∈ 𝐼 ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑘 ∈ 𝐼 ) ) → ( dom dom 𝑥 ∈ V ∧ dom dom 𝑥 ∈ V ) )
111 mpoexga ⊢ ( ( dom dom 𝑥 ∈ V ∧ dom dom 𝑥 ∈ V ) → ( 𝑖 ∈ dom dom 𝑥 , 𝑗 ∈ dom dom 𝑥 ↦ ( ( coe1 ‘ ( 𝑖 𝑥 𝑗 ) ) ‘ 𝑘 ) ) ∈ V )
112 110 111 syl ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝐼 ⊆ ℕ0 ∧ 𝐼 ≠ ∅ ) ) ∧ 𝑛 ∈ 𝐼 ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑘 ∈ 𝐼 ) ) → ( 𝑖 ∈ dom dom 𝑥 , 𝑗 ∈ dom dom 𝑥 ↦ ( ( coe1 ‘ ( 𝑖 𝑥 𝑗 ) ) ‘ 𝑘 ) ) ∈ V )
113 112 ralrimivva ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝐼 ⊆ ℕ0 ∧ 𝐼 ≠ ∅ ) ) ∧ 𝑛 ∈ 𝐼 ) → ∀ 𝑥 ∈ 𝐵 ∀ 𝑘 ∈ 𝐼 ( 𝑖 ∈ dom dom 𝑥 , 𝑗 ∈ dom dom 𝑥 ↦ ( ( coe1 ‘ ( 𝑖 𝑥 𝑗 ) ) ‘ 𝑘 ) ) ∈ V )
114 29 adantr ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝐼 ⊆ ℕ0 ∧ 𝐼 ≠ ∅ ) ) ∧ 𝑛 ∈ 𝐼 ) → 𝐼 ∈ V )
115 31 adantr ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝐼 ⊆ ℕ0 ∧ 𝐼 ≠ ∅ ) ) ∧ 𝑛 ∈ 𝐼 ) → 𝑀 ∈ 𝐵 )
116 simpr ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝐼 ⊆ ℕ0 ∧ 𝐼 ≠ ∅ ) ) ∧ 𝑛 ∈ 𝐼 ) → 𝑛 ∈ 𝐼 )
117 106 113 114 115 116 fvmpocurryd ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝐼 ⊆ ℕ0 ∧ 𝐼 ≠ ∅ ) ) ∧ 𝑛 ∈ 𝐼 ) → ( ( curry ( 𝑥 ∈ 𝐵 , 𝑘 ∈ 𝐼 ↦ ( 𝑖 ∈ dom dom 𝑥 , 𝑗 ∈ dom dom 𝑥 ↦ ( ( coe1 ‘ ( 𝑖 𝑥 𝑗 ) ) ‘ 𝑘 ) ) ) ‘ 𝑀 ) ‘ 𝑛 ) = ( 𝑀 ( 𝑥 ∈ 𝐵 , 𝑘 ∈ 𝐼 ↦ ( 𝑖 ∈ dom dom 𝑥 , 𝑗 ∈ dom dom 𝑥 ↦ ( ( coe1 ‘ ( 𝑖 𝑥 𝑗 ) ) ‘ 𝑘 ) ) ) 𝑛 ) )
118 df-decpmat ⊢ decompPMat = ( 𝑥 ∈ V , 𝑘 ∈ ℕ0 ↦ ( 𝑖 ∈ dom dom 𝑥 , 𝑗 ∈ dom dom 𝑥 ↦ ( ( coe1 ‘ ( 𝑖 𝑥 𝑗 ) ) ‘ 𝑘 ) ) )
119 118 reseq1i ⊢ ( decompPMat ↾ ( 𝐵 × 𝐼 ) ) = ( ( 𝑥 ∈ V , 𝑘 ∈ ℕ0 ↦ ( 𝑖 ∈ dom dom 𝑥 , 𝑗 ∈ dom dom 𝑥 ↦ ( ( coe1 ‘ ( 𝑖 𝑥 𝑗 ) ) ‘ 𝑘 ) ) ) ↾ ( 𝐵 × 𝐼 ) )
120 ssv ⊢ 𝐵 ⊆ V
121 120 a1i ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → 𝐵 ⊆ V )
122 simpl ⊢ ( ( 𝐼 ⊆ ℕ0 ∧ 𝐼 ≠ ∅ ) → 𝐼 ⊆ ℕ0 )
123 121 122 anim12i ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝐼 ⊆ ℕ0 ∧ 𝐼 ≠ ∅ ) ) → ( 𝐵 ⊆ V ∧ 𝐼 ⊆ ℕ0 ) )
124 123 adantr ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝐼 ⊆ ℕ0 ∧ 𝐼 ≠ ∅ ) ) ∧ 𝑛 ∈ 𝐼 ) → ( 𝐵 ⊆ V ∧ 𝐼 ⊆ ℕ0 ) )
125 resmpo ⊢ ( ( 𝐵 ⊆ V ∧ 𝐼 ⊆ ℕ0 ) → ( ( 𝑥 ∈ V , 𝑘 ∈ ℕ0 ↦ ( 𝑖 ∈ dom dom 𝑥 , 𝑗 ∈ dom dom 𝑥 ↦ ( ( coe1 ‘ ( 𝑖 𝑥 𝑗 ) ) ‘ 𝑘 ) ) ) ↾ ( 𝐵 × 𝐼 ) ) = ( 𝑥 ∈ 𝐵 , 𝑘 ∈ 𝐼 ↦ ( 𝑖 ∈ dom dom 𝑥 , 𝑗 ∈ dom dom 𝑥 ↦ ( ( coe1 ‘ ( 𝑖 𝑥 𝑗 ) ) ‘ 𝑘 ) ) ) )
126 124 125 syl ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝐼 ⊆ ℕ0 ∧ 𝐼 ≠ ∅ ) ) ∧ 𝑛 ∈ 𝐼 ) → ( ( 𝑥 ∈ V , 𝑘 ∈ ℕ0 ↦ ( 𝑖 ∈ dom dom 𝑥 , 𝑗 ∈ dom dom 𝑥 ↦ ( ( coe1 ‘ ( 𝑖 𝑥 𝑗 ) ) ‘ 𝑘 ) ) ) ↾ ( 𝐵 × 𝐼 ) ) = ( 𝑥 ∈ 𝐵 , 𝑘 ∈ 𝐼 ↦ ( 𝑖 ∈ dom dom 𝑥 , 𝑗 ∈ dom dom 𝑥 ↦ ( ( coe1 ‘ ( 𝑖 𝑥 𝑗 ) ) ‘ 𝑘 ) ) ) )
127 119 126 eqtr2id ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝐼 ⊆ ℕ0 ∧ 𝐼 ≠ ∅ ) ) ∧ 𝑛 ∈ 𝐼 ) → ( 𝑥 ∈ 𝐵 , 𝑘 ∈ 𝐼 ↦ ( 𝑖 ∈ dom dom 𝑥 , 𝑗 ∈ dom dom 𝑥 ↦ ( ( coe1 ‘ ( 𝑖 𝑥 𝑗 ) ) ‘ 𝑘 ) ) ) = ( decompPMat ↾ ( 𝐵 × 𝐼 ) ) )
128 127 oveqd ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝐼 ⊆ ℕ0 ∧ 𝐼 ≠ ∅ ) ) ∧ 𝑛 ∈ 𝐼 ) → ( 𝑀 ( 𝑥 ∈ 𝐵 , 𝑘 ∈ 𝐼 ↦ ( 𝑖 ∈ dom dom 𝑥 , 𝑗 ∈ dom dom 𝑥 ↦ ( ( coe1 ‘ ( 𝑖 𝑥 𝑗 ) ) ‘ 𝑘 ) ) ) 𝑛 ) = ( 𝑀 ( decompPMat ↾ ( 𝐵 × 𝐼 ) ) 𝑛 ) )
129 117 128 eqtrd ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝐼 ⊆ ℕ0 ∧ 𝐼 ≠ ∅ ) ) ∧ 𝑛 ∈ 𝐼 ) → ( ( curry ( 𝑥 ∈ 𝐵 , 𝑘 ∈ 𝐼 ↦ ( 𝑖 ∈ dom dom 𝑥 , 𝑗 ∈ dom dom 𝑥 ↦ ( ( coe1 ‘ ( 𝑖 𝑥 𝑗 ) ) ‘ 𝑘 ) ) ) ‘ 𝑀 ) ‘ 𝑛 ) = ( 𝑀 ( decompPMat ↾ ( 𝐵 × 𝐼 ) ) 𝑛 ) )
130 129 adantlr ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝐼 ⊆ ℕ0 ∧ 𝐼 ≠ ∅ ) ) ∧ 𝑓 = ( curry ( 𝑥 ∈ 𝐵 , 𝑘 ∈ 𝐼 ↦ ( 𝑖 ∈ dom dom 𝑥 , 𝑗 ∈ dom dom 𝑥 ↦ ( ( coe1 ‘ ( 𝑖 𝑥 𝑗 ) ) ‘ 𝑘 ) ) ) ‘ 𝑀 ) ) ∧ 𝑛 ∈ 𝐼 ) → ( ( curry ( 𝑥 ∈ 𝐵 , 𝑘 ∈ 𝐼 ↦ ( 𝑖 ∈ dom dom 𝑥 , 𝑗 ∈ dom dom 𝑥 ↦ ( ( coe1 ‘ ( 𝑖 𝑥 𝑗 ) ) ‘ 𝑘 ) ) ) ‘ 𝑀 ) ‘ 𝑛 ) = ( 𝑀 ( decompPMat ↾ ( 𝐵 × 𝐼 ) ) 𝑛 ) )
131 105 130 eqtrd ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝐼 ⊆ ℕ0 ∧ 𝐼 ≠ ∅ ) ) ∧ 𝑓 = ( curry ( 𝑥 ∈ 𝐵 , 𝑘 ∈ 𝐼 ↦ ( 𝑖 ∈ dom dom 𝑥 , 𝑗 ∈ dom dom 𝑥 ↦ ( ( coe1 ‘ ( 𝑖 𝑥 𝑗 ) ) ‘ 𝑘 ) ) ) ‘ 𝑀 ) ) ∧ 𝑛 ∈ 𝐼 ) → ( 𝑓 ‘ 𝑛 ) = ( 𝑀 ( decompPMat ↾ ( 𝐵 × 𝐼 ) ) 𝑛 ) )
132 131 fveq2d ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝐼 ⊆ ℕ0 ∧ 𝐼 ≠ ∅ ) ) ∧ 𝑓 = ( curry ( 𝑥 ∈ 𝐵 , 𝑘 ∈ 𝐼 ↦ ( 𝑖 ∈ dom dom 𝑥 , 𝑗 ∈ dom dom 𝑥 ↦ ( ( coe1 ‘ ( 𝑖 𝑥 𝑗 ) ) ‘ 𝑘 ) ) ) ‘ 𝑀 ) ) ∧ 𝑛 ∈ 𝐼 ) → ( 𝑇 ‘ ( 𝑓 ‘ 𝑛 ) ) = ( 𝑇 ‘ ( 𝑀 ( decompPMat ↾ ( 𝐵 × 𝐼 ) ) 𝑛 ) ) )
133 30 ad2antrr ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝐼 ⊆ ℕ0 ∧ 𝐼 ≠ ∅ ) ) ∧ 𝑓 = ( curry ( 𝑥 ∈ 𝐵 , 𝑘 ∈ 𝐼 ↦ ( 𝑖 ∈ dom dom 𝑥 , 𝑗 ∈ dom dom 𝑥 ↦ ( ( coe1 ‘ ( 𝑖 𝑥 𝑗 ) ) ‘ 𝑘 ) ) ) ‘ 𝑀 ) ) → 𝑀 ∈ 𝐵 )
134 ovres ⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝑛 ∈ 𝐼 ) → ( 𝑀 ( decompPMat ↾ ( 𝐵 × 𝐼 ) ) 𝑛 ) = ( 𝑀 decompPMat 𝑛 ) )
135 133 134 sylan ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝐼 ⊆ ℕ0 ∧ 𝐼 ≠ ∅ ) ) ∧ 𝑓 = ( curry ( 𝑥 ∈ 𝐵 , 𝑘 ∈ 𝐼 ↦ ( 𝑖 ∈ dom dom 𝑥 , 𝑗 ∈ dom dom 𝑥 ↦ ( ( coe1 ‘ ( 𝑖 𝑥 𝑗 ) ) ‘ 𝑘 ) ) ) ‘ 𝑀 ) ) ∧ 𝑛 ∈ 𝐼 ) → ( 𝑀 ( decompPMat ↾ ( 𝐵 × 𝐼 ) ) 𝑛 ) = ( 𝑀 decompPMat 𝑛 ) )
136 135 fveq2d ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝐼 ⊆ ℕ0 ∧ 𝐼 ≠ ∅ ) ) ∧ 𝑓 = ( curry ( 𝑥 ∈ 𝐵 , 𝑘 ∈ 𝐼 ↦ ( 𝑖 ∈ dom dom 𝑥 , 𝑗 ∈ dom dom 𝑥 ↦ ( ( coe1 ‘ ( 𝑖 𝑥 𝑗 ) ) ‘ 𝑘 ) ) ) ‘ 𝑀 ) ) ∧ 𝑛 ∈ 𝐼 ) → ( 𝑇 ‘ ( 𝑀 ( decompPMat ↾ ( 𝐵 × 𝐼 ) ) 𝑛 ) ) = ( 𝑇 ‘ ( 𝑀 decompPMat 𝑛 ) ) )
137 132 136 eqtrd ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝐼 ⊆ ℕ0 ∧ 𝐼 ≠ ∅ ) ) ∧ 𝑓 = ( curry ( 𝑥 ∈ 𝐵 , 𝑘 ∈ 𝐼 ↦ ( 𝑖 ∈ dom dom 𝑥 , 𝑗 ∈ dom dom 𝑥 ↦ ( ( coe1 ‘ ( 𝑖 𝑥 𝑗 ) ) ‘ 𝑘 ) ) ) ‘ 𝑀 ) ) ∧ 𝑛 ∈ 𝐼 ) → ( 𝑇 ‘ ( 𝑓 ‘ 𝑛 ) ) = ( 𝑇 ‘ ( 𝑀 decompPMat 𝑛 ) ) )
138 137 oveq2d ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝐼 ⊆ ℕ0 ∧ 𝐼 ≠ ∅ ) ) ∧ 𝑓 = ( curry ( 𝑥 ∈ 𝐵 , 𝑘 ∈ 𝐼 ↦ ( 𝑖 ∈ dom dom 𝑥 , 𝑗 ∈ dom dom 𝑥 ↦ ( ( coe1 ‘ ( 𝑖 𝑥 𝑗 ) ) ‘ 𝑘 ) ) ) ‘ 𝑀 ) ) ∧ 𝑛 ∈ 𝐼 ) → ( ( 𝑛 ↑ 𝑋 ) ∗ ( 𝑇 ‘ ( 𝑓 ‘ 𝑛 ) ) ) = ( ( 𝑛 ↑ 𝑋 ) ∗ ( 𝑇 ‘ ( 𝑀 decompPMat 𝑛 ) ) ) )
139 138 mpteq2dva ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝐼 ⊆ ℕ0 ∧ 𝐼 ≠ ∅ ) ) ∧ 𝑓 = ( curry ( 𝑥 ∈ 𝐵 , 𝑘 ∈ 𝐼 ↦ ( 𝑖 ∈ dom dom 𝑥 , 𝑗 ∈ dom dom 𝑥 ↦ ( ( coe1 ‘ ( 𝑖 𝑥 𝑗 ) ) ‘ 𝑘 ) ) ) ‘ 𝑀 ) ) → ( 𝑛 ∈ 𝐼 ↦ ( ( 𝑛 ↑ 𝑋 ) ∗ ( 𝑇 ‘ ( 𝑓 ‘ 𝑛 ) ) ) ) = ( 𝑛 ∈ 𝐼 ↦ ( ( 𝑛 ↑ 𝑋 ) ∗ ( 𝑇 ‘ ( 𝑀 decompPMat 𝑛 ) ) ) ) )
140 139 oveq2d ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝐼 ⊆ ℕ0 ∧ 𝐼 ≠ ∅ ) ) ∧ 𝑓 = ( curry ( 𝑥 ∈ 𝐵 , 𝑘 ∈ 𝐼 ↦ ( 𝑖 ∈ dom dom 𝑥 , 𝑗 ∈ dom dom 𝑥 ↦ ( ( coe1 ‘ ( 𝑖 𝑥 𝑗 ) ) ‘ 𝑘 ) ) ) ‘ 𝑀 ) ) → ( 𝐶 Σg ( 𝑛 ∈ 𝐼 ↦ ( ( 𝑛 ↑ 𝑋 ) ∗ ( 𝑇 ‘ ( 𝑓 ‘ 𝑛 ) ) ) ) ) = ( 𝐶 Σg ( 𝑛 ∈ 𝐼 ↦ ( ( 𝑛 ↑ 𝑋 ) ∗ ( 𝑇 ‘ ( 𝑀 decompPMat 𝑛 ) ) ) ) ) )
141 140 eqeq2d ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝐼 ⊆ ℕ0 ∧ 𝐼 ≠ ∅ ) ) ∧ 𝑓 = ( curry ( 𝑥 ∈ 𝐵 , 𝑘 ∈ 𝐼 ↦ ( 𝑖 ∈ dom dom 𝑥 , 𝑗 ∈ dom dom 𝑥 ↦ ( ( coe1 ‘ ( 𝑖 𝑥 𝑗 ) ) ‘ 𝑘 ) ) ) ‘ 𝑀 ) ) → ( 𝑀 = ( 𝐶 Σg ( 𝑛 ∈ 𝐼 ↦ ( ( 𝑛 ↑ 𝑋 ) ∗ ( 𝑇 ‘ ( 𝑓 ‘ 𝑛 ) ) ) ) ) ↔ 𝑀 = ( 𝐶 Σg ( 𝑛 ∈ 𝐼 ↦ ( ( 𝑛 ↑ 𝑋 ) ∗ ( 𝑇 ‘ ( 𝑀 decompPMat 𝑛 ) ) ) ) ) ) )
142 102 141 rspcedv ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝐼 ⊆ ℕ0 ∧ 𝐼 ≠ ∅ ) ) → ( 𝑀 = ( 𝐶 Σg ( 𝑛 ∈ 𝐼 ↦ ( ( 𝑛 ↑ 𝑋 ) ∗ ( 𝑇 ‘ ( 𝑀 decompPMat 𝑛 ) ) ) ) ) → ∃ 𝑓 ∈ ( 𝐷 ↑m 𝐼 ) 𝑀 = ( 𝐶 Σg ( 𝑛 ∈ 𝐼 ↦ ( ( 𝑛 ↑ 𝑋 ) ∗ ( 𝑇 ‘ ( 𝑓 ‘ 𝑛 ) ) ) ) ) ) )