Metamath Proof Explorer


Theorem mamudi

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

Ref Expression
Hypotheses mamucl.b 𝐵 = ( Base ‘ 𝑅 )
mamucl.r ( 𝜑𝑅 ∈ Ring )
mamudi.f 𝐹 = ( 𝑅 maMul ⟨ 𝑀 , 𝑁 , 𝑂 ⟩ )
mamudi.m ( 𝜑𝑀 ∈ Fin )
mamudi.n ( 𝜑𝑁 ∈ Fin )
mamudi.o ( 𝜑𝑂 ∈ Fin )
mamudi.p + = ( +g𝑅 )
mamudi.x ( 𝜑𝑋 ∈ ( 𝐵m ( 𝑀 × 𝑁 ) ) )
mamudi.y ( 𝜑𝑌 ∈ ( 𝐵m ( 𝑀 × 𝑁 ) ) )
mamudi.z ( 𝜑𝑍 ∈ ( 𝐵m ( 𝑁 × 𝑂 ) ) )
Assertion mamudi ( 𝜑 → ( ( 𝑋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 mamudi.p + = ( +g𝑅 )
8 mamudi.x ( 𝜑𝑋 ∈ ( 𝐵m ( 𝑀 × 𝑁 ) ) )
9 mamudi.y ( 𝜑𝑌 ∈ ( 𝐵m ( 𝑀 × 𝑁 ) ) )
10 mamudi.z ( 𝜑𝑍 ∈ ( 𝐵m ( 𝑁 × 𝑂 ) ) )
11 ringcmn ( 𝑅 ∈ Ring → 𝑅 ∈ CMnd )
12 2 11 syl ( 𝜑𝑅 ∈ CMnd )
13 12 adantr ( ( 𝜑 ∧ ( 𝑖𝑀𝑘𝑂 ) ) → 𝑅 ∈ CMnd )
14 5 adantr ( ( 𝜑 ∧ ( 𝑖𝑀𝑘𝑂 ) ) → 𝑁 ∈ Fin )
15 2 ad2antrr ( ( ( 𝜑 ∧ ( 𝑖𝑀𝑘𝑂 ) ) ∧ 𝑗𝑁 ) → 𝑅 ∈ Ring )
16 elmapi ( 𝑋 ∈ ( 𝐵m ( 𝑀 × 𝑁 ) ) → 𝑋 : ( 𝑀 × 𝑁 ) ⟶ 𝐵 )
17 8 16 syl ( 𝜑𝑋 : ( 𝑀 × 𝑁 ) ⟶ 𝐵 )
18 17 ad2antrr ( ( ( 𝜑 ∧ ( 𝑖𝑀𝑘𝑂 ) ) ∧ 𝑗𝑁 ) → 𝑋 : ( 𝑀 × 𝑁 ) ⟶ 𝐵 )
19 simplrl ( ( ( 𝜑 ∧ ( 𝑖𝑀𝑘𝑂 ) ) ∧ 𝑗𝑁 ) → 𝑖𝑀 )
20 simpr ( ( ( 𝜑 ∧ ( 𝑖𝑀𝑘𝑂 ) ) ∧ 𝑗𝑁 ) → 𝑗𝑁 )
21 18 19 20 fovrnd ( ( ( 𝜑 ∧ ( 𝑖𝑀𝑘𝑂 ) ) ∧ 𝑗𝑁 ) → ( 𝑖 𝑋 𝑗 ) ∈ 𝐵 )
22 elmapi ( 𝑍 ∈ ( 𝐵m ( 𝑁 × 𝑂 ) ) → 𝑍 : ( 𝑁 × 𝑂 ) ⟶ 𝐵 )
23 10 22 syl ( 𝜑𝑍 : ( 𝑁 × 𝑂 ) ⟶ 𝐵 )
24 23 ad2antrr ( ( ( 𝜑 ∧ ( 𝑖𝑀𝑘𝑂 ) ) ∧ 𝑗𝑁 ) → 𝑍 : ( 𝑁 × 𝑂 ) ⟶ 𝐵 )
25 simplrr ( ( ( 𝜑 ∧ ( 𝑖𝑀𝑘𝑂 ) ) ∧ 𝑗𝑁 ) → 𝑘𝑂 )
26 24 20 25 fovrnd ( ( ( 𝜑 ∧ ( 𝑖𝑀𝑘𝑂 ) ) ∧ 𝑗𝑁 ) → ( 𝑗 𝑍 𝑘 ) ∈ 𝐵 )
27 eqid ( .r𝑅 ) = ( .r𝑅 )
28 1 27 ringcl ( ( 𝑅 ∈ Ring ∧ ( 𝑖 𝑋 𝑗 ) ∈ 𝐵 ∧ ( 𝑗 𝑍 𝑘 ) ∈ 𝐵 ) → ( ( 𝑖 𝑋 𝑗 ) ( .r𝑅 ) ( 𝑗 𝑍 𝑘 ) ) ∈ 𝐵 )
29 15 21 26 28 syl3anc ( ( ( 𝜑 ∧ ( 𝑖𝑀𝑘𝑂 ) ) ∧ 𝑗𝑁 ) → ( ( 𝑖 𝑋 𝑗 ) ( .r𝑅 ) ( 𝑗 𝑍 𝑘 ) ) ∈ 𝐵 )
30 elmapi ( 𝑌 ∈ ( 𝐵m ( 𝑀 × 𝑁 ) ) → 𝑌 : ( 𝑀 × 𝑁 ) ⟶ 𝐵 )
31 9 30 syl ( 𝜑𝑌 : ( 𝑀 × 𝑁 ) ⟶ 𝐵 )
32 31 ad2antrr ( ( ( 𝜑 ∧ ( 𝑖𝑀𝑘𝑂 ) ) ∧ 𝑗𝑁 ) → 𝑌 : ( 𝑀 × 𝑁 ) ⟶ 𝐵 )
33 32 19 20 fovrnd ( ( ( 𝜑 ∧ ( 𝑖𝑀𝑘𝑂 ) ) ∧ 𝑗𝑁 ) → ( 𝑖 𝑌 𝑗 ) ∈ 𝐵 )
34 1 27 ringcl ( ( 𝑅 ∈ Ring ∧ ( 𝑖 𝑌 𝑗 ) ∈ 𝐵 ∧ ( 𝑗 𝑍 𝑘 ) ∈ 𝐵 ) → ( ( 𝑖 𝑌 𝑗 ) ( .r𝑅 ) ( 𝑗 𝑍 𝑘 ) ) ∈ 𝐵 )
35 15 33 26 34 syl3anc ( ( ( 𝜑 ∧ ( 𝑖𝑀𝑘𝑂 ) ) ∧ 𝑗𝑁 ) → ( ( 𝑖 𝑌 𝑗 ) ( .r𝑅 ) ( 𝑗 𝑍 𝑘 ) ) ∈ 𝐵 )
36 eqid ( 𝑗𝑁 ↦ ( ( 𝑖 𝑋 𝑗 ) ( .r𝑅 ) ( 𝑗 𝑍 𝑘 ) ) ) = ( 𝑗𝑁 ↦ ( ( 𝑖 𝑋 𝑗 ) ( .r𝑅 ) ( 𝑗 𝑍 𝑘 ) ) )
37 eqid ( 𝑗𝑁 ↦ ( ( 𝑖 𝑌 𝑗 ) ( .r𝑅 ) ( 𝑗 𝑍 𝑘 ) ) ) = ( 𝑗𝑁 ↦ ( ( 𝑖 𝑌 𝑗 ) ( .r𝑅 ) ( 𝑗 𝑍 𝑘 ) ) )
38 1 7 13 14 29 35 36 37 gsummptfidmadd2 ( ( 𝜑 ∧ ( 𝑖𝑀𝑘𝑂 ) ) → ( 𝑅 Σg ( ( 𝑗𝑁 ↦ ( ( 𝑖 𝑋 𝑗 ) ( .r𝑅 ) ( 𝑗 𝑍 𝑘 ) ) ) ∘f + ( 𝑗𝑁 ↦ ( ( 𝑖 𝑌 𝑗 ) ( .r𝑅 ) ( 𝑗 𝑍 𝑘 ) ) ) ) ) = ( ( 𝑅 Σg ( 𝑗𝑁 ↦ ( ( 𝑖 𝑋 𝑗 ) ( .r𝑅 ) ( 𝑗 𝑍 𝑘 ) ) ) ) + ( 𝑅 Σg ( 𝑗𝑁 ↦ ( ( 𝑖 𝑌 𝑗 ) ( .r𝑅 ) ( 𝑗 𝑍 𝑘 ) ) ) ) ) )
39 8 ad2antrr ( ( ( 𝜑 ∧ ( 𝑖𝑀𝑘𝑂 ) ) ∧ 𝑗𝑁 ) → 𝑋 ∈ ( 𝐵m ( 𝑀 × 𝑁 ) ) )
40 ffn ( 𝑋 : ( 𝑀 × 𝑁 ) ⟶ 𝐵𝑋 Fn ( 𝑀 × 𝑁 ) )
41 39 16 40 3syl ( ( ( 𝜑 ∧ ( 𝑖𝑀𝑘𝑂 ) ) ∧ 𝑗𝑁 ) → 𝑋 Fn ( 𝑀 × 𝑁 ) )
42 9 ad2antrr ( ( ( 𝜑 ∧ ( 𝑖𝑀𝑘𝑂 ) ) ∧ 𝑗𝑁 ) → 𝑌 ∈ ( 𝐵m ( 𝑀 × 𝑁 ) ) )
43 ffn ( 𝑌 : ( 𝑀 × 𝑁 ) ⟶ 𝐵𝑌 Fn ( 𝑀 × 𝑁 ) )
44 42 30 43 3syl ( ( ( 𝜑 ∧ ( 𝑖𝑀𝑘𝑂 ) ) ∧ 𝑗𝑁 ) → 𝑌 Fn ( 𝑀 × 𝑁 ) )
45 xpfi ( ( 𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ) → ( 𝑀 × 𝑁 ) ∈ Fin )
46 4 5 45 syl2anc ( 𝜑 → ( 𝑀 × 𝑁 ) ∈ Fin )
47 46 ad2antrr ( ( ( 𝜑 ∧ ( 𝑖𝑀𝑘𝑂 ) ) ∧ 𝑗𝑁 ) → ( 𝑀 × 𝑁 ) ∈ Fin )
48 opelxpi ( ( 𝑖𝑀𝑗𝑁 ) → ⟨ 𝑖 , 𝑗 ⟩ ∈ ( 𝑀 × 𝑁 ) )
49 48 adantlr ( ( ( 𝑖𝑀𝑘𝑂 ) ∧ 𝑗𝑁 ) → ⟨ 𝑖 , 𝑗 ⟩ ∈ ( 𝑀 × 𝑁 ) )
50 49 adantll ( ( ( 𝜑 ∧ ( 𝑖𝑀𝑘𝑂 ) ) ∧ 𝑗𝑁 ) → ⟨ 𝑖 , 𝑗 ⟩ ∈ ( 𝑀 × 𝑁 ) )
51 fnfvof ( ( ( 𝑋 Fn ( 𝑀 × 𝑁 ) ∧ 𝑌 Fn ( 𝑀 × 𝑁 ) ) ∧ ( ( 𝑀 × 𝑁 ) ∈ Fin ∧ ⟨ 𝑖 , 𝑗 ⟩ ∈ ( 𝑀 × 𝑁 ) ) ) → ( ( 𝑋f + 𝑌 ) ‘ ⟨ 𝑖 , 𝑗 ⟩ ) = ( ( 𝑋 ‘ ⟨ 𝑖 , 𝑗 ⟩ ) + ( 𝑌 ‘ ⟨ 𝑖 , 𝑗 ⟩ ) ) )
52 41 44 47 50 51 syl22anc ( ( ( 𝜑 ∧ ( 𝑖𝑀𝑘𝑂 ) ) ∧ 𝑗𝑁 ) → ( ( 𝑋f + 𝑌 ) ‘ ⟨ 𝑖 , 𝑗 ⟩ ) = ( ( 𝑋 ‘ ⟨ 𝑖 , 𝑗 ⟩ ) + ( 𝑌 ‘ ⟨ 𝑖 , 𝑗 ⟩ ) ) )
53 df-ov ( 𝑖 ( 𝑋f + 𝑌 ) 𝑗 ) = ( ( 𝑋f + 𝑌 ) ‘ ⟨ 𝑖 , 𝑗 ⟩ )
54 df-ov ( 𝑖 𝑋 𝑗 ) = ( 𝑋 ‘ ⟨ 𝑖 , 𝑗 ⟩ )
55 df-ov ( 𝑖 𝑌 𝑗 ) = ( 𝑌 ‘ ⟨ 𝑖 , 𝑗 ⟩ )
56 54 55 oveq12i ( ( 𝑖 𝑋 𝑗 ) + ( 𝑖 𝑌 𝑗 ) ) = ( ( 𝑋 ‘ ⟨ 𝑖 , 𝑗 ⟩ ) + ( 𝑌 ‘ ⟨ 𝑖 , 𝑗 ⟩ ) )
57 52 53 56 3eqtr4g ( ( ( 𝜑 ∧ ( 𝑖𝑀𝑘𝑂 ) ) ∧ 𝑗𝑁 ) → ( 𝑖 ( 𝑋f + 𝑌 ) 𝑗 ) = ( ( 𝑖 𝑋 𝑗 ) + ( 𝑖 𝑌 𝑗 ) ) )
58 57 oveq1d ( ( ( 𝜑 ∧ ( 𝑖𝑀𝑘𝑂 ) ) ∧ 𝑗𝑁 ) → ( ( 𝑖 ( 𝑋f + 𝑌 ) 𝑗 ) ( .r𝑅 ) ( 𝑗 𝑍 𝑘 ) ) = ( ( ( 𝑖 𝑋 𝑗 ) + ( 𝑖 𝑌 𝑗 ) ) ( .r𝑅 ) ( 𝑗 𝑍 𝑘 ) ) )
59 1 7 27 ringdir ( ( 𝑅 ∈ Ring ∧ ( ( 𝑖 𝑋 𝑗 ) ∈ 𝐵 ∧ ( 𝑖 𝑌 𝑗 ) ∈ 𝐵 ∧ ( 𝑗 𝑍 𝑘 ) ∈ 𝐵 ) ) → ( ( ( 𝑖 𝑋 𝑗 ) + ( 𝑖 𝑌 𝑗 ) ) ( .r𝑅 ) ( 𝑗 𝑍 𝑘 ) ) = ( ( ( 𝑖 𝑋 𝑗 ) ( .r𝑅 ) ( 𝑗 𝑍 𝑘 ) ) + ( ( 𝑖 𝑌 𝑗 ) ( .r𝑅 ) ( 𝑗 𝑍 𝑘 ) ) ) )
60 15 21 33 26 59 syl13anc ( ( ( 𝜑 ∧ ( 𝑖𝑀𝑘𝑂 ) ) ∧ 𝑗𝑁 ) → ( ( ( 𝑖 𝑋 𝑗 ) + ( 𝑖 𝑌 𝑗 ) ) ( .r𝑅 ) ( 𝑗 𝑍 𝑘 ) ) = ( ( ( 𝑖 𝑋 𝑗 ) ( .r𝑅 ) ( 𝑗 𝑍 𝑘 ) ) + ( ( 𝑖 𝑌 𝑗 ) ( .r𝑅 ) ( 𝑗 𝑍 𝑘 ) ) ) )
61 58 60 eqtrd ( ( ( 𝜑 ∧ ( 𝑖𝑀𝑘𝑂 ) ) ∧ 𝑗𝑁 ) → ( ( 𝑖 ( 𝑋f + 𝑌 ) 𝑗 ) ( .r𝑅 ) ( 𝑗 𝑍 𝑘 ) ) = ( ( ( 𝑖 𝑋 𝑗 ) ( .r𝑅 ) ( 𝑗 𝑍 𝑘 ) ) + ( ( 𝑖 𝑌 𝑗 ) ( .r𝑅 ) ( 𝑗 𝑍 𝑘 ) ) ) )
62 61 mpteq2dva ( ( 𝜑 ∧ ( 𝑖𝑀𝑘𝑂 ) ) → ( 𝑗𝑁 ↦ ( ( 𝑖 ( 𝑋f + 𝑌 ) 𝑗 ) ( .r𝑅 ) ( 𝑗 𝑍 𝑘 ) ) ) = ( 𝑗𝑁 ↦ ( ( ( 𝑖 𝑋 𝑗 ) ( .r𝑅 ) ( 𝑗 𝑍 𝑘 ) ) + ( ( 𝑖 𝑌 𝑗 ) ( .r𝑅 ) ( 𝑗 𝑍 𝑘 ) ) ) ) )
63 eqidd ( ( 𝜑 ∧ ( 𝑖𝑀𝑘𝑂 ) ) → ( 𝑗𝑁 ↦ ( ( 𝑖 𝑋 𝑗 ) ( .r𝑅 ) ( 𝑗 𝑍 𝑘 ) ) ) = ( 𝑗𝑁 ↦ ( ( 𝑖 𝑋 𝑗 ) ( .r𝑅 ) ( 𝑗 𝑍 𝑘 ) ) ) )
64 eqidd ( ( 𝜑 ∧ ( 𝑖𝑀𝑘𝑂 ) ) → ( 𝑗𝑁 ↦ ( ( 𝑖 𝑌 𝑗 ) ( .r𝑅 ) ( 𝑗 𝑍 𝑘 ) ) ) = ( 𝑗𝑁 ↦ ( ( 𝑖 𝑌 𝑗 ) ( .r𝑅 ) ( 𝑗 𝑍 𝑘 ) ) ) )
65 14 29 35 63 64 offval2 ( ( 𝜑 ∧ ( 𝑖𝑀𝑘𝑂 ) ) → ( ( 𝑗𝑁 ↦ ( ( 𝑖 𝑋 𝑗 ) ( .r𝑅 ) ( 𝑗 𝑍 𝑘 ) ) ) ∘f + ( 𝑗𝑁 ↦ ( ( 𝑖 𝑌 𝑗 ) ( .r𝑅 ) ( 𝑗 𝑍 𝑘 ) ) ) ) = ( 𝑗𝑁 ↦ ( ( ( 𝑖 𝑋 𝑗 ) ( .r𝑅 ) ( 𝑗 𝑍 𝑘 ) ) + ( ( 𝑖 𝑌 𝑗 ) ( .r𝑅 ) ( 𝑗 𝑍 𝑘 ) ) ) ) )
66 62 65 eqtr4d ( ( 𝜑 ∧ ( 𝑖𝑀𝑘𝑂 ) ) → ( 𝑗𝑁 ↦ ( ( 𝑖 ( 𝑋f + 𝑌 ) 𝑗 ) ( .r𝑅 ) ( 𝑗 𝑍 𝑘 ) ) ) = ( ( 𝑗𝑁 ↦ ( ( 𝑖 𝑋 𝑗 ) ( .r𝑅 ) ( 𝑗 𝑍 𝑘 ) ) ) ∘f + ( 𝑗𝑁 ↦ ( ( 𝑖 𝑌 𝑗 ) ( .r𝑅 ) ( 𝑗 𝑍 𝑘 ) ) ) ) )
67 66 oveq2d ( ( 𝜑 ∧ ( 𝑖𝑀𝑘𝑂 ) ) → ( 𝑅 Σg ( 𝑗𝑁 ↦ ( ( 𝑖 ( 𝑋f + 𝑌 ) 𝑗 ) ( .r𝑅 ) ( 𝑗 𝑍 𝑘 ) ) ) ) = ( 𝑅 Σg ( ( 𝑗𝑁 ↦ ( ( 𝑖 𝑋 𝑗 ) ( .r𝑅 ) ( 𝑗 𝑍 𝑘 ) ) ) ∘f + ( 𝑗𝑁 ↦ ( ( 𝑖 𝑌 𝑗 ) ( .r𝑅 ) ( 𝑗 𝑍 𝑘 ) ) ) ) ) )
68 2 adantr ( ( 𝜑 ∧ ( 𝑖𝑀𝑘𝑂 ) ) → 𝑅 ∈ Ring )
69 4 adantr ( ( 𝜑 ∧ ( 𝑖𝑀𝑘𝑂 ) ) → 𝑀 ∈ Fin )
70 6 adantr ( ( 𝜑 ∧ ( 𝑖𝑀𝑘𝑂 ) ) → 𝑂 ∈ Fin )
71 8 adantr ( ( 𝜑 ∧ ( 𝑖𝑀𝑘𝑂 ) ) → 𝑋 ∈ ( 𝐵m ( 𝑀 × 𝑁 ) ) )
72 10 adantr ( ( 𝜑 ∧ ( 𝑖𝑀𝑘𝑂 ) ) → 𝑍 ∈ ( 𝐵m ( 𝑁 × 𝑂 ) ) )
73 simprl ( ( 𝜑 ∧ ( 𝑖𝑀𝑘𝑂 ) ) → 𝑖𝑀 )
74 simprr ( ( 𝜑 ∧ ( 𝑖𝑀𝑘𝑂 ) ) → 𝑘𝑂 )
75 3 1 27 68 69 14 70 71 72 73 74 mamufv ( ( 𝜑 ∧ ( 𝑖𝑀𝑘𝑂 ) ) → ( 𝑖 ( 𝑋 𝐹 𝑍 ) 𝑘 ) = ( 𝑅 Σg ( 𝑗𝑁 ↦ ( ( 𝑖 𝑋 𝑗 ) ( .r𝑅 ) ( 𝑗 𝑍 𝑘 ) ) ) ) )
76 9 adantr ( ( 𝜑 ∧ ( 𝑖𝑀𝑘𝑂 ) ) → 𝑌 ∈ ( 𝐵m ( 𝑀 × 𝑁 ) ) )
77 3 1 27 68 69 14 70 76 72 73 74 mamufv ( ( 𝜑 ∧ ( 𝑖𝑀𝑘𝑂 ) ) → ( 𝑖 ( 𝑌 𝐹 𝑍 ) 𝑘 ) = ( 𝑅 Σg ( 𝑗𝑁 ↦ ( ( 𝑖 𝑌 𝑗 ) ( .r𝑅 ) ( 𝑗 𝑍 𝑘 ) ) ) ) )
78 75 77 oveq12d ( ( 𝜑 ∧ ( 𝑖𝑀𝑘𝑂 ) ) → ( ( 𝑖 ( 𝑋 𝐹 𝑍 ) 𝑘 ) + ( 𝑖 ( 𝑌 𝐹 𝑍 ) 𝑘 ) ) = ( ( 𝑅 Σg ( 𝑗𝑁 ↦ ( ( 𝑖 𝑋 𝑗 ) ( .r𝑅 ) ( 𝑗 𝑍 𝑘 ) ) ) ) + ( 𝑅 Σg ( 𝑗𝑁 ↦ ( ( 𝑖 𝑌 𝑗 ) ( .r𝑅 ) ( 𝑗 𝑍 𝑘 ) ) ) ) ) )
79 38 67 78 3eqtr4d ( ( 𝜑 ∧ ( 𝑖𝑀𝑘𝑂 ) ) → ( 𝑅 Σg ( 𝑗𝑁 ↦ ( ( 𝑖 ( 𝑋f + 𝑌 ) 𝑗 ) ( .r𝑅 ) ( 𝑗 𝑍 𝑘 ) ) ) ) = ( ( 𝑖 ( 𝑋 𝐹 𝑍 ) 𝑘 ) + ( 𝑖 ( 𝑌 𝐹 𝑍 ) 𝑘 ) ) )
80 ringmnd ( 𝑅 ∈ Ring → 𝑅 ∈ Mnd )
81 2 80 syl ( 𝜑𝑅 ∈ Mnd )
82 1 7 mndvcl ( ( 𝑅 ∈ Mnd ∧ 𝑋 ∈ ( 𝐵m ( 𝑀 × 𝑁 ) ) ∧ 𝑌 ∈ ( 𝐵m ( 𝑀 × 𝑁 ) ) ) → ( 𝑋f + 𝑌 ) ∈ ( 𝐵m ( 𝑀 × 𝑁 ) ) )
83 81 8 9 82 syl3anc ( 𝜑 → ( 𝑋f + 𝑌 ) ∈ ( 𝐵m ( 𝑀 × 𝑁 ) ) )
84 83 adantr ( ( 𝜑 ∧ ( 𝑖𝑀𝑘𝑂 ) ) → ( 𝑋f + 𝑌 ) ∈ ( 𝐵m ( 𝑀 × 𝑁 ) ) )
85 3 1 27 68 69 14 70 84 72 73 74 mamufv ( ( 𝜑 ∧ ( 𝑖𝑀𝑘𝑂 ) ) → ( 𝑖 ( ( 𝑋f + 𝑌 ) 𝐹 𝑍 ) 𝑘 ) = ( 𝑅 Σg ( 𝑗𝑁 ↦ ( ( 𝑖 ( 𝑋f + 𝑌 ) 𝑗 ) ( .r𝑅 ) ( 𝑗 𝑍 𝑘 ) ) ) ) )
86 1 2 3 4 5 6 8 10 mamucl ( 𝜑 → ( 𝑋 𝐹 𝑍 ) ∈ ( 𝐵m ( 𝑀 × 𝑂 ) ) )
87 elmapi ( ( 𝑋 𝐹 𝑍 ) ∈ ( 𝐵m ( 𝑀 × 𝑂 ) ) → ( 𝑋 𝐹 𝑍 ) : ( 𝑀 × 𝑂 ) ⟶ 𝐵 )
88 ffn ( ( 𝑋 𝐹 𝑍 ) : ( 𝑀 × 𝑂 ) ⟶ 𝐵 → ( 𝑋 𝐹 𝑍 ) Fn ( 𝑀 × 𝑂 ) )
89 86 87 88 3syl ( 𝜑 → ( 𝑋 𝐹 𝑍 ) Fn ( 𝑀 × 𝑂 ) )
90 89 adantr ( ( 𝜑 ∧ ( 𝑖𝑀𝑘𝑂 ) ) → ( 𝑋 𝐹 𝑍 ) Fn ( 𝑀 × 𝑂 ) )
91 1 2 3 4 5 6 9 10 mamucl ( 𝜑 → ( 𝑌 𝐹 𝑍 ) ∈ ( 𝐵m ( 𝑀 × 𝑂 ) ) )
92 elmapi ( ( 𝑌 𝐹 𝑍 ) ∈ ( 𝐵m ( 𝑀 × 𝑂 ) ) → ( 𝑌 𝐹 𝑍 ) : ( 𝑀 × 𝑂 ) ⟶ 𝐵 )
93 ffn ( ( 𝑌 𝐹 𝑍 ) : ( 𝑀 × 𝑂 ) ⟶ 𝐵 → ( 𝑌 𝐹 𝑍 ) Fn ( 𝑀 × 𝑂 ) )
94 91 92 93 3syl ( 𝜑 → ( 𝑌 𝐹 𝑍 ) Fn ( 𝑀 × 𝑂 ) )
95 94 adantr ( ( 𝜑 ∧ ( 𝑖𝑀𝑘𝑂 ) ) → ( 𝑌 𝐹 𝑍 ) Fn ( 𝑀 × 𝑂 ) )
96 xpfi ( ( 𝑀 ∈ Fin ∧ 𝑂 ∈ Fin ) → ( 𝑀 × 𝑂 ) ∈ Fin )
97 4 6 96 syl2anc ( 𝜑 → ( 𝑀 × 𝑂 ) ∈ Fin )
98 97 adantr ( ( 𝜑 ∧ ( 𝑖𝑀𝑘𝑂 ) ) → ( 𝑀 × 𝑂 ) ∈ Fin )
99 opelxpi ( ( 𝑖𝑀𝑘𝑂 ) → ⟨ 𝑖 , 𝑘 ⟩ ∈ ( 𝑀 × 𝑂 ) )
100 99 adantl ( ( 𝜑 ∧ ( 𝑖𝑀𝑘𝑂 ) ) → ⟨ 𝑖 , 𝑘 ⟩ ∈ ( 𝑀 × 𝑂 ) )
101 fnfvof ( ( ( ( 𝑋 𝐹 𝑍 ) Fn ( 𝑀 × 𝑂 ) ∧ ( 𝑌 𝐹 𝑍 ) Fn ( 𝑀 × 𝑂 ) ) ∧ ( ( 𝑀 × 𝑂 ) ∈ Fin ∧ ⟨ 𝑖 , 𝑘 ⟩ ∈ ( 𝑀 × 𝑂 ) ) ) → ( ( ( 𝑋 𝐹 𝑍 ) ∘f + ( 𝑌 𝐹 𝑍 ) ) ‘ ⟨ 𝑖 , 𝑘 ⟩ ) = ( ( ( 𝑋 𝐹 𝑍 ) ‘ ⟨ 𝑖 , 𝑘 ⟩ ) + ( ( 𝑌 𝐹 𝑍 ) ‘ ⟨ 𝑖 , 𝑘 ⟩ ) ) )
102 90 95 98 100 101 syl22anc ( ( 𝜑 ∧ ( 𝑖𝑀𝑘𝑂 ) ) → ( ( ( 𝑋 𝐹 𝑍 ) ∘f + ( 𝑌 𝐹 𝑍 ) ) ‘ ⟨ 𝑖 , 𝑘 ⟩ ) = ( ( ( 𝑋 𝐹 𝑍 ) ‘ ⟨ 𝑖 , 𝑘 ⟩ ) + ( ( 𝑌 𝐹 𝑍 ) ‘ ⟨ 𝑖 , 𝑘 ⟩ ) ) )
103 df-ov ( 𝑖 ( ( 𝑋 𝐹 𝑍 ) ∘f + ( 𝑌 𝐹 𝑍 ) ) 𝑘 ) = ( ( ( 𝑋 𝐹 𝑍 ) ∘f + ( 𝑌 𝐹 𝑍 ) ) ‘ ⟨ 𝑖 , 𝑘 ⟩ )
104 df-ov ( 𝑖 ( 𝑋 𝐹 𝑍 ) 𝑘 ) = ( ( 𝑋 𝐹 𝑍 ) ‘ ⟨ 𝑖 , 𝑘 ⟩ )
105 df-ov ( 𝑖 ( 𝑌 𝐹 𝑍 ) 𝑘 ) = ( ( 𝑌 𝐹 𝑍 ) ‘ ⟨ 𝑖 , 𝑘 ⟩ )
106 104 105 oveq12i ( ( 𝑖 ( 𝑋 𝐹 𝑍 ) 𝑘 ) + ( 𝑖 ( 𝑌 𝐹 𝑍 ) 𝑘 ) ) = ( ( ( 𝑋 𝐹 𝑍 ) ‘ ⟨ 𝑖 , 𝑘 ⟩ ) + ( ( 𝑌 𝐹 𝑍 ) ‘ ⟨ 𝑖 , 𝑘 ⟩ ) )
107 102 103 106 3eqtr4g ( ( 𝜑 ∧ ( 𝑖𝑀𝑘𝑂 ) ) → ( 𝑖 ( ( 𝑋 𝐹 𝑍 ) ∘f + ( 𝑌 𝐹 𝑍 ) ) 𝑘 ) = ( ( 𝑖 ( 𝑋 𝐹 𝑍 ) 𝑘 ) + ( 𝑖 ( 𝑌 𝐹 𝑍 ) 𝑘 ) ) )
108 79 85 107 3eqtr4d ( ( 𝜑 ∧ ( 𝑖𝑀𝑘𝑂 ) ) → ( 𝑖 ( ( 𝑋f + 𝑌 ) 𝐹 𝑍 ) 𝑘 ) = ( 𝑖 ( ( 𝑋 𝐹 𝑍 ) ∘f + ( 𝑌 𝐹 𝑍 ) ) 𝑘 ) )
109 108 ralrimivva ( 𝜑 → ∀ 𝑖𝑀𝑘𝑂 ( 𝑖 ( ( 𝑋f + 𝑌 ) 𝐹 𝑍 ) 𝑘 ) = ( 𝑖 ( ( 𝑋 𝐹 𝑍 ) ∘f + ( 𝑌 𝐹 𝑍 ) ) 𝑘 ) )
110 1 2 3 4 5 6 83 10 mamucl ( 𝜑 → ( ( 𝑋f + 𝑌 ) 𝐹 𝑍 ) ∈ ( 𝐵m ( 𝑀 × 𝑂 ) ) )
111 elmapi ( ( ( 𝑋f + 𝑌 ) 𝐹 𝑍 ) ∈ ( 𝐵m ( 𝑀 × 𝑂 ) ) → ( ( 𝑋f + 𝑌 ) 𝐹 𝑍 ) : ( 𝑀 × 𝑂 ) ⟶ 𝐵 )
112 ffn ( ( ( 𝑋f + 𝑌 ) 𝐹 𝑍 ) : ( 𝑀 × 𝑂 ) ⟶ 𝐵 → ( ( 𝑋f + 𝑌 ) 𝐹 𝑍 ) Fn ( 𝑀 × 𝑂 ) )
113 110 111 112 3syl ( 𝜑 → ( ( 𝑋f + 𝑌 ) 𝐹 𝑍 ) Fn ( 𝑀 × 𝑂 ) )
114 1 7 mndvcl ( ( 𝑅 ∈ Mnd ∧ ( 𝑋 𝐹 𝑍 ) ∈ ( 𝐵m ( 𝑀 × 𝑂 ) ) ∧ ( 𝑌 𝐹 𝑍 ) ∈ ( 𝐵m ( 𝑀 × 𝑂 ) ) ) → ( ( 𝑋 𝐹 𝑍 ) ∘f + ( 𝑌 𝐹 𝑍 ) ) ∈ ( 𝐵m ( 𝑀 × 𝑂 ) ) )
115 81 86 91 114 syl3anc ( 𝜑 → ( ( 𝑋 𝐹 𝑍 ) ∘f + ( 𝑌 𝐹 𝑍 ) ) ∈ ( 𝐵m ( 𝑀 × 𝑂 ) ) )
116 elmapi ( ( ( 𝑋 𝐹 𝑍 ) ∘f + ( 𝑌 𝐹 𝑍 ) ) ∈ ( 𝐵m ( 𝑀 × 𝑂 ) ) → ( ( 𝑋 𝐹 𝑍 ) ∘f + ( 𝑌 𝐹 𝑍 ) ) : ( 𝑀 × 𝑂 ) ⟶ 𝐵 )
117 ffn ( ( ( 𝑋 𝐹 𝑍 ) ∘f + ( 𝑌 𝐹 𝑍 ) ) : ( 𝑀 × 𝑂 ) ⟶ 𝐵 → ( ( 𝑋 𝐹 𝑍 ) ∘f + ( 𝑌 𝐹 𝑍 ) ) Fn ( 𝑀 × 𝑂 ) )
118 115 116 117 3syl ( 𝜑 → ( ( 𝑋 𝐹 𝑍 ) ∘f + ( 𝑌 𝐹 𝑍 ) ) Fn ( 𝑀 × 𝑂 ) )
119 eqfnov2 ( ( ( ( 𝑋f + 𝑌 ) 𝐹 𝑍 ) Fn ( 𝑀 × 𝑂 ) ∧ ( ( 𝑋 𝐹 𝑍 ) ∘f + ( 𝑌 𝐹 𝑍 ) ) Fn ( 𝑀 × 𝑂 ) ) → ( ( ( 𝑋f + 𝑌 ) 𝐹 𝑍 ) = ( ( 𝑋 𝐹 𝑍 ) ∘f + ( 𝑌 𝐹 𝑍 ) ) ↔ ∀ 𝑖𝑀𝑘𝑂 ( 𝑖 ( ( 𝑋f + 𝑌 ) 𝐹 𝑍 ) 𝑘 ) = ( 𝑖 ( ( 𝑋 𝐹 𝑍 ) ∘f + ( 𝑌 𝐹 𝑍 ) ) 𝑘 ) ) )
120 113 118 119 syl2anc ( 𝜑 → ( ( ( 𝑋f + 𝑌 ) 𝐹 𝑍 ) = ( ( 𝑋 𝐹 𝑍 ) ∘f + ( 𝑌 𝐹 𝑍 ) ) ↔ ∀ 𝑖𝑀𝑘𝑂 ( 𝑖 ( ( 𝑋f + 𝑌 ) 𝐹 𝑍 ) 𝑘 ) = ( 𝑖 ( ( 𝑋 𝐹 𝑍 ) ∘f + ( 𝑌 𝐹 𝑍 ) ) 𝑘 ) ) )
121 109 120 mpbird ( 𝜑 → ( ( 𝑋f + 𝑌 ) 𝐹 𝑍 ) = ( ( 𝑋 𝐹 𝑍 ) ∘f + ( 𝑌 𝐹 𝑍 ) ) )