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 ( 𝑛 ∈ 𝐼 ↦ ( ( 𝑛 ↑ 𝑋 ) ∗ ( 𝑇 ‘ ( 𝑓 ‘ 𝑛 ) ) ) ) ) ) )