mdetrsca2

Description: The determinant function is homogeneous for each row (matrices are given explicitly by their entries). (Contributed by SO, 16-Jul-2018)

	Ref	Expression
Hypotheses	mdetrsca2.d	\|- D = ( N maDet R )
	mdetrsca2.k	\|- K = ( Base ` R )
	mdetrsca2.t	\|- .x. = ( .r ` R )
	mdetrsca2.r	\|- ( ph -> R e. CRing )
	mdetrsca2.n	\|- ( ph -> N e. Fin )
	mdetrsca2.x	\|- ( ( ph /\ i e. N /\ j e. N ) -> X e. K )
	mdetrsca2.y	\|- ( ( ph /\ i e. N /\ j e. N ) -> Y e. K )
	mdetrsca2.f	\|- ( ph -> F e. K )
	mdetrsca2.i	\|- ( ph -> I e. N )
Assertion	mdetrsca2	\|- ( ph -> ( D ` ( i e. N , j e. N \|-> if ( i = I , ( F .x. X ) , Y ) ) ) = ( F .x. ( D ` ( i e. N , j e. N \|-> if ( i = I , X , Y ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		mdetrsca2.d	\|- D = ( N maDet R )
2		mdetrsca2.k	\|- K = ( Base ` R )
3		mdetrsca2.t	\|- .x. = ( .r ` R )
4		mdetrsca2.r	\|- ( ph -> R e. CRing )
5		mdetrsca2.n	\|- ( ph -> N e. Fin )
6		mdetrsca2.x	\|- ( ( ph /\ i e. N /\ j e. N ) -> X e. K )
7		mdetrsca2.y	\|- ( ( ph /\ i e. N /\ j e. N ) -> Y e. K )
8		mdetrsca2.f	\|- ( ph -> F e. K )
9		mdetrsca2.i	\|- ( ph -> I e. N )
10		eqid	\|- ( N Mat R ) = ( N Mat R )
11		eqid	\|- ( Base ` ( N Mat R ) ) = ( Base ` ( N Mat R ) )
12		crngring	\|- ( R e. CRing -> R e. Ring )
13	4 12	syl	\|- ( ph -> R e. Ring )
14	13	3ad2ant1	\|- ( ( ph /\ i e. N /\ j e. N ) -> R e. Ring )
15	8	3ad2ant1	\|- ( ( ph /\ i e. N /\ j e. N ) -> F e. K )
16	2 3	ringcl	\|- ( ( R e. Ring /\ F e. K /\ X e. K ) -> ( F .x. X ) e. K )
17	14 15 6 16	syl3anc	\|- ( ( ph /\ i e. N /\ j e. N ) -> ( F .x. X ) e. K )
18	17 7	ifcld	\|- ( ( ph /\ i e. N /\ j e. N ) -> if ( i = I , ( F .x. X ) , Y ) e. K )
19	10 2 11 5 4 18	matbas2d	\|- ( ph -> ( i e. N , j e. N \|-> if ( i = I , ( F .x. X ) , Y ) ) e. ( Base ` ( N Mat R ) ) )
20	6 7	ifcld	\|- ( ( ph /\ i e. N /\ j e. N ) -> if ( i = I , X , Y ) e. K )
21	10 2 11 5 4 20	matbas2d	\|- ( ph -> ( i e. N , j e. N \|-> if ( i = I , X , Y ) ) e. ( Base ` ( N Mat R ) ) )
22		snex	\|- { I } e. _V
23	22	a1i	\|- ( ph -> { I } e. _V )
24	8	3ad2ant1	\|- ( ( ph /\ i e. { I } /\ j e. N ) -> F e. K )
25	9	snssd	\|- ( ph -> { I } C_ N )
26	25	sselda	\|- ( ( ph /\ i e. { I } ) -> i e. N )
27	26	3adant3	\|- ( ( ph /\ i e. { I } /\ j e. N ) -> i e. N )
28	27 6	syld3an2	\|- ( ( ph /\ i e. { I } /\ j e. N ) -> X e. K )
29		fconstmpo	\|- ( ( { I } X. N ) X. { F } ) = ( i e. { I } , j e. N \|-> F )
30	29	a1i	\|- ( ph -> ( ( { I } X. N ) X. { F } ) = ( i e. { I } , j e. N \|-> F ) )
31		eqidd	\|- ( ph -> ( i e. { I } , j e. N \|-> X ) = ( i e. { I } , j e. N \|-> X ) )
32	23 5 24 28 30 31	offval22	\|- ( ph -> ( ( ( { I } X. N ) X. { F } ) oF .x. ( i e. { I } , j e. N \|-> X ) ) = ( i e. { I } , j e. N \|-> ( F .x. X ) ) )
33		mposnif	\|- ( i e. { I } , j e. N \|-> if ( i = I , X , Y ) ) = ( i e. { I } , j e. N \|-> X )
34	33	oveq2i	\|- ( ( ( { I } X. N ) X. { F } ) oF .x. ( i e. { I } , j e. N \|-> if ( i = I , X , Y ) ) ) = ( ( ( { I } X. N ) X. { F } ) oF .x. ( i e. { I } , j e. N \|-> X ) )
35		mposnif	\|- ( i e. { I } , j e. N \|-> if ( i = I , ( F .x. X ) , Y ) ) = ( i e. { I } , j e. N \|-> ( F .x. X ) )
36	32 34 35	3eqtr4g	\|- ( ph -> ( ( ( { I } X. N ) X. { F } ) oF .x. ( i e. { I } , j e. N \|-> if ( i = I , X , Y ) ) ) = ( i e. { I } , j e. N \|-> if ( i = I , ( F .x. X ) , Y ) ) )
37		ssid	\|- N C_ N
38		resmpo	\|- ( ( { I } C_ N /\ N C_ N ) -> ( ( i e. N , j e. N \|-> if ( i = I , X , Y ) ) \|` ( { I } X. N ) ) = ( i e. { I } , j e. N \|-> if ( i = I , X , Y ) ) )
39	25 37 38	sylancl	\|- ( ph -> ( ( i e. N , j e. N \|-> if ( i = I , X , Y ) ) \|` ( { I } X. N ) ) = ( i e. { I } , j e. N \|-> if ( i = I , X , Y ) ) )
40	39	oveq2d	\|- ( ph -> ( ( ( { I } X. N ) X. { F } ) oF .x. ( ( i e. N , j e. N \|-> if ( i = I , X , Y ) ) \|` ( { I } X. N ) ) ) = ( ( ( { I } X. N ) X. { F } ) oF .x. ( i e. { I } , j e. N \|-> if ( i = I , X , Y ) ) ) )
41		resmpo	\|- ( ( { I } C_ N /\ N C_ N ) -> ( ( i e. N , j e. N \|-> if ( i = I , ( F .x. X ) , Y ) ) \|` ( { I } X. N ) ) = ( i e. { I } , j e. N \|-> if ( i = I , ( F .x. X ) , Y ) ) )
42	25 37 41	sylancl	\|- ( ph -> ( ( i e. N , j e. N \|-> if ( i = I , ( F .x. X ) , Y ) ) \|` ( { I } X. N ) ) = ( i e. { I } , j e. N \|-> if ( i = I , ( F .x. X ) , Y ) ) )
43	36 40 42	3eqtr4rd	\|- ( ph -> ( ( i e. N , j e. N \|-> if ( i = I , ( F .x. X ) , Y ) ) \|` ( { I } X. N ) ) = ( ( ( { I } X. N ) X. { F } ) oF .x. ( ( i e. N , j e. N \|-> if ( i = I , X , Y ) ) \|` ( { I } X. N ) ) ) )
44		eldifsni	\|- ( i e. ( N \ { I } ) -> i =/= I )
45	44	3ad2ant2	\|- ( ( ph /\ i e. ( N \ { I } ) /\ j e. N ) -> i =/= I )
46	45	neneqd	\|- ( ( ph /\ i e. ( N \ { I } ) /\ j e. N ) -> -. i = I )
47		iffalse	\|- ( -. i = I -> if ( i = I , ( F .x. X ) , Y ) = Y )
48		iffalse	\|- ( -. i = I -> if ( i = I , X , Y ) = Y )
49	47 48	eqtr4d	\|- ( -. i = I -> if ( i = I , ( F .x. X ) , Y ) = if ( i = I , X , Y ) )
50	46 49	syl	\|- ( ( ph /\ i e. ( N \ { I } ) /\ j e. N ) -> if ( i = I , ( F .x. X ) , Y ) = if ( i = I , X , Y ) )
51	50	mpoeq3dva	\|- ( ph -> ( i e. ( N \ { I } ) , j e. N \|-> if ( i = I , ( F .x. X ) , Y ) ) = ( i e. ( N \ { I } ) , j e. N \|-> if ( i = I , X , Y ) ) )
52		difss	\|- ( N \ { I } ) C_ N
53		resmpo	\|- ( ( ( N \ { I } ) C_ N /\ N C_ N ) -> ( ( i e. N , j e. N \|-> if ( i = I , ( F .x. X ) , Y ) ) \|` ( ( N \ { I } ) X. N ) ) = ( i e. ( N \ { I } ) , j e. N \|-> if ( i = I , ( F .x. X ) , Y ) ) )
54	52 37 53	mp2an	\|- ( ( i e. N , j e. N \|-> if ( i = I , ( F .x. X ) , Y ) ) \|` ( ( N \ { I } ) X. N ) ) = ( i e. ( N \ { I } ) , j e. N \|-> if ( i = I , ( F .x. X ) , Y ) )
55		resmpo	\|- ( ( ( N \ { I } ) C_ N /\ N C_ N ) -> ( ( i e. N , j e. N \|-> if ( i = I , X , Y ) ) \|` ( ( N \ { I } ) X. N ) ) = ( i e. ( N \ { I } ) , j e. N \|-> if ( i = I , X , Y ) ) )
56	52 37 55	mp2an	\|- ( ( i e. N , j e. N \|-> if ( i = I , X , Y ) ) \|` ( ( N \ { I } ) X. N ) ) = ( i e. ( N \ { I } ) , j e. N \|-> if ( i = I , X , Y ) )
57	51 54 56	3eqtr4g	\|- ( ph -> ( ( i e. N , j e. N \|-> if ( i = I , ( F .x. X ) , Y ) ) \|` ( ( N \ { I } ) X. N ) ) = ( ( i e. N , j e. N \|-> if ( i = I , X , Y ) ) \|` ( ( N \ { I } ) X. N ) ) )
58	1 10 11 2 3 4 19 8 21 9 43 57	mdetrsca	\|- ( ph -> ( D ` ( i e. N , j e. N \|-> if ( i = I , ( F .x. X ) , Y ) ) ) = ( F .x. ( D ` ( i e. N , j e. N \|-> if ( i = I , X , Y ) ) ) ) )

Metamath Proof Explorer

Theorem mdetrsca2

Proof