Definition df-madu 21783

Description: Define the adjugate or adjunct (matrix of cofactors) of a square matrix. This definition gives the standard cofactors, however the internal minors are not the standard minors, see definition in [Lang] p. 518. (Contributed by Stefan O'Rear, 7-Sep-2015.) (Revised by SO, 10-Jul-2018.)

Assertion

Ref	Expression
df-madu	⊢ maAdju = (𝑛 ∈ V, 𝑟 ∈ V ↦ (𝑚 ∈ (Base‘(𝑛 Mat 𝑟)) ↦ (𝑖 ∈ 𝑛, 𝑗 ∈ 𝑛 ↦ ((𝑛 maDet 𝑟)‘(𝑘 ∈ 𝑛, 𝑙 ∈ 𝑛 ↦ if(𝑘 = 𝑗, if(𝑙 = 𝑖, (1r‘𝑟), (0g‘𝑟)), (𝑘𝑚𝑙)))))))

Distinct variable group:   𝑛,𝑟,𝑚,𝑖,𝑗,𝑘,𝑙

Detailed syntax breakdown of Definition df-madu

Step	Hyp	Ref	Expression
1		cmadu 21781	. 2 class maAdju
2		vn	. . 3 setvar 𝑛
3		vr	. . 3 setvar 𝑟
4		cvv 3432	. . 3 class V
5		vm	. . . 4 setvar 𝑚
6	2	cv 1538	. . . . . 6 class 𝑛
7	3	cv 1538	. . . . . 6 class 𝑟
8		cmat 21554	. . . . . 6 class Mat
9	6, 7, 8	co 7275	. . . . 5 class (𝑛 Mat 𝑟)
10		cbs 16912	. . . . 5 class Base
11	9, 10	cfv 6433	. . . 4 class (Base‘(𝑛 Mat 𝑟))
12		vi	. . . . 5 setvar 𝑖
13		vj	. . . . 5 setvar 𝑗
14		vk	. . . . . . 7 setvar 𝑘
15		vl	. . . . . . 7 setvar 𝑙
16	14, 13	weq 1966	. . . . . . . 8 wff 𝑘 = 𝑗
17	15, 12	weq 1966	. . . . . . . . 9 wff 𝑙 = 𝑖
18		cur 19737	. . . . . . . . . 10 class 1r
19	7, 18	cfv 6433	. . . . . . . . 9 class (1r‘𝑟)
20		c0g 17150	. . . . . . . . . 10 class 0g
21	7, 20	cfv 6433	. . . . . . . . 9 class (0g‘𝑟)
22	17, 19, 21	cif 4459	. . . . . . . 8 class if(𝑙 = 𝑖, (1r‘𝑟), (0g‘𝑟))
23	14	cv 1538	. . . . . . . . 9 class 𝑘
24	15	cv 1538	. . . . . . . . 9 class 𝑙
25	5	cv 1538	. . . . . . . . 9 class 𝑚
26	23, 24, 25	co 7275	. . . . . . . 8 class (𝑘𝑚𝑙)
27	16, 22, 26	cif 4459	. . . . . . 7 class if(𝑘 = 𝑗, if(𝑙 = 𝑖, (1r‘𝑟), (0g‘𝑟)), (𝑘𝑚𝑙))
28	14, 15, 6, 6, 27	cmpo 7277	. . . . . 6 class (𝑘 ∈ 𝑛, 𝑙 ∈ 𝑛 ↦ if(𝑘 = 𝑗, if(𝑙 = 𝑖, (1r‘𝑟), (0g‘𝑟)), (𝑘𝑚𝑙)))
29		cmdat 21733	. . . . . . 7 class maDet
30	6, 7, 29	co 7275	. . . . . 6 class (𝑛 maDet 𝑟)
31	28, 30	cfv 6433	. . . . 5 class ((𝑛 maDet 𝑟)‘(𝑘 ∈ 𝑛, 𝑙 ∈ 𝑛 ↦ if(𝑘 = 𝑗, if(𝑙 = 𝑖, (1r‘𝑟), (0g‘𝑟)), (𝑘𝑚𝑙))))
32	12, 13, 6, 6, 31	cmpo 7277	. . . 4 class (𝑖 ∈ 𝑛, 𝑗 ∈ 𝑛 ↦ ((𝑛 maDet 𝑟)‘(𝑘 ∈ 𝑛, 𝑙 ∈ 𝑛 ↦ if(𝑘 = 𝑗, if(𝑙 = 𝑖, (1r‘𝑟), (0g‘𝑟)), (𝑘𝑚𝑙)))))
33	5, 11, 32	cmpt 5157	. . 3 class (𝑚 ∈ (Base‘(𝑛 Mat 𝑟)) ↦ (𝑖 ∈ 𝑛, 𝑗 ∈ 𝑛 ↦ ((𝑛 maDet 𝑟)‘(𝑘 ∈ 𝑛, 𝑙 ∈ 𝑛 ↦ if(𝑘 = 𝑗, if(𝑙 = 𝑖, (1r‘𝑟), (0g‘𝑟)), (𝑘𝑚𝑙))))))
34	2, 3, 4, 4, 33	cmpo 7277	. 2 class (𝑛 ∈ V, 𝑟 ∈ V ↦ (𝑚 ∈ (Base‘(𝑛 Mat 𝑟)) ↦ (𝑖 ∈ 𝑛, 𝑗 ∈ 𝑛 ↦ ((𝑛 maDet 𝑟)‘(𝑘 ∈ 𝑛, 𝑙 ∈ 𝑛 ↦ if(𝑘 = 𝑗, if(𝑙 = 𝑖, (1r‘𝑟), (0g‘𝑟)), (𝑘𝑚𝑙)))))))
35	1, 34	wceq 1539	1 wff maAdju = (𝑛 ∈ V, 𝑟 ∈ V ↦ (𝑚 ∈ (Base‘(𝑛 Mat 𝑟)) ↦ (𝑖 ∈ 𝑛, 𝑗 ∈ 𝑛 ↦ ((𝑛 maDet 𝑟)‘(𝑘 ∈ 𝑛, 𝑙 ∈ 𝑛 ↦ if(𝑘 = 𝑗, if(𝑙 = 𝑖, (1r‘𝑟), (0g‘𝑟)), (𝑘𝑚𝑙)))))))

This definition is referenced by:  madufval  21786