Theorem mulmarep1gsum2 19648

Description: The sum of element by element multiplications of a matrix with an identity matrix with a column replaced by a vector. (Contributed by AV, 18-Feb-2019.) (Revised by AV, 26-Feb-2019.)

Hypotheses

Ref	Expression
marepvcl.a	|- A = ( N Mat R )
marepvcl.b	|- B = ( Base ` A )
marepvcl.v	|- V = ( ( Base ` R ) ^m N )
ma1repvcl.1	|- .1. = ( 1r ` A )
mulmarep1el.0	|- .0. = ( 0g ` R )
mulmarep1el.e	|- E = ( ( .1. ( N matRepV R ) C ) ` K )
mulmarep1gsum2.x	|- .X. = ( R maVecMul <. N , N >. )

Assertion

Ref	Expression
mulmarep1gsum2	|- ( ( R e. Ring /\ ( X e. B /\ C e. V /\ K e. N ) /\ ( I e. N /\ J e. N /\ ( X .X. C ) = Z ) ) -> ( R gsumg ( l e. N |-> ( ( I X l ) ( .r ` R ) ( l E J ) ) ) ) = if ( J = K , ( Z ` I ) , ( I X J ) ) )

Distinct variable groups:   B, l   C, l   I, l   J, l   K, l   N, l   R, l   V, l   X, l   .0. , l   A, l   Z, l   .X. , l

Allowed substitution hints:   .1. ( l)   E( l)

Proof of Theorem mulmarep1gsum2

Step	Hyp	Ref	Expression
1		simp1 1014	. . . . . . . . . . 11 |- ( ( R e. Ring /\ ( X e. B /\ C e. V /\ K e. N ) /\ ( I e. N /\ J e. N /\ ( X .X. C ) = Z ) ) -> R e. Ring )
2	1	adantr 471	. . . . . . . . . 10 |- ( ( ( R e. Ring /\ ( X e. B /\ C e. V /\ K e. N ) /\ ( I e. N /\ J e. N /\ ( X .X. C ) = Z ) ) /\ l e. N ) -> R e. Ring )
3		simpl2 1018	. . . . . . . . . 10 |- ( ( ( R e. Ring /\ ( X e. B /\ C e. V /\ K e. N ) /\ ( I e. N /\ J e. N /\ ( X .X. C ) = Z ) ) /\ l e. N ) -> ( X e. B /\ C e. V /\ K e. N ) )
4		simp1 1014	. . . . . . . . . . . . 13 |- ( ( I e. N /\ J e. N /\ ( X .X. C ) = Z ) -> I e. N )
5	4	3ad2ant3 1037	. . . . . . . . . . . 12 |- ( ( R e. Ring /\ ( X e. B /\ C e. V /\ K e. N ) /\ ( I e. N /\ J e. N /\ ( X .X. C ) = Z ) ) -> I e. N )
6	5	adantr 471	. . . . . . . . . . 11 |- ( ( ( R e. Ring /\ ( X e. B /\ C e. V /\ K e. N ) /\ ( I e. N /\ J e. N /\ ( X .X. C ) = Z ) ) /\ l e. N ) -> I e. N )
7		simpl32 1096	. . . . . . . . . . 11 |- ( ( ( R e. Ring /\ ( X e. B /\ C e. V /\ K e. N ) /\ ( I e. N /\ J e. N /\ ( X .X. C ) = Z ) ) /\ l e. N ) -> J e. N )
8		simpr 467	. . . . . . . . . . 11 |- ( ( ( R e. Ring /\ ( X e. B /\ C e. V /\ K e. N ) /\ ( I e. N /\ J e. N /\ ( X .X. C ) = Z ) ) /\ l e. N ) -> l e. N )
9	6, 7, 8	3jca 1194	. . . . . . . . . 10 |- ( ( ( R e. Ring /\ ( X e. B /\ C e. V /\ K e. N ) /\ ( I e. N /\ J e. N /\ ( X .X. C ) = Z ) ) /\ l e. N ) -> ( I e. N /\ J e. N /\ l e. N ) )
10	2, 3, 9	3jca 1194	. . . . . . . . 9 |- ( ( ( R e. Ring /\ ( X e. B /\ C e. V /\ K e. N ) /\ ( I e. N /\ J e. N /\ ( X .X. C ) = Z ) ) /\ l e. N ) -> ( R e. Ring /\ ( X e. B /\ C e. V /\ K e. N ) /\ ( I e. N /\ J e. N /\ l e. N ) ) )
11	10	adantll 725	. . . . . . . 8 |- ( ( ( J = K /\ ( R e. Ring /\ ( X e. B /\ C e. V /\ K e. N ) /\ ( I e. N /\ J e. N /\ ( X .X. C ) = Z ) ) ) /\ l e. N ) -> ( R e. Ring /\ ( X e. B /\ C e. V /\ K e. N ) /\ ( I e. N /\ J e. N /\ l e. N ) ) )
12		marepvcl.a	. . . . . . . . 9 |- A = ( N Mat R )
13		marepvcl.b	. . . . . . . . 9 |- B = ( Base ` A )
14		marepvcl.v	. . . . . . . . 9 |- V = ( ( Base ` R ) ^m N )
15		ma1repvcl.1	. . . . . . . . 9 |- .1. = ( 1r ` A )
16		mulmarep1el.0	. . . . . . . . 9 |- .0. = ( 0g ` R )
17		mulmarep1el.e	. . . . . . . . 9 |- E = ( ( .1. ( N matRepV R ) C ) ` K )
18	12, 13, 14, 15, 16, 17	mulmarep1el 19646	. . . . . . . 8 |- ( ( R e. Ring /\ ( X e. B /\ C e. V /\ K e. N ) /\ ( I e. N /\ J e. N /\ l e. N ) ) -> ( ( I X l ) ( .r ` R ) ( l E J ) ) = if ( J = K , ( ( I X l ) ( .r ` R ) ( C ` l ) ) , if ( J = l , ( I X l ) , .0. ) ) )
19	11, 18	syl 17	. . . . . . 7 |- ( ( ( J = K /\ ( R e. Ring /\ ( X e. B /\ C e. V /\ K e. N ) /\ ( I e. N /\ J e. N /\ ( X .X. C ) = Z ) ) ) /\ l e. N ) -> ( ( I X l ) ( .r ` R ) ( l E J ) ) = if ( J = K , ( ( I X l ) ( .r ` R ) ( C ` l ) ) , if ( J = l , ( I X l ) , .0. ) ) )
20		iftrue 3899	. . . . . . . . 9 |- ( J = K -> if ( J = K , ( ( I X l ) ( .r ` R ) ( C ` l ) ) , if ( J = l , ( I X l ) , .0. ) ) = ( ( I X l ) ( .r ` R ) ( C ` l ) ) )
21	20	adantr 471	. . . . . . . 8 |- ( ( J = K /\ ( R e. Ring /\ ( X e. B /\ C e. V /\ K e. N ) /\ ( I e. N /\ J e. N /\ ( X .X. C ) = Z ) ) ) -> if ( J = K , ( ( I X l ) ( .r ` R ) ( C ` l ) ) , if ( J = l , ( I X l ) , .0. ) ) = ( ( I X l ) ( .r ` R ) ( C ` l ) ) )
22	21	adantr 471	. . . . . . 7 |- ( ( ( J = K /\ ( R e. Ring /\ ( X e. B /\ C e. V /\ K e. N ) /\ ( I e. N /\ J e. N /\ ( X .X. C ) = Z ) ) ) /\ l e. N ) -> if ( J = K , ( ( I X l ) ( .r ` R ) ( C ` l ) ) , if ( J = l , ( I X l ) , .0. ) ) = ( ( I X l ) ( .r ` R ) ( C ` l ) ) )
23	19, 22	eqtrd 2496	. . . . . 6 |- ( ( ( J = K /\ ( R e. Ring /\ ( X e. B /\ C e. V /\ K e. N ) /\ ( I e. N /\ J e. N /\ ( X .X. C ) = Z ) ) ) /\ l e. N ) -> ( ( I X l ) ( .r ` R ) ( l E J ) ) = ( ( I X l ) ( .r ` R ) ( C ` l ) ) )
24	23	mpteq2dva 4503	. . . . 5 |- ( ( J = K /\ ( R e. Ring /\ ( X e. B /\ C e. V /\ K e. N ) /\ ( I e. N /\ J e. N /\ ( X .X. C ) = Z ) ) ) -> ( l e. N |-> ( ( I X l ) ( .r ` R ) ( l E J ) ) ) = ( l e. N |-> ( ( I X l ) ( .r ` R ) ( C ` l ) ) ) )
25	24	oveq2d 6331	. . . 4 |- ( ( J = K /\ ( R e. Ring /\ ( X e. B /\ C e. V /\ K e. N ) /\ ( I e. N /\ J e. N /\ ( X .X. C ) = Z ) ) ) -> ( R gsumg ( l e. N |-> ( ( I X l ) ( .r ` R ) ( l E J ) ) ) ) = ( R gsumg ( l e. N |-> ( ( I X l ) ( .r ` R ) ( C ` l ) ) ) ) )
26		fveq1 5887	. . . . . . . . 9 |- ( ( X .X. C ) = Z -> ( ( X .X. C ) ` I ) = ( Z ` I ) )
27	26	eqcomd 2468	. . . . . . . 8 |- ( ( X .X. C ) = Z -> ( Z ` I ) = ( ( X .X. C ) ` I ) )
28	27	3ad2ant3 1037	. . . . . . 7 |- ( ( I e. N /\ J e. N /\ ( X .X. C ) = Z ) -> ( Z ` I ) = ( ( X .X. C ) ` I ) )
29	28	3ad2ant3 1037	. . . . . 6 |- ( ( R e. Ring /\ ( X e. B /\ C e. V /\ K e. N ) /\ ( I e. N /\ J e. N /\ ( X .X. C ) = Z ) ) -> ( Z ` I ) = ( ( X .X. C ) ` I ) )
30	29	adantl 472	. . . . 5 |- ( ( J = K /\ ( R e. Ring /\ ( X e. B /\ C e. V /\ K e. N ) /\ ( I e. N /\ J e. N /\ ( X .X. C ) = Z ) ) ) -> ( Z ` I ) = ( ( X .X. C ) ` I ) )
31		mulmarep1gsum2.x	. . . . . 6 |- .X. = ( R maVecMul <. N , N >. )
32		eqid 2462	. . . . . 6 |- ( Base ` R ) = ( Base ` R )
33		eqid 2462	. . . . . 6 |- ( .r ` R ) = ( .r ` R )
34	1	adantl 472	. . . . . 6 |- ( ( J = K /\ ( R e. Ring /\ ( X e. B /\ C e. V /\ K e. N ) /\ ( I e. N /\ J e. N /\ ( X .X. C ) = Z ) ) ) -> R e. Ring )
35	12, 13	matrcl 19486	. . . . . . . . . 10 |- ( X e. B -> ( N e. Fin /\ R e. _V ) )
36	35	simpld 465	. . . . . . . . 9 |- ( X e. B -> N e. Fin )
37	36	3ad2ant1 1035	. . . . . . . 8 |- ( ( X e. B /\ C e. V /\ K e. N ) -> N e. Fin )
38	37	3ad2ant2 1036	. . . . . . 7 |- ( ( R e. Ring /\ ( X e. B /\ C e. V /\ K e. N ) /\ ( I e. N /\ J e. N /\ ( X .X. C ) = Z ) ) -> N e. Fin )
39	38	adantl 472	. . . . . 6 |- ( ( J = K /\ ( R e. Ring /\ ( X e. B /\ C e. V /\ K e. N ) /\ ( I e. N /\ J e. N /\ ( X .X. C ) = Z ) ) ) -> N e. Fin )
40	13	eleq2i 2532	. . . . . . . . . 10 |- ( X e. B <-> X e. ( Base ` A ) )
41	40	biimpi 199	. . . . . . . . 9 |- ( X e. B -> X e. ( Base ` A ) )
42	41	3ad2ant1 1035	. . . . . . . 8 |- ( ( X e. B /\ C e. V /\ K e. N ) -> X e. ( Base ` A ) )
43	42	3ad2ant2 1036	. . . . . . 7 |- ( ( R e. Ring /\ ( X e. B /\ C e. V /\ K e. N ) /\ ( I e. N /\ J e. N /\ ( X .X. C ) = Z ) ) -> X e. ( Base ` A ) )
44	43	adantl 472	. . . . . 6 |- ( ( J = K /\ ( R e. Ring /\ ( X e. B /\ C e. V /\ K e. N ) /\ ( I e. N /\ J e. N /\ ( X .X. C ) = Z ) ) ) -> X e. ( Base ` A ) )
45	14	eleq2i 2532	. . . . . . . . . 10 |- ( C e. V <-> C e. ( ( Base ` R ) ^m N ) )
46	45	biimpi 199	. . . . . . . . 9 |- ( C e. V -> C e. ( ( Base ` R ) ^m N ) )
47	46	3ad2ant2 1036	. . . . . . . 8 |- ( ( X e. B /\ C e. V /\ K e. N ) -> C e. ( ( Base ` R ) ^m N ) )
48	47	3ad2ant2 1036	. . . . . . 7 |- ( ( R e. Ring /\ ( X e. B /\ C e. V /\ K e. N ) /\ ( I e. N /\ J e. N /\ ( X .X. C ) = Z ) ) -> C e. ( ( Base ` R ) ^m N ) )
49	48	adantl 472	. . . . . 6 |- ( ( J = K /\ ( R e. Ring /\ ( X e. B /\ C e. V /\ K e. N ) /\ ( I e. N /\ J e. N /\ ( X .X. C ) = Z ) ) ) -> C e. ( ( Base ` R ) ^m N ) )
50	5	adantl 472	. . . . . 6 |- ( ( J = K /\ ( R e. Ring /\ ( X e. B /\ C e. V /\ K e. N ) /\ ( I e. N /\ J e. N /\ ( X .X. C ) = Z ) ) ) -> I e. N )
51	12, 31, 32, 33, 34, 39, 44, 49, 50	mavmulfv 19620	. . . . 5 |- ( ( J = K /\ ( R e. Ring /\ ( X e. B /\ C e. V /\ K e. N ) /\ ( I e. N /\ J e. N /\ ( X .X. C ) = Z ) ) ) -> ( ( X .X. C ) ` I ) = ( R gsumg ( l e. N |-> ( ( I X l ) ( .r ` R ) ( C ` l ) ) ) ) )
52	30, 51	eqtrd 2496	. . . 4 |- ( ( J = K /\ ( R e. Ring /\ ( X e. B /\ C e. V /\ K e. N ) /\ ( I e. N /\ J e. N /\ ( X .X. C ) = Z ) ) ) -> ( Z ` I ) = ( R gsumg ( l e. N |-> ( ( I X l ) ( .r ` R ) ( C ` l ) ) ) ) )
53		iftrue 3899	. . . . . 6 |- ( J = K -> if ( J = K , ( Z ` I ) , ( I X J ) ) = ( Z ` I ) )
54	53	eqcomd 2468	. . . . 5 |- ( J = K -> ( Z ` I ) = if ( J = K , ( Z ` I ) , ( I X J ) ) )
55	54	adantr 471	. . . 4 |- ( ( J = K /\ ( R e. Ring /\ ( X e. B /\ C e. V /\ K e. N ) /\ ( I e. N /\ J e. N /\ ( X .X. C ) = Z ) ) ) -> ( Z ` I ) = if ( J = K , ( Z ` I ) , ( I X J ) ) )
56	25, 52, 55	3eqtr2d 2502	. . 3 |- ( ( J = K /\ ( R e. Ring /\ ( X e. B /\ C e. V /\ K e. N ) /\ ( I e. N /\ J e. N /\ ( X .X. C ) = Z ) ) ) -> ( R gsumg ( l e. N |-> ( ( I X l ) ( .r ` R ) ( l E J ) ) ) ) = if ( J = K , ( Z ` I ) , ( I X J ) ) )
57	56	ex 440	. 2 |- ( J = K -> ( ( R e. Ring /\ ( X e. B /\ C e. V /\ K e. N ) /\ ( I e. N /\ J e. N /\ ( X .X. C ) = Z ) ) -> ( R gsumg ( l e. N |-> ( ( I X l ) ( .r ` R ) ( l E J ) ) ) ) = if ( J = K , ( Z ` I ) , ( I X J ) ) ) )
58	1	adantr 471	. . . . 5 |- ( ( ( R e. Ring /\ ( X e. B /\ C e. V /\ K e. N ) /\ ( I e. N /\ J e. N /\ ( X .X. C ) = Z ) ) /\ J =/= K ) -> R e. Ring )
59		simpl2 1018	. . . . 5 |- ( ( ( R e. Ring /\ ( X e. B /\ C e. V /\ K e. N ) /\ ( I e. N /\ J e. N /\ ( X .X. C ) = Z ) ) /\ J =/= K ) -> ( X e. B /\ C e. V /\ K e. N ) )
60	5	adantr 471	. . . . 5 |- ( ( ( R e. Ring /\ ( X e. B /\ C e. V /\ K e. N ) /\ ( I e. N /\ J e. N /\ ( X .X. C ) = Z ) ) /\ J =/= K ) -> I e. N )
61		simpl32 1096	. . . . 5 |- ( ( ( R e. Ring /\ ( X e. B /\ C e. V /\ K e. N ) /\ ( I e. N /\ J e. N /\ ( X .X. C ) = Z ) ) /\ J =/= K ) -> J e. N )
62		simpr 467	. . . . 5 |- ( ( ( R e. Ring /\ ( X e. B /\ C e. V /\ K e. N ) /\ ( I e. N /\ J e. N /\ ( X .X. C ) = Z ) ) /\ J =/= K ) -> J =/= K )
63	12, 13, 14, 15, 16, 17	mulmarep1gsum1 19647	. . . . 5 |- ( ( R e. Ring /\ ( X e. B /\ C e. V /\ K e. N ) /\ ( I e. N /\ J e. N /\ J =/= K ) ) -> ( R gsumg ( l e. N |-> ( ( I X l ) ( .r ` R ) ( l E J ) ) ) ) = ( I X J ) )
64	58, 59, 60, 61, 62, 63	syl113anc 1288	. . . 4 |- ( ( ( R e. Ring /\ ( X e. B /\ C e. V /\ K e. N ) /\ ( I e. N /\ J e. N /\ ( X .X. C ) = Z ) ) /\ J =/= K ) -> ( R gsumg ( l e. N |-> ( ( I X l ) ( .r ` R ) ( l E J ) ) ) ) = ( I X J ) )
65		df-ne 2635	. . . . . 6 |- ( J =/= K <-> -. J = K )
66		iffalse 3902	. . . . . . 7 |- ( -. J = K -> if ( J = K , ( Z ` I ) , ( I X J ) ) = ( I X J ) )
67	66	eqcomd 2468	. . . . . 6 |- ( -. J = K -> ( I X J ) = if ( J = K , ( Z ` I ) , ( I X J ) ) )
68	65, 67	sylbi 200	. . . . 5 |- ( J =/= K -> ( I X J ) = if ( J = K , ( Z ` I ) , ( I X J ) ) )
69	68	adantl 472	. . . 4 |- ( ( ( R e. Ring /\ ( X e. B /\ C e. V /\ K e. N ) /\ ( I e. N /\ J e. N /\ ( X .X. C ) = Z ) ) /\ J =/= K ) -> ( I X J ) = if ( J = K , ( Z ` I ) , ( I X J ) ) )
70	64, 69	eqtrd 2496	. . 3 |- ( ( ( R e. Ring /\ ( X e. B /\ C e. V /\ K e. N ) /\ ( I e. N /\ J e. N /\ ( X .X. C ) = Z ) ) /\ J =/= K ) -> ( R gsumg ( l e. N |-> ( ( I X l ) ( .r ` R ) ( l E J ) ) ) ) = if ( J = K , ( Z ` I ) , ( I X J ) ) )
71	70	expcom 441	. 2 |- ( J =/= K -> ( ( R e. Ring /\ ( X e. B /\ C e. V /\ K e. N ) /\ ( I e. N /\ J e. N /\ ( X .X. C ) = Z ) ) -> ( R gsumg ( l e. N |-> ( ( I X l ) ( .r ` R ) ( l E J ) ) ) ) = if ( J = K , ( Z ` I ) , ( I X J ) ) ) )
72	57, 71	pm2.61ine 2719	1 |- ( ( R e. Ring /\ ( X e. B /\ C e. V /\ K e. N ) /\ ( I e. N /\ J e. N /\ ( X .X. C ) = Z ) ) -> ( R gsumg ( l e. N |-> ( ( I X l ) ( .r ` R ) ( l E J ) ) ) ) = if ( J = K , ( Z ` I ) , ( I X J ) ) )

Syntax hints:   -. wn 3   -> wi 4   /\ wa 375   /\ w3a 991   = wceq 1455   e. wcel 1898   =/= wne 2633   _Vcvv 3057   ifcif 3893   <.cop 3986   |-> cmpt 4475   ` cfv 5601  (class class class)co 6315   ^m cmap 7498   Fincfn 7595   Basecbs 15170   .rcmulr 15240   0gc0g 15387   gsum_g cgsu 15388   1rcur 17784   Ringcrg 17829   Mat cmat 19481   maVecMul cmvmul 19614   matRepV cmatrepV 19631

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 4529  ax-sep 4539  ax-nul 4548  ax-pow 4595  ax-pr 4653  ax-un 6610  ax-inf2 8172  ax-cnex 9621  ax-resscn 9622  ax-1cn 9623  ax-icn 9624  ax-addcl 9625  ax-addrcl 9626  ax-mulcl 9627  ax-mulrcl 9628  ax-mulcom 9629  ax-addass 9630  ax-mulass 9631  ax-distr 9632  ax-i2m1 9633  ax-1ne0 9634  ax-1rid 9635  ax-rnegex 9636  ax-rrecex 9637  ax-cnre 9638  ax-pre-lttri 9639  ax-pre-lttrn 9640  ax-pre-ltadd 9641  ax-pre-mulgt0 9642

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3or 992  df-3an 993  df-tru 1458  df-fal 1461  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 4417  df-opab 4476  df-mpt 4477  df-tr 4512  df-eprel 4764  df-id 4768  df-po 4774  df-so 4775  df-fr 4812  df-se 4813  df-we 4814  df-xp 4859  df-rel 4860  df-cnv 4861  df-co 4862  df-dm 4863  df-rn 4864  df-res 4865  df-ima 4866  df-pred 5399  df-ord 5445  df-on 5446  df-lim 5447  df-suc 5448  df-iota 5565  df-fun 5603  df-fn 5604  df-f 5605  df-f1 5606  df-fo 5607  df-f1o 5608  df-fv 5609  df-isom 5610  df-riota 6277  df-ov 6318  df-oprab 6319  df-mpt2 6320  df-of 6558  df-om 6720  df-1st 6820  df-2nd 6821  df-supp 6942  df-wrecs 7054  df-recs 7116  df-rdg 7154  df-1o 7208  df-oadd 7212  df-er 7389  df-map 7500  df-ixp 7549  df-en 7596  df-dom 7597  df-sdom 7598  df-fin 7599  df-fsupp 7910  df-sup 7982  df-oi 8051  df-card 8399  df-pnf 9703  df-mnf 9704  df-xr 9705  df-ltxr 9706  df-le 9707  df-sub 9888  df-neg 9889  df-nn 10638  df-2 10696  df-3 10697  df-4 10698  df-5 10699  df-6 10700  df-7 10701  df-8 10702  df-9 10703  df-10 10704  df-n0 10899  df-z 10967  df-dec 11081  df-uz 11189  df-fz 11814  df-fzo 11947  df-seq 12246  df-hash 12548  df-struct 15172  df-ndx 15173  df-slot 15174  df-base 15175  df-sets 15176  df-ress 15177  df-plusg 15252  df-mulr 15253  df-sca 15255  df-vsca 15256  df-ip 15257  df-tset 15258  df-ple 15259  df-ds 15261  df-hom 15263  df-cco 15264  df-0g 15389  df-gsum 15390  df-prds 15395  df-pws 15397  df-mre 15541  df-mrc 15542  df-acs 15544  df-mgm 16537  df-sgrp 16576  df-mnd 16586  df-mhm 16631  df-submnd 16632  df-grp 16722  df-minusg 16723  df-sbg 16724  df-mulg 16725  df-subg 16863  df-ghm 16930  df-cntz 17020  df-cmn 17481  df-abl 17482  df-mgp 17773  df-ur 17785  df-ring 17831  df-subrg 18055  df-lmod 18142  df-lss 18205  df-sra 18444  df-rgmod 18445  df-dsmm 19344  df-frlm 19359  df-mamu 19458  df-mat 19482  df-mvmul 19615  df-marepv 19633

This theorem is referenced by:  cramerimplem2  19758