Theorem minmar1eval

Description: An entry of a matrix for a minor. (Contributed by AV, 31-Dec-2018)

	Ref	Expression
Hypotheses	minmar1fval.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
	minmar1fval.b	⊢ 𝐵 = ( Base ‘ 𝐴 )
	minmar1fval.q	⊢ 𝑄 = ( 𝑁 minMatR1 𝑅 )
	minmar1fval.o	⊢ 1 = ( 1r ‘ 𝑅 )
	minmar1fval.z	⊢ 0 = ( 0g ‘ 𝑅 )
Assertion	minmar1eval	⊢ ( ( 𝑀 ∈ 𝐵 ∧ ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) ) → ( 𝐼 ( 𝐾 ( 𝑄 ‘ 𝑀 ) 𝐿 ) 𝐽 ) = if ( 𝐼 = 𝐾 , if ( 𝐽 = 𝐿 , 1 , 0 ) , ( 𝐼 𝑀 𝐽 ) ) )

Proof

Step	Hyp	Ref	Expression
1		minmar1fval.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
2		minmar1fval.b	⊢ 𝐵 = ( Base ‘ 𝐴 )
3		minmar1fval.q	⊢ 𝑄 = ( 𝑁 minMatR1 𝑅 )
4		minmar1fval.o	⊢ 1 = ( 1r ‘ 𝑅 )
5		minmar1fval.z	⊢ 0 = ( 0g ‘ 𝑅 )
6	1 2 3 4 5	minmar1val	⊢ ( ( 𝑀 ∈ 𝐵 ∧ 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ) → ( 𝐾 ( 𝑄 ‘ 𝑀 ) 𝐿 ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐾 , if ( 𝑗 = 𝐿 , 1 , 0 ) , ( 𝑖 𝑀 𝑗 ) ) ) )
7	6	3expb	⊢ ( ( 𝑀 ∈ 𝐵 ∧ ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ) ) → ( 𝐾 ( 𝑄 ‘ 𝑀 ) 𝐿 ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐾 , if ( 𝑗 = 𝐿 , 1 , 0 ) , ( 𝑖 𝑀 𝑗 ) ) ) )
8	7	3adant3	⊢ ( ( 𝑀 ∈ 𝐵 ∧ ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) ) → ( 𝐾 ( 𝑄 ‘ 𝑀 ) 𝐿 ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐾 , if ( 𝑗 = 𝐿 , 1 , 0 ) , ( 𝑖 𝑀 𝑗 ) ) ) )
9		simp3l	⊢ ( ( 𝑀 ∈ 𝐵 ∧ ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) ) → 𝐼 ∈ 𝑁 )
10		simpl3r	⊢ ( ( ( 𝑀 ∈ 𝐵 ∧ ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) ) ∧ 𝑖 = 𝐼 ) → 𝐽 ∈ 𝑁 )
11	4	fvexi	⊢ 1 ∈ V
12	5	fvexi	⊢ 0 ∈ V
13	11 12	ifex	⊢ if ( 𝑗 = 𝐿 , 1 , 0 ) ∈ V
14		ovex	⊢ ( 𝑖 𝑀 𝑗 ) ∈ V
15	13 14	ifex	⊢ if ( 𝑖 = 𝐾 , if ( 𝑗 = 𝐿 , 1 , 0 ) , ( 𝑖 𝑀 𝑗 ) ) ∈ V
16	15	a1i	⊢ ( ( ( 𝑀 ∈ 𝐵 ∧ ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) ) ∧ ( 𝑖 = 𝐼 ∧ 𝑗 = 𝐽 ) ) → if ( 𝑖 = 𝐾 , if ( 𝑗 = 𝐿 , 1 , 0 ) , ( 𝑖 𝑀 𝑗 ) ) ∈ V )
17		eqeq1	⊢ ( 𝑖 = 𝐼 → ( 𝑖 = 𝐾 ↔ 𝐼 = 𝐾 ) )
18	17	adantr	⊢ ( ( 𝑖 = 𝐼 ∧ 𝑗 = 𝐽 ) → ( 𝑖 = 𝐾 ↔ 𝐼 = 𝐾 ) )
19		eqeq1	⊢ ( 𝑗 = 𝐽 → ( 𝑗 = 𝐿 ↔ 𝐽 = 𝐿 ) )
20	19	adantl	⊢ ( ( 𝑖 = 𝐼 ∧ 𝑗 = 𝐽 ) → ( 𝑗 = 𝐿 ↔ 𝐽 = 𝐿 ) )
21	20	ifbid	⊢ ( ( 𝑖 = 𝐼 ∧ 𝑗 = 𝐽 ) → if ( 𝑗 = 𝐿 , 1 , 0 ) = if ( 𝐽 = 𝐿 , 1 , 0 ) )
22		oveq12	⊢ ( ( 𝑖 = 𝐼 ∧ 𝑗 = 𝐽 ) → ( 𝑖 𝑀 𝑗 ) = ( 𝐼 𝑀 𝐽 ) )
23	18 21 22	ifbieq12d	⊢ ( ( 𝑖 = 𝐼 ∧ 𝑗 = 𝐽 ) → if ( 𝑖 = 𝐾 , if ( 𝑗 = 𝐿 , 1 , 0 ) , ( 𝑖 𝑀 𝑗 ) ) = if ( 𝐼 = 𝐾 , if ( 𝐽 = 𝐿 , 1 , 0 ) , ( 𝐼 𝑀 𝐽 ) ) )
24	23	adantl	⊢ ( ( ( 𝑀 ∈ 𝐵 ∧ ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) ) ∧ ( 𝑖 = 𝐼 ∧ 𝑗 = 𝐽 ) ) → if ( 𝑖 = 𝐾 , if ( 𝑗 = 𝐿 , 1 , 0 ) , ( 𝑖 𝑀 𝑗 ) ) = if ( 𝐼 = 𝐾 , if ( 𝐽 = 𝐿 , 1 , 0 ) , ( 𝐼 𝑀 𝐽 ) ) )
25	9 10 16 24	ovmpodv2	⊢ ( ( 𝑀 ∈ 𝐵 ∧ ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) ) → ( ( 𝐾 ( 𝑄 ‘ 𝑀 ) 𝐿 ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝐾 , if ( 𝑗 = 𝐿 , 1 , 0 ) , ( 𝑖 𝑀 𝑗 ) ) ) → ( 𝐼 ( 𝐾 ( 𝑄 ‘ 𝑀 ) 𝐿 ) 𝐽 ) = if ( 𝐼 = 𝐾 , if ( 𝐽 = 𝐿 , 1 , 0 ) , ( 𝐼 𝑀 𝐽 ) ) ) )
26	8 25	mpd	⊢ ( ( 𝑀 ∈ 𝐵 ∧ ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ) ∧ ( 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁 ) ) → ( 𝐼 ( 𝐾 ( 𝑄 ‘ 𝑀 ) 𝐿 ) 𝐽 ) = if ( 𝐼 = 𝐾 , if ( 𝐽 = 𝐿 , 1 , 0 ) , ( 𝐼 𝑀 𝐽 ) ) )