Metamath Proof Explorer


Theorem mamudir

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