Metamath Proof Explorer

Theorem mamuvs1

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

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

Proof

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