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 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 · ( 𝑋 𝐹 𝑍 ) ) )