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 ‘ 𝑅 ) ( 𝑗 𝑌 𝐽 ) ) ) ) )