This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem mavmulcl

Description: Multiplication of an NxN matrix with an N-dimensional vector results in an N-dimensional vector. (Contributed by AV, 6-Dec-2018) (Revised by AV, 23-Feb-2019) (Proof shortened by AV, 23-Jul-2019)

Ref Expression
Hypotheses mavmulcl.a ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
mavmulcl.m ⊢ × = ( 𝑅 maVecMul ⟨ 𝑁 , 𝑁 ⟩ )
mavmulcl.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
mavmulcl.t ⊢ · = ( .r ‘ 𝑅 )
mavmulcl.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
mavmulcl.n ⊢ ( 𝜑 → 𝑁 ∈ Fin )
mavmulcl.x ⊢ ( 𝜑 → 𝑋 ∈ ( Base ‘ 𝐴 ) )
mavmulcl.y ⊢ ( 𝜑 → 𝑌 ∈ ( 𝐵 ↑m 𝑁 ) )
Assertion mavmulcl ( 𝜑 → ( 𝑋 × 𝑌 ) ∈ ( 𝐵 ↑m 𝑁 ) )

Proof

Step Hyp Ref Expression
1 mavmulcl.a ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
2 mavmulcl.m ⊢ × = ( 𝑅 maVecMul ⟨ 𝑁 , 𝑁 ⟩ )
3 mavmulcl.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
4 mavmulcl.t ⊢ · = ( .r ‘ 𝑅 )
5 mavmulcl.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
6 mavmulcl.n ⊢ ( 𝜑 → 𝑁 ∈ Fin )
7 mavmulcl.x ⊢ ( 𝜑 → 𝑋 ∈ ( Base ‘ 𝐴 ) )
8 mavmulcl.y ⊢ ( 𝜑 → 𝑌 ∈ ( 𝐵 ↑m 𝑁 ) )
9 1 2 3 4 5 6 7 8 mavmulval ⊢ ( 𝜑 → ( 𝑋 × 𝑌 ) = ( 𝑖 ∈ 𝑁 ↦ ( 𝑅 Σg ( 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 𝑋 𝑗 ) · ( 𝑌 ‘ 𝑗 ) ) ) ) ) )
10 ringcmn ⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ CMnd )
11 5 10 syl ⊢ ( 𝜑 → 𝑅 ∈ CMnd )
12 11 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) → 𝑅 ∈ CMnd )
13 6 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) → 𝑁 ∈ Fin )
14 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑗 ∈ 𝑁 ) → 𝑅 ∈ Ring )
15 1 3 matbas2 ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 𝐵 ↑m ( 𝑁 × 𝑁 ) ) = ( Base ‘ 𝐴 ) )
16 6 5 15 syl2anc ⊢ ( 𝜑 → ( 𝐵 ↑m ( 𝑁 × 𝑁 ) ) = ( Base ‘ 𝐴 ) )
17 7 16 eleqtrrd ⊢ ( 𝜑 → 𝑋 ∈ ( 𝐵 ↑m ( 𝑁 × 𝑁 ) ) )
18 elmapi ⊢ ( 𝑋 ∈ ( 𝐵 ↑m ( 𝑁 × 𝑁 ) ) → 𝑋 : ( 𝑁 × 𝑁 ) ⟶ 𝐵 )
19 17 18 syl ⊢ ( 𝜑 → 𝑋 : ( 𝑁 × 𝑁 ) ⟶ 𝐵 )
20 19 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑗 ∈ 𝑁 ) → 𝑋 : ( 𝑁 × 𝑁 ) ⟶ 𝐵 )
21 simpr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) → 𝑖 ∈ 𝑁 )
22 21 adantr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑗 ∈ 𝑁 ) → 𝑖 ∈ 𝑁 )
23 simpr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑗 ∈ 𝑁 ) → 𝑗 ∈ 𝑁 )
24 20 22 23 fovcdmd ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑗 ∈ 𝑁 ) → ( 𝑖 𝑋 𝑗 ) ∈ 𝐵 )
25 elmapi ⊢ ( 𝑌 ∈ ( 𝐵 ↑m 𝑁 ) → 𝑌 : 𝑁 ⟶ 𝐵 )
26 8 25 syl ⊢ ( 𝜑 → 𝑌 : 𝑁 ⟶ 𝐵 )
27 26 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑗 ∈ 𝑁 ) → 𝑌 : 𝑁 ⟶ 𝐵 )
28 27 23 ffvelcdmd ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑗 ∈ 𝑁 ) → ( 𝑌 ‘ 𝑗 ) ∈ 𝐵 )
29 3 4 ringcl ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑖 𝑋 𝑗 ) ∈ 𝐵 ∧ ( 𝑌 ‘ 𝑗 ) ∈ 𝐵 ) → ( ( 𝑖 𝑋 𝑗 ) · ( 𝑌 ‘ 𝑗 ) ) ∈ 𝐵 )
30 14 24 28 29 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) ∧ 𝑗 ∈ 𝑁 ) → ( ( 𝑖 𝑋 𝑗 ) · ( 𝑌 ‘ 𝑗 ) ) ∈ 𝐵 )
31 30 ralrimiva ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) → ∀ 𝑗 ∈ 𝑁 ( ( 𝑖 𝑋 𝑗 ) · ( 𝑌 ‘ 𝑗 ) ) ∈ 𝐵 )
32 3 12 13 31 gsummptcl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝑁 ) → ( 𝑅 Σg ( 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 𝑋 𝑗 ) · ( 𝑌 ‘ 𝑗 ) ) ) ) ∈ 𝐵 )
33 32 ralrimiva ⊢ ( 𝜑 → ∀ 𝑖 ∈ 𝑁 ( 𝑅 Σg ( 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 𝑋 𝑗 ) · ( 𝑌 ‘ 𝑗 ) ) ) ) ∈ 𝐵 )
34 eqid ⊢ ( 𝑖 ∈ 𝑁 ↦ ( 𝑅 Σg ( 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 𝑋 𝑗 ) · ( 𝑌 ‘ 𝑗 ) ) ) ) ) = ( 𝑖 ∈ 𝑁 ↦ ( 𝑅 Σg ( 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 𝑋 𝑗 ) · ( 𝑌 ‘ 𝑗 ) ) ) ) )
35 34 fmpt ⊢ ( ∀ 𝑖 ∈ 𝑁 ( 𝑅 Σg ( 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 𝑋 𝑗 ) · ( 𝑌 ‘ 𝑗 ) ) ) ) ∈ 𝐵 ↔ ( 𝑖 ∈ 𝑁 ↦ ( 𝑅 Σg ( 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 𝑋 𝑗 ) · ( 𝑌 ‘ 𝑗 ) ) ) ) ) : 𝑁 ⟶ 𝐵 )
36 3 fvexi ⊢ 𝐵 ∈ V
37 elmapg ⊢ ( ( 𝐵 ∈ V ∧ 𝑁 ∈ Fin ) → ( ( 𝑖 ∈ 𝑁 ↦ ( 𝑅 Σg ( 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 𝑋 𝑗 ) · ( 𝑌 ‘ 𝑗 ) ) ) ) ) ∈ ( 𝐵 ↑m 𝑁 ) ↔ ( 𝑖 ∈ 𝑁 ↦ ( 𝑅 Σg ( 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 𝑋 𝑗 ) · ( 𝑌 ‘ 𝑗 ) ) ) ) ) : 𝑁 ⟶ 𝐵 ) )
38 36 6 37 sylancr ⊢ ( 𝜑 → ( ( 𝑖 ∈ 𝑁 ↦ ( 𝑅 Σg ( 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 𝑋 𝑗 ) · ( 𝑌 ‘ 𝑗 ) ) ) ) ) ∈ ( 𝐵 ↑m 𝑁 ) ↔ ( 𝑖 ∈ 𝑁 ↦ ( 𝑅 Σg ( 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 𝑋 𝑗 ) · ( 𝑌 ‘ 𝑗 ) ) ) ) ) : 𝑁 ⟶ 𝐵 ) )
39 35 38 bitr4id ⊢ ( 𝜑 → ( ∀ 𝑖 ∈ 𝑁 ( 𝑅 Σg ( 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 𝑋 𝑗 ) · ( 𝑌 ‘ 𝑗 ) ) ) ) ∈ 𝐵 ↔ ( 𝑖 ∈ 𝑁 ↦ ( 𝑅 Σg ( 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 𝑋 𝑗 ) · ( 𝑌 ‘ 𝑗 ) ) ) ) ) ∈ ( 𝐵 ↑m 𝑁 ) ) )
40 33 39 mpbid ⊢ ( 𝜑 → ( 𝑖 ∈ 𝑁 ↦ ( 𝑅 Σg ( 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 𝑋 𝑗 ) · ( 𝑌 ‘ 𝑗 ) ) ) ) ) ∈ ( 𝐵 ↑m 𝑁 ) )
41 9 40 eqeltrd ⊢ ( 𝜑 → ( 𝑋 × 𝑌 ) ∈ ( 𝐵 ↑m 𝑁 ) )