matgsum

Description: Finite commutative sums in a matrix algebra are taken componentwise. (Contributed by AV, 26-Sep-2019)

	Ref	Expression
Hypotheses	matgsum.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
	matgsum.b	⊢ 𝐵 = ( Base ‘ 𝐴 )
	matgsum.z	⊢ 0 = ( 0_g ‘ 𝐴 )
	matgsum.i	⊢ ( 𝜑 → 𝑁 ∈ Fin )
	matgsum.j	⊢ ( 𝜑 → 𝐽 ∈ 𝑊 )
	matgsum.r	⊢ ( 𝜑 → 𝑅 ∈ Ring )
	matgsum.f	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐽 ) → ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ 𝑈 ) ∈ 𝐵 )
	matgsum.w	⊢ ( 𝜑 → ( 𝑦 ∈ 𝐽 ↦ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ 𝑈 ) ) finSupp 0 )
Assertion	matgsum	⊢ ( 𝜑 → ( 𝐴 Σ_g ( 𝑦 ∈ 𝐽 ↦ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ 𝑈 ) ) ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 𝑅 Σ_g ( 𝑦 ∈ 𝐽 ↦ 𝑈 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		matgsum.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
2		matgsum.b	⊢ 𝐵 = ( Base ‘ 𝐴 )
3		matgsum.z	⊢ 0 = ( 0_g ‘ 𝐴 )
4		matgsum.i	⊢ ( 𝜑 → 𝑁 ∈ Fin )
5		matgsum.j	⊢ ( 𝜑 → 𝐽 ∈ 𝑊 )
6		matgsum.r	⊢ ( 𝜑 → 𝑅 ∈ Ring )
7		matgsum.f	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐽 ) → ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ 𝑈 ) ∈ 𝐵 )
8		matgsum.w	⊢ ( 𝜑 → ( 𝑦 ∈ 𝐽 ↦ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ 𝑈 ) ) finSupp 0 )
9	5	mptexd	⊢ ( 𝜑 → ( 𝑦 ∈ 𝐽 ↦ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ 𝑈 ) ) ∈ V )
10	1	ovexi	⊢ 𝐴 ∈ V
11	10	a1i	⊢ ( 𝜑 → 𝐴 ∈ V )
12		ovexd	⊢ ( 𝜑 → ( 𝑅 freeLMod ( 𝑁 × 𝑁 ) ) ∈ V )
13		eqid	⊢ ( 𝑅 freeLMod ( 𝑁 × 𝑁 ) ) = ( 𝑅 freeLMod ( 𝑁 × 𝑁 ) )
14	1 13	matbas	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( Base ‘ ( 𝑅 freeLMod ( 𝑁 × 𝑁 ) ) ) = ( Base ‘ 𝐴 ) )
15	4 6 14	syl2anc	⊢ ( 𝜑 → ( Base ‘ ( 𝑅 freeLMod ( 𝑁 × 𝑁 ) ) ) = ( Base ‘ 𝐴 ) )
16	15	eqcomd	⊢ ( 𝜑 → ( Base ‘ 𝐴 ) = ( Base ‘ ( 𝑅 freeLMod ( 𝑁 × 𝑁 ) ) ) )
17	1 13	matplusg	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( +_g ‘ ( 𝑅 freeLMod ( 𝑁 × 𝑁 ) ) ) = ( +_g ‘ 𝐴 ) )
18	4 6 17	syl2anc	⊢ ( 𝜑 → ( +_g ‘ ( 𝑅 freeLMod ( 𝑁 × 𝑁 ) ) ) = ( +_g ‘ 𝐴 ) )
19	18	eqcomd	⊢ ( 𝜑 → ( +_g ‘ 𝐴 ) = ( +_g ‘ ( 𝑅 freeLMod ( 𝑁 × 𝑁 ) ) ) )
20	9 11 12 16 19	gsumpropd	⊢ ( 𝜑 → ( 𝐴 Σ_g ( 𝑦 ∈ 𝐽 ↦ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ 𝑈 ) ) ) = ( ( 𝑅 freeLMod ( 𝑁 × 𝑁 ) ) Σ_g ( 𝑦 ∈ 𝐽 ↦ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ 𝑈 ) ) ) )
21		mpompts	⊢ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ 𝑈 ) = ( 𝑧 ∈ ( 𝑁 × 𝑁 ) ↦ ⦋ ( 1^st ‘ 𝑧 ) / 𝑖 ⦌ ⦋ ( 2^nd ‘ 𝑧 ) / 𝑗 ⦌ 𝑈 )
22	21	a1i	⊢ ( 𝜑 → ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ 𝑈 ) = ( 𝑧 ∈ ( 𝑁 × 𝑁 ) ↦ ⦋ ( 1^st ‘ 𝑧 ) / 𝑖 ⦌ ⦋ ( 2^nd ‘ 𝑧 ) / 𝑗 ⦌ 𝑈 ) )
23	22	mpteq2dv	⊢ ( 𝜑 → ( 𝑦 ∈ 𝐽 ↦ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ 𝑈 ) ) = ( 𝑦 ∈ 𝐽 ↦ ( 𝑧 ∈ ( 𝑁 × 𝑁 ) ↦ ⦋ ( 1^st ‘ 𝑧 ) / 𝑖 ⦌ ⦋ ( 2^nd ‘ 𝑧 ) / 𝑗 ⦌ 𝑈 ) ) )
24	23	oveq2d	⊢ ( 𝜑 → ( ( 𝑅 freeLMod ( 𝑁 × 𝑁 ) ) Σ_g ( 𝑦 ∈ 𝐽 ↦ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ 𝑈 ) ) ) = ( ( 𝑅 freeLMod ( 𝑁 × 𝑁 ) ) Σ_g ( 𝑦 ∈ 𝐽 ↦ ( 𝑧 ∈ ( 𝑁 × 𝑁 ) ↦ ⦋ ( 1^st ‘ 𝑧 ) / 𝑖 ⦌ ⦋ ( 2^nd ‘ 𝑧 ) / 𝑗 ⦌ 𝑈 ) ) ) )
25		eqid	⊢ ( Base ‘ ( 𝑅 freeLMod ( 𝑁 × 𝑁 ) ) ) = ( Base ‘ ( 𝑅 freeLMod ( 𝑁 × 𝑁 ) ) )
26		eqid	⊢ ( 0_g ‘ ( 𝑅 freeLMod ( 𝑁 × 𝑁 ) ) ) = ( 0_g ‘ ( 𝑅 freeLMod ( 𝑁 × 𝑁 ) ) )
27		xpfi	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑁 ∈ Fin ) → ( 𝑁 × 𝑁 ) ∈ Fin )
28	4 4 27	syl2anc	⊢ ( 𝜑 → ( 𝑁 × 𝑁 ) ∈ Fin )
29	7 2	eleqtrdi	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐽 ) → ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ 𝑈 ) ∈ ( Base ‘ 𝐴 ) )
30	21	eqcomi	⊢ ( 𝑧 ∈ ( 𝑁 × 𝑁 ) ↦ ⦋ ( 1^st ‘ 𝑧 ) / 𝑖 ⦌ ⦋ ( 2^nd ‘ 𝑧 ) / 𝑗 ⦌ 𝑈 ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ 𝑈 )
31	30	a1i	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐽 ) → ( 𝑧 ∈ ( 𝑁 × 𝑁 ) ↦ ⦋ ( 1^st ‘ 𝑧 ) / 𝑖 ⦌ ⦋ ( 2^nd ‘ 𝑧 ) / 𝑗 ⦌ 𝑈 ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ 𝑈 ) )
32	4 6	jca	⊢ ( 𝜑 → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) )
33	32	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐽 ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) )
34	33 14	syl	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐽 ) → ( Base ‘ ( 𝑅 freeLMod ( 𝑁 × 𝑁 ) ) ) = ( Base ‘ 𝐴 ) )
35	29 31 34	3eltr4d	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐽 ) → ( 𝑧 ∈ ( 𝑁 × 𝑁 ) ↦ ⦋ ( 1^st ‘ 𝑧 ) / 𝑖 ⦌ ⦋ ( 2^nd ‘ 𝑧 ) / 𝑗 ⦌ 𝑈 ) ∈ ( Base ‘ ( 𝑅 freeLMod ( 𝑁 × 𝑁 ) ) ) )
36	30	mpteq2i	⊢ ( 𝑦 ∈ 𝐽 ↦ ( 𝑧 ∈ ( 𝑁 × 𝑁 ) ↦ ⦋ ( 1^st ‘ 𝑧 ) / 𝑖 ⦌ ⦋ ( 2^nd ‘ 𝑧 ) / 𝑗 ⦌ 𝑈 ) ) = ( 𝑦 ∈ 𝐽 ↦ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ 𝑈 ) )
37	3	eqcomi	⊢ ( 0_g ‘ 𝐴 ) = 0
38	8 36 37	3brtr4g	⊢ ( 𝜑 → ( 𝑦 ∈ 𝐽 ↦ ( 𝑧 ∈ ( 𝑁 × 𝑁 ) ↦ ⦋ ( 1^st ‘ 𝑧 ) / 𝑖 ⦌ ⦋ ( 2^nd ‘ 𝑧 ) / 𝑗 ⦌ 𝑈 ) ) finSupp ( 0_g ‘ 𝐴 ) )
39	1 13	mat0	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 0_g ‘ ( 𝑅 freeLMod ( 𝑁 × 𝑁 ) ) ) = ( 0_g ‘ 𝐴 ) )
40	4 6 39	syl2anc	⊢ ( 𝜑 → ( 0_g ‘ ( 𝑅 freeLMod ( 𝑁 × 𝑁 ) ) ) = ( 0_g ‘ 𝐴 ) )
41	38 40	breqtrrd	⊢ ( 𝜑 → ( 𝑦 ∈ 𝐽 ↦ ( 𝑧 ∈ ( 𝑁 × 𝑁 ) ↦ ⦋ ( 1^st ‘ 𝑧 ) / 𝑖 ⦌ ⦋ ( 2^nd ‘ 𝑧 ) / 𝑗 ⦌ 𝑈 ) ) finSupp ( 0_g ‘ ( 𝑅 freeLMod ( 𝑁 × 𝑁 ) ) ) )
42	13 25 26 28 5 6 35 41	frlmgsum	⊢ ( 𝜑 → ( ( 𝑅 freeLMod ( 𝑁 × 𝑁 ) ) Σ_g ( 𝑦 ∈ 𝐽 ↦ ( 𝑧 ∈ ( 𝑁 × 𝑁 ) ↦ ⦋ ( 1^st ‘ 𝑧 ) / 𝑖 ⦌ ⦋ ( 2^nd ‘ 𝑧 ) / 𝑗 ⦌ 𝑈 ) ) ) = ( 𝑧 ∈ ( 𝑁 × 𝑁 ) ↦ ( 𝑅 Σ_g ( 𝑦 ∈ 𝐽 ↦ ⦋ ( 1^st ‘ 𝑧 ) / 𝑖 ⦌ ⦋ ( 2^nd ‘ 𝑧 ) / 𝑗 ⦌ 𝑈 ) ) ) )
43	24 42	eqtrd	⊢ ( 𝜑 → ( ( 𝑅 freeLMod ( 𝑁 × 𝑁 ) ) Σ_g ( 𝑦 ∈ 𝐽 ↦ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ 𝑈 ) ) ) = ( 𝑧 ∈ ( 𝑁 × 𝑁 ) ↦ ( 𝑅 Σ_g ( 𝑦 ∈ 𝐽 ↦ ⦋ ( 1^st ‘ 𝑧 ) / 𝑖 ⦌ ⦋ ( 2^nd ‘ 𝑧 ) / 𝑗 ⦌ 𝑈 ) ) ) )
44		fvex	⊢ ( 2^nd ‘ 𝑧 ) ∈ V
45		csbov2g	⊢ ( ( 2^nd ‘ 𝑧 ) ∈ V → ⦋ ( 2^nd ‘ 𝑧 ) / 𝑗 ⦌ ( 𝑅 Σ_g ( 𝑦 ∈ 𝐽 ↦ 𝑈 ) ) = ( 𝑅 Σ_g ⦋ ( 2^nd ‘ 𝑧 ) / 𝑗 ⦌ ( 𝑦 ∈ 𝐽 ↦ 𝑈 ) ) )
46	44 45	ax-mp	⊢ ⦋ ( 2^nd ‘ 𝑧 ) / 𝑗 ⦌ ( 𝑅 Σ_g ( 𝑦 ∈ 𝐽 ↦ 𝑈 ) ) = ( 𝑅 Σ_g ⦋ ( 2^nd ‘ 𝑧 ) / 𝑗 ⦌ ( 𝑦 ∈ 𝐽 ↦ 𝑈 ) )
47	46	csbeq2i	⊢ ⦋ ( 1^st ‘ 𝑧 ) / 𝑖 ⦌ ⦋ ( 2^nd ‘ 𝑧 ) / 𝑗 ⦌ ( 𝑅 Σ_g ( 𝑦 ∈ 𝐽 ↦ 𝑈 ) ) = ⦋ ( 1^st ‘ 𝑧 ) / 𝑖 ⦌ ( 𝑅 Σ_g ⦋ ( 2^nd ‘ 𝑧 ) / 𝑗 ⦌ ( 𝑦 ∈ 𝐽 ↦ 𝑈 ) )
48		fvex	⊢ ( 1^st ‘ 𝑧 ) ∈ V
49		csbov2g	⊢ ( ( 1^st ‘ 𝑧 ) ∈ V → ⦋ ( 1^st ‘ 𝑧 ) / 𝑖 ⦌ ( 𝑅 Σ_g ⦋ ( 2^nd ‘ 𝑧 ) / 𝑗 ⦌ ( 𝑦 ∈ 𝐽 ↦ 𝑈 ) ) = ( 𝑅 Σ_g ⦋ ( 1^st ‘ 𝑧 ) / 𝑖 ⦌ ⦋ ( 2^nd ‘ 𝑧 ) / 𝑗 ⦌ ( 𝑦 ∈ 𝐽 ↦ 𝑈 ) ) )
50	48 49	ax-mp	⊢ ⦋ ( 1^st ‘ 𝑧 ) / 𝑖 ⦌ ( 𝑅 Σ_g ⦋ ( 2^nd ‘ 𝑧 ) / 𝑗 ⦌ ( 𝑦 ∈ 𝐽 ↦ 𝑈 ) ) = ( 𝑅 Σ_g ⦋ ( 1^st ‘ 𝑧 ) / 𝑖 ⦌ ⦋ ( 2^nd ‘ 𝑧 ) / 𝑗 ⦌ ( 𝑦 ∈ 𝐽 ↦ 𝑈 ) )
51		csbmpt2	⊢ ( ( 2^nd ‘ 𝑧 ) ∈ V → ⦋ ( 2^nd ‘ 𝑧 ) / 𝑗 ⦌ ( 𝑦 ∈ 𝐽 ↦ 𝑈 ) = ( 𝑦 ∈ 𝐽 ↦ ⦋ ( 2^nd ‘ 𝑧 ) / 𝑗 ⦌ 𝑈 ) )
52	44 51	ax-mp	⊢ ⦋ ( 2^nd ‘ 𝑧 ) / 𝑗 ⦌ ( 𝑦 ∈ 𝐽 ↦ 𝑈 ) = ( 𝑦 ∈ 𝐽 ↦ ⦋ ( 2^nd ‘ 𝑧 ) / 𝑗 ⦌ 𝑈 )
53	52	csbeq2i	⊢ ⦋ ( 1^st ‘ 𝑧 ) / 𝑖 ⦌ ⦋ ( 2^nd ‘ 𝑧 ) / 𝑗 ⦌ ( 𝑦 ∈ 𝐽 ↦ 𝑈 ) = ⦋ ( 1^st ‘ 𝑧 ) / 𝑖 ⦌ ( 𝑦 ∈ 𝐽 ↦ ⦋ ( 2^nd ‘ 𝑧 ) / 𝑗 ⦌ 𝑈 )
54		csbmpt2	⊢ ( ( 1^st ‘ 𝑧 ) ∈ V → ⦋ ( 1^st ‘ 𝑧 ) / 𝑖 ⦌ ( 𝑦 ∈ 𝐽 ↦ ⦋ ( 2^nd ‘ 𝑧 ) / 𝑗 ⦌ 𝑈 ) = ( 𝑦 ∈ 𝐽 ↦ ⦋ ( 1^st ‘ 𝑧 ) / 𝑖 ⦌ ⦋ ( 2^nd ‘ 𝑧 ) / 𝑗 ⦌ 𝑈 ) )
55	48 54	ax-mp	⊢ ⦋ ( 1^st ‘ 𝑧 ) / 𝑖 ⦌ ( 𝑦 ∈ 𝐽 ↦ ⦋ ( 2^nd ‘ 𝑧 ) / 𝑗 ⦌ 𝑈 ) = ( 𝑦 ∈ 𝐽 ↦ ⦋ ( 1^st ‘ 𝑧 ) / 𝑖 ⦌ ⦋ ( 2^nd ‘ 𝑧 ) / 𝑗 ⦌ 𝑈 )
56	53 55	eqtri	⊢ ⦋ ( 1^st ‘ 𝑧 ) / 𝑖 ⦌ ⦋ ( 2^nd ‘ 𝑧 ) / 𝑗 ⦌ ( 𝑦 ∈ 𝐽 ↦ 𝑈 ) = ( 𝑦 ∈ 𝐽 ↦ ⦋ ( 1^st ‘ 𝑧 ) / 𝑖 ⦌ ⦋ ( 2^nd ‘ 𝑧 ) / 𝑗 ⦌ 𝑈 )
57	56	oveq2i	⊢ ( 𝑅 Σ_g ⦋ ( 1^st ‘ 𝑧 ) / 𝑖 ⦌ ⦋ ( 2^nd ‘ 𝑧 ) / 𝑗 ⦌ ( 𝑦 ∈ 𝐽 ↦ 𝑈 ) ) = ( 𝑅 Σ_g ( 𝑦 ∈ 𝐽 ↦ ⦋ ( 1^st ‘ 𝑧 ) / 𝑖 ⦌ ⦋ ( 2^nd ‘ 𝑧 ) / 𝑗 ⦌ 𝑈 ) )
58	47 50 57	3eqtrri	⊢ ( 𝑅 Σ_g ( 𝑦 ∈ 𝐽 ↦ ⦋ ( 1^st ‘ 𝑧 ) / 𝑖 ⦌ ⦋ ( 2^nd ‘ 𝑧 ) / 𝑗 ⦌ 𝑈 ) ) = ⦋ ( 1^st ‘ 𝑧 ) / 𝑖 ⦌ ⦋ ( 2^nd ‘ 𝑧 ) / 𝑗 ⦌ ( 𝑅 Σ_g ( 𝑦 ∈ 𝐽 ↦ 𝑈 ) )
59	58	mpteq2i	⊢ ( 𝑧 ∈ ( 𝑁 × 𝑁 ) ↦ ( 𝑅 Σ_g ( 𝑦 ∈ 𝐽 ↦ ⦋ ( 1^st ‘ 𝑧 ) / 𝑖 ⦌ ⦋ ( 2^nd ‘ 𝑧 ) / 𝑗 ⦌ 𝑈 ) ) ) = ( 𝑧 ∈ ( 𝑁 × 𝑁 ) ↦ ⦋ ( 1^st ‘ 𝑧 ) / 𝑖 ⦌ ⦋ ( 2^nd ‘ 𝑧 ) / 𝑗 ⦌ ( 𝑅 Σ_g ( 𝑦 ∈ 𝐽 ↦ 𝑈 ) ) )
60		mpompts	⊢ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 𝑅 Σ_g ( 𝑦 ∈ 𝐽 ↦ 𝑈 ) ) ) = ( 𝑧 ∈ ( 𝑁 × 𝑁 ) ↦ ⦋ ( 1^st ‘ 𝑧 ) / 𝑖 ⦌ ⦋ ( 2^nd ‘ 𝑧 ) / 𝑗 ⦌ ( 𝑅 Σ_g ( 𝑦 ∈ 𝐽 ↦ 𝑈 ) ) )
61	59 60	eqtr4i	⊢ ( 𝑧 ∈ ( 𝑁 × 𝑁 ) ↦ ( 𝑅 Σ_g ( 𝑦 ∈ 𝐽 ↦ ⦋ ( 1^st ‘ 𝑧 ) / 𝑖 ⦌ ⦋ ( 2^nd ‘ 𝑧 ) / 𝑗 ⦌ 𝑈 ) ) ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 𝑅 Σ_g ( 𝑦 ∈ 𝐽 ↦ 𝑈 ) ) )
62	61	a1i	⊢ ( 𝜑 → ( 𝑧 ∈ ( 𝑁 × 𝑁 ) ↦ ( 𝑅 Σ_g ( 𝑦 ∈ 𝐽 ↦ ⦋ ( 1^st ‘ 𝑧 ) / 𝑖 ⦌ ⦋ ( 2^nd ‘ 𝑧 ) / 𝑗 ⦌ 𝑈 ) ) ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 𝑅 Σ_g ( 𝑦 ∈ 𝐽 ↦ 𝑈 ) ) ) )
63	20 43 62	3eqtrd	⊢ ( 𝜑 → ( 𝐴 Σ_g ( 𝑦 ∈ 𝐽 ↦ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ 𝑈 ) ) ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( 𝑅 Σ_g ( 𝑦 ∈ 𝐽 ↦ 𝑈 ) ) ) )

Metamath Proof Explorer

Theorem matgsum

Proof