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

Metamath Proof Explorer

Definition df-minmar1

Description: Define the matrices whose determinants are the minors of a square matrix. In contrast to the standard definition of minors, a row is replaced by 0's and one 1 instead of deleting the column and row (e.g., definition in Lang p. 515). By this, the determinant of such a matrix is equal to the minor determined in the standard way (as determinant of a submatrix, see df-subma - note that the matrix is transposed compared with the submatrix defined in df-subma , but this does not matter because the determinants are the same, see mdettpos ). Such matrices are used in the definition of an adjunct of a square matrix, see df-madu . (Contributed by AV, 27-Dec-2018)

Ref Expression
Assertion df-minmar1 minMatR1 = ( 𝑛 ∈ V , 𝑟 ∈ V ↦ ( 𝑚 ∈ ( Base ‘ ( 𝑛 Mat 𝑟 ) ) ↦ ( 𝑘 ∈ 𝑛 , 𝑙 ∈ 𝑛 ↦ ( 𝑖 ∈ 𝑛 , 𝑗 ∈ 𝑛 ↦ if ( 𝑖 = 𝑘 , if ( 𝑗 = 𝑙 , ( 1r ‘ 𝑟 ) , ( 0g ‘ 𝑟 ) ) , ( 𝑖 𝑚 𝑗 ) ) ) ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cminmar1 ⊢ minMatR1
1 vn ⊢ 𝑛
2 cvv ⊢ V
3 vr ⊢ 𝑟
4 vm ⊢ 𝑚
5 cbs ⊢ Base
6 1 cv ⊢ 𝑛
7 cmat ⊢ Mat
8 3 cv ⊢ 𝑟
9 6 8 7 co ⊢ ( 𝑛 Mat 𝑟 )
10 9 5 cfv ⊢ ( Base ‘ ( 𝑛 Mat 𝑟 ) )
11 vk ⊢ 𝑘
12 vl ⊢ 𝑙
13 vi ⊢ 𝑖
14 vj ⊢ 𝑗
15 13 cv ⊢ 𝑖
16 11 cv ⊢ 𝑘
17 15 16 wceq ⊢ 𝑖 = 𝑘
18 14 cv ⊢ 𝑗
19 12 cv ⊢ 𝑙
20 18 19 wceq ⊢ 𝑗 = 𝑙
21 cur ⊢ 1r
22 8 21 cfv ⊢ ( 1r ‘ 𝑟 )
23 c0g ⊢ 0g
24 8 23 cfv ⊢ ( 0g ‘ 𝑟 )
25 20 22 24 cif ⊢ if ( 𝑗 = 𝑙 , ( 1r ‘ 𝑟 ) , ( 0g ‘ 𝑟 ) )
26 4 cv ⊢ 𝑚
27 15 18 26 co ⊢ ( 𝑖 𝑚 𝑗 )
28 17 25 27 cif ⊢ if ( 𝑖 = 𝑘 , if ( 𝑗 = 𝑙 , ( 1r ‘ 𝑟 ) , ( 0g ‘ 𝑟 ) ) , ( 𝑖 𝑚 𝑗 ) )
29 13 14 6 6 28 cmpo ⊢ ( 𝑖 ∈ 𝑛 , 𝑗 ∈ 𝑛 ↦ if ( 𝑖 = 𝑘 , if ( 𝑗 = 𝑙 , ( 1r ‘ 𝑟 ) , ( 0g ‘ 𝑟 ) ) , ( 𝑖 𝑚 𝑗 ) ) )
30 11 12 6 6 29 cmpo ⊢ ( 𝑘 ∈ 𝑛 , 𝑙 ∈ 𝑛 ↦ ( 𝑖 ∈ 𝑛 , 𝑗 ∈ 𝑛 ↦ if ( 𝑖 = 𝑘 , if ( 𝑗 = 𝑙 , ( 1r ‘ 𝑟 ) , ( 0g ‘ 𝑟 ) ) , ( 𝑖 𝑚 𝑗 ) ) ) )
31 4 10 30 cmpt ⊢ ( 𝑚 ∈ ( Base ‘ ( 𝑛 Mat 𝑟 ) ) ↦ ( 𝑘 ∈ 𝑛 , 𝑙 ∈ 𝑛 ↦ ( 𝑖 ∈ 𝑛 , 𝑗 ∈ 𝑛 ↦ if ( 𝑖 = 𝑘 , if ( 𝑗 = 𝑙 , ( 1r ‘ 𝑟 ) , ( 0g ‘ 𝑟 ) ) , ( 𝑖 𝑚 𝑗 ) ) ) ) )
32 1 3 2 2 31 cmpo ⊢ ( 𝑛 ∈ V , 𝑟 ∈ V ↦ ( 𝑚 ∈ ( Base ‘ ( 𝑛 Mat 𝑟 ) ) ↦ ( 𝑘 ∈ 𝑛 , 𝑙 ∈ 𝑛 ↦ ( 𝑖 ∈ 𝑛 , 𝑗 ∈ 𝑛 ↦ if ( 𝑖 = 𝑘 , if ( 𝑗 = 𝑙 , ( 1r ‘ 𝑟 ) , ( 0g ‘ 𝑟 ) ) , ( 𝑖 𝑚 𝑗 ) ) ) ) ) )
33 0 32 wceq ⊢ minMatR1 = ( 𝑛 ∈ V , 𝑟 ∈ V ↦ ( 𝑚 ∈ ( Base ‘ ( 𝑛 Mat 𝑟 ) ) ↦ ( 𝑘 ∈ 𝑛 , 𝑙 ∈ 𝑛 ↦ ( 𝑖 ∈ 𝑛 , 𝑗 ∈ 𝑛 ↦ if ( 𝑖 = 𝑘 , if ( 𝑗 = 𝑙 , ( 1r ‘ 𝑟 ) , ( 0g ‘ 𝑟 ) ) , ( 𝑖 𝑚 𝑗 ) ) ) ) ) )