Metamath Proof Explorer

Theorem mamudm

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

Ref Expression
Hypotheses mamudm.e ⊢ 𝐸 = ( 𝑅 freeLMod ( 𝑀 × 𝑁 ) )
mamudm.b ⊢ 𝐵 = ( Base ‘ 𝐸 )
mamudm.f ⊢ 𝐹 = ( 𝑅 freeLMod ( 𝑁 × 𝑃 ) )
mamudm.c ⊢ 𝐶 = ( Base ‘ 𝐹 )
mamudm.m ⊢ × = ( 𝑅 maMul ⟨ 𝑀 , 𝑁 , 𝑃 ⟩ )
Assertion mamudm ( ( 𝑅 ∈ 𝑉 ∧ ( 𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ∧ 𝑃 ∈ Fin ) ) → dom × = ( 𝐵 × 𝐶 ) )

Proof

Step Hyp Ref Expression
1 mamudm.e ⊢ 𝐸 = ( 𝑅 freeLMod ( 𝑀 × 𝑁 ) )
2 mamudm.b ⊢ 𝐵 = ( Base ‘ 𝐸 )
3 mamudm.f ⊢ 𝐹 = ( 𝑅 freeLMod ( 𝑁 × 𝑃 ) )
4 mamudm.c ⊢ 𝐶 = ( Base ‘ 𝐹 )
5 mamudm.m ⊢ × = ( 𝑅 maMul ⟨ 𝑀 , 𝑁 , 𝑃 ⟩ )
6 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
7 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
8 simpl ⊢ ( ( 𝑅 ∈ 𝑉 ∧ ( 𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ∧ 𝑃 ∈ Fin ) ) → 𝑅 ∈ 𝑉 )
9 simpr1 ⊢ ( ( 𝑅 ∈ 𝑉 ∧ ( 𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ∧ 𝑃 ∈ Fin ) ) → 𝑀 ∈ Fin )
10 simpr2 ⊢ ( ( 𝑅 ∈ 𝑉 ∧ ( 𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ∧ 𝑃 ∈ Fin ) ) → 𝑁 ∈ Fin )
11 simpr3 ⊢ ( ( 𝑅 ∈ 𝑉 ∧ ( 𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ∧ 𝑃 ∈ Fin ) ) → 𝑃 ∈ Fin )
12 5 6 7 8 9 10 11 mamufval ⊢ ( ( 𝑅 ∈ 𝑉 ∧ ( 𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ∧ 𝑃 ∈ Fin ) ) → × = ( 𝑥 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑀 × 𝑁 ) ) , 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑃 ) ) ↦ ( 𝑖 ∈ 𝑀 , 𝑘 ∈ 𝑃 ↦ ( 𝑅 Σg ( 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 𝑥 𝑗 ) ( .r ‘ 𝑅 ) ( 𝑗 𝑦 𝑘 ) ) ) ) ) ) )
13 12 dmeqd ⊢ ( ( 𝑅 ∈ 𝑉 ∧ ( 𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ∧ 𝑃 ∈ Fin ) ) → dom × = dom ( 𝑥 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑀 × 𝑁 ) ) , 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑃 ) ) ↦ ( 𝑖 ∈ 𝑀 , 𝑘 ∈ 𝑃 ↦ ( 𝑅 Σg ( 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 𝑥 𝑗 ) ( .r ‘ 𝑅 ) ( 𝑗 𝑦 𝑘 ) ) ) ) ) ) )
14 mpoexga ⊢ ( ( 𝑀 ∈ Fin ∧ 𝑃 ∈ Fin ) → ( 𝑖 ∈ 𝑀 , 𝑘 ∈ 𝑃 ↦ ( 𝑅 Σg ( 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 𝑥 𝑗 ) ( .r ‘ 𝑅 ) ( 𝑗 𝑦 𝑘 ) ) ) ) ) ∈ V )
15 14 3adant2 ⊢ ( ( 𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ∧ 𝑃 ∈ Fin ) → ( 𝑖 ∈ 𝑀 , 𝑘 ∈ 𝑃 ↦ ( 𝑅 Σg ( 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 𝑥 𝑗 ) ( .r ‘ 𝑅 ) ( 𝑗 𝑦 𝑘 ) ) ) ) ) ∈ V )
16 15 adantl ⊢ ( ( 𝑅 ∈ 𝑉 ∧ ( 𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ∧ 𝑃 ∈ Fin ) ) → ( 𝑖 ∈ 𝑀 , 𝑘 ∈ 𝑃 ↦ ( 𝑅 Σg ( 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 𝑥 𝑗 ) ( .r ‘ 𝑅 ) ( 𝑗 𝑦 𝑘 ) ) ) ) ) ∈ V )
17 16 a1d ⊢ ( ( 𝑅 ∈ 𝑉 ∧ ( 𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ∧ 𝑃 ∈ Fin ) ) → ( ( 𝑥 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑀 × 𝑁 ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑃 ) ) ) → ( 𝑖 ∈ 𝑀 , 𝑘 ∈ 𝑃 ↦ ( 𝑅 Σg ( 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 𝑥 𝑗 ) ( .r ‘ 𝑅 ) ( 𝑗 𝑦 𝑘 ) ) ) ) ) ∈ V ) )
18 17 ralrimivv ⊢ ( ( 𝑅 ∈ 𝑉 ∧ ( 𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ∧ 𝑃 ∈ Fin ) ) → ∀ 𝑥 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑀 × 𝑁 ) ) ∀ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑃 ) ) ( 𝑖 ∈ 𝑀 , 𝑘 ∈ 𝑃 ↦ ( 𝑅 Σg ( 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 𝑥 𝑗 ) ( .r ‘ 𝑅 ) ( 𝑗 𝑦 𝑘 ) ) ) ) ) ∈ V )
19 eqid ⊢ ( 𝑥 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑀 × 𝑁 ) ) , 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑃 ) ) ↦ ( 𝑖 ∈ 𝑀 , 𝑘 ∈ 𝑃 ↦ ( 𝑅 Σg ( 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 𝑥 𝑗 ) ( .r ‘ 𝑅 ) ( 𝑗 𝑦 𝑘 ) ) ) ) ) ) = ( 𝑥 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑀 × 𝑁 ) ) , 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑃 ) ) ↦ ( 𝑖 ∈ 𝑀 , 𝑘 ∈ 𝑃 ↦ ( 𝑅 Σg ( 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 𝑥 𝑗 ) ( .r ‘ 𝑅 ) ( 𝑗 𝑦 𝑘 ) ) ) ) ) )
20 19 dmmpoga ⊢ ( ∀ 𝑥 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑀 × 𝑁 ) ) ∀ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑃 ) ) ( 𝑖 ∈ 𝑀 , 𝑘 ∈ 𝑃 ↦ ( 𝑅 Σg ( 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 𝑥 𝑗 ) ( .r ‘ 𝑅 ) ( 𝑗 𝑦 𝑘 ) ) ) ) ) ∈ V → dom ( 𝑥 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑀 × 𝑁 ) ) , 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑃 ) ) ↦ ( 𝑖 ∈ 𝑀 , 𝑘 ∈ 𝑃 ↦ ( 𝑅 Σg ( 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 𝑥 𝑗 ) ( .r ‘ 𝑅 ) ( 𝑗 𝑦 𝑘 ) ) ) ) ) ) = ( ( ( Base ‘ 𝑅 ) ↑m ( 𝑀 × 𝑁 ) ) × ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑃 ) ) ) )
21 18 20 syl ⊢ ( ( 𝑅 ∈ 𝑉 ∧ ( 𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ∧ 𝑃 ∈ Fin ) ) → dom ( 𝑥 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑀 × 𝑁 ) ) , 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑃 ) ) ↦ ( 𝑖 ∈ 𝑀 , 𝑘 ∈ 𝑃 ↦ ( 𝑅 Σg ( 𝑗 ∈ 𝑁 ↦ ( ( 𝑖 𝑥 𝑗 ) ( .r ‘ 𝑅 ) ( 𝑗 𝑦 𝑘 ) ) ) ) ) ) = ( ( ( Base ‘ 𝑅 ) ↑m ( 𝑀 × 𝑁 ) ) × ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑃 ) ) ) )
22 xpfi ⊢ ( ( 𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ) → ( 𝑀 × 𝑁 ) ∈ Fin )
23 22 3adant3 ⊢ ( ( 𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ∧ 𝑃 ∈ Fin ) → ( 𝑀 × 𝑁 ) ∈ Fin )
24 1 6 frlmfibas ⊢ ( ( 𝑅 ∈ 𝑉 ∧ ( 𝑀 × 𝑁 ) ∈ Fin ) → ( ( Base ‘ 𝑅 ) ↑m ( 𝑀 × 𝑁 ) ) = ( Base ‘ 𝐸 ) )
25 23 24 sylan2 ⊢ ( ( 𝑅 ∈ 𝑉 ∧ ( 𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ∧ 𝑃 ∈ Fin ) ) → ( ( Base ‘ 𝑅 ) ↑m ( 𝑀 × 𝑁 ) ) = ( Base ‘ 𝐸 ) )
26 25 2 eqtr4di ⊢ ( ( 𝑅 ∈ 𝑉 ∧ ( 𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ∧ 𝑃 ∈ Fin ) ) → ( ( Base ‘ 𝑅 ) ↑m ( 𝑀 × 𝑁 ) ) = 𝐵 )
27 xpfi ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑃 ∈ Fin ) → ( 𝑁 × 𝑃 ) ∈ Fin )
28 27 3adant1 ⊢ ( ( 𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ∧ 𝑃 ∈ Fin ) → ( 𝑁 × 𝑃 ) ∈ Fin )
29 3 6 frlmfibas ⊢ ( ( 𝑅 ∈ 𝑉 ∧ ( 𝑁 × 𝑃 ) ∈ Fin ) → ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑃 ) ) = ( Base ‘ 𝐹 ) )
30 28 29 sylan2 ⊢ ( ( 𝑅 ∈ 𝑉 ∧ ( 𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ∧ 𝑃 ∈ Fin ) ) → ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑃 ) ) = ( Base ‘ 𝐹 ) )
31 30 4 eqtr4di ⊢ ( ( 𝑅 ∈ 𝑉 ∧ ( 𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ∧ 𝑃 ∈ Fin ) ) → ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑃 ) ) = 𝐶 )
32 26 31 xpeq12d ⊢ ( ( 𝑅 ∈ 𝑉 ∧ ( 𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ∧ 𝑃 ∈ Fin ) ) → ( ( ( Base ‘ 𝑅 ) ↑m ( 𝑀 × 𝑁 ) ) × ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑃 ) ) ) = ( 𝐵 × 𝐶 ) )
33 13 21 32 3eqtrd ⊢ ( ( 𝑅 ∈ 𝑉 ∧ ( 𝑀 ∈ Fin ∧ 𝑁 ∈ Fin ∧ 𝑃 ∈ Fin ) ) → dom × = ( 𝐵 × 𝐶 ) )