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

Metamath Proof Explorer

Theorem mat1comp

Description: The components of the identity matrix (as operation in maps-to notation). (Contributed by AV, 22-Jul-2019)

Ref Expression
Hypotheses mamumat1cl.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
mamumat1cl.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
mamumat1cl.o ⊢ 1 = ( 1r ‘ 𝑅 )
mamumat1cl.z ⊢ 0 = ( 0g ‘ 𝑅 )
mamumat1cl.i ⊢ 𝐼 = ( 𝑖 ∈ 𝑀 , 𝑗 ∈ 𝑀 ↦ if ( 𝑖 = 𝑗 , 1 , 0 ) )
mamumat1cl.m ⊢ ( 𝜑 → 𝑀 ∈ Fin )
Assertion mat1comp ( ( 𝐴 ∈ 𝑀 ∧ 𝐽 ∈ 𝑀 ) → ( 𝐴 𝐼 𝐽 ) = if ( 𝐴 = 𝐽 , 1 , 0 ) )

Proof

Step Hyp Ref Expression
1 mamumat1cl.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
2 mamumat1cl.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
3 mamumat1cl.o ⊢ 1 = ( 1r ‘ 𝑅 )
4 mamumat1cl.z ⊢ 0 = ( 0g ‘ 𝑅 )
5 mamumat1cl.i ⊢ 𝐼 = ( 𝑖 ∈ 𝑀 , 𝑗 ∈ 𝑀 ↦ if ( 𝑖 = 𝑗 , 1 , 0 ) )
6 mamumat1cl.m ⊢ ( 𝜑 → 𝑀 ∈ Fin )
7 eqeq1 ⊢ ( 𝑖 = 𝐴 → ( 𝑖 = 𝑗 ↔ 𝐴 = 𝑗 ) )
8 7 ifbid ⊢ ( 𝑖 = 𝐴 → if ( 𝑖 = 𝑗 , 1 , 0 ) = if ( 𝐴 = 𝑗 , 1 , 0 ) )
9 eqeq2 ⊢ ( 𝑗 = 𝐽 → ( 𝐴 = 𝑗 ↔ 𝐴 = 𝐽 ) )
10 9 ifbid ⊢ ( 𝑗 = 𝐽 → if ( 𝐴 = 𝑗 , 1 , 0 ) = if ( 𝐴 = 𝐽 , 1 , 0 ) )
11 3 fvexi ⊢ 1 ∈ V
12 4 fvexi ⊢ 0 ∈ V
13 11 12 ifex ⊢ if ( 𝐴 = 𝐽 , 1 , 0 ) ∈ V
14 8 10 5 13 ovmpo ⊢ ( ( 𝐴 ∈ 𝑀 ∧ 𝐽 ∈ 𝑀 ) → ( 𝐴 𝐼 𝐽 ) = if ( 𝐴 = 𝐽 , 1 , 0 ) )