Theorem mamuvs2

Description: Matrix multiplication distributes over scalar multiplication on the left. (Contributed by Stefan O'Rear, 5-Sep-2015) (Proof shortened by AV, 22-Jul-2019)

	Ref	Expression
Hypotheses	mamuvs2.r	⊢ ( 𝜑 → 𝑅 ∈ CRing )
	mamuvs2.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
	mamuvs2.t	⊢ · = ( .r ‘ 𝑅 )
	mamuvs2.f	⊢ 𝐹 = ( 𝑅 maMul ⟨ 𝑀 , 𝑁 , 𝑂 ⟩ )
	mamuvs2.m	⊢ ( 𝜑 → 𝑀 ∈ Fin )
	mamuvs2.n	⊢ ( 𝜑 → 𝑁 ∈ Fin )
	mamuvs2.o	⊢ ( 𝜑 → 𝑂 ∈ Fin )
	mamuvs2.x	⊢ ( 𝜑 → 𝑋 ∈ ( 𝐵 ↑m ( 𝑀 × 𝑁 ) ) )
	mamuvs2.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
	mamuvs2.z	⊢ ( 𝜑 → 𝑍 ∈ ( 𝐵 ↑m ( 𝑁 × 𝑂 ) ) )
Assertion	mamuvs2	⊢ ( 𝜑 → ( 𝑋 𝐹 ( ( ( 𝑁 × 𝑂 ) × { 𝑌 } ) ∘f · 𝑍 ) ) = ( ( ( 𝑀 × 𝑂 ) × { 𝑌 } ) ∘f · ( 𝑋 𝐹 𝑍 ) ) )

Proof

Step	Hyp	Ref	Expression
1		mamuvs2.r	⊢ ( 𝜑 → 𝑅 ∈ CRing )
2		mamuvs2.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
3		mamuvs2.t	⊢ · = ( .r ‘ 𝑅 )
4		mamuvs2.f	⊢ 𝐹 = ( 𝑅 maMul ⟨ 𝑀 , 𝑁 , 𝑂 ⟩ )
5		mamuvs2.m	⊢ ( 𝜑 → 𝑀 ∈ Fin )
6		mamuvs2.n	⊢ ( 𝜑 → 𝑁 ∈ Fin )
7		mamuvs2.o	⊢ ( 𝜑 → 𝑂 ∈ Fin )
8		mamuvs2.x	⊢ ( 𝜑 → 𝑋 ∈ ( 𝐵 ↑m ( 𝑀 × 𝑁 ) ) )
9		mamuvs2.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
10		mamuvs2.z	⊢ ( 𝜑 → 𝑍 ∈ ( 𝐵 ↑m ( 𝑁 × 𝑂 ) ) )
11		df-ov	⊢ ( 𝑗 ( ( ( 𝑁 × 𝑂 ) × { 𝑌 } ) ∘f · 𝑍 ) 𝑘 ) = ( ( ( ( 𝑁 × 𝑂 ) × { 𝑌 } ) ∘f · 𝑍 ) ‘ ⟨ 𝑗 , 𝑘 ⟩ )
12		simpr	⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂 ) ) ∧ 𝑗 ∈ 𝑁 ) → 𝑗 ∈ 𝑁 )
13		simplrr	⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂 ) ) ∧ 𝑗 ∈ 𝑁 ) → 𝑘 ∈ 𝑂 )
14		opelxpi	⊢ ( ( 𝑗 ∈ 𝑁 ∧ 𝑘 ∈ 𝑂 ) → ⟨ 𝑗 , 𝑘 ⟩ ∈ ( 𝑁 × 𝑂 ) )
15	12 13 14	syl2anc	⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂 ) ) ∧ 𝑗 ∈ 𝑁 ) → ⟨ 𝑗 , 𝑘 ⟩ ∈ ( 𝑁 × 𝑂 ) )
16		xpfi	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑂 ∈ Fin ) → ( 𝑁 × 𝑂 ) ∈ Fin )
17	6 7 16	syl2anc	⊢ ( 𝜑 → ( 𝑁 × 𝑂 ) ∈ Fin )
18	17	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂 ) ) ∧ 𝑗 ∈ 𝑁 ) → ( 𝑁 × 𝑂 ) ∈ Fin )
19	9	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂 ) ) ∧ 𝑗 ∈ 𝑁 ) → 𝑌 ∈ 𝐵 )
20		elmapi	⊢ ( 𝑍 ∈ ( 𝐵 ↑m ( 𝑁 × 𝑂 ) ) → 𝑍 : ( 𝑁 × 𝑂 ) ⟶ 𝐵 )
21		ffn	⊢ ( 𝑍 : ( 𝑁 × 𝑂 ) ⟶ 𝐵 → 𝑍 Fn ( 𝑁 × 𝑂 ) )
22	10 20 21	3syl	⊢ ( 𝜑 → 𝑍 Fn ( 𝑁 × 𝑂 ) )
23	22	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂 ) ) ∧ 𝑗 ∈ 𝑁 ) → 𝑍 Fn ( 𝑁 × 𝑂 ) )
24		df-ov	⊢ ( 𝑗 𝑍 𝑘 ) = ( 𝑍 ‘ ⟨ 𝑗 , 𝑘 ⟩ )
25	24	eqcomi	⊢ ( 𝑍 ‘ ⟨ 𝑗 , 𝑘 ⟩ ) = ( 𝑗 𝑍 𝑘 )
26	25	a1i	⊢ ( ( ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂 ) ) ∧ 𝑗 ∈ 𝑁 ) ∧ ⟨ 𝑗 , 𝑘 ⟩ ∈ ( 𝑁 × 𝑂 ) ) → ( 𝑍 ‘ ⟨ 𝑗 , 𝑘 ⟩ ) = ( 𝑗 𝑍 𝑘 ) )
27	18 19 23 26	ofc1	⊢ ( ( ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂 ) ) ∧ 𝑗 ∈ 𝑁 ) ∧ ⟨ 𝑗 , 𝑘 ⟩ ∈ ( 𝑁 × 𝑂 ) ) → ( ( ( ( 𝑁 × 𝑂 ) × { 𝑌 } ) ∘f · 𝑍 ) ‘ ⟨ 𝑗 , 𝑘 ⟩ ) = ( 𝑌 · ( 𝑗 𝑍 𝑘 ) ) )
28	15 27	mpdan	⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂 ) ) ∧ 𝑗 ∈ 𝑁 ) → ( ( ( ( 𝑁 × 𝑂 ) × { 𝑌 } ) ∘f · 𝑍 ) ‘ ⟨ 𝑗 , 𝑘 ⟩ ) = ( 𝑌 · ( 𝑗 𝑍 𝑘 ) ) )
29	11 28	eqtrid	⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂 ) ) ∧ 𝑗 ∈ 𝑁 ) → ( 𝑗 ( ( ( 𝑁 × 𝑂 ) × { 𝑌 } ) ∘f · 𝑍 ) 𝑘 ) = ( 𝑌 · ( 𝑗 𝑍 𝑘 ) ) )
30	29	oveq2d	⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂 ) ) ∧ 𝑗 ∈ 𝑁 ) → ( ( 𝑖 𝑋 𝑗 ) · ( 𝑗 ( ( ( 𝑁 × 𝑂 ) × { 𝑌 } ) ∘f · 𝑍 ) 𝑘 ) ) = ( ( 𝑖 𝑋 𝑗 ) · ( 𝑌 · ( 𝑗 𝑍 𝑘 ) ) ) )
31		eqid	⊢ ( mulGrp ‘ 𝑅 ) = ( mulGrp ‘ 𝑅 )
32	31	crngmgp	⊢ ( 𝑅 ∈ CRing → ( mulGrp ‘ 𝑅 ) ∈ CMnd )
33	1 32	syl	⊢ ( 𝜑 → ( mulGrp ‘ 𝑅 ) ∈ CMnd )
34	33	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂 ) ) ∧ 𝑗 ∈ 𝑁 ) → ( mulGrp ‘ 𝑅 ) ∈ CMnd )
35		elmapi	⊢ ( 𝑋 ∈ ( 𝐵 ↑m ( 𝑀 × 𝑁 ) ) → 𝑋 : ( 𝑀 × 𝑁 ) ⟶ 𝐵 )
36	8 35	syl	⊢ ( 𝜑 → 𝑋 : ( 𝑀 × 𝑁 ) ⟶ 𝐵 )
37	36	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂 ) ) ∧ 𝑗 ∈ 𝑁 ) → 𝑋 : ( 𝑀 × 𝑁 ) ⟶ 𝐵 )
38		simplrl	⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂 ) ) ∧ 𝑗 ∈ 𝑁 ) → 𝑖 ∈ 𝑀 )
39	37 38 12	fovcdmd	⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂 ) ) ∧ 𝑗 ∈ 𝑁 ) → ( 𝑖 𝑋 𝑗 ) ∈ 𝐵 )
40	10 20	syl	⊢ ( 𝜑 → 𝑍 : ( 𝑁 × 𝑂 ) ⟶ 𝐵 )
41	40	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂 ) ) ∧ 𝑗 ∈ 𝑁 ) → 𝑍 : ( 𝑁 × 𝑂 ) ⟶ 𝐵 )
42	41 12 13	fovcdmd	⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂 ) ) ∧ 𝑗 ∈ 𝑁 ) → ( 𝑗 𝑍 𝑘 ) ∈ 𝐵 )
43	31 2	mgpbas	⊢ 𝐵 = ( Base ‘ ( mulGrp ‘ 𝑅 ) )
44	31 3	mgpplusg	⊢ · = ( +g ‘ ( mulGrp ‘ 𝑅 ) )
45	43 44	cmn12	⊢ ( ( ( mulGrp ‘ 𝑅 ) ∈ CMnd ∧ ( ( 𝑖 𝑋 𝑗 ) ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ ( 𝑗 𝑍 𝑘 ) ∈ 𝐵 ) ) → ( ( 𝑖 𝑋 𝑗 ) · ( 𝑌 · ( 𝑗 𝑍 𝑘 ) ) ) = ( 𝑌 · ( ( 𝑖 𝑋 𝑗 ) · ( 𝑗 𝑍 𝑘 ) ) ) )
46	34 39 19 42 45	syl13anc	⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂 ) ) ∧ 𝑗 ∈ 𝑁 ) → ( ( 𝑖 𝑋 𝑗 ) · ( 𝑌 · ( 𝑗 𝑍 𝑘 ) ) ) = ( 𝑌 · ( ( 𝑖 𝑋 𝑗 ) · ( 𝑗 𝑍 𝑘 ) ) ) )
47	30 46	eqtrd	⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂 ) ) ∧ 𝑗 ∈ 𝑁 ) → ( ( 𝑖 𝑋 𝑗 ) · ( 𝑗 ( ( ( 𝑁 × 𝑂 ) × { 𝑌 } ) ∘f · 𝑍 ) 𝑘 ) ) = ( 𝑌 · ( ( 𝑖 𝑋 𝑗 ) · ( 𝑗 𝑍 𝑘 ) ) ) )
48	47	mpteq2dva	⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂 ) ) → ( 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 𝑋 𝑗 ) · ( 𝑗 ( ( ( 𝑁 × 𝑂 ) × { 𝑌 } ) ∘f · 𝑍 ) 𝑘 ) ) ) = ( 𝑗 ∈ 𝑁 ↦ ( 𝑌 · ( ( 𝑖 𝑋 𝑗 ) · ( 𝑗 𝑍 𝑘 ) ) ) ) )
49	48	oveq2d	⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂 ) ) → ( 𝑅 Σg ( 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 𝑋 𝑗 ) · ( 𝑗 ( ( ( 𝑁 × 𝑂 ) × { 𝑌 } ) ∘f · 𝑍 ) 𝑘 ) ) ) ) = ( 𝑅 Σg ( 𝑗 ∈ 𝑁 ↦ ( 𝑌 · ( ( 𝑖 𝑋 𝑗 ) · ( 𝑗 𝑍 𝑘 ) ) ) ) ) )
50		eqid	⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
51		crngring	⊢ ( 𝑅 ∈ CRing → 𝑅 ∈ Ring )
52	1 51	syl	⊢ ( 𝜑 → 𝑅 ∈ Ring )
53	52	adantr	⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂 ) ) → 𝑅 ∈ Ring )
54	6	adantr	⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂 ) ) → 𝑁 ∈ Fin )
55	9	adantr	⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂 ) ) → 𝑌 ∈ 𝐵 )
56	52	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂 ) ) ∧ 𝑗 ∈ 𝑁 ) → 𝑅 ∈ Ring )
57	2 3 56 39 42	ringcld	⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂 ) ) ∧ 𝑗 ∈ 𝑁 ) → ( ( 𝑖 𝑋 𝑗 ) · ( 𝑗 𝑍 𝑘 ) ) ∈ 𝐵 )
58		eqid	⊢ ( 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 𝑋 𝑗 ) · ( 𝑗 𝑍 𝑘 ) ) ) = ( 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 𝑋 𝑗 ) · ( 𝑗 𝑍 𝑘 ) ) )
59		ovexd	⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂 ) ) ∧ 𝑗 ∈ 𝑁 ) → ( ( 𝑖 𝑋 𝑗 ) · ( 𝑗 𝑍 𝑘 ) ) ∈ V )
60		fvexd	⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂 ) ) → ( 0g ‘ 𝑅 ) ∈ V )
61	58 54 59 60	fsuppmptdm	⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂 ) ) → ( 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 𝑋 𝑗 ) · ( 𝑗 𝑍 𝑘 ) ) ) finSupp ( 0g ‘ 𝑅 ) )
62	2 50 3 53 54 55 57 61	gsummulc2	⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂 ) ) → ( 𝑅 Σg ( 𝑗 ∈ 𝑁 ↦ ( 𝑌 · ( ( 𝑖 𝑋 𝑗 ) · ( 𝑗 𝑍 𝑘 ) ) ) ) ) = ( 𝑌 · ( 𝑅 Σg ( 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 𝑋 𝑗 ) · ( 𝑗 𝑍 𝑘 ) ) ) ) ) )
63	49 62	eqtrd	⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂 ) ) → ( 𝑅 Σg ( 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 𝑋 𝑗 ) · ( 𝑗 ( ( ( 𝑁 × 𝑂 ) × { 𝑌 } ) ∘f · 𝑍 ) 𝑘 ) ) ) ) = ( 𝑌 · ( 𝑅 Σg ( 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 𝑋 𝑗 ) · ( 𝑗 𝑍 𝑘 ) ) ) ) ) )
64	1	adantr	⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂 ) ) → 𝑅 ∈ CRing )
65	5	adantr	⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂 ) ) → 𝑀 ∈ Fin )
66	7	adantr	⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂 ) ) → 𝑂 ∈ Fin )
67	8	adantr	⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂 ) ) → 𝑋 ∈ ( 𝐵 ↑m ( 𝑀 × 𝑁 ) ) )
68		fconst6g	⊢ ( 𝑌 ∈ 𝐵 → ( ( 𝑁 × 𝑂 ) × { 𝑌 } ) : ( 𝑁 × 𝑂 ) ⟶ 𝐵 )
69	9 68	syl	⊢ ( 𝜑 → ( ( 𝑁 × 𝑂 ) × { 𝑌 } ) : ( 𝑁 × 𝑂 ) ⟶ 𝐵 )
70	2	fvexi	⊢ 𝐵 ∈ V
71		elmapg	⊢ ( ( 𝐵 ∈ V ∧ ( 𝑁 × 𝑂 ) ∈ Fin ) → ( ( ( 𝑁 × 𝑂 ) × { 𝑌 } ) ∈ ( 𝐵 ↑m ( 𝑁 × 𝑂 ) ) ↔ ( ( 𝑁 × 𝑂 ) × { 𝑌 } ) : ( 𝑁 × 𝑂 ) ⟶ 𝐵 ) )
72	70 17 71	sylancr	⊢ ( 𝜑 → ( ( ( 𝑁 × 𝑂 ) × { 𝑌 } ) ∈ ( 𝐵 ↑m ( 𝑁 × 𝑂 ) ) ↔ ( ( 𝑁 × 𝑂 ) × { 𝑌 } ) : ( 𝑁 × 𝑂 ) ⟶ 𝐵 ) )
73	69 72	mpbird	⊢ ( 𝜑 → ( ( 𝑁 × 𝑂 ) × { 𝑌 } ) ∈ ( 𝐵 ↑m ( 𝑁 × 𝑂 ) ) )
74	2 3	ringvcl	⊢ ( ( 𝑅 ∈ Ring ∧ ( ( 𝑁 × 𝑂 ) × { 𝑌 } ) ∈ ( 𝐵 ↑m ( 𝑁 × 𝑂 ) ) ∧ 𝑍 ∈ ( 𝐵 ↑m ( 𝑁 × 𝑂 ) ) ) → ( ( ( 𝑁 × 𝑂 ) × { 𝑌 } ) ∘f · 𝑍 ) ∈ ( 𝐵 ↑m ( 𝑁 × 𝑂 ) ) )
75	52 73 10 74	syl3anc	⊢ ( 𝜑 → ( ( ( 𝑁 × 𝑂 ) × { 𝑌 } ) ∘f · 𝑍 ) ∈ ( 𝐵 ↑m ( 𝑁 × 𝑂 ) ) )
76	75	adantr	⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂 ) ) → ( ( ( 𝑁 × 𝑂 ) × { 𝑌 } ) ∘f · 𝑍 ) ∈ ( 𝐵 ↑m ( 𝑁 × 𝑂 ) ) )
77		simprl	⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂 ) ) → 𝑖 ∈ 𝑀 )
78		simprr	⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂 ) ) → 𝑘 ∈ 𝑂 )
79	4 2 3 64 65 54 66 67 76 77 78	mamufv	⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂 ) ) → ( 𝑖 ( 𝑋 𝐹 ( ( ( 𝑁 × 𝑂 ) × { 𝑌 } ) ∘f · 𝑍 ) ) 𝑘 ) = ( 𝑅 Σg ( 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 𝑋 𝑗 ) · ( 𝑗 ( ( ( 𝑁 × 𝑂 ) × { 𝑌 } ) ∘f · 𝑍 ) 𝑘 ) ) ) ) )
80		df-ov	⊢ ( 𝑖 ( ( ( 𝑀 × 𝑂 ) × { 𝑌 } ) ∘f · ( 𝑋 𝐹 𝑍 ) ) 𝑘 ) = ( ( ( ( 𝑀 × 𝑂 ) × { 𝑌 } ) ∘f · ( 𝑋 𝐹 𝑍 ) ) ‘ ⟨ 𝑖 , 𝑘 ⟩ )
81		opelxpi	⊢ ( ( 𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂 ) → ⟨ 𝑖 , 𝑘 ⟩ ∈ ( 𝑀 × 𝑂 ) )
82	81	adantl	⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂 ) ) → ⟨ 𝑖 , 𝑘 ⟩ ∈ ( 𝑀 × 𝑂 ) )
83		xpfi	⊢ ( ( 𝑀 ∈ Fin ∧ 𝑂 ∈ Fin ) → ( 𝑀 × 𝑂 ) ∈ Fin )
84	5 7 83	syl2anc	⊢ ( 𝜑 → ( 𝑀 × 𝑂 ) ∈ Fin )
85	84	adantr	⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂 ) ) → ( 𝑀 × 𝑂 ) ∈ Fin )
86	2 52 4 5 6 7 8 10	mamucl	⊢ ( 𝜑 → ( 𝑋 𝐹 𝑍 ) ∈ ( 𝐵 ↑m ( 𝑀 × 𝑂 ) ) )
87		elmapi	⊢ ( ( 𝑋 𝐹 𝑍 ) ∈ ( 𝐵 ↑m ( 𝑀 × 𝑂 ) ) → ( 𝑋 𝐹 𝑍 ) : ( 𝑀 × 𝑂 ) ⟶ 𝐵 )
88		ffn	⊢ ( ( 𝑋 𝐹 𝑍 ) : ( 𝑀 × 𝑂 ) ⟶ 𝐵 → ( 𝑋 𝐹 𝑍 ) Fn ( 𝑀 × 𝑂 ) )
89	86 87 88	3syl	⊢ ( 𝜑 → ( 𝑋 𝐹 𝑍 ) Fn ( 𝑀 × 𝑂 ) )
90	89	adantr	⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂 ) ) → ( 𝑋 𝐹 𝑍 ) Fn ( 𝑀 × 𝑂 ) )
91		df-ov	⊢ ( 𝑖 ( 𝑋 𝐹 𝑍 ) 𝑘 ) = ( ( 𝑋 𝐹 𝑍 ) ‘ ⟨ 𝑖 , 𝑘 ⟩ )
92	10	adantr	⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂 ) ) → 𝑍 ∈ ( 𝐵 ↑m ( 𝑁 × 𝑂 ) ) )
93	4 2 3 64 65 54 66 67 92 77 78	mamufv	⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂 ) ) → ( 𝑖 ( 𝑋 𝐹 𝑍 ) 𝑘 ) = ( 𝑅 Σg ( 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 𝑋 𝑗 ) · ( 𝑗 𝑍 𝑘 ) ) ) ) )
94	91 93	eqtr3id	⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂 ) ) → ( ( 𝑋 𝐹 𝑍 ) ‘ ⟨ 𝑖 , 𝑘 ⟩ ) = ( 𝑅 Σg ( 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 𝑋 𝑗 ) · ( 𝑗 𝑍 𝑘 ) ) ) ) )
95	94	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂 ) ) ∧ ⟨ 𝑖 , 𝑘 ⟩ ∈ ( 𝑀 × 𝑂 ) ) → ( ( 𝑋 𝐹 𝑍 ) ‘ ⟨ 𝑖 , 𝑘 ⟩ ) = ( 𝑅 Σg ( 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 𝑋 𝑗 ) · ( 𝑗 𝑍 𝑘 ) ) ) ) )
96	85 55 90 95	ofc1	⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂 ) ) ∧ ⟨ 𝑖 , 𝑘 ⟩ ∈ ( 𝑀 × 𝑂 ) ) → ( ( ( ( 𝑀 × 𝑂 ) × { 𝑌 } ) ∘f · ( 𝑋 𝐹 𝑍 ) ) ‘ ⟨ 𝑖 , 𝑘 ⟩ ) = ( 𝑌 · ( 𝑅 Σg ( 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 𝑋 𝑗 ) · ( 𝑗 𝑍 𝑘 ) ) ) ) ) )
97	82 96	mpdan	⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂 ) ) → ( ( ( ( 𝑀 × 𝑂 ) × { 𝑌 } ) ∘f · ( 𝑋 𝐹 𝑍 ) ) ‘ ⟨ 𝑖 , 𝑘 ⟩ ) = ( 𝑌 · ( 𝑅 Σg ( 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 𝑋 𝑗 ) · ( 𝑗 𝑍 𝑘 ) ) ) ) ) )
98	80 97	eqtrid	⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂 ) ) → ( 𝑖 ( ( ( 𝑀 × 𝑂 ) × { 𝑌 } ) ∘f · ( 𝑋 𝐹 𝑍 ) ) 𝑘 ) = ( 𝑌 · ( 𝑅 Σg ( 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 𝑋 𝑗 ) · ( 𝑗 𝑍 𝑘 ) ) ) ) ) )
99	63 79 98	3eqtr4d	⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑂 ) ) → ( 𝑖 ( 𝑋 𝐹 ( ( ( 𝑁 × 𝑂 ) × { 𝑌 } ) ∘f · 𝑍 ) ) 𝑘 ) = ( 𝑖 ( ( ( 𝑀 × 𝑂 ) × { 𝑌 } ) ∘f · ( 𝑋 𝐹 𝑍 ) ) 𝑘 ) )
100	99	ralrimivva	⊢ ( 𝜑 → ∀ 𝑖 ∈ 𝑀 ∀ 𝑘 ∈ 𝑂 ( 𝑖 ( 𝑋 𝐹 ( ( ( 𝑁 × 𝑂 ) × { 𝑌 } ) ∘f · 𝑍 ) ) 𝑘 ) = ( 𝑖 ( ( ( 𝑀 × 𝑂 ) × { 𝑌 } ) ∘f · ( 𝑋 𝐹 𝑍 ) ) 𝑘 ) )
101	2 52 4 5 6 7 8 75	mamucl	⊢ ( 𝜑 → ( 𝑋 𝐹 ( ( ( 𝑁 × 𝑂 ) × { 𝑌 } ) ∘f · 𝑍 ) ) ∈ ( 𝐵 ↑m ( 𝑀 × 𝑂 ) ) )
102		elmapi	⊢ ( ( 𝑋 𝐹 ( ( ( 𝑁 × 𝑂 ) × { 𝑌 } ) ∘f · 𝑍 ) ) ∈ ( 𝐵 ↑m ( 𝑀 × 𝑂 ) ) → ( 𝑋 𝐹 ( ( ( 𝑁 × 𝑂 ) × { 𝑌 } ) ∘f · 𝑍 ) ) : ( 𝑀 × 𝑂 ) ⟶ 𝐵 )
103		ffn	⊢ ( ( 𝑋 𝐹 ( ( ( 𝑁 × 𝑂 ) × { 𝑌 } ) ∘f · 𝑍 ) ) : ( 𝑀 × 𝑂 ) ⟶ 𝐵 → ( 𝑋 𝐹 ( ( ( 𝑁 × 𝑂 ) × { 𝑌 } ) ∘f · 𝑍 ) ) Fn ( 𝑀 × 𝑂 ) )
104	101 102 103	3syl	⊢ ( 𝜑 → ( 𝑋 𝐹 ( ( ( 𝑁 × 𝑂 ) × { 𝑌 } ) ∘f · 𝑍 ) ) Fn ( 𝑀 × 𝑂 ) )
105		fconst6g	⊢ ( 𝑌 ∈ 𝐵 → ( ( 𝑀 × 𝑂 ) × { 𝑌 } ) : ( 𝑀 × 𝑂 ) ⟶ 𝐵 )
106	9 105	syl	⊢ ( 𝜑 → ( ( 𝑀 × 𝑂 ) × { 𝑌 } ) : ( 𝑀 × 𝑂 ) ⟶ 𝐵 )
107		elmapg	⊢ ( ( 𝐵 ∈ V ∧ ( 𝑀 × 𝑂 ) ∈ Fin ) → ( ( ( 𝑀 × 𝑂 ) × { 𝑌 } ) ∈ ( 𝐵 ↑m ( 𝑀 × 𝑂 ) ) ↔ ( ( 𝑀 × 𝑂 ) × { 𝑌 } ) : ( 𝑀 × 𝑂 ) ⟶ 𝐵 ) )
108	70 84 107	sylancr	⊢ ( 𝜑 → ( ( ( 𝑀 × 𝑂 ) × { 𝑌 } ) ∈ ( 𝐵 ↑m ( 𝑀 × 𝑂 ) ) ↔ ( ( 𝑀 × 𝑂 ) × { 𝑌 } ) : ( 𝑀 × 𝑂 ) ⟶ 𝐵 ) )
109	106 108	mpbird	⊢ ( 𝜑 → ( ( 𝑀 × 𝑂 ) × { 𝑌 } ) ∈ ( 𝐵 ↑m ( 𝑀 × 𝑂 ) ) )
110	2 3	ringvcl	⊢ ( ( 𝑅 ∈ Ring ∧ ( ( 𝑀 × 𝑂 ) × { 𝑌 } ) ∈ ( 𝐵 ↑m ( 𝑀 × 𝑂 ) ) ∧ ( 𝑋 𝐹 𝑍 ) ∈ ( 𝐵 ↑m ( 𝑀 × 𝑂 ) ) ) → ( ( ( 𝑀 × 𝑂 ) × { 𝑌 } ) ∘f · ( 𝑋 𝐹 𝑍 ) ) ∈ ( 𝐵 ↑m ( 𝑀 × 𝑂 ) ) )
111	52 109 86 110	syl3anc	⊢ ( 𝜑 → ( ( ( 𝑀 × 𝑂 ) × { 𝑌 } ) ∘f · ( 𝑋 𝐹 𝑍 ) ) ∈ ( 𝐵 ↑m ( 𝑀 × 𝑂 ) ) )
112		elmapi	⊢ ( ( ( ( 𝑀 × 𝑂 ) × { 𝑌 } ) ∘f · ( 𝑋 𝐹 𝑍 ) ) ∈ ( 𝐵 ↑m ( 𝑀 × 𝑂 ) ) → ( ( ( 𝑀 × 𝑂 ) × { 𝑌 } ) ∘f · ( 𝑋 𝐹 𝑍 ) ) : ( 𝑀 × 𝑂 ) ⟶ 𝐵 )
113		ffn	⊢ ( ( ( ( 𝑀 × 𝑂 ) × { 𝑌 } ) ∘f · ( 𝑋 𝐹 𝑍 ) ) : ( 𝑀 × 𝑂 ) ⟶ 𝐵 → ( ( ( 𝑀 × 𝑂 ) × { 𝑌 } ) ∘f · ( 𝑋 𝐹 𝑍 ) ) Fn ( 𝑀 × 𝑂 ) )
114	111 112 113	3syl	⊢ ( 𝜑 → ( ( ( 𝑀 × 𝑂 ) × { 𝑌 } ) ∘f · ( 𝑋 𝐹 𝑍 ) ) Fn ( 𝑀 × 𝑂 ) )
115		eqfnov2	⊢ ( ( ( 𝑋 𝐹 ( ( ( 𝑁 × 𝑂 ) × { 𝑌 } ) ∘f · 𝑍 ) ) Fn ( 𝑀 × 𝑂 ) ∧ ( ( ( 𝑀 × 𝑂 ) × { 𝑌 } ) ∘f · ( 𝑋 𝐹 𝑍 ) ) Fn ( 𝑀 × 𝑂 ) ) → ( ( 𝑋 𝐹 ( ( ( 𝑁 × 𝑂 ) × { 𝑌 } ) ∘f · 𝑍 ) ) = ( ( ( 𝑀 × 𝑂 ) × { 𝑌 } ) ∘f · ( 𝑋 𝐹 𝑍 ) ) ↔ ∀ 𝑖 ∈ 𝑀 ∀ 𝑘 ∈ 𝑂 ( 𝑖 ( 𝑋 𝐹 ( ( ( 𝑁 × 𝑂 ) × { 𝑌 } ) ∘f · 𝑍 ) ) 𝑘 ) = ( 𝑖 ( ( ( 𝑀 × 𝑂 ) × { 𝑌 } ) ∘f · ( 𝑋 𝐹 𝑍 ) ) 𝑘 ) ) )
116	104 114 115	syl2anc	⊢ ( 𝜑 → ( ( 𝑋 𝐹 ( ( ( 𝑁 × 𝑂 ) × { 𝑌 } ) ∘f · 𝑍 ) ) = ( ( ( 𝑀 × 𝑂 ) × { 𝑌 } ) ∘f · ( 𝑋 𝐹 𝑍 ) ) ↔ ∀ 𝑖 ∈ 𝑀 ∀ 𝑘 ∈ 𝑂 ( 𝑖 ( 𝑋 𝐹 ( ( ( 𝑁 × 𝑂 ) × { 𝑌 } ) ∘f · 𝑍 ) ) 𝑘 ) = ( 𝑖 ( ( ( 𝑀 × 𝑂 ) × { 𝑌 } ) ∘f · ( 𝑋 𝐹 𝑍 ) ) 𝑘 ) ) )
117	100 116	mpbird	⊢ ( 𝜑 → ( 𝑋 𝐹 ( ( ( 𝑁 × 𝑂 ) × { 𝑌 } ) ∘f · 𝑍 ) ) = ( ( ( 𝑀 × 𝑂 ) × { 𝑌 } ) ∘f · ( 𝑋 𝐹 𝑍 ) ) )