Theorem mat2pmatlin

Description: The transformation of matrices into polynomial matrices is "linear", analogous to lmhmlin . Since A and C have different scalar rings, T cannot be a left module homomorphism as defined in df-lmhm , see lmhmsca . (Contributed by AV, 13-Nov-2019) (Proof shortened by AV, 28-Nov-2019)

	Ref	Expression
Hypotheses	mat2pmatbas.t	⊢ 𝑇 = ( 𝑁 matToPolyMat 𝑅 )
	mat2pmatbas.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
	mat2pmatbas.b	⊢ 𝐵 = ( Base ‘ 𝐴 )
	mat2pmatbas.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
	mat2pmatbas.c	⊢ 𝐶 = ( 𝑁 Mat 𝑃 )
	mat2pmatbas0.h	⊢ 𝐻 = ( Base ‘ 𝐶 )
	mat2pmatlin.k	⊢ 𝐾 = ( Base ‘ 𝑅 )
	mat2pmatlin.s	⊢ 𝑆 = ( algSc ‘ 𝑃 )
	mat2pmatlin.m	⊢ · = ( ·𝑠 ‘ 𝐴 )
	mat2pmatlin.n	⊢ × = ( ·𝑠 ‘ 𝐶 )
Assertion	mat2pmatlin	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) ) → ( 𝑇 ‘ ( 𝑋 · 𝑌 ) ) = ( ( 𝑆 ‘ 𝑋 ) × ( 𝑇 ‘ 𝑌 ) ) )

Proof

Step	Hyp	Ref	Expression
1		mat2pmatbas.t	⊢ 𝑇 = ( 𝑁 matToPolyMat 𝑅 )
2		mat2pmatbas.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
3		mat2pmatbas.b	⊢ 𝐵 = ( Base ‘ 𝐴 )
4		mat2pmatbas.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
5		mat2pmatbas.c	⊢ 𝐶 = ( 𝑁 Mat 𝑃 )
6		mat2pmatbas0.h	⊢ 𝐻 = ( Base ‘ 𝐶 )
7		mat2pmatlin.k	⊢ 𝐾 = ( Base ‘ 𝑅 )
8		mat2pmatlin.s	⊢ 𝑆 = ( algSc ‘ 𝑃 )
9		mat2pmatlin.m	⊢ · = ( ·𝑠 ‘ 𝐴 )
10		mat2pmatlin.n	⊢ × = ( ·𝑠 ‘ 𝐶 )
11		simpr	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → 𝑅 ∈ CRing )
12	4	ply1assa	⊢ ( 𝑅 ∈ CRing → 𝑃 ∈ AssAlg )
13		eqid	⊢ ( Scalar ‘ 𝑃 ) = ( Scalar ‘ 𝑃 )
14	8 13	asclrhm	⊢ ( 𝑃 ∈ AssAlg → 𝑆 ∈ ( ( Scalar ‘ 𝑃 ) RingHom 𝑃 ) )
15	11 12 14	3syl	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → 𝑆 ∈ ( ( Scalar ‘ 𝑃 ) RingHom 𝑃 ) )
16	4	ply1sca	⊢ ( 𝑅 ∈ CRing → 𝑅 = ( Scalar ‘ 𝑃 ) )
17	16	adantl	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → 𝑅 = ( Scalar ‘ 𝑃 ) )
18	17	oveq1d	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → ( 𝑅 RingHom 𝑃 ) = ( ( Scalar ‘ 𝑃 ) RingHom 𝑃 ) )
19	15 18	eleqtrrd	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → 𝑆 ∈ ( 𝑅 RingHom 𝑃 ) )
20	19	adantr	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) ) → 𝑆 ∈ ( 𝑅 RingHom 𝑃 ) )
21	20	adantr	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → 𝑆 ∈ ( 𝑅 RingHom 𝑃 ) )
22	7	eleq2i	⊢ ( 𝑋 ∈ 𝐾 ↔ 𝑋 ∈ ( Base ‘ 𝑅 ) )
23	22	biimpi	⊢ ( 𝑋 ∈ 𝐾 → 𝑋 ∈ ( Base ‘ 𝑅 ) )
24	23	adantr	⊢ ( ( 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) → 𝑋 ∈ ( Base ‘ 𝑅 ) )
25	24	ad2antlr	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → 𝑋 ∈ ( Base ‘ 𝑅 ) )
26		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
27		simprl	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → 𝑖 ∈ 𝑁 )
28		simpr	⊢ ( ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → 𝑗 ∈ 𝑁 )
29	28	adantl	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → 𝑗 ∈ 𝑁 )
30		simplrr	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → 𝑌 ∈ 𝐵 )
31	2 26 3 27 29 30	matecld	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → ( 𝑖 𝑌 𝑗 ) ∈ ( Base ‘ 𝑅 ) )
32		eqid	⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
33		eqid	⊢ ( .r ‘ 𝑃 ) = ( .r ‘ 𝑃 )
34	26 32 33	rhmmul	⊢ ( ( 𝑆 ∈ ( 𝑅 RingHom 𝑃 ) ∧ 𝑋 ∈ ( Base ‘ 𝑅 ) ∧ ( 𝑖 𝑌 𝑗 ) ∈ ( Base ‘ 𝑅 ) ) → ( 𝑆 ‘ ( 𝑋 ( .r ‘ 𝑅 ) ( 𝑖 𝑌 𝑗 ) ) ) = ( ( 𝑆 ‘ 𝑋 ) ( .r ‘ 𝑃 ) ( 𝑆 ‘ ( 𝑖 𝑌 𝑗 ) ) ) )
35	21 25 31 34	syl3anc	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → ( 𝑆 ‘ ( 𝑋 ( .r ‘ 𝑅 ) ( 𝑖 𝑌 𝑗 ) ) ) = ( ( 𝑆 ‘ 𝑋 ) ( .r ‘ 𝑃 ) ( 𝑆 ‘ ( 𝑖 𝑌 𝑗 ) ) ) )
36		crngring	⊢ ( 𝑅 ∈ CRing → 𝑅 ∈ Ring )
37	36	ad2antlr	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) ) → 𝑅 ∈ Ring )
38	37	adantr	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → 𝑅 ∈ Ring )
39		simpr	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) ) → ( 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) )
40	39	adantr	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → ( 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) )
41		simpr	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) )
42	2 3 7 9 32	matvscacell	⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → ( 𝑖 ( 𝑋 · 𝑌 ) 𝑗 ) = ( 𝑋 ( .r ‘ 𝑅 ) ( 𝑖 𝑌 𝑗 ) ) )
43	38 40 41 42	syl3anc	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → ( 𝑖 ( 𝑋 · 𝑌 ) 𝑗 ) = ( 𝑋 ( .r ‘ 𝑅 ) ( 𝑖 𝑌 𝑗 ) ) )
44	43	fveq2d	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → ( 𝑆 ‘ ( 𝑖 ( 𝑋 · 𝑌 ) 𝑗 ) ) = ( 𝑆 ‘ ( 𝑋 ( .r ‘ 𝑅 ) ( 𝑖 𝑌 𝑗 ) ) ) )
45	36	anim2i	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) )
46		simpr	⊢ ( ( 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) → 𝑌 ∈ 𝐵 )
47	45 46	anim12i	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) ) → ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑌 ∈ 𝐵 ) )
48		df-3an	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑌 ∈ 𝐵 ) ↔ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑌 ∈ 𝐵 ) )
49	47 48	sylibr	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑌 ∈ 𝐵 ) )
50	1 2 3 4 8	mat2pmatvalel	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → ( 𝑖 ( 𝑇 ‘ 𝑌 ) 𝑗 ) = ( 𝑆 ‘ ( 𝑖 𝑌 𝑗 ) ) )
51	49 50	sylan	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → ( 𝑖 ( 𝑇 ‘ 𝑌 ) 𝑗 ) = ( 𝑆 ‘ ( 𝑖 𝑌 𝑗 ) ) )
52	51	oveq2d	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → ( ( 𝑆 ‘ 𝑋 ) ( .r ‘ 𝑃 ) ( 𝑖 ( 𝑇 ‘ 𝑌 ) 𝑗 ) ) = ( ( 𝑆 ‘ 𝑋 ) ( .r ‘ 𝑃 ) ( 𝑆 ‘ ( 𝑖 𝑌 𝑗 ) ) ) )
53	35 44 52	3eqtr4d	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → ( 𝑆 ‘ ( 𝑖 ( 𝑋 · 𝑌 ) 𝑗 ) ) = ( ( 𝑆 ‘ 𝑋 ) ( .r ‘ 𝑃 ) ( 𝑖 ( 𝑇 ‘ 𝑌 ) 𝑗 ) ) )
54		simpll	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) ) → 𝑁 ∈ Fin )
55	54	adantr	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → 𝑁 ∈ Fin )
56	7 2 3 9	matvscl	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) ) → ( 𝑋 · 𝑌 ) ∈ 𝐵 )
57	45 56	sylan	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) ) → ( 𝑋 · 𝑌 ) ∈ 𝐵 )
58	57	adantr	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → ( 𝑋 · 𝑌 ) ∈ 𝐵 )
59	1 2 3 4 8	mat2pmatvalel	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ ( 𝑋 · 𝑌 ) ∈ 𝐵 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → ( 𝑖 ( 𝑇 ‘ ( 𝑋 · 𝑌 ) ) 𝑗 ) = ( 𝑆 ‘ ( 𝑖 ( 𝑋 · 𝑌 ) 𝑗 ) ) )
60	55 38 58 41 59	syl31anc	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → ( 𝑖 ( 𝑇 ‘ ( 𝑋 · 𝑌 ) ) 𝑗 ) = ( 𝑆 ‘ ( 𝑖 ( 𝑋 · 𝑌 ) 𝑗 ) ) )
61	4	ply1ring	⊢ ( 𝑅 ∈ Ring → 𝑃 ∈ Ring )
62	36 61	syl	⊢ ( 𝑅 ∈ CRing → 𝑃 ∈ Ring )
63	62	ad2antlr	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) ) → 𝑃 ∈ Ring )
64	63	adantr	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → 𝑃 ∈ Ring )
65	36	adantl	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → 𝑅 ∈ Ring )
66		simpl	⊢ ( ( 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) → 𝑋 ∈ 𝐾 )
67		eqid	⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
68	4 8 7 67	ply1sclcl	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐾 ) → ( 𝑆 ‘ 𝑋 ) ∈ ( Base ‘ 𝑃 ) )
69	65 66 68	syl2an	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) ) → ( 𝑆 ‘ 𝑋 ) ∈ ( Base ‘ 𝑃 ) )
70	1 2 3 4 5 6	mat2pmatbas0	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑌 ∈ 𝐵 ) → ( 𝑇 ‘ 𝑌 ) ∈ 𝐻 )
71	49 70	syl	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) ) → ( 𝑇 ‘ 𝑌 ) ∈ 𝐻 )
72	69 71	jca	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) ) → ( ( 𝑆 ‘ 𝑋 ) ∈ ( Base ‘ 𝑃 ) ∧ ( 𝑇 ‘ 𝑌 ) ∈ 𝐻 ) )
73	72	adantr	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → ( ( 𝑆 ‘ 𝑋 ) ∈ ( Base ‘ 𝑃 ) ∧ ( 𝑇 ‘ 𝑌 ) ∈ 𝐻 ) )
74	5 6 67 10 33	matvscacell	⊢ ( ( 𝑃 ∈ Ring ∧ ( ( 𝑆 ‘ 𝑋 ) ∈ ( Base ‘ 𝑃 ) ∧ ( 𝑇 ‘ 𝑌 ) ∈ 𝐻 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → ( 𝑖 ( ( 𝑆 ‘ 𝑋 ) × ( 𝑇 ‘ 𝑌 ) ) 𝑗 ) = ( ( 𝑆 ‘ 𝑋 ) ( .r ‘ 𝑃 ) ( 𝑖 ( 𝑇 ‘ 𝑌 ) 𝑗 ) ) )
75	64 73 41 74	syl3anc	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → ( 𝑖 ( ( 𝑆 ‘ 𝑋 ) × ( 𝑇 ‘ 𝑌 ) ) 𝑗 ) = ( ( 𝑆 ‘ 𝑋 ) ( .r ‘ 𝑃 ) ( 𝑖 ( 𝑇 ‘ 𝑌 ) 𝑗 ) ) )
76	53 60 75	3eqtr4d	⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → ( 𝑖 ( 𝑇 ‘ ( 𝑋 · 𝑌 ) ) 𝑗 ) = ( 𝑖 ( ( 𝑆 ‘ 𝑋 ) × ( 𝑇 ‘ 𝑌 ) ) 𝑗 ) )
77	76	ralrimivva	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) ) → ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ( 𝑇 ‘ ( 𝑋 · 𝑌 ) ) 𝑗 ) = ( 𝑖 ( ( 𝑆 ‘ 𝑋 ) × ( 𝑇 ‘ 𝑌 ) ) 𝑗 ) )
78	1 2 3 4 5 6	mat2pmatbas0	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ ( 𝑋 · 𝑌 ) ∈ 𝐵 ) → ( 𝑇 ‘ ( 𝑋 · 𝑌 ) ) ∈ 𝐻 )
79	54 37 57 78	syl3anc	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) ) → ( 𝑇 ‘ ( 𝑋 · 𝑌 ) ) ∈ 𝐻 )
80	67 5 6 10	matvscl	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑃 ∈ Ring ) ∧ ( ( 𝑆 ‘ 𝑋 ) ∈ ( Base ‘ 𝑃 ) ∧ ( 𝑇 ‘ 𝑌 ) ∈ 𝐻 ) ) → ( ( 𝑆 ‘ 𝑋 ) × ( 𝑇 ‘ 𝑌 ) ) ∈ 𝐻 )
81	54 63 72 80	syl21anc	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) ) → ( ( 𝑆 ‘ 𝑋 ) × ( 𝑇 ‘ 𝑌 ) ) ∈ 𝐻 )
82	5 6	eqmat	⊢ ( ( ( 𝑇 ‘ ( 𝑋 · 𝑌 ) ) ∈ 𝐻 ∧ ( ( 𝑆 ‘ 𝑋 ) × ( 𝑇 ‘ 𝑌 ) ) ∈ 𝐻 ) → ( ( 𝑇 ‘ ( 𝑋 · 𝑌 ) ) = ( ( 𝑆 ‘ 𝑋 ) × ( 𝑇 ‘ 𝑌 ) ) ↔ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ( 𝑇 ‘ ( 𝑋 · 𝑌 ) ) 𝑗 ) = ( 𝑖 ( ( 𝑆 ‘ 𝑋 ) × ( 𝑇 ‘ 𝑌 ) ) 𝑗 ) ) )
83	79 81 82	syl2anc	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) ) → ( ( 𝑇 ‘ ( 𝑋 · 𝑌 ) ) = ( ( 𝑆 ‘ 𝑋 ) × ( 𝑇 ‘ 𝑌 ) ) ↔ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ( 𝑖 ( 𝑇 ‘ ( 𝑋 · 𝑌 ) ) 𝑗 ) = ( 𝑖 ( ( 𝑆 ‘ 𝑋 ) × ( 𝑇 ‘ 𝑌 ) ) 𝑗 ) ) )
84	77 83	mpbird	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) ) → ( 𝑇 ‘ ( 𝑋 · 𝑌 ) ) = ( ( 𝑆 ‘ 𝑋 ) × ( 𝑇 ‘ 𝑌 ) ) )