Metamath Proof Explorer

Theorem mamucl

Description: Operation closure of matrix multiplication. (Contributed by Stefan O'Rear, 2-Sep-2015) (Proof shortened by AV, 23-Jul-2019)

Ref Expression
Hypotheses mamucl.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
mamucl.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
mamucl.f ⊢ 𝐹 = ( 𝑅 maMul ⟨ 𝑀 , 𝑁 , 𝑃 ⟩ )
mamucl.m ⊢ ( 𝜑 → 𝑀 ∈ Fin )
mamucl.n ⊢ ( 𝜑 → 𝑁 ∈ Fin )
mamucl.p ⊢ ( 𝜑 → 𝑃 ∈ Fin )
mamucl.x ⊢ ( 𝜑 → 𝑋 ∈ ( 𝐵 ↑m ( 𝑀 × 𝑁 ) ) )
mamucl.y ⊢ ( 𝜑 → 𝑌 ∈ ( 𝐵 ↑m ( 𝑁 × 𝑃 ) ) )
Assertion mamucl ( 𝜑 → ( 𝑋 𝐹 𝑌 ) ∈ ( 𝐵 ↑m ( 𝑀 × 𝑃 ) ) )

Proof

Step Hyp Ref Expression
1 mamucl.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
2 mamucl.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
3 mamucl.f ⊢ 𝐹 = ( 𝑅 maMul ⟨ 𝑀 , 𝑁 , 𝑃 ⟩ )
4 mamucl.m ⊢ ( 𝜑 → 𝑀 ∈ Fin )
5 mamucl.n ⊢ ( 𝜑 → 𝑁 ∈ Fin )
6 mamucl.p ⊢ ( 𝜑 → 𝑃 ∈ Fin )
7 mamucl.x ⊢ ( 𝜑 → 𝑋 ∈ ( 𝐵 ↑m ( 𝑀 × 𝑁 ) ) )
8 mamucl.y ⊢ ( 𝜑 → 𝑌 ∈ ( 𝐵 ↑m ( 𝑁 × 𝑃 ) ) )
9 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
10 3 1 9 2 4 5 6 7 8 mamuval ⊢ ( 𝜑 → ( 𝑋 𝐹 𝑌 ) = ( 𝑖 ∈ 𝑀 , 𝑘 ∈ 𝑃 ↦ ( 𝑅 Σg ( 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 𝑋 𝑗 ) ( .r ‘ 𝑅 ) ( 𝑗 𝑌 𝑘 ) ) ) ) ) )
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 7 16 syl ⊢ ( 𝜑 → 𝑋 : ( 𝑀 × 𝑁 ) ⟶ 𝐵 )
18 17 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑃 ) ) ∧ 𝑗 ∈ 𝑁 ) → 𝑋 : ( 𝑀 × 𝑁 ) ⟶ 𝐵 )
19 simplrl ⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑃 ) ) ∧ 𝑗 ∈ 𝑁 ) → 𝑖 ∈ 𝑀 )
20 simpr ⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑃 ) ) ∧ 𝑗 ∈ 𝑁 ) → 𝑗 ∈ 𝑁 )
21 18 19 20 fovrnd ⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑃 ) ) ∧ 𝑗 ∈ 𝑁 ) → ( 𝑖 𝑋 𝑗 ) ∈ 𝐵 )
22 elmapi ⊢ ( 𝑌 ∈ ( 𝐵 ↑m ( 𝑁 × 𝑃 ) ) → 𝑌 : ( 𝑁 × 𝑃 ) ⟶ 𝐵 )
23 8 22 syl ⊢ ( 𝜑 → 𝑌 : ( 𝑁 × 𝑃 ) ⟶ 𝐵 )
24 23 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑃 ) ) ∧ 𝑗 ∈ 𝑁 ) → 𝑌 : ( 𝑁 × 𝑃 ) ⟶ 𝐵 )
25 simplrr ⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑃 ) ) ∧ 𝑗 ∈ 𝑁 ) → 𝑘 ∈ 𝑃 )
26 24 20 25 fovrnd ⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑃 ) ) ∧ 𝑗 ∈ 𝑁 ) → ( 𝑗 𝑌 𝑘 ) ∈ 𝐵 )
27 1 9 ringcl ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑖 𝑋 𝑗 ) ∈ 𝐵 ∧ ( 𝑗 𝑌 𝑘 ) ∈ 𝐵 ) → ( ( 𝑖 𝑋 𝑗 ) ( .r ‘ 𝑅 ) ( 𝑗 𝑌 𝑘 ) ) ∈ 𝐵 )
28 15 21 26 27 syl3anc ⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑃 ) ) ∧ 𝑗 ∈ 𝑁 ) → ( ( 𝑖 𝑋 𝑗 ) ( .r ‘ 𝑅 ) ( 𝑗 𝑌 𝑘 ) ) ∈ 𝐵 )
29 28 ralrimiva ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑃 ) ) → ∀ 𝑗 ∈ 𝑁 ( ( 𝑖 𝑋 𝑗 ) ( .r ‘ 𝑅 ) ( 𝑗 𝑌 𝑘 ) ) ∈ 𝐵 )
30 1 13 14 29 gsummptcl ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ 𝑀 ∧ 𝑘 ∈ 𝑃 ) ) → ( 𝑅 Σg ( 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 𝑋 𝑗 ) ( .r ‘ 𝑅 ) ( 𝑗 𝑌 𝑘 ) ) ) ) ∈ 𝐵 )
31 30 ralrimivva ⊢ ( 𝜑 → ∀ 𝑖 ∈ 𝑀 ∀ 𝑘 ∈ 𝑃 ( 𝑅 Σg ( 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 𝑋 𝑗 ) ( .r ‘ 𝑅 ) ( 𝑗 𝑌 𝑘 ) ) ) ) ∈ 𝐵 )
32 eqid ⊢ ( 𝑖 ∈ 𝑀 , 𝑘 ∈ 𝑃 ↦ ( 𝑅 Σg ( 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 𝑋 𝑗 ) ( .r ‘ 𝑅 ) ( 𝑗 𝑌 𝑘 ) ) ) ) ) = ( 𝑖 ∈ 𝑀 , 𝑘 ∈ 𝑃 ↦ ( 𝑅 Σg ( 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 𝑋 𝑗 ) ( .r ‘ 𝑅 ) ( 𝑗 𝑌 𝑘 ) ) ) ) )
33 32 fmpo ⊢ ( ∀ 𝑖 ∈ 𝑀 ∀ 𝑘 ∈ 𝑃 ( 𝑅 Σg ( 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 𝑋 𝑗 ) ( .r ‘ 𝑅 ) ( 𝑗 𝑌 𝑘 ) ) ) ) ∈ 𝐵 ↔ ( 𝑖 ∈ 𝑀 , 𝑘 ∈ 𝑃 ↦ ( 𝑅 Σg ( 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 𝑋 𝑗 ) ( .r ‘ 𝑅 ) ( 𝑗 𝑌 𝑘 ) ) ) ) ) : ( 𝑀 × 𝑃 ) ⟶ 𝐵 )
34 1 fvexi ⊢ 𝐵 ∈ V
35 xpfi ⊢ ( ( 𝑀 ∈ Fin ∧ 𝑃 ∈ Fin ) → ( 𝑀 × 𝑃 ) ∈ Fin )
36 4 6 35 syl2anc ⊢ ( 𝜑 → ( 𝑀 × 𝑃 ) ∈ Fin )
37 elmapg ⊢ ( ( 𝐵 ∈ V ∧ ( 𝑀 × 𝑃 ) ∈ Fin ) → ( ( 𝑖 ∈ 𝑀 , 𝑘 ∈ 𝑃 ↦ ( 𝑅 Σg ( 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 𝑋 𝑗 ) ( .r ‘ 𝑅 ) ( 𝑗 𝑌 𝑘 ) ) ) ) ) ∈ ( 𝐵 ↑m ( 𝑀 × 𝑃 ) ) ↔ ( 𝑖 ∈ 𝑀 , 𝑘 ∈ 𝑃 ↦ ( 𝑅 Σg ( 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 𝑋 𝑗 ) ( .r ‘ 𝑅 ) ( 𝑗 𝑌 𝑘 ) ) ) ) ) : ( 𝑀 × 𝑃 ) ⟶ 𝐵 ) )
38 34 36 37 sylancr ⊢ ( 𝜑 → ( ( 𝑖 ∈ 𝑀 , 𝑘 ∈ 𝑃 ↦ ( 𝑅 Σg ( 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 𝑋 𝑗 ) ( .r ‘ 𝑅 ) ( 𝑗 𝑌 𝑘 ) ) ) ) ) ∈ ( 𝐵 ↑m ( 𝑀 × 𝑃 ) ) ↔ ( 𝑖 ∈ 𝑀 , 𝑘 ∈ 𝑃 ↦ ( 𝑅 Σg ( 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 𝑋 𝑗 ) ( .r ‘ 𝑅 ) ( 𝑗 𝑌 𝑘 ) ) ) ) ) : ( 𝑀 × 𝑃 ) ⟶ 𝐵 ) )
39 33 38 bitr4id ⊢ ( 𝜑 → ( ∀ 𝑖 ∈ 𝑀 ∀ 𝑘 ∈ 𝑃 ( 𝑅 Σg ( 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 𝑋 𝑗 ) ( .r ‘ 𝑅 ) ( 𝑗 𝑌 𝑘 ) ) ) ) ∈ 𝐵 ↔ ( 𝑖 ∈ 𝑀 , 𝑘 ∈ 𝑃 ↦ ( 𝑅 Σg ( 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 𝑋 𝑗 ) ( .r ‘ 𝑅 ) ( 𝑗 𝑌 𝑘 ) ) ) ) ) ∈ ( 𝐵 ↑m ( 𝑀 × 𝑃 ) ) ) )
40 31 39 mpbid ⊢ ( 𝜑 → ( 𝑖 ∈ 𝑀 , 𝑘 ∈ 𝑃 ↦ ( 𝑅 Σg ( 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 𝑋 𝑗 ) ( .r ‘ 𝑅 ) ( 𝑗 𝑌 𝑘 ) ) ) ) ) ∈ ( 𝐵 ↑m ( 𝑀 × 𝑃 ) ) )
41 10 40 eqeltrd ⊢ ( 𝜑 → ( 𝑋 𝐹 𝑌 ) ∈ ( 𝐵 ↑m ( 𝑀 × 𝑃 ) ) )