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