Definition df-marrep 20364

Description: Define the matrices whose k-th row is replaced by 0's and an arbitrary element of the underlying ring at the l-th column. (Contributed by AV, 12-Feb-2019.)

Assertion

Ref	Expression
df-marrep	|- matRRep = ( n e. _V , r e. _V |-> ( m e. ( Base ` ( n Mat r ) ) , s e. ( Base ` r ) |-> ( k e. n , l e. n |-> ( i e. n , j e. n |-> if ( i = k , if ( j = l , s , ( 0g ` r ) ) , ( i m j ) ) ) ) ) )

Distinct variable group:   n, r, m, i, j, k, l, s

Detailed syntax breakdown of Definition df-marrep

Step	Hyp	Ref	Expression
1		cmarrep 20362	. 2 class matRRep
2		vn	. . 3 setvar n
3		vr	. . 3 setvar r
4		cvv 3200	. . 3 class _V
5		vm	. . . 4 setvar m
6		vs	. . . 4 setvar s
7	2	cv 1482	. . . . . 6 class n
8	3	cv 1482	. . . . . 6 class r
9		cmat 20213	. . . . . 6 class Mat
10	7, 8, 9	co 6650	. . . . 5 class ( n Mat r )
11		cbs 15857	. . . . 5 class Base
12	10, 11	cfv 5888	. . . 4 class ( Base ` ( n Mat r ) )
13	8, 11	cfv 5888	. . . 4 class ( Base ` r )
14		vk	. . . . 5 setvar k
15		vl	. . . . 5 setvar l
16		vi	. . . . . 6 setvar i
17		vj	. . . . . 6 setvar j
18	16, 14	weq 1874	. . . . . . 7 wff i = k
19	17, 15	weq 1874	. . . . . . . 8 wff j = l
20	6	cv 1482	. . . . . . . 8 class s
21		c0g 16100	. . . . . . . . 9 class 0g
22	8, 21	cfv 5888	. . . . . . . 8 class ( 0g ` r )
23	19, 20, 22	cif 4086	. . . . . . 7 class if ( j = l , s , ( 0g ` r ) )
24	16	cv 1482	. . . . . . . 8 class i
25	17	cv 1482	. . . . . . . 8 class j
26	5	cv 1482	. . . . . . . 8 class m
27	24, 25, 26	co 6650	. . . . . . 7 class ( i m j )
28	18, 23, 27	cif 4086	. . . . . 6 class if ( i = k , if ( j = l , s , ( 0g ` r ) ) , ( i m j ) )
29	16, 17, 7, 7, 28	cmpt2 6652	. . . . 5 class ( i e. n , j e. n |-> if ( i = k , if ( j = l , s , ( 0g ` r ) ) , ( i m j ) ) )
30	14, 15, 7, 7, 29	cmpt2 6652	. . . 4 class ( k e. n , l e. n |-> ( i e. n , j e. n |-> if ( i = k , if ( j = l , s , ( 0g ` r ) ) , ( i m j ) ) ) )
31	5, 6, 12, 13, 30	cmpt2 6652	. . 3 class ( m e. ( Base ` ( n Mat r ) ) , s e. ( Base ` r ) |-> ( k e. n , l e. n |-> ( i e. n , j e. n |-> if ( i = k , if ( j = l , s , ( 0g ` r ) ) , ( i m j ) ) ) ) )
32	2, 3, 4, 4, 31	cmpt2 6652	. 2 class ( n e. _V , r e. _V |-> ( m e. ( Base ` ( n Mat r ) ) , s e. ( Base ` r ) |-> ( k e. n , l e. n |-> ( i e. n , j e. n |-> if ( i = k , if ( j = l , s , ( 0g ` r ) ) , ( i m j ) ) ) ) ) )
33	1, 32	wceq 1483	1 wff matRRep = ( n e. _V , r e. _V |-> ( m e. ( Base ` ( n Mat r ) ) , s e. ( Base ` r ) |-> ( k e. n , l e. n |-> ( i e. n , j e. n |-> if ( i = k , if ( j = l , s , ( 0g ` r ) ) , ( i m j ) ) ) ) ) )

This definition is referenced by:  marrepfval  20366