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