Theorem mdet0pr 19672

Description: The determinant for 0-dimensional matrices is a singleton containing an ordered pair with the singleton containing the empty set as first component, and the singleton containing the 1 element of the underlying ring as second component. (Contributed by AV, 28-Feb-2019.)

Assertion

Ref	Expression
mdet0pr	|- ( R e. Ring -> ( (/) maDet R ) = { <. (/) , ( 1r ` R ) >. } )

Proof of Theorem mdet0pr

Dummy variables m p x are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		eqid 2462	. . . 4 |- ( (/) maDet R ) = ( (/) maDet R )
2		eqid 2462	. . . 4 |- ( (/) Mat R ) = ( (/) Mat R )
3		eqid 2462	. . . 4 |- ( Base ` ( (/) Mat R ) ) = ( Base ` ( (/) Mat R ) )
4		eqid 2462	. . . 4 |- ( Base ` ( SymGrp ` (/) ) ) = ( Base ` ( SymGrp ` (/) ) )
5		eqid 2462	. . . 4 |- ( ZRHom ` R ) = ( ZRHom ` R )
6		eqid 2462	. . . 4 |- (pmSgn ` (/) ) = (pmSgn ` (/) )
7		eqid 2462	. . . 4 |- ( .r ` R ) = ( .r ` R )
8		eqid 2462	. . . 4 |- (mulGrp ` R ) = (mulGrp ` R )
9	1, 2, 3, 4, 5, 6, 7, 8	mdetfval 19666	. . 3 |- ( (/) maDet R ) = ( m e. ( Base ` ( (/) Mat R ) ) |-> ( R gsumg ( p e. ( Base ` ( SymGrp ` (/) ) ) |-> ( ( ( ( ZRHom ` R ) o. (pmSgn ` (/) ) ) ` p ) ( .r ` R ) ( (mulGrp ` R ) gsumg ( x e. (/) |-> ( ( p ` x ) m x ) ) ) ) ) ) )
10	9	a1i 11	. 2 |- ( R e. Ring -> ( (/) maDet R ) = ( m e. ( Base ` ( (/) Mat R ) ) |-> ( R gsumg ( p e. ( Base ` ( SymGrp ` (/) ) ) |-> ( ( ( ( ZRHom ` R ) o. (pmSgn ` (/) ) ) ` p ) ( .r ` R ) ( (mulGrp ` R ) gsumg ( x e. (/) |-> ( ( p ` x ) m x ) ) ) ) ) ) ) )
11		mat0dimbas0 19546	. . 3 |- ( R e. Ring -> ( Base ` ( (/) Mat R ) ) = { (/) } )
12	11	mpteq1d 4500	. 2 |- ( R e. Ring -> ( m e. ( Base ` ( (/) Mat R ) ) |-> ( R gsumg ( p e. ( Base ` ( SymGrp ` (/) ) ) |-> ( ( ( ( ZRHom ` R ) o. (pmSgn ` (/) ) ) ` p ) ( .r ` R ) ( (mulGrp ` R ) gsumg ( x e. (/) |-> ( ( p ` x ) m x ) ) ) ) ) ) ) = ( m e. { (/) } |-> ( R gsumg ( p e. ( Base ` ( SymGrp ` (/) ) ) |-> ( ( ( ( ZRHom ` R ) o. (pmSgn ` (/) ) ) ` p ) ( .r ` R ) ( (mulGrp ` R ) gsumg ( x e. (/) |-> ( ( p ` x ) m x ) ) ) ) ) ) ) )
13		0ex 4551	. . . . 5 |- (/) e. _V
14	13	a1i 11	. . . 4 |- ( R e. Ring -> (/) e. _V )
15		ovex 6348	. . . 4 |- ( R gsumg ( p e. ( Base ` ( SymGrp ` (/) ) ) |-> ( ( ( ( ZRHom ` R ) o. (pmSgn ` (/) ) ) ` p ) ( .r ` R ) ( (mulGrp ` R ) gsumg ( x e. (/) |-> ( ( p ` x ) (/) x ) ) ) ) ) ) e. _V
16		oveq 6326	. . . . . . . . . 10 |- ( m = (/) -> ( ( p ` x ) m x ) = ( ( p ` x ) (/) x ) )
17	16	mpteq2dv 4506	. . . . . . . . 9 |- ( m = (/) -> ( x e. (/) |-> ( ( p ` x ) m x ) ) = ( x e. (/) |-> ( ( p ` x ) (/) x ) ) )
18	17	oveq2d 6336	. . . . . . . 8 |- ( m = (/) -> ( (mulGrp ` R ) gsumg ( x e. (/) |-> ( ( p ` x ) m x ) ) ) = ( (mulGrp ` R ) gsumg ( x e. (/) |-> ( ( p ` x ) (/) x ) ) ) )
19	18	oveq2d 6336	. . . . . . 7 |- ( m = (/) -> ( ( ( ( ZRHom ` R ) o. (pmSgn ` (/) ) ) ` p ) ( .r ` R ) ( (mulGrp ` R ) gsumg ( x e. (/) |-> ( ( p ` x ) m x ) ) ) ) = ( ( ( ( ZRHom ` R ) o. (pmSgn ` (/) ) ) ` p ) ( .r ` R ) ( (mulGrp ` R ) gsumg ( x e. (/) |-> ( ( p ` x ) (/) x ) ) ) ) )
20	19	mpteq2dv 4506	. . . . . 6 |- ( m = (/) -> ( p e. ( Base ` ( SymGrp ` (/) ) ) |-> ( ( ( ( ZRHom ` R ) o. (pmSgn ` (/) ) ) ` p ) ( .r ` R ) ( (mulGrp ` R ) gsumg ( x e. (/) |-> ( ( p ` x ) m x ) ) ) ) ) = ( p e. ( Base ` ( SymGrp ` (/) ) ) |-> ( ( ( ( ZRHom ` R ) o. (pmSgn ` (/) ) ) ` p ) ( .r ` R ) ( (mulGrp ` R ) gsumg ( x e. (/) |-> ( ( p ` x ) (/) x ) ) ) ) ) )
21	20	oveq2d 6336	. . . . 5 |- ( m = (/) -> ( R gsumg ( p e. ( Base ` ( SymGrp ` (/) ) ) |-> ( ( ( ( ZRHom ` R ) o. (pmSgn ` (/) ) ) ` p ) ( .r ` R ) ( (mulGrp ` R ) gsumg ( x e. (/) |-> ( ( p ` x ) m x ) ) ) ) ) ) = ( R gsumg ( p e. ( Base ` ( SymGrp ` (/) ) ) |-> ( ( ( ( ZRHom ` R ) o. (pmSgn ` (/) ) ) ` p ) ( .r ` R ) ( (mulGrp ` R ) gsumg ( x e. (/) |-> ( ( p ` x ) (/) x ) ) ) ) ) ) )
22	21	fmptsng 6114	. . . 4 |- ( ( (/) e. _V /\ ( R gsumg ( p e. ( Base ` ( SymGrp ` (/) ) ) |-> ( ( ( ( ZRHom ` R ) o. (pmSgn ` (/) ) ) ` p ) ( .r ` R ) ( (mulGrp ` R ) gsumg ( x e. (/) |-> ( ( p ` x ) (/) x ) ) ) ) ) ) e. _V ) -> { <. (/) , ( R gsumg ( p e. ( Base ` ( SymGrp ` (/) ) ) |-> ( ( ( ( ZRHom ` R ) o. (pmSgn ` (/) ) ) ` p ) ( .r ` R ) ( (mulGrp ` R ) gsumg ( x e. (/) |-> ( ( p ` x ) (/) x ) ) ) ) ) ) >. } = ( m e. { (/) } |-> ( R gsumg ( p e. ( Base ` ( SymGrp ` (/) ) ) |-> ( ( ( ( ZRHom ` R ) o. (pmSgn ` (/) ) ) ` p ) ( .r ` R ) ( (mulGrp ` R ) gsumg ( x e. (/) |-> ( ( p ` x ) m x ) ) ) ) ) ) ) )
23	14, 15, 22	sylancl 673	. . 3 |- ( R e. Ring -> { <. (/) , ( R gsumg ( p e. ( Base ` ( SymGrp ` (/) ) ) |-> ( ( ( ( ZRHom ` R ) o. (pmSgn ` (/) ) ) ` p ) ( .r ` R ) ( (mulGrp ` R ) gsumg ( x e. (/) |-> ( ( p ` x ) (/) x ) ) ) ) ) ) >. } = ( m e. { (/) } |-> ( R gsumg ( p e. ( Base ` ( SymGrp ` (/) ) ) |-> ( ( ( ( ZRHom ` R ) o. (pmSgn ` (/) ) ) ` p ) ( .r ` R ) ( (mulGrp ` R ) gsumg ( x e. (/) |-> ( ( p ` x ) m x ) ) ) ) ) ) ) )
24		mpt0 5731	. . . . . . . . . . . 12 |- ( x e. (/) |-> ( ( p ` x ) (/) x ) ) = (/)
25	24	a1i 11	. . . . . . . . . . 11 |- ( R e. Ring -> ( x e. (/) |-> ( ( p ` x ) (/) x ) ) = (/) )
26	25	oveq2d 6336	. . . . . . . . . 10 |- ( R e. Ring -> ( (mulGrp ` R ) gsumg ( x e. (/) |-> ( ( p ` x ) (/) x ) ) ) = ( (mulGrp ` R ) gsumg (/) ) )
27		eqid 2462	. . . . . . . . . . 11 |- ( 0g ` (mulGrp ` R ) ) = ( 0g ` (mulGrp ` R ) )
28	27	gsum0 16576	. . . . . . . . . 10 |- ( (mulGrp ` R ) gsumg (/) ) = ( 0g ` (mulGrp ` R ) )
29	26, 28	syl6eq 2512	. . . . . . . . 9 |- ( R e. Ring -> ( (mulGrp ` R ) gsumg ( x e. (/) |-> ( ( p ` x ) (/) x ) ) ) = ( 0g ` (mulGrp ` R ) ) )
30	29	oveq2d 6336	. . . . . . . 8 |- ( R e. Ring -> ( ( ( ( ZRHom ` R ) o. (pmSgn ` (/) ) ) ` p ) ( .r ` R ) ( (mulGrp ` R ) gsumg ( x e. (/) |-> ( ( p ` x ) (/) x ) ) ) ) = ( ( ( ( ZRHom ` R ) o. (pmSgn ` (/) ) ) ` p ) ( .r ` R ) ( 0g ` (mulGrp ` R ) ) ) )
31	30	mpteq2dv 4506	. . . . . . 7 |- ( R e. Ring -> ( p e. ( Base ` ( SymGrp ` (/) ) ) |-> ( ( ( ( ZRHom ` R ) o. (pmSgn ` (/) ) ) ` p ) ( .r ` R ) ( (mulGrp ` R ) gsumg ( x e. (/) |-> ( ( p ` x ) (/) x ) ) ) ) ) = ( p e. ( Base ` ( SymGrp ` (/) ) ) |-> ( ( ( ( ZRHom ` R ) o. (pmSgn ` (/) ) ) ` p ) ( .r ` R ) ( 0g ` (mulGrp ` R ) ) ) ) )
32	31	oveq2d 6336	. . . . . 6 |- ( R e. Ring -> ( R gsumg ( p e. ( Base ` ( SymGrp ` (/) ) ) |-> ( ( ( ( ZRHom ` R ) o. (pmSgn ` (/) ) ) ` p ) ( .r ` R ) ( (mulGrp ` R ) gsumg ( x e. (/) |-> ( ( p ` x ) (/) x ) ) ) ) ) ) = ( R gsumg ( p e. ( Base ` ( SymGrp ` (/) ) ) |-> ( ( ( ( ZRHom ` R ) o. (pmSgn ` (/) ) ) ` p ) ( .r ` R ) ( 0g ` (mulGrp ` R ) ) ) ) ) )
33		eqid 2462	. . . . . . . . . . . . 13 |- ( 1r ` R ) = ( 1r ` R )
34	8, 33	ringidval 17792	. . . . . . . . . . . 12 |- ( 1r ` R ) = ( 0g ` (mulGrp ` R ) )
35	34	eqcomi 2471	. . . . . . . . . . 11 |- ( 0g ` (mulGrp ` R ) ) = ( 1r ` R )
36	35	a1i 11	. . . . . . . . . 10 |- ( ( R e. Ring /\ p e. ( Base ` ( SymGrp ` (/) ) ) ) -> ( 0g ` (mulGrp ` R ) ) = ( 1r ` R ) )
37	36	oveq2d 6336	. . . . . . . . 9 |- ( ( R e. Ring /\ p e. ( Base ` ( SymGrp ` (/) ) ) ) -> ( ( ( ( ZRHom ` R ) o. (pmSgn ` (/) ) ) ` p ) ( .r ` R ) ( 0g ` (mulGrp ` R ) ) ) = ( ( ( ( ZRHom ` R ) o. (pmSgn ` (/) ) ) ` p ) ( .r ` R ) ( 1r ` R ) ) )
38		0fin 7830	. . . . . . . . . . 11 |- (/) e. Fin
39	4, 6, 5	zrhcopsgnelbas 19218	. . . . . . . . . . 11 |- ( ( R e. Ring /\ (/) e. Fin /\ p e. ( Base ` ( SymGrp ` (/) ) ) ) -> ( ( ( ZRHom ` R ) o. (pmSgn ` (/) ) ) ` p ) e. ( Base ` R ) )
40	38, 39	mp3an2 1361	. . . . . . . . . 10 |- ( ( R e. Ring /\ p e. ( Base ` ( SymGrp ` (/) ) ) ) -> ( ( ( ZRHom ` R ) o. (pmSgn ` (/) ) ) ` p ) e. ( Base ` R ) )
41		eqid 2462	. . . . . . . . . . 11 |- ( Base ` R ) = ( Base ` R )
42	41, 7, 33	ringridm 17860	. . . . . . . . . 10 |- ( ( R e. Ring /\ ( ( ( ZRHom ` R ) o. (pmSgn ` (/) ) ) ` p ) e. ( Base ` R ) ) -> ( ( ( ( ZRHom ` R ) o. (pmSgn ` (/) ) ) ` p ) ( .r ` R ) ( 1r ` R ) ) = ( ( ( ZRHom ` R ) o. (pmSgn ` (/) ) ) ` p ) )
43	40, 42	syldan 477	. . . . . . . . 9 |- ( ( R e. Ring /\ p e. ( Base ` ( SymGrp ` (/) ) ) ) -> ( ( ( ( ZRHom ` R ) o. (pmSgn ` (/) ) ) ` p ) ( .r ` R ) ( 1r ` R ) ) = ( ( ( ZRHom ` R ) o. (pmSgn ` (/) ) ) ` p ) )
44	37, 43	eqtrd 2496	. . . . . . . 8 |- ( ( R e. Ring /\ p e. ( Base ` ( SymGrp ` (/) ) ) ) -> ( ( ( ( ZRHom ` R ) o. (pmSgn ` (/) ) ) ` p ) ( .r ` R ) ( 0g ` (mulGrp ` R ) ) ) = ( ( ( ZRHom ` R ) o. (pmSgn ` (/) ) ) ` p ) )
45	44	mpteq2dva 4505	. . . . . . 7 |- ( R e. Ring -> ( p e. ( Base ` ( SymGrp ` (/) ) ) |-> ( ( ( ( ZRHom ` R ) o. (pmSgn ` (/) ) ) ` p ) ( .r ` R ) ( 0g ` (mulGrp ` R ) ) ) ) = ( p e. ( Base ` ( SymGrp ` (/) ) ) |-> ( ( ( ZRHom ` R ) o. (pmSgn ` (/) ) ) ` p ) ) )
46	45	oveq2d 6336	. . . . . 6 |- ( R e. Ring -> ( R gsumg ( p e. ( Base ` ( SymGrp ` (/) ) ) |-> ( ( ( ( ZRHom ` R ) o. (pmSgn ` (/) ) ) ` p ) ( .r ` R ) ( 0g ` (mulGrp ` R ) ) ) ) ) = ( R gsumg ( p e. ( Base ` ( SymGrp ` (/) ) ) |-> ( ( ( ZRHom ` R ) o. (pmSgn ` (/) ) ) ` p ) ) ) )
47		simpl 463	. . . . . . . . . 10 |- ( ( R e. Ring /\ p e. ( Base ` ( SymGrp ` (/) ) ) ) -> R e. Ring )
48	38	a1i 11	. . . . . . . . . 10 |- ( ( R e. Ring /\ p e. ( Base ` ( SymGrp ` (/) ) ) ) -> (/) e. Fin )
49		simpr 467	. . . . . . . . . . 11 |- ( ( R e. Ring /\ p e. ( Base ` ( SymGrp ` (/) ) ) ) -> p e. ( Base ` ( SymGrp ` (/) ) ) )
50		elsni 4005	. . . . . . . . . . . . . 14 |- ( p e. { (/) } -> p = (/) )
51		fveq2 5892	. . . . . . . . . . . . . . 15 |- ( p = (/) -> ( (pmSgn ` (/) ) ` p ) = ( (pmSgn ` (/) ) ` (/) ) )
52		psgn0fv0 17207	. . . . . . . . . . . . . . 15 |- ( (pmSgn ` (/) ) ` (/) ) = 1
53	51, 52	syl6eq 2512	. . . . . . . . . . . . . 14 |- ( p = (/) -> ( (pmSgn ` (/) ) ` p ) = 1 )
54	50, 53	syl 17	. . . . . . . . . . . . 13 |- ( p e. { (/) } -> ( (pmSgn ` (/) ) ` p ) = 1 )
55		symgbas0 17090	. . . . . . . . . . . . 13 |- ( Base ` ( SymGrp ` (/) ) ) = { (/) }
56	54, 55	eleq2s 2558	. . . . . . . . . . . 12 |- ( p e. ( Base ` ( SymGrp ` (/) ) ) -> ( (pmSgn ` (/) ) ` p ) = 1 )
57	56	adantl 472	. . . . . . . . . . 11 |- ( ( R e. Ring /\ p e. ( Base ` ( SymGrp ` (/) ) ) ) -> ( (pmSgn ` (/) ) ` p ) = 1 )
58		eqid 2462	. . . . . . . . . . . . 13 |- ( SymGrp ` (/) ) = ( SymGrp ` (/) )
59	58, 4, 6	psgnevpmb 19210	. . . . . . . . . . . 12 |- ( (/) e. Fin -> ( p e. (pmEven ` (/) ) <-> ( p e. ( Base ` ( SymGrp ` (/) ) ) /\ ( (pmSgn ` (/) ) ` p ) = 1 ) ) )
60	48, 59	syl 17	. . . . . . . . . . 11 |- ( ( R e. Ring /\ p e. ( Base ` ( SymGrp ` (/) ) ) ) -> ( p e. (pmEven ` (/) ) <-> ( p e. ( Base ` ( SymGrp ` (/) ) ) /\ ( (pmSgn ` (/) ) ` p ) = 1 ) ) )
61	49, 57, 60	mpbir2and 938	. . . . . . . . . 10 |- ( ( R e. Ring /\ p e. ( Base ` ( SymGrp ` (/) ) ) ) -> p e. (pmEven ` (/) ) )
62	5, 6, 33	zrhpsgnevpm 19214	. . . . . . . . . 10 |- ( ( R e. Ring /\ (/) e. Fin /\ p e. (pmEven ` (/) ) ) -> ( ( ( ZRHom ` R ) o. (pmSgn ` (/) ) ) ` p ) = ( 1r ` R ) )
63	47, 48, 61, 62	syl3anc 1276	. . . . . . . . 9 |- ( ( R e. Ring /\ p e. ( Base ` ( SymGrp ` (/) ) ) ) -> ( ( ( ZRHom ` R ) o. (pmSgn ` (/) ) ) ` p ) = ( 1r ` R ) )
64	63	mpteq2dva 4505	. . . . . . . 8 |- ( R e. Ring -> ( p e. ( Base ` ( SymGrp ` (/) ) ) |-> ( ( ( ZRHom ` R ) o. (pmSgn ` (/) ) ) ` p ) ) = ( p e. ( Base ` ( SymGrp ` (/) ) ) |-> ( 1r ` R ) ) )
65	64	oveq2d 6336	. . . . . . 7 |- ( R e. Ring -> ( R gsumg ( p e. ( Base ` ( SymGrp ` (/) ) ) |-> ( ( ( ZRHom ` R ) o. (pmSgn ` (/) ) ) ` p ) ) ) = ( R gsumg ( p e. ( Base ` ( SymGrp ` (/) ) ) |-> ( 1r ` R ) ) ) )
66	55	a1i 11	. . . . . . . . 9 |- ( R e. Ring -> ( Base ` ( SymGrp ` (/) ) ) = { (/) } )
67	66	mpteq1d 4500	. . . . . . . 8 |- ( R e. Ring -> ( p e. ( Base ` ( SymGrp ` (/) ) ) |-> ( 1r ` R ) ) = ( p e. { (/) } |-> ( 1r ` R ) ) )
68	67	oveq2d 6336	. . . . . . 7 |- ( R e. Ring -> ( R gsumg ( p e. ( Base ` ( SymGrp ` (/) ) ) |-> ( 1r ` R ) ) ) = ( R gsumg ( p e. { (/) } |-> ( 1r ` R ) ) ) )
69		ringmnd 17844	. . . . . . . 8 |- ( R e. Ring -> R e. Mnd )
70	41, 33	ringidcl 17856	. . . . . . . 8 |- ( R e. Ring -> ( 1r ` R ) e. ( Base ` R ) )
71		eqidd 2463	. . . . . . . . 9 |- ( p = (/) -> ( 1r ` R ) = ( 1r ` R ) )
72	41, 71	gsumsn 17642	. . . . . . . 8 |- ( ( R e. Mnd /\ (/) e. _V /\ ( 1r ` R ) e. ( Base ` R ) ) -> ( R gsumg ( p e. { (/) } |-> ( 1r ` R ) ) ) = ( 1r ` R ) )
73	69, 14, 70, 72	syl3anc 1276	. . . . . . 7 |- ( R e. Ring -> ( R gsumg ( p e. { (/) } |-> ( 1r ` R ) ) ) = ( 1r ` R ) )
74	65, 68, 73	3eqtrd 2500	. . . . . 6 |- ( R e. Ring -> ( R gsumg ( p e. ( Base ` ( SymGrp ` (/) ) ) |-> ( ( ( ZRHom ` R ) o. (pmSgn ` (/) ) ) ` p ) ) ) = ( 1r ` R ) )
75	32, 46, 74	3eqtrd 2500	. . . . 5 |- ( R e. Ring -> ( R gsumg ( p e. ( Base ` ( SymGrp ` (/) ) ) |-> ( ( ( ( ZRHom ` R ) o. (pmSgn ` (/) ) ) ` p ) ( .r ` R ) ( (mulGrp ` R ) gsumg ( x e. (/) |-> ( ( p ` x ) (/) x ) ) ) ) ) ) = ( 1r ` R ) )
76	75	opeq2d 4187	. . . 4 |- ( R e. Ring -> <. (/) , ( R gsumg ( p e. ( Base ` ( SymGrp ` (/) ) ) |-> ( ( ( ( ZRHom ` R ) o. (pmSgn ` (/) ) ) ` p ) ( .r ` R ) ( (mulGrp ` R ) gsumg ( x e. (/) |-> ( ( p ` x ) (/) x ) ) ) ) ) ) >. = <. (/) , ( 1r ` R ) >. )
77	76	sneqd 3992	. . 3 |- ( R e. Ring -> { <. (/) , ( R gsumg ( p e. ( Base ` ( SymGrp ` (/) ) ) |-> ( ( ( ( ZRHom ` R ) o. (pmSgn ` (/) ) ) ` p ) ( .r ` R ) ( (mulGrp ` R ) gsumg ( x e. (/) |-> ( ( p ` x ) (/) x ) ) ) ) ) ) >. } = { <. (/) , ( 1r ` R ) >. } )
78	23, 77	eqtr3d 2498	. 2 |- ( R e. Ring -> ( m e. { (/) } |-> ( R gsumg ( p e. ( Base ` ( SymGrp ` (/) ) ) |-> ( ( ( ( ZRHom ` R ) o. (pmSgn ` (/) ) ) ` p ) ( .r ` R ) ( (mulGrp ` R ) gsumg ( x e. (/) |-> ( ( p ` x ) m x ) ) ) ) ) ) ) = { <. (/) , ( 1r ` R ) >. } )
79	10, 12, 78	3eqtrd 2500	1 |- ( R e. Ring -> ( (/) maDet R ) = { <. (/) , ( 1r ` R ) >. } )

Syntax hints:   -> wi 4   <-> wb 189   /\ wa 375   = wceq 1455   e. wcel 1898   _Vcvv 3057   (/)c0 3743   {csn 3980   <.cop 3986   |-> cmpt 4477   o. ccom 4860   ` cfv 5605  (class class class)co 6320   Fincfn 7600   1c1 9571   Basecbs 15176   .rcmulr 15246   0gc0g 15393   gsum_g cgsu 15394   Mndcmnd 16590   SymGrpcsymg 17073  pmSgncpsgn 17185  pmEvencevpm 17186  mulGrpcmgp 17778   1rcur 17790   Ringcrg 17835   ZRHomczrh 19126   Mat cmat 19487   maDet cmdat 19664

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-8 1900  ax-9 1907  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442  ax-rep 4531  ax-sep 4541  ax-nul 4550  ax-pow 4598  ax-pr 4656  ax-un 6615  ax-inf2 8177  ax-cnex 9626  ax-resscn 9627  ax-1cn 9628  ax-icn 9629  ax-addcl 9630  ax-addrcl 9631  ax-mulcl 9632  ax-mulrcl 9633  ax-mulcom 9634  ax-addass 9635  ax-mulass 9636  ax-distr 9637  ax-i2m1 9638  ax-1ne0 9639  ax-1rid 9640  ax-rnegex 9641  ax-rrecex 9642  ax-cnre 9643  ax-pre-lttri 9644  ax-pre-lttrn 9645  ax-pre-ltadd 9646  ax-pre-mulgt0 9647  ax-addf 9649  ax-mulf 9650

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3or 992  df-3an 993  df-xor 1416  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-eu 2314  df-mo 2315  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-ne 2635  df-nel 2636  df-ral 2754  df-rex 2755  df-reu 2756  df-rmo 2757  df-rab 2758  df-v 3059  df-sbc 3280  df-csb 3376  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-pss 3432  df-nul 3744  df-if 3894  df-pw 3965  df-sn 3981  df-pr 3983  df-tp 3985  df-op 3987  df-ot 3989  df-uni 4213  df-int 4249  df-iun 4294  df-iin 4295  df-br 4419  df-opab 4478  df-mpt 4479  df-tr 4514  df-eprel 4767  df-id 4771  df-po 4777  df-so 4778  df-fr 4815  df-se 4816  df-we 4817  df-xp 4862  df-rel 4863  df-cnv 4864  df-co 4865  df-dm 4866  df-rn 4867  df-res 4868  df-ima 4869  df-pred 5403  df-ord 5449  df-on 5450  df-lim 5451  df-suc 5452  df-iota 5569  df-fun 5607  df-fn 5608  df-f 5609  df-f1 5610  df-fo 5611  df-f1o 5612  df-fv 5613  df-isom 5614  df-riota 6282  df-ov 6323  df-oprab 6324  df-mpt2 6325  df-om 6725  df-1st 6825  df-2nd 6826  df-supp 6947  df-tpos 7004  df-wrecs 7059  df-recs 7121  df-rdg 7159  df-1o 7213  df-2o 7214  df-oadd 7217  df-er 7394  df-map 7505  df-ixp 7554  df-en 7601  df-dom 7602  df-sdom 7603  df-fin 7604  df-fsupp 7915  df-sup 7987  df-oi 8056  df-card 8404  df-cda 8629  df-pnf 9708  df-mnf 9709  df-xr 9710  df-ltxr 9711  df-le 9712  df-sub 9893  df-neg 9894  df-div 10303  df-nn 10643  df-2 10701  df-3 10702  df-4 10703  df-5 10704  df-6 10705  df-7 10706  df-8 10707  df-9 10708  df-10 10709  df-n0 10904  df-z 10972  df-dec 11086  df-uz 11194  df-rp 11337  df-fz 11820  df-fzo 11953  df-seq 12252  df-exp 12311  df-hash 12554  df-word 12703  df-lsw 12704  df-concat 12705  df-s1 12706  df-substr 12707  df-splice 12708  df-reverse 12709  df-s2 12987  df-struct 15178  df-ndx 15179  df-slot 15180  df-base 15181  df-sets 15182  df-ress 15183  df-plusg 15258  df-mulr 15259  df-starv 15260  df-sca 15261  df-vsca 15262  df-ip 15263  df-tset 15264  df-ple 15265  df-ds 15267  df-unif 15268  df-hom 15269  df-cco 15270  df-0g 15395  df-gsum 15396  df-prds 15401  df-pws 15403  df-mre 15547  df-mrc 15548  df-acs 15550  df-mgm 16543  df-sgrp 16582  df-mnd 16592  df-mhm 16637  df-submnd 16638  df-grp 16728  df-minusg 16729  df-mulg 16731  df-subg 16869  df-ghm 16936  df-gim 16978  df-cntz 17026  df-oppg 17052  df-symg 17074  df-pmtr 17138  df-psgn 17187  df-evpm 17188  df-cmn 17487  df-abl 17488  df-mgp 17779  df-ur 17791  df-ring 17837  df-cring 17838  df-oppr 17906  df-dvdsr 17924  df-unit 17925  df-invr 17955  df-dvr 17966  df-rnghom 17998  df-drng 18032  df-subrg 18061  df-sra 18450  df-rgmod 18451  df-cnfld 19026  df-zring 19095  df-zrh 19130  df-dsmm 19350  df-frlm 19365  df-mat 19488  df-mdet 19665

This theorem is referenced by:  mdet0f1o  19673  mdet0fv0  19674  chpmat0d  19913