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

Metamath Proof Explorer

Theorem mat1ov

Description: Entries of an identity matrix, deduction form. (Contributed by Stefan O'Rear, 10-Jul-2018)

Ref Expression
Hypotheses mat1.a ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
mat1.o ⊢ 1 = ( 1r ‘ 𝑅 )
mat1.z ⊢ 0 = ( 0g ‘ 𝑅 )
mat1ov.n ⊢ ( 𝜑 → 𝑁 ∈ Fin )
mat1ov.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
mat1ov.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑁 )
mat1ov.j ⊢ ( 𝜑 → 𝐽 ∈ 𝑁 )
mat1ov.u ⊢ 𝑈 = ( 1r ‘ 𝐴 )
Assertion mat1ov ( 𝜑 → ( 𝐼 𝑈 𝐽 ) = if ( 𝐼 = 𝐽 , 1 , 0 ) )

Proof

Step Hyp Ref Expression
1 mat1.a ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
2 mat1.o ⊢ 1 = ( 1r ‘ 𝑅 )
3 mat1.z ⊢ 0 = ( 0g ‘ 𝑅 )
4 mat1ov.n ⊢ ( 𝜑 → 𝑁 ∈ Fin )
5 mat1ov.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
6 mat1ov.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑁 )
7 mat1ov.j ⊢ ( 𝜑 → 𝐽 ∈ 𝑁 )
8 mat1ov.u ⊢ 𝑈 = ( 1r ‘ 𝐴 )
9 1 2 3 mat1 ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 1r ‘ 𝐴 ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝑗 , 1 , 0 ) ) )
10 4 5 9 syl2anc ⊢ ( 𝜑 → ( 1r ‘ 𝐴 ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝑗 , 1 , 0 ) ) )
11 8 10 eqtrid ⊢ ( 𝜑 → 𝑈 = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝑗 , 1 , 0 ) ) )
12 eqeq12 ⊢ ( ( 𝑖 = 𝐼 ∧ 𝑗 = 𝐽 ) → ( 𝑖 = 𝑗 ↔ 𝐼 = 𝐽 ) )
13 12 ifbid ⊢ ( ( 𝑖 = 𝐼 ∧ 𝑗 = 𝐽 ) → if ( 𝑖 = 𝑗 , 1 , 0 ) = if ( 𝐼 = 𝐽 , 1 , 0 ) )
14 13 adantl ⊢ ( ( 𝜑 ∧ ( 𝑖 = 𝐼 ∧ 𝑗 = 𝐽 ) ) → if ( 𝑖 = 𝑗 , 1 , 0 ) = if ( 𝐼 = 𝐽 , 1 , 0 ) )
15 2 fvexi ⊢ 1 ∈ V
16 3 fvexi ⊢ 0 ∈ V
17 15 16 ifex ⊢ if ( 𝐼 = 𝐽 , 1 , 0 ) ∈ V
18 17 a1i ⊢ ( 𝜑 → if ( 𝐼 = 𝐽 , 1 , 0 ) ∈ V )
19 11 14 6 7 18 ovmpod ⊢ ( 𝜑 → ( 𝐼 𝑈 𝐽 ) = if ( 𝐼 = 𝐽 , 1 , 0 ) )