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

Metamath Proof Explorer

Theorem matmulcell

Description: Multiplication in the matrix ring for a single cell of a matrix. (Contributed by AV, 17-Nov-2019) (Revised by AV, 3-Jul-2022)

Ref Expression
Hypotheses matmulcell.a ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
matmulcell.b ⊢ 𝐵 = ( Base ‘ 𝐴 )
matmulcell.m ⊢ × = ( .r ‘ 𝐴 )
Assertion matmulcell ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) ) → ( 𝐼 ( 𝑋 × 𝑌 ) 𝐽 ) = ( 𝑅 Σg ( 𝑗 ∈ 𝑁 ↦ ( ( 𝐼 𝑋 𝑗 ) ( .r ‘ 𝑅 ) ( 𝑗 𝑌 𝐽 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 matmulcell.a ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
2 matmulcell.b ⊢ 𝐵 = ( Base ‘ 𝐴 )
3 matmulcell.m ⊢ × = ( .r ‘ 𝐴 )
4 1 2 matrcl ⊢ ( 𝑋 ∈ 𝐵 → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ V ) )
5 eqid ⊢ ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) = ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ )
6 1 5 matmulr ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ V ) → ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) = ( .r ‘ 𝐴 ) )
7 3 6 eqtr4id ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ V ) → × = ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) )
8 7 a1d ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ V ) → ( 𝑅 ∈ Ring → × = ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) ) )
9 4 8 syl ⊢ ( 𝑋 ∈ 𝐵 → ( 𝑅 ∈ Ring → × = ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) ) )
10 9 adantr ⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑅 ∈ Ring → × = ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) ) )
11 10 impcom ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → × = ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) )
12 11 3adant3 ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) ) → × = ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) )
13 12 oveqd ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) ) → ( 𝑋 × 𝑌 ) = ( 𝑋 ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) 𝑌 ) )
14 13 oveqd ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) ) → ( 𝐼 ( 𝑋 × 𝑌 ) 𝐽 ) = ( 𝐼 ( 𝑋 ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) 𝑌 ) 𝐽 ) )
15 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
16 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
17 simp1 ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) ) → 𝑅 ∈ Ring )
18 4 simpld ⊢ ( 𝑋 ∈ 𝐵 → 𝑁 ∈ Fin )
19 18 adantr ⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → 𝑁 ∈ Fin )
20 19 3ad2ant2 ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) ) → 𝑁 ∈ Fin )
21 1 15 2 matbas2i ⊢ ( 𝑋 ∈ 𝐵 → 𝑋 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) )
22 21 adantr ⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → 𝑋 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) )
23 22 3ad2ant2 ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) ) → 𝑋 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) )
24 1 15 2 matbas2i ⊢ ( 𝑌 ∈ 𝐵 → 𝑌 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) )
25 24 adantl ⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → 𝑌 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) )
26 25 3ad2ant2 ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) ) → 𝑌 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) )
27 simp3l ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) ) → 𝐼 ∈ 𝑁 )
28 simp3r ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) ) → 𝐽 ∈ 𝑁 )
29 5 15 16 17 20 20 20 23 26 27 28 mamufv ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) ) → ( 𝐼 ( 𝑋 ( 𝑅 maMul ⟨ 𝑁 , 𝑁 , 𝑁 ⟩ ) 𝑌 ) 𝐽 ) = ( 𝑅 Σg ( 𝑗 ∈ 𝑁 ↦ ( ( 𝐼 𝑋 𝑗 ) ( .r ‘ 𝑅 ) ( 𝑗 𝑌 𝐽 ) ) ) ) )
30 14 29 eqtrd ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) ) → ( 𝐼 ( 𝑋 × 𝑌 ) 𝐽 ) = ( 𝑅 Σg ( 𝑗 ∈ 𝑁 ↦ ( ( 𝐼 𝑋 𝑗 ) ( .r ‘ 𝑅 ) ( 𝑗 𝑌 𝐽 ) ) ) ) )