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