Theorem minmar1fval

Description: First substitution for the definition 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	minmar1fval	⊢ 𝑄 = ( 𝑚 ∈ 𝐵 ↦ ( 𝑘 ∈ 𝑁 , 𝑙 ∈ 𝑁 ↦ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ 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		oveq12	⊢ ( ( 𝑛 = 𝑁 ∧ 𝑟 = 𝑅 ) → ( 𝑛 Mat 𝑟 ) = ( 𝑁 Mat 𝑅 ) )
7	6 1	eqtr4di	⊢ ( ( 𝑛 = 𝑁 ∧ 𝑟 = 𝑅 ) → ( 𝑛 Mat 𝑟 ) = 𝐴 )
8	7	fveq2d	⊢ ( ( 𝑛 = 𝑁 ∧ 𝑟 = 𝑅 ) → ( Base ‘ ( 𝑛 Mat 𝑟 ) ) = ( Base ‘ 𝐴 ) )
9	8 2	eqtr4di	⊢ ( ( 𝑛 = 𝑁 ∧ 𝑟 = 𝑅 ) → ( Base ‘ ( 𝑛 Mat 𝑟 ) ) = 𝐵 )
10		simpl	⊢ ( ( 𝑛 = 𝑁 ∧ 𝑟 = 𝑅 ) → 𝑛 = 𝑁 )
11		fveq2	⊢ ( 𝑟 = 𝑅 → ( 1r ‘ 𝑟 ) = ( 1r ‘ 𝑅 ) )
12	11 4	eqtr4di	⊢ ( 𝑟 = 𝑅 → ( 1r ‘ 𝑟 ) = 1 )
13		fveq2	⊢ ( 𝑟 = 𝑅 → ( 0g ‘ 𝑟 ) = ( 0g ‘ 𝑅 ) )
14	13 5	eqtr4di	⊢ ( 𝑟 = 𝑅 → ( 0g ‘ 𝑟 ) = 0 )
15	12 14	ifeq12d	⊢ ( 𝑟 = 𝑅 → if ( 𝑗 = 𝑙 , ( 1r ‘ 𝑟 ) , ( 0g ‘ 𝑟 ) ) = if ( 𝑗 = 𝑙 , 1 , 0 ) )
16	15	ifeq1d	⊢ ( 𝑟 = 𝑅 → if ( 𝑖 = 𝑘 , if ( 𝑗 = 𝑙 , ( 1r ‘ 𝑟 ) , ( 0g ‘ 𝑟 ) ) , ( 𝑖 𝑚 𝑗 ) ) = if ( 𝑖 = 𝑘 , if ( 𝑗 = 𝑙 , 1 , 0 ) , ( 𝑖 𝑚 𝑗 ) ) )
17	16	adantl	⊢ ( ( 𝑛 = 𝑁 ∧ 𝑟 = 𝑅 ) → if ( 𝑖 = 𝑘 , if ( 𝑗 = 𝑙 , ( 1r ‘ 𝑟 ) , ( 0g ‘ 𝑟 ) ) , ( 𝑖 𝑚 𝑗 ) ) = if ( 𝑖 = 𝑘 , if ( 𝑗 = 𝑙 , 1 , 0 ) , ( 𝑖 𝑚 𝑗 ) ) )
18	10 10 17	mpoeq123dv	⊢ ( ( 𝑛 = 𝑁 ∧ 𝑟 = 𝑅 ) → ( 𝑖 ∈ 𝑛 , 𝑗 ∈ 𝑛 ↦ if ( 𝑖 = 𝑘 , if ( 𝑗 = 𝑙 , ( 1r ‘ 𝑟 ) , ( 0g ‘ 𝑟 ) ) , ( 𝑖 𝑚 𝑗 ) ) ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝑘 , if ( 𝑗 = 𝑙 , 1 , 0 ) , ( 𝑖 𝑚 𝑗 ) ) ) )
19	10 10 18	mpoeq123dv	⊢ ( ( 𝑛 = 𝑁 ∧ 𝑟 = 𝑅 ) → ( 𝑘 ∈ 𝑛 , 𝑙 ∈ 𝑛 ↦ ( 𝑖 ∈ 𝑛 , 𝑗 ∈ 𝑛 ↦ if ( 𝑖 = 𝑘 , if ( 𝑗 = 𝑙 , ( 1r ‘ 𝑟 ) , ( 0g ‘ 𝑟 ) ) , ( 𝑖 𝑚 𝑗 ) ) ) ) = ( 𝑘 ∈ 𝑁 , 𝑙 ∈ 𝑁 ↦ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝑘 , if ( 𝑗 = 𝑙 , 1 , 0 ) , ( 𝑖 𝑚 𝑗 ) ) ) ) )
20	9 19	mpteq12dv	⊢ ( ( 𝑛 = 𝑁 ∧ 𝑟 = 𝑅 ) → ( 𝑚 ∈ ( Base ‘ ( 𝑛 Mat 𝑟 ) ) ↦ ( 𝑘 ∈ 𝑛 , 𝑙 ∈ 𝑛 ↦ ( 𝑖 ∈ 𝑛 , 𝑗 ∈ 𝑛 ↦ if ( 𝑖 = 𝑘 , if ( 𝑗 = 𝑙 , ( 1r ‘ 𝑟 ) , ( 0g ‘ 𝑟 ) ) , ( 𝑖 𝑚 𝑗 ) ) ) ) ) = ( 𝑚 ∈ 𝐵 ↦ ( 𝑘 ∈ 𝑁 , 𝑙 ∈ 𝑁 ↦ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝑘 , if ( 𝑗 = 𝑙 , 1 , 0 ) , ( 𝑖 𝑚 𝑗 ) ) ) ) ) )
21		df-minmar1	⊢ minMatR1 = ( 𝑛 ∈ V , 𝑟 ∈ V ↦ ( 𝑚 ∈ ( Base ‘ ( 𝑛 Mat 𝑟 ) ) ↦ ( 𝑘 ∈ 𝑛 , 𝑙 ∈ 𝑛 ↦ ( 𝑖 ∈ 𝑛 , 𝑗 ∈ 𝑛 ↦ if ( 𝑖 = 𝑘 , if ( 𝑗 = 𝑙 , ( 1r ‘ 𝑟 ) , ( 0g ‘ 𝑟 ) ) , ( 𝑖 𝑚 𝑗 ) ) ) ) ) )
22	2	fvexi	⊢ 𝐵 ∈ V
23	22	mptex	⊢ ( 𝑚 ∈ 𝐵 ↦ ( 𝑘 ∈ 𝑁 , 𝑙 ∈ 𝑁 ↦ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝑘 , if ( 𝑗 = 𝑙 , 1 , 0 ) , ( 𝑖 𝑚 𝑗 ) ) ) ) ) ∈ V
24	20 21 23	ovmpoa	⊢ ( ( 𝑁 ∈ V ∧ 𝑅 ∈ V ) → ( 𝑁 minMatR1 𝑅 ) = ( 𝑚 ∈ 𝐵 ↦ ( 𝑘 ∈ 𝑁 , 𝑙 ∈ 𝑁 ↦ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝑘 , if ( 𝑗 = 𝑙 , 1 , 0 ) , ( 𝑖 𝑚 𝑗 ) ) ) ) ) )
25	21	mpondm0	⊢ ( ¬ ( 𝑁 ∈ V ∧ 𝑅 ∈ V ) → ( 𝑁 minMatR1 𝑅 ) = ∅ )
26		mpt0	⊢ ( 𝑚 ∈ ∅ ↦ ( 𝑘 ∈ 𝑁 , 𝑙 ∈ 𝑁 ↦ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝑘 , if ( 𝑗 = 𝑙 , 1 , 0 ) , ( 𝑖 𝑚 𝑗 ) ) ) ) ) = ∅
27	25 26	eqtr4di	⊢ ( ¬ ( 𝑁 ∈ V ∧ 𝑅 ∈ V ) → ( 𝑁 minMatR1 𝑅 ) = ( 𝑚 ∈ ∅ ↦ ( 𝑘 ∈ 𝑁 , 𝑙 ∈ 𝑁 ↦ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝑘 , if ( 𝑗 = 𝑙 , 1 , 0 ) , ( 𝑖 𝑚 𝑗 ) ) ) ) ) )
28	1	fveq2i	⊢ ( Base ‘ 𝐴 ) = ( Base ‘ ( 𝑁 Mat 𝑅 ) )
29	2 28	eqtri	⊢ 𝐵 = ( Base ‘ ( 𝑁 Mat 𝑅 ) )
30		matbas0pc	⊢ ( ¬ ( 𝑁 ∈ V ∧ 𝑅 ∈ V ) → ( Base ‘ ( 𝑁 Mat 𝑅 ) ) = ∅ )
31	29 30	syl5eq	⊢ ( ¬ ( 𝑁 ∈ V ∧ 𝑅 ∈ V ) → 𝐵 = ∅ )
32	31	mpteq1d	⊢ ( ¬ ( 𝑁 ∈ V ∧ 𝑅 ∈ V ) → ( 𝑚 ∈ 𝐵 ↦ ( 𝑘 ∈ 𝑁 , 𝑙 ∈ 𝑁 ↦ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝑘 , if ( 𝑗 = 𝑙 , 1 , 0 ) , ( 𝑖 𝑚 𝑗 ) ) ) ) ) = ( 𝑚 ∈ ∅ ↦ ( 𝑘 ∈ 𝑁 , 𝑙 ∈ 𝑁 ↦ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝑘 , if ( 𝑗 = 𝑙 , 1 , 0 ) , ( 𝑖 𝑚 𝑗 ) ) ) ) ) )
33	27 32	eqtr4d	⊢ ( ¬ ( 𝑁 ∈ V ∧ 𝑅 ∈ V ) → ( 𝑁 minMatR1 𝑅 ) = ( 𝑚 ∈ 𝐵 ↦ ( 𝑘 ∈ 𝑁 , 𝑙 ∈ 𝑁 ↦ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝑘 , if ( 𝑗 = 𝑙 , 1 , 0 ) , ( 𝑖 𝑚 𝑗 ) ) ) ) ) )
34	24 33	pm2.61i	⊢ ( 𝑁 minMatR1 𝑅 ) = ( 𝑚 ∈ 𝐵 ↦ ( 𝑘 ∈ 𝑁 , 𝑙 ∈ 𝑁 ↦ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝑘 , if ( 𝑗 = 𝑙 , 1 , 0 ) , ( 𝑖 𝑚 𝑗 ) ) ) ) )
35	3 34	eqtri	⊢ 𝑄 = ( 𝑚 ∈ 𝐵 ↦ ( 𝑘 ∈ 𝑁 , 𝑙 ∈ 𝑁 ↦ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ if ( 𝑖 = 𝑘 , if ( 𝑗 = 𝑙 , 1 , 0 ) , ( 𝑖 𝑚 𝑗 ) ) ) ) )