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