Theorem mpomatmul

Description: Multiplication of two N x N matrices given in maps-to notation. (Contributed by AV, 29-Oct-2019)

	Ref	Expression
Hypotheses	mpomatmul.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
	mpomatmul.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
	mpomatmul.m	⊢ × = ( .r ‘ 𝐴 )
	mpomatmul.t	⊢ · = ( .r ‘ 𝑅 )
	mpomatmul.r	⊢ ( 𝜑 → 𝑅 ∈ 𝑉 )
	mpomatmul.n	⊢ ( 𝜑 → 𝑁 ∈ Fin )
	mpomatmul.x	⊢ 𝑋 = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ 𝐶 )
	mpomatmul.y	⊢ 𝑌 = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ 𝐸 )
	mpomatmul.c	⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → 𝐶 ∈ 𝐵 )
	mpomatmul.e	⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → 𝐸 ∈ 𝐵 )
	mpomatmul.d	⊢ ( ( 𝜑 ∧ ( 𝑘 = 𝑖 ∧ 𝑚 = 𝑗 ) ) → 𝐷 = 𝐶 )
	mpomatmul.f	⊢ ( ( 𝜑 ∧ ( 𝑚 = 𝑖 ∧ 𝑙 = 𝑗 ) ) → 𝐹 = 𝐸 )
	mpomatmul.1	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑁 ∧ 𝑚 ∈ 𝑁 ) → 𝐷 ∈ 𝑈 )
	mpomatmul.2	⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁 ) → 𝐹 ∈ 𝑊 )
Assertion	mpomatmul	⊢ ( 𝜑 → ( 𝑋 × 𝑌 ) = ( 𝑘 ∈ 𝑁 , 𝑙 ∈ 𝑁 ↦ ( 𝑅 Σg ( 𝑚 ∈ 𝑁 ↦ ( 𝐷 · 𝐹 ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		mpomatmul.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
2		mpomatmul.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
3		mpomatmul.m	⊢ × = ( .r ‘ 𝐴 )
4		mpomatmul.t	⊢ · = ( .r ‘ 𝑅 )
5		mpomatmul.r	⊢ ( 𝜑 → 𝑅 ∈ 𝑉 )
6		mpomatmul.n	⊢ ( 𝜑 → 𝑁 ∈ Fin )
7		mpomatmul.x	⊢ 𝑋 = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ 𝐶 )
8		mpomatmul.y	⊢ 𝑌 = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ 𝐸 )
9		mpomatmul.c	⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → 𝐶 ∈ 𝐵 )
10		mpomatmul.e	⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → 𝐸 ∈ 𝐵 )
11		mpomatmul.d	⊢ ( ( 𝜑 ∧ ( 𝑘 = 𝑖 ∧ 𝑚 = 𝑗 ) ) → 𝐷 = 𝐶 )
12		mpomatmul.f	⊢ ( ( 𝜑 ∧ ( 𝑚 = 𝑖 ∧ 𝑙 = 𝑗 ) ) → 𝐹 = 𝐸 )
13		mpomatmul.1	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑁 ∧ 𝑚 ∈ 𝑁 ) → 𝐷 ∈ 𝑈 )
14		mpomatmul.2	⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁 ) → 𝐹 ∈ 𝑊 )
15		eqid	⊢ ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) = ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ )
16	1 15	matmulr	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉 ) → ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) = ( .r ‘ 𝐴 ) )
17	16 3	eqtr4di	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉 ) → ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) = × )
18	17	oveqd	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉 ) → ( 𝑋 ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) 𝑌 ) = ( 𝑋 × 𝑌 ) )
19	18	eqcomd	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉 ) → ( 𝑋 × 𝑌 ) = ( 𝑋 ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) 𝑌 ) )
20	6 5 19	syl2anc	⊢ ( 𝜑 → ( 𝑋 × 𝑌 ) = ( 𝑋 ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) 𝑌 ) )
21		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
22		eqid	⊢ ( Base ‘ 𝐴 ) = ( Base ‘ 𝐴 )
23	9 2	eleqtrdi	⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → 𝐶 ∈ ( Base ‘ 𝑅 ) )
24	1 21 22 6 5 23	matbas2d	⊢ ( 𝜑 → ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ 𝐶 ) ∈ ( Base ‘ 𝐴 ) )
25	7 24	eqeltrid	⊢ ( 𝜑 → 𝑋 ∈ ( Base ‘ 𝐴 ) )
26	1 21	matbas2	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉 ) → ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) = ( Base ‘ 𝐴 ) )
27	6 5 26	syl2anc	⊢ ( 𝜑 → ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) = ( Base ‘ 𝐴 ) )
28	25 27	eleqtrrd	⊢ ( 𝜑 → 𝑋 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) )
29	10 2	eleqtrdi	⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → 𝐸 ∈ ( Base ‘ 𝑅 ) )
30	1 21 22 6 5 29	matbas2d	⊢ ( 𝜑 → ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ 𝐸 ) ∈ ( Base ‘ 𝐴 ) )
31	8 30	eqeltrid	⊢ ( 𝜑 → 𝑌 ∈ ( Base ‘ 𝐴 ) )
32	31 27	eleqtrrd	⊢ ( 𝜑 → 𝑌 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) )
33	15 21 4 5 6 6 6 28 32	mamuval	⊢ ( 𝜑 → ( 𝑋 ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) 𝑌 ) = ( 𝑘 ∈ 𝑁 , 𝑙 ∈ 𝑁 ↦ ( 𝑅 Σg ( 𝑚 ∈ 𝑁 ↦ ( ( 𝑘 𝑋 𝑚 ) · ( 𝑚 𝑌 𝑙 ) ) ) ) ) )
34	7	a1i	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁 ) ∧ 𝑚 ∈ 𝑁 ) → 𝑋 = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ 𝐶 ) )
35		equcom	⊢ ( 𝑖 = 𝑘 ↔ 𝑘 = 𝑖 )
36		equcom	⊢ ( 𝑗 = 𝑚 ↔ 𝑚 = 𝑗 )
37	35 36	anbi12i	⊢ ( ( 𝑖 = 𝑘 ∧ 𝑗 = 𝑚 ) ↔ ( 𝑘 = 𝑖 ∧ 𝑚 = 𝑗 ) )
38	37 11	sylan2b	⊢ ( ( 𝜑 ∧ ( 𝑖 = 𝑘 ∧ 𝑗 = 𝑚 ) ) → 𝐷 = 𝐶 )
39	38	eqcomd	⊢ ( ( 𝜑 ∧ ( 𝑖 = 𝑘 ∧ 𝑗 = 𝑚 ) ) → 𝐶 = 𝐷 )
40	39	ex	⊢ ( 𝜑 → ( ( 𝑖 = 𝑘 ∧ 𝑗 = 𝑚 ) → 𝐶 = 𝐷 ) )
41	40	3ad2ant1	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁 ) → ( ( 𝑖 = 𝑘 ∧ 𝑗 = 𝑚 ) → 𝐶 = 𝐷 ) )
42	41	adantr	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁 ) ∧ 𝑚 ∈ 𝑁 ) → ( ( 𝑖 = 𝑘 ∧ 𝑗 = 𝑚 ) → 𝐶 = 𝐷 ) )
43	42	imp	⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁 ) ∧ 𝑚 ∈ 𝑁 ) ∧ ( 𝑖 = 𝑘 ∧ 𝑗 = 𝑚 ) ) → 𝐶 = 𝐷 )
44		simpl2	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁 ) ∧ 𝑚 ∈ 𝑁 ) → 𝑘 ∈ 𝑁 )
45		simpr	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁 ) ∧ 𝑚 ∈ 𝑁 ) → 𝑚 ∈ 𝑁 )
46		simpl1	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁 ) ∧ 𝑚 ∈ 𝑁 ) → 𝜑 )
47	46 44 45 13	syl3anc	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁 ) ∧ 𝑚 ∈ 𝑁 ) → 𝐷 ∈ 𝑈 )
48	34 43 44 45 47	ovmpod	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁 ) ∧ 𝑚 ∈ 𝑁 ) → ( 𝑘 𝑋 𝑚 ) = 𝐷 )
49	8	a1i	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁 ) ∧ 𝑚 ∈ 𝑁 ) → 𝑌 = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ 𝐸 ) )
50		equcomi	⊢ ( 𝑖 = 𝑚 → 𝑚 = 𝑖 )
51		equcomi	⊢ ( 𝑗 = 𝑙 → 𝑙 = 𝑗 )
52	50 51	anim12i	⊢ ( ( 𝑖 = 𝑚 ∧ 𝑗 = 𝑙 ) → ( 𝑚 = 𝑖 ∧ 𝑙 = 𝑗 ) )
53	52 12	sylan2	⊢ ( ( 𝜑 ∧ ( 𝑖 = 𝑚 ∧ 𝑗 = 𝑙 ) ) → 𝐹 = 𝐸 )
54	53	ex	⊢ ( 𝜑 → ( ( 𝑖 = 𝑚 ∧ 𝑗 = 𝑙 ) → 𝐹 = 𝐸 ) )
55	54	3ad2ant1	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁 ) → ( ( 𝑖 = 𝑚 ∧ 𝑗 = 𝑙 ) → 𝐹 = 𝐸 ) )
56	55	adantr	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁 ) ∧ 𝑚 ∈ 𝑁 ) → ( ( 𝑖 = 𝑚 ∧ 𝑗 = 𝑙 ) → 𝐹 = 𝐸 ) )
57	56	imp	⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁 ) ∧ 𝑚 ∈ 𝑁 ) ∧ ( 𝑖 = 𝑚 ∧ 𝑗 = 𝑙 ) ) → 𝐹 = 𝐸 )
58	57	eqcomd	⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁 ) ∧ 𝑚 ∈ 𝑁 ) ∧ ( 𝑖 = 𝑚 ∧ 𝑗 = 𝑙 ) ) → 𝐸 = 𝐹 )
59		simpl3	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁 ) ∧ 𝑚 ∈ 𝑁 ) → 𝑙 ∈ 𝑁 )
60	46 45 59 14	syl3anc	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁 ) ∧ 𝑚 ∈ 𝑁 ) → 𝐹 ∈ 𝑊 )
61	49 58 45 59 60	ovmpod	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁 ) ∧ 𝑚 ∈ 𝑁 ) → ( 𝑚 𝑌 𝑙 ) = 𝐹 )
62	48 61	oveq12d	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁 ) ∧ 𝑚 ∈ 𝑁 ) → ( ( 𝑘 𝑋 𝑚 ) · ( 𝑚 𝑌 𝑙 ) ) = ( 𝐷 · 𝐹 ) )
63	62	mpteq2dva	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁 ) → ( 𝑚 ∈ 𝑁 ↦ ( ( 𝑘 𝑋 𝑚 ) · ( 𝑚 𝑌 𝑙 ) ) ) = ( 𝑚 ∈ 𝑁 ↦ ( 𝐷 · 𝐹 ) ) )
64	63	oveq2d	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑁 ∧ 𝑙 ∈ 𝑁 ) → ( 𝑅 Σg ( 𝑚 ∈ 𝑁 ↦ ( ( 𝑘 𝑋 𝑚 ) · ( 𝑚 𝑌 𝑙 ) ) ) ) = ( 𝑅 Σg ( 𝑚 ∈ 𝑁 ↦ ( 𝐷 · 𝐹 ) ) ) )
65	64	mpoeq3dva	⊢ ( 𝜑 → ( 𝑘 ∈ 𝑁 , 𝑙 ∈ 𝑁 ↦ ( 𝑅 Σg ( 𝑚 ∈ 𝑁 ↦ ( ( 𝑘 𝑋 𝑚 ) · ( 𝑚 𝑌 𝑙 ) ) ) ) ) = ( 𝑘 ∈ 𝑁 , 𝑙 ∈ 𝑁 ↦ ( 𝑅 Σg ( 𝑚 ∈ 𝑁 ↦ ( 𝐷 · 𝐹 ) ) ) ) )
66	20 33 65	3eqtrd	⊢ ( 𝜑 → ( 𝑋 × 𝑌 ) = ( 𝑘 ∈ 𝑁 , 𝑙 ∈ 𝑁 ↦ ( 𝑅 Σg ( 𝑚 ∈ 𝑁 ↦ ( 𝐷 · 𝐹 ) ) ) ) )