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 · = ( 𝐶 × 𝐷 ) )