Metamath Proof Explorer


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 syl5eq ( ( ( 𝜑 ∧ ( 𝑖𝑀𝑘𝑂 ) ) ∧ 𝑗𝑁 ) → ( 𝑗 ( ( ( 𝑁 × 𝑂 ) × { 𝑌 } ) ∘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 fovrnd ( ( ( 𝜑 ∧ ( 𝑖𝑀𝑘𝑂 ) ) ∧ 𝑗𝑁 ) → ( 𝑖 𝑋 𝑗 ) ∈ 𝐵 )
40 10 20 syl ( 𝜑𝑍 : ( 𝑁 × 𝑂 ) ⟶ 𝐵 )
41 40 ad2antrr ( ( ( 𝜑 ∧ ( 𝑖𝑀𝑘𝑂 ) ) ∧ 𝑗𝑁 ) → 𝑍 : ( 𝑁 × 𝑂 ) ⟶ 𝐵 )
42 41 12 13 fovrnd ( ( ( 𝜑 ∧ ( 𝑖𝑀𝑘𝑂 ) ) ∧ 𝑗𝑁 ) → ( 𝑗 𝑍 𝑘 ) ∈ 𝐵 )
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 eqid ( +g𝑅 ) = ( +g𝑅 )
52 crngring ( 𝑅 ∈ CRing → 𝑅 ∈ Ring )
53 1 52 syl ( 𝜑𝑅 ∈ Ring )
54 53 adantr ( ( 𝜑 ∧ ( 𝑖𝑀𝑘𝑂 ) ) → 𝑅 ∈ Ring )
55 6 adantr ( ( 𝜑 ∧ ( 𝑖𝑀𝑘𝑂 ) ) → 𝑁 ∈ Fin )
56 9 adantr ( ( 𝜑 ∧ ( 𝑖𝑀𝑘𝑂 ) ) → 𝑌𝐵 )
57 53 ad2antrr ( ( ( 𝜑 ∧ ( 𝑖𝑀𝑘𝑂 ) ) ∧ 𝑗𝑁 ) → 𝑅 ∈ Ring )
58 2 3 ringcl ( ( 𝑅 ∈ Ring ∧ ( 𝑖 𝑋 𝑗 ) ∈ 𝐵 ∧ ( 𝑗 𝑍 𝑘 ) ∈ 𝐵 ) → ( ( 𝑖 𝑋 𝑗 ) · ( 𝑗 𝑍 𝑘 ) ) ∈ 𝐵 )
59 57 39 42 58 syl3anc ( ( ( 𝜑 ∧ ( 𝑖𝑀𝑘𝑂 ) ) ∧ 𝑗𝑁 ) → ( ( 𝑖 𝑋 𝑗 ) · ( 𝑗 𝑍 𝑘 ) ) ∈ 𝐵 )
60 eqid ( 𝑗𝑁 ↦ ( ( 𝑖 𝑋 𝑗 ) · ( 𝑗 𝑍 𝑘 ) ) ) = ( 𝑗𝑁 ↦ ( ( 𝑖 𝑋 𝑗 ) · ( 𝑗 𝑍 𝑘 ) ) )
61 ovexd ( ( ( 𝜑 ∧ ( 𝑖𝑀𝑘𝑂 ) ) ∧ 𝑗𝑁 ) → ( ( 𝑖 𝑋 𝑗 ) · ( 𝑗 𝑍 𝑘 ) ) ∈ V )
62 fvexd ( ( 𝜑 ∧ ( 𝑖𝑀𝑘𝑂 ) ) → ( 0g𝑅 ) ∈ V )
63 60 55 61 62 fsuppmptdm ( ( 𝜑 ∧ ( 𝑖𝑀𝑘𝑂 ) ) → ( 𝑗𝑁 ↦ ( ( 𝑖 𝑋 𝑗 ) · ( 𝑗 𝑍 𝑘 ) ) ) finSupp ( 0g𝑅 ) )
64 2 50 51 3 54 55 56 59 63 gsummulc2 ( ( 𝜑 ∧ ( 𝑖𝑀𝑘𝑂 ) ) → ( 𝑅 Σg ( 𝑗𝑁 ↦ ( 𝑌 · ( ( 𝑖 𝑋 𝑗 ) · ( 𝑗 𝑍 𝑘 ) ) ) ) ) = ( 𝑌 · ( 𝑅 Σg ( 𝑗𝑁 ↦ ( ( 𝑖 𝑋 𝑗 ) · ( 𝑗 𝑍 𝑘 ) ) ) ) ) )
65 49 64 eqtrd ( ( 𝜑 ∧ ( 𝑖𝑀𝑘𝑂 ) ) → ( 𝑅 Σg ( 𝑗𝑁 ↦ ( ( 𝑖 𝑋 𝑗 ) · ( 𝑗 ( ( ( 𝑁 × 𝑂 ) × { 𝑌 } ) ∘f · 𝑍 ) 𝑘 ) ) ) ) = ( 𝑌 · ( 𝑅 Σg ( 𝑗𝑁 ↦ ( ( 𝑖 𝑋 𝑗 ) · ( 𝑗 𝑍 𝑘 ) ) ) ) ) )
66 1 adantr ( ( 𝜑 ∧ ( 𝑖𝑀𝑘𝑂 ) ) → 𝑅 ∈ CRing )
67 5 adantr ( ( 𝜑 ∧ ( 𝑖𝑀𝑘𝑂 ) ) → 𝑀 ∈ Fin )
68 7 adantr ( ( 𝜑 ∧ ( 𝑖𝑀𝑘𝑂 ) ) → 𝑂 ∈ Fin )
69 8 adantr ( ( 𝜑 ∧ ( 𝑖𝑀𝑘𝑂 ) ) → 𝑋 ∈ ( 𝐵m ( 𝑀 × 𝑁 ) ) )
70 fconst6g ( 𝑌𝐵 → ( ( 𝑁 × 𝑂 ) × { 𝑌 } ) : ( 𝑁 × 𝑂 ) ⟶ 𝐵 )
71 9 70 syl ( 𝜑 → ( ( 𝑁 × 𝑂 ) × { 𝑌 } ) : ( 𝑁 × 𝑂 ) ⟶ 𝐵 )
72 2 fvexi 𝐵 ∈ V
73 elmapg ( ( 𝐵 ∈ V ∧ ( 𝑁 × 𝑂 ) ∈ Fin ) → ( ( ( 𝑁 × 𝑂 ) × { 𝑌 } ) ∈ ( 𝐵m ( 𝑁 × 𝑂 ) ) ↔ ( ( 𝑁 × 𝑂 ) × { 𝑌 } ) : ( 𝑁 × 𝑂 ) ⟶ 𝐵 ) )
74 72 17 73 sylancr ( 𝜑 → ( ( ( 𝑁 × 𝑂 ) × { 𝑌 } ) ∈ ( 𝐵m ( 𝑁 × 𝑂 ) ) ↔ ( ( 𝑁 × 𝑂 ) × { 𝑌 } ) : ( 𝑁 × 𝑂 ) ⟶ 𝐵 ) )
75 71 74 mpbird ( 𝜑 → ( ( 𝑁 × 𝑂 ) × { 𝑌 } ) ∈ ( 𝐵m ( 𝑁 × 𝑂 ) ) )
76 2 3 ringvcl ( ( 𝑅 ∈ Ring ∧ ( ( 𝑁 × 𝑂 ) × { 𝑌 } ) ∈ ( 𝐵m ( 𝑁 × 𝑂 ) ) ∧ 𝑍 ∈ ( 𝐵m ( 𝑁 × 𝑂 ) ) ) → ( ( ( 𝑁 × 𝑂 ) × { 𝑌 } ) ∘f · 𝑍 ) ∈ ( 𝐵m ( 𝑁 × 𝑂 ) ) )
77 53 75 10 76 syl3anc ( 𝜑 → ( ( ( 𝑁 × 𝑂 ) × { 𝑌 } ) ∘f · 𝑍 ) ∈ ( 𝐵m ( 𝑁 × 𝑂 ) ) )
78 77 adantr ( ( 𝜑 ∧ ( 𝑖𝑀𝑘𝑂 ) ) → ( ( ( 𝑁 × 𝑂 ) × { 𝑌 } ) ∘f · 𝑍 ) ∈ ( 𝐵m ( 𝑁 × 𝑂 ) ) )
79 simprl ( ( 𝜑 ∧ ( 𝑖𝑀𝑘𝑂 ) ) → 𝑖𝑀 )
80 simprr ( ( 𝜑 ∧ ( 𝑖𝑀𝑘𝑂 ) ) → 𝑘𝑂 )
81 4 2 3 66 67 55 68 69 78 79 80 mamufv ( ( 𝜑 ∧ ( 𝑖𝑀𝑘𝑂 ) ) → ( 𝑖 ( 𝑋 𝐹 ( ( ( 𝑁 × 𝑂 ) × { 𝑌 } ) ∘f · 𝑍 ) ) 𝑘 ) = ( 𝑅 Σg ( 𝑗𝑁 ↦ ( ( 𝑖 𝑋 𝑗 ) · ( 𝑗 ( ( ( 𝑁 × 𝑂 ) × { 𝑌 } ) ∘f · 𝑍 ) 𝑘 ) ) ) ) )
82 df-ov ( 𝑖 ( ( ( 𝑀 × 𝑂 ) × { 𝑌 } ) ∘f · ( 𝑋 𝐹 𝑍 ) ) 𝑘 ) = ( ( ( ( 𝑀 × 𝑂 ) × { 𝑌 } ) ∘f · ( 𝑋 𝐹 𝑍 ) ) ‘ ⟨ 𝑖 , 𝑘 ⟩ )
83 opelxpi ( ( 𝑖𝑀𝑘𝑂 ) → ⟨ 𝑖 , 𝑘 ⟩ ∈ ( 𝑀 × 𝑂 ) )
84 83 adantl ( ( 𝜑 ∧ ( 𝑖𝑀𝑘𝑂 ) ) → ⟨ 𝑖 , 𝑘 ⟩ ∈ ( 𝑀 × 𝑂 ) )
85 xpfi ( ( 𝑀 ∈ Fin ∧ 𝑂 ∈ Fin ) → ( 𝑀 × 𝑂 ) ∈ Fin )
86 5 7 85 syl2anc ( 𝜑 → ( 𝑀 × 𝑂 ) ∈ Fin )
87 86 adantr ( ( 𝜑 ∧ ( 𝑖𝑀𝑘𝑂 ) ) → ( 𝑀 × 𝑂 ) ∈ Fin )
88 2 53 4 5 6 7 8 10 mamucl ( 𝜑 → ( 𝑋 𝐹 𝑍 ) ∈ ( 𝐵m ( 𝑀 × 𝑂 ) ) )
89 elmapi ( ( 𝑋 𝐹 𝑍 ) ∈ ( 𝐵m ( 𝑀 × 𝑂 ) ) → ( 𝑋 𝐹 𝑍 ) : ( 𝑀 × 𝑂 ) ⟶ 𝐵 )
90 ffn ( ( 𝑋 𝐹 𝑍 ) : ( 𝑀 × 𝑂 ) ⟶ 𝐵 → ( 𝑋 𝐹 𝑍 ) Fn ( 𝑀 × 𝑂 ) )
91 88 89 90 3syl ( 𝜑 → ( 𝑋 𝐹 𝑍 ) Fn ( 𝑀 × 𝑂 ) )
92 91 adantr ( ( 𝜑 ∧ ( 𝑖𝑀𝑘𝑂 ) ) → ( 𝑋 𝐹 𝑍 ) Fn ( 𝑀 × 𝑂 ) )
93 df-ov ( 𝑖 ( 𝑋 𝐹 𝑍 ) 𝑘 ) = ( ( 𝑋 𝐹 𝑍 ) ‘ ⟨ 𝑖 , 𝑘 ⟩ )
94 10 adantr ( ( 𝜑 ∧ ( 𝑖𝑀𝑘𝑂 ) ) → 𝑍 ∈ ( 𝐵m ( 𝑁 × 𝑂 ) ) )
95 4 2 3 66 67 55 68 69 94 79 80 mamufv ( ( 𝜑 ∧ ( 𝑖𝑀𝑘𝑂 ) ) → ( 𝑖 ( 𝑋 𝐹 𝑍 ) 𝑘 ) = ( 𝑅 Σg ( 𝑗𝑁 ↦ ( ( 𝑖 𝑋 𝑗 ) · ( 𝑗 𝑍 𝑘 ) ) ) ) )
96 93 95 eqtr3id ( ( 𝜑 ∧ ( 𝑖𝑀𝑘𝑂 ) ) → ( ( 𝑋 𝐹 𝑍 ) ‘ ⟨ 𝑖 , 𝑘 ⟩ ) = ( 𝑅 Σg ( 𝑗𝑁 ↦ ( ( 𝑖 𝑋 𝑗 ) · ( 𝑗 𝑍 𝑘 ) ) ) ) )
97 96 adantr ( ( ( 𝜑 ∧ ( 𝑖𝑀𝑘𝑂 ) ) ∧ ⟨ 𝑖 , 𝑘 ⟩ ∈ ( 𝑀 × 𝑂 ) ) → ( ( 𝑋 𝐹 𝑍 ) ‘ ⟨ 𝑖 , 𝑘 ⟩ ) = ( 𝑅 Σg ( 𝑗𝑁 ↦ ( ( 𝑖 𝑋 𝑗 ) · ( 𝑗 𝑍 𝑘 ) ) ) ) )
98 87 56 92 97 ofc1 ( ( ( 𝜑 ∧ ( 𝑖𝑀𝑘𝑂 ) ) ∧ ⟨ 𝑖 , 𝑘 ⟩ ∈ ( 𝑀 × 𝑂 ) ) → ( ( ( ( 𝑀 × 𝑂 ) × { 𝑌 } ) ∘f · ( 𝑋 𝐹 𝑍 ) ) ‘ ⟨ 𝑖 , 𝑘 ⟩ ) = ( 𝑌 · ( 𝑅 Σg ( 𝑗𝑁 ↦ ( ( 𝑖 𝑋 𝑗 ) · ( 𝑗 𝑍 𝑘 ) ) ) ) ) )
99 84 98 mpdan ( ( 𝜑 ∧ ( 𝑖𝑀𝑘𝑂 ) ) → ( ( ( ( 𝑀 × 𝑂 ) × { 𝑌 } ) ∘f · ( 𝑋 𝐹 𝑍 ) ) ‘ ⟨ 𝑖 , 𝑘 ⟩ ) = ( 𝑌 · ( 𝑅 Σg ( 𝑗𝑁 ↦ ( ( 𝑖 𝑋 𝑗 ) · ( 𝑗 𝑍 𝑘 ) ) ) ) ) )
100 82 99 syl5eq ( ( 𝜑 ∧ ( 𝑖𝑀𝑘𝑂 ) ) → ( 𝑖 ( ( ( 𝑀 × 𝑂 ) × { 𝑌 } ) ∘f · ( 𝑋 𝐹 𝑍 ) ) 𝑘 ) = ( 𝑌 · ( 𝑅 Σg ( 𝑗𝑁 ↦ ( ( 𝑖 𝑋 𝑗 ) · ( 𝑗 𝑍 𝑘 ) ) ) ) ) )
101 65 81 100 3eqtr4d ( ( 𝜑 ∧ ( 𝑖𝑀𝑘𝑂 ) ) → ( 𝑖 ( 𝑋 𝐹 ( ( ( 𝑁 × 𝑂 ) × { 𝑌 } ) ∘f · 𝑍 ) ) 𝑘 ) = ( 𝑖 ( ( ( 𝑀 × 𝑂 ) × { 𝑌 } ) ∘f · ( 𝑋 𝐹 𝑍 ) ) 𝑘 ) )
102 101 ralrimivva ( 𝜑 → ∀ 𝑖𝑀𝑘𝑂 ( 𝑖 ( 𝑋 𝐹 ( ( ( 𝑁 × 𝑂 ) × { 𝑌 } ) ∘f · 𝑍 ) ) 𝑘 ) = ( 𝑖 ( ( ( 𝑀 × 𝑂 ) × { 𝑌 } ) ∘f · ( 𝑋 𝐹 𝑍 ) ) 𝑘 ) )
103 2 53 4 5 6 7 8 77 mamucl ( 𝜑 → ( 𝑋 𝐹 ( ( ( 𝑁 × 𝑂 ) × { 𝑌 } ) ∘f · 𝑍 ) ) ∈ ( 𝐵m ( 𝑀 × 𝑂 ) ) )
104 elmapi ( ( 𝑋 𝐹 ( ( ( 𝑁 × 𝑂 ) × { 𝑌 } ) ∘f · 𝑍 ) ) ∈ ( 𝐵m ( 𝑀 × 𝑂 ) ) → ( 𝑋 𝐹 ( ( ( 𝑁 × 𝑂 ) × { 𝑌 } ) ∘f · 𝑍 ) ) : ( 𝑀 × 𝑂 ) ⟶ 𝐵 )
105 ffn ( ( 𝑋 𝐹 ( ( ( 𝑁 × 𝑂 ) × { 𝑌 } ) ∘f · 𝑍 ) ) : ( 𝑀 × 𝑂 ) ⟶ 𝐵 → ( 𝑋 𝐹 ( ( ( 𝑁 × 𝑂 ) × { 𝑌 } ) ∘f · 𝑍 ) ) Fn ( 𝑀 × 𝑂 ) )
106 103 104 105 3syl ( 𝜑 → ( 𝑋 𝐹 ( ( ( 𝑁 × 𝑂 ) × { 𝑌 } ) ∘f · 𝑍 ) ) Fn ( 𝑀 × 𝑂 ) )
107 fconst6g ( 𝑌𝐵 → ( ( 𝑀 × 𝑂 ) × { 𝑌 } ) : ( 𝑀 × 𝑂 ) ⟶ 𝐵 )
108 9 107 syl ( 𝜑 → ( ( 𝑀 × 𝑂 ) × { 𝑌 } ) : ( 𝑀 × 𝑂 ) ⟶ 𝐵 )
109 elmapg ( ( 𝐵 ∈ V ∧ ( 𝑀 × 𝑂 ) ∈ Fin ) → ( ( ( 𝑀 × 𝑂 ) × { 𝑌 } ) ∈ ( 𝐵m ( 𝑀 × 𝑂 ) ) ↔ ( ( 𝑀 × 𝑂 ) × { 𝑌 } ) : ( 𝑀 × 𝑂 ) ⟶ 𝐵 ) )
110 72 86 109 sylancr ( 𝜑 → ( ( ( 𝑀 × 𝑂 ) × { 𝑌 } ) ∈ ( 𝐵m ( 𝑀 × 𝑂 ) ) ↔ ( ( 𝑀 × 𝑂 ) × { 𝑌 } ) : ( 𝑀 × 𝑂 ) ⟶ 𝐵 ) )
111 108 110 mpbird ( 𝜑 → ( ( 𝑀 × 𝑂 ) × { 𝑌 } ) ∈ ( 𝐵m ( 𝑀 × 𝑂 ) ) )
112 2 3 ringvcl ( ( 𝑅 ∈ Ring ∧ ( ( 𝑀 × 𝑂 ) × { 𝑌 } ) ∈ ( 𝐵m ( 𝑀 × 𝑂 ) ) ∧ ( 𝑋 𝐹 𝑍 ) ∈ ( 𝐵m ( 𝑀 × 𝑂 ) ) ) → ( ( ( 𝑀 × 𝑂 ) × { 𝑌 } ) ∘f · ( 𝑋 𝐹 𝑍 ) ) ∈ ( 𝐵m ( 𝑀 × 𝑂 ) ) )
113 53 111 88 112 syl3anc ( 𝜑 → ( ( ( 𝑀 × 𝑂 ) × { 𝑌 } ) ∘f · ( 𝑋 𝐹 𝑍 ) ) ∈ ( 𝐵m ( 𝑀 × 𝑂 ) ) )
114 elmapi ( ( ( ( 𝑀 × 𝑂 ) × { 𝑌 } ) ∘f · ( 𝑋 𝐹 𝑍 ) ) ∈ ( 𝐵m ( 𝑀 × 𝑂 ) ) → ( ( ( 𝑀 × 𝑂 ) × { 𝑌 } ) ∘f · ( 𝑋 𝐹 𝑍 ) ) : ( 𝑀 × 𝑂 ) ⟶ 𝐵 )
115 ffn ( ( ( ( 𝑀 × 𝑂 ) × { 𝑌 } ) ∘f · ( 𝑋 𝐹 𝑍 ) ) : ( 𝑀 × 𝑂 ) ⟶ 𝐵 → ( ( ( 𝑀 × 𝑂 ) × { 𝑌 } ) ∘f · ( 𝑋 𝐹 𝑍 ) ) Fn ( 𝑀 × 𝑂 ) )
116 113 114 115 3syl ( 𝜑 → ( ( ( 𝑀 × 𝑂 ) × { 𝑌 } ) ∘f · ( 𝑋 𝐹 𝑍 ) ) Fn ( 𝑀 × 𝑂 ) )
117 eqfnov2 ( ( ( 𝑋 𝐹 ( ( ( 𝑁 × 𝑂 ) × { 𝑌 } ) ∘f · 𝑍 ) ) Fn ( 𝑀 × 𝑂 ) ∧ ( ( ( 𝑀 × 𝑂 ) × { 𝑌 } ) ∘f · ( 𝑋 𝐹 𝑍 ) ) Fn ( 𝑀 × 𝑂 ) ) → ( ( 𝑋 𝐹 ( ( ( 𝑁 × 𝑂 ) × { 𝑌 } ) ∘f · 𝑍 ) ) = ( ( ( 𝑀 × 𝑂 ) × { 𝑌 } ) ∘f · ( 𝑋 𝐹 𝑍 ) ) ↔ ∀ 𝑖𝑀𝑘𝑂 ( 𝑖 ( 𝑋 𝐹 ( ( ( 𝑁 × 𝑂 ) × { 𝑌 } ) ∘f · 𝑍 ) ) 𝑘 ) = ( 𝑖 ( ( ( 𝑀 × 𝑂 ) × { 𝑌 } ) ∘f · ( 𝑋 𝐹 𝑍 ) ) 𝑘 ) ) )
118 106 116 117 syl2anc ( 𝜑 → ( ( 𝑋 𝐹 ( ( ( 𝑁 × 𝑂 ) × { 𝑌 } ) ∘f · 𝑍 ) ) = ( ( ( 𝑀 × 𝑂 ) × { 𝑌 } ) ∘f · ( 𝑋 𝐹 𝑍 ) ) ↔ ∀ 𝑖𝑀𝑘𝑂 ( 𝑖 ( 𝑋 𝐹 ( ( ( 𝑁 × 𝑂 ) × { 𝑌 } ) ∘f · 𝑍 ) ) 𝑘 ) = ( 𝑖 ( ( ( 𝑀 × 𝑂 ) × { 𝑌 } ) ∘f · ( 𝑋 𝐹 𝑍 ) ) 𝑘 ) ) )
119 102 118 mpbird ( 𝜑 → ( 𝑋 𝐹 ( ( ( 𝑁 × 𝑂 ) × { 𝑌 } ) ∘f · 𝑍 ) ) = ( ( ( 𝑀 × 𝑂 ) × { 𝑌 } ) ∘f · ( 𝑋 𝐹 𝑍 ) ) )