Metamath Proof Explorer

Theorem mavmuldm

Description: The domain of the matrix vector multiplication function. (Contributed by AV, 27-Feb-2019)

Ref Expression
Hypotheses mavmuldm.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
mavmuldm.c ⊢ 𝐶 = ( 𝐵 ↑m ( 𝑀 × 𝑁 ) )
mavmuldm.d ⊢ 𝐷 = ( 𝐵 ↑m 𝑁 )
mavmuldm.t ⊢ · = ( 𝑅 maVecMul ⟨ 𝑀 , 𝑁 ⟩ )
Assertion mavmuldm ( ( 𝑅 ∈ 𝑉 ∧ 𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ) → dom · = ( 𝐶 × 𝐷 ) )

Proof

Step Hyp Ref Expression
1 mavmuldm.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
2 mavmuldm.c ⊢ 𝐶 = ( 𝐵 ↑m ( 𝑀 × 𝑁 ) )
3 mavmuldm.d ⊢ 𝐷 = ( 𝐵 ↑m 𝑁 )
4 mavmuldm.t ⊢ · = ( 𝑅 maVecMul ⟨ 𝑀 , 𝑁 ⟩ )
5 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
6 simp1 ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ) → 𝑅 ∈ 𝑉 )
7 simp2 ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ) → 𝑀 ∈ Fin )
8 simp3 ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ) → 𝑁 ∈ Fin )
9 4 1 5 6 7 8 mvmulfval ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ) → · = ( 𝑥 ∈ ( 𝐵 ↑m ( 𝑀 × 𝑁 ) ) , 𝑦 ∈ ( 𝐵 ↑m 𝑁 ) ↦ ( 𝑖 ∈ 𝑀 ↦ ( 𝑅 Σg ( 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 𝑥 𝑗 ) ( .r ‘ 𝑅 ) ( 𝑦 ‘ 𝑗 ) ) ) ) ) ) )
10 9 dmeqd ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ) → dom · = dom ( 𝑥 ∈ ( 𝐵 ↑m ( 𝑀 × 𝑁 ) ) , 𝑦 ∈ ( 𝐵 ↑m 𝑁 ) ↦ ( 𝑖 ∈ 𝑀 ↦ ( 𝑅 Σg ( 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 𝑥 𝑗 ) ( .r ‘ 𝑅 ) ( 𝑦 ‘ 𝑗 ) ) ) ) ) ) )
11 mptexg ⊢ ( 𝑀 ∈ Fin → ( 𝑖 ∈ 𝑀 ↦ ( 𝑅 Σg ( 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 𝑥 𝑗 ) ( .r ‘ 𝑅 ) ( 𝑦 ‘ 𝑗 ) ) ) ) ) ∈ V )
12 11 3ad2ant2 ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ) → ( 𝑖 ∈ 𝑀 ↦ ( 𝑅 Σg ( 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 𝑥 𝑗 ) ( .r ‘ 𝑅 ) ( 𝑦 ‘ 𝑗 ) ) ) ) ) ∈ V )
13 12 a1d ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ) → ( ( 𝑥 ∈ ( 𝐵 ↑m ( 𝑀 × 𝑁 ) ) ∧ 𝑦 ∈ ( 𝐵 ↑m 𝑁 ) ) → ( 𝑖 ∈ 𝑀 ↦ ( 𝑅 Σg ( 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 𝑥 𝑗 ) ( .r ‘ 𝑅 ) ( 𝑦 ‘ 𝑗 ) ) ) ) ) ∈ V ) )
14 13 ralrimivv ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ) → ∀ 𝑥 ∈ ( 𝐵 ↑m ( 𝑀 × 𝑁 ) ) ∀ 𝑦 ∈ ( 𝐵 ↑m 𝑁 ) ( 𝑖 ∈ 𝑀 ↦ ( 𝑅 Σg ( 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 𝑥 𝑗 ) ( .r ‘ 𝑅 ) ( 𝑦 ‘ 𝑗 ) ) ) ) ) ∈ V )
15 eqid ⊢ ( 𝑥 ∈ ( 𝐵 ↑m ( 𝑀 × 𝑁 ) ) , 𝑦 ∈ ( 𝐵 ↑m 𝑁 ) ↦ ( 𝑖 ∈ 𝑀 ↦ ( 𝑅 Σg ( 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 𝑥 𝑗 ) ( .r ‘ 𝑅 ) ( 𝑦 ‘ 𝑗 ) ) ) ) ) ) = ( 𝑥 ∈ ( 𝐵 ↑m ( 𝑀 × 𝑁 ) ) , 𝑦 ∈ ( 𝐵 ↑m 𝑁 ) ↦ ( 𝑖 ∈ 𝑀 ↦ ( 𝑅 Σg ( 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 𝑥 𝑗 ) ( .r ‘ 𝑅 ) ( 𝑦 ‘ 𝑗 ) ) ) ) ) )
16 15 dmmpoga ⊢ ( ∀ 𝑥 ∈ ( 𝐵 ↑m ( 𝑀 × 𝑁 ) ) ∀ 𝑦 ∈ ( 𝐵 ↑m 𝑁 ) ( 𝑖 ∈ 𝑀 ↦ ( 𝑅 Σg ( 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 𝑥 𝑗 ) ( .r ‘ 𝑅 ) ( 𝑦 ‘ 𝑗 ) ) ) ) ) ∈ V → dom ( 𝑥 ∈ ( 𝐵 ↑m ( 𝑀 × 𝑁 ) ) , 𝑦 ∈ ( 𝐵 ↑m 𝑁 ) ↦ ( 𝑖 ∈ 𝑀 ↦ ( 𝑅 Σg ( 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 𝑥 𝑗 ) ( .r ‘ 𝑅 ) ( 𝑦 ‘ 𝑗 ) ) ) ) ) ) = ( ( 𝐵 ↑m ( 𝑀 × 𝑁 ) ) × ( 𝐵 ↑m 𝑁 ) ) )
17 14 16 syl ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ) → dom ( 𝑥 ∈ ( 𝐵 ↑m ( 𝑀 × 𝑁 ) ) , 𝑦 ∈ ( 𝐵 ↑m 𝑁 ) ↦ ( 𝑖 ∈ 𝑀 ↦ ( 𝑅 Σg ( 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 𝑥 𝑗 ) ( .r ‘ 𝑅 ) ( 𝑦 ‘ 𝑗 ) ) ) ) ) ) = ( ( 𝐵 ↑m ( 𝑀 × 𝑁 ) ) × ( 𝐵 ↑m 𝑁 ) ) )
18 2 eqcomi ⊢ ( 𝐵 ↑m ( 𝑀 × 𝑁 ) ) = 𝐶
19 18 a1i ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ) → ( 𝐵 ↑m ( 𝑀 × 𝑁 ) ) = 𝐶 )
20 3 a1i ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ) → 𝐷 = ( 𝐵 ↑m 𝑁 ) )
21 20 eqcomd ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ) → ( 𝐵 ↑m 𝑁 ) = 𝐷 )
22 19 21 xpeq12d ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ) → ( ( 𝐵 ↑m ( 𝑀 × 𝑁 ) ) × ( 𝐵 ↑m 𝑁 ) ) = ( 𝐶 × 𝐷 ) )
23 10 17 22 3eqtrd ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ) → dom · = ( 𝐶 × 𝐷 ) )