Theorem 1mavmul 18496

Description: Multiplication of the identity NxN matrix with an N-dimensional vector results in the vector itself. (Contributed by AV, 9-Feb-2019.) (Revised by AV, 23-Feb-2019.)

Hypotheses

Ref	Expression
1mavmul.a	|- A = ( N Mat R )
1mavmul.b	|- B = ( Base ` R )
1mavmul.t	|- .x. = ( R maVecMul <. N , N >. )
1mavmul.r	|- ( ph -> R e. Ring )
1mavmul.n	|- ( ph -> N e. Fin )
1mavmul.y	|- ( ph -> Y e. ( B ^m N ) )

Assertion

Ref	Expression
1mavmul	|- ( ph -> ( ( 1r ` A ) .x. Y ) = Y )

Proof of Theorem 1mavmul

Dummy variables i j x y are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		1mavmul.a	. . 3 |- A = ( N Mat R )
2		1mavmul.t	. . 3 |- .x. = ( R maVecMul <. N , N >. )
3		1mavmul.b	. . 3 |- B = ( Base ` R )
4		eqid 2454	. . 3 |- ( .r ` R ) = ( .r ` R )
5		1mavmul.r	. . 3 |- ( ph -> R e. Ring )
6		1mavmul.n	. . 3 |- ( ph -> N e. Fin )
7		eqid 2454	. . . . 5 |- ( Base ` A ) = ( Base ` A )
8	1	fveq2i 5805	. . . . 5 |- ( 1r ` A ) = ( 1r ` ( N Mat R ) )
9	1, 7, 8	mat1bas 18473	. . . 4 |- ( ( R e. Ring /\ N e. Fin ) -> ( 1r ` A ) e. ( Base ` A ) )
10	5, 6, 9	syl2anc 661	. . 3 |- ( ph -> ( 1r ` A ) e. ( Base ` A ) )
11		1mavmul.y	. . 3 |- ( ph -> Y e. ( B ^m N ) )
12	1, 2, 3, 4, 5, 6, 10, 11	mavmulval 18493	. 2 |- ( ph -> ( ( 1r ` A ) .x. Y ) = ( i e. N |-> ( R gsumg ( j e. N |-> ( ( i ( 1r ` A ) j ) ( .r ` R ) ( Y ` j ) ) ) ) ) )
13		eqid 2454	. . . . . . . . . 10 |- ( 1r ` R ) = ( 1r ` R )
14		eqid 2454	. . . . . . . . . 10 |- ( 0g ` R ) = ( 0g ` R )
15	1, 13, 14	mat1 18471	. . . . . . . . 9 |- ( ( N e. Fin /\ R e. Ring ) -> ( 1r ` A ) = ( x e. N , y e. N |-> if ( x = y , ( 1r ` R ) , ( 0g ` R ) ) ) )
16	6, 5, 15	syl2anc 661	. . . . . . . 8 |- ( ph -> ( 1r ` A ) = ( x e. N , y e. N |-> if ( x = y , ( 1r ` R ) , ( 0g ` R ) ) ) )
17	16	proplem3 14752	. . . . . . 7 |- ( ( ph /\ i e. N ) -> ( i ( 1r ` A ) j ) = ( i ( x e. N , y e. N |-> if ( x = y , ( 1r ` R ) , ( 0g ` R ) ) ) j ) )
18	17	oveq1d 6218	. . . . . 6 |- ( ( ph /\ i e. N ) -> ( ( i ( 1r ` A ) j ) ( .r ` R ) ( Y ` j ) ) = ( ( i ( x e. N , y e. N |-> if ( x = y , ( 1r ` R ) , ( 0g ` R ) ) ) j ) ( .r ` R ) ( Y ` j ) ) )
19	18	mpteq2dv 4490	. . . . 5 |- ( ( ph /\ i e. N ) -> ( j e. N |-> ( ( i ( 1r ` A ) j ) ( .r ` R ) ( Y ` j ) ) ) = ( j e. N |-> ( ( i ( x e. N , y e. N |-> if ( x = y , ( 1r ` R ) , ( 0g ` R ) ) ) j ) ( .r ` R ) ( Y ` j ) ) ) )
20	19	oveq2d 6219	. . . 4 |- ( ( ph /\ i e. N ) -> ( R gsumg ( j e. N |-> ( ( i ( 1r ` A ) j ) ( .r ` R ) ( Y ` j ) ) ) ) = ( R gsumg ( j e. N |-> ( ( i ( x e. N , y e. N |-> if ( x = y , ( 1r ` R ) , ( 0g ` R ) ) ) j ) ( .r ` R ) ( Y ` j ) ) ) ) )
21		eqidd 2455	. . . . . . . . 9 |- ( ( ( ph /\ i e. N ) /\ j e. N ) -> ( x e. N , y e. N |-> if ( x = y , ( 1r ` R ) , ( 0g ` R ) ) ) = ( x e. N , y e. N |-> if ( x = y , ( 1r ` R ) , ( 0g ` R ) ) ) )
22		eqeq12 2473	. . . . . . . . . . 11 |- ( ( x = i /\ y = j ) -> ( x = y <-> i = j ) )
23	22	ifbid 3922	. . . . . . . . . 10 |- ( ( x = i /\ y = j ) -> if ( x = y , ( 1r ` R ) , ( 0g ` R ) ) = if ( i = j , ( 1r ` R ) , ( 0g ` R ) ) )
24	23	adantl 466	. . . . . . . . 9 |- ( ( ( ( ph /\ i e. N ) /\ j e. N ) /\ ( x = i /\ y = j ) ) -> if ( x = y , ( 1r ` R ) , ( 0g ` R ) ) = if ( i = j , ( 1r ` R ) , ( 0g ` R ) ) )
25		simpr 461	. . . . . . . . . 10 |- ( ( ph /\ i e. N ) -> i e. N )
26	25	adantr 465	. . . . . . . . 9 |- ( ( ( ph /\ i e. N ) /\ j e. N ) -> i e. N )
27		simpr 461	. . . . . . . . 9 |- ( ( ( ph /\ i e. N ) /\ j e. N ) -> j e. N )
28		fvex 5812	. . . . . . . . . . 11 |- ( 1r ` R ) e. _V
29	28	a1i 11	. . . . . . . . . 10 |- ( ( ( ph /\ i e. N ) /\ j e. N ) -> ( 1r ` R ) e. _V )
30		fvex 5812	. . . . . . . . . . 11 |- ( 0g ` R ) e. _V
31	30	a1i 11	. . . . . . . . . 10 |- ( ( ( ph /\ i e. N ) /\ j e. N ) -> ( 0g ` R ) e. _V )
32	29, 31	ifcld 3943	. . . . . . . . 9 |- ( ( ( ph /\ i e. N ) /\ j e. N ) -> if ( i = j , ( 1r ` R ) , ( 0g ` R ) ) e. _V )
33	21, 24, 26, 27, 32	ovmpt2d 6331	. . . . . . . 8 |- ( ( ( ph /\ i e. N ) /\ j e. N ) -> ( i ( x e. N , y e. N |-> if ( x = y , ( 1r ` R ) , ( 0g ` R ) ) ) j ) = if ( i = j , ( 1r ` R ) , ( 0g ` R ) ) )
34	33	oveq1d 6218	. . . . . . 7 |- ( ( ( ph /\ i e. N ) /\ j e. N ) -> ( ( i ( x e. N , y e. N |-> if ( x = y , ( 1r ` R ) , ( 0g ` R ) ) ) j ) ( .r ` R ) ( Y ` j ) ) = ( if ( i = j , ( 1r ` R ) , ( 0g ` R ) ) ( .r ` R ) ( Y ` j ) ) )
35		iftrue 3908	. . . . . . . . . . . 12 |- ( i = j -> if ( i = j , ( 1r ` R ) , ( 0g ` R ) ) = ( 1r ` R ) )
36	35	adantr 465	. . . . . . . . . . 11 |- ( ( i = j /\ ( ( ph /\ i e. N ) /\ j e. N ) ) -> if ( i = j , ( 1r ` R ) , ( 0g ` R ) ) = ( 1r ` R ) )
37	36	oveq1d 6218	. . . . . . . . . 10 |- ( ( i = j /\ ( ( ph /\ i e. N ) /\ j e. N ) ) -> ( if ( i = j , ( 1r ` R ) , ( 0g ` R ) ) ( .r ` R ) ( Y ` j ) ) = ( ( 1r ` R ) ( .r ` R ) ( Y ` j ) ) )
38	5	adantr 465	. . . . . . . . . . . . 13 |- ( ( ph /\ i e. N ) -> R e. Ring )
39	38	adantr 465	. . . . . . . . . . . 12 |- ( ( ( ph /\ i e. N ) /\ j e. N ) -> R e. Ring )
40		fvex 5812	. . . . . . . . . . . . . . . . . . 19 |- ( Base ` R ) e. _V
41	3, 40	eqeltri 2538	. . . . . . . . . . . . . . . . . 18 |- B e. _V
42	41	a1i 11	. . . . . . . . . . . . . . . . 17 |- ( ph -> B e. _V )
43		elmapg 7340	. . . . . . . . . . . . . . . . 17 |- ( ( B e. _V /\ N e. Fin ) -> ( Y e. ( B ^m N ) <-> Y : N --> B ) )
44	42, 6, 43	syl2anc 661	. . . . . . . . . . . . . . . 16 |- ( ph -> ( Y e. ( B ^m N ) <-> Y : N --> B ) )
45		ffvelrn 5953	. . . . . . . . . . . . . . . . 17 |- ( ( Y : N --> B /\ j e. N ) -> ( Y ` j ) e. B )
46	45	ex 434	. . . . . . . . . . . . . . . 16 |- ( Y : N --> B -> ( j e. N -> ( Y ` j ) e. B ) )
47	44, 46	syl6bi 228	. . . . . . . . . . . . . . 15 |- ( ph -> ( Y e. ( B ^m N ) -> ( j e. N -> ( Y ` j ) e. B ) ) )
48	11, 47	mpd 15	. . . . . . . . . . . . . 14 |- ( ph -> ( j e. N -> ( Y ` j ) e. B ) )
49	48	adantr 465	. . . . . . . . . . . . 13 |- ( ( ph /\ i e. N ) -> ( j e. N -> ( Y ` j ) e. B ) )
50	49	imp 429	. . . . . . . . . . . 12 |- ( ( ( ph /\ i e. N ) /\ j e. N ) -> ( Y ` j ) e. B )
51	3, 4, 13	rnglidm 16801	. . . . . . . . . . . 12 |- ( ( R e. Ring /\ ( Y ` j ) e. B ) -> ( ( 1r ` R ) ( .r ` R ) ( Y ` j ) ) = ( Y ` j ) )
52	39, 50, 51	syl2anc 661	. . . . . . . . . . 11 |- ( ( ( ph /\ i e. N ) /\ j e. N ) -> ( ( 1r ` R ) ( .r ` R ) ( Y ` j ) ) = ( Y ` j ) )
53	52	adantl 466	. . . . . . . . . 10 |- ( ( i = j /\ ( ( ph /\ i e. N ) /\ j e. N ) ) -> ( ( 1r ` R ) ( .r ` R ) ( Y ` j ) ) = ( Y ` j ) )
54		fveq2 5802	. . . . . . . . . . . 12 |- ( j = i -> ( Y ` j ) = ( Y ` i ) )
55	54	equcoms 1735	. . . . . . . . . . 11 |- ( i = j -> ( Y ` j ) = ( Y ` i ) )
56	55	adantr 465	. . . . . . . . . 10 |- ( ( i = j /\ ( ( ph /\ i e. N ) /\ j e. N ) ) -> ( Y ` j ) = ( Y ` i ) )
57	37, 53, 56	3eqtrd 2499	. . . . . . . . 9 |- ( ( i = j /\ ( ( ph /\ i e. N ) /\ j e. N ) ) -> ( if ( i = j , ( 1r ` R ) , ( 0g ` R ) ) ( .r ` R ) ( Y ` j ) ) = ( Y ` i ) )
58		iftrue 3908	. . . . . . . . . . 11 |- ( j = i -> if ( j = i , ( Y ` i ) , ( 0g ` R ) ) = ( Y ` i ) )
59	58	equcoms 1735	. . . . . . . . . 10 |- ( i = j -> if ( j = i , ( Y ` i ) , ( 0g ` R ) ) = ( Y ` i ) )
60	59	adantr 465	. . . . . . . . 9 |- ( ( i = j /\ ( ( ph /\ i e. N ) /\ j e. N ) ) -> if ( j = i , ( Y ` i ) , ( 0g ` R ) ) = ( Y ` i ) )
61	57, 60	eqtr4d 2498	. . . . . . . 8 |- ( ( i = j /\ ( ( ph /\ i e. N ) /\ j e. N ) ) -> ( if ( i = j , ( 1r ` R ) , ( 0g ` R ) ) ( .r ` R ) ( Y ` j ) ) = if ( j = i , ( Y ` i ) , ( 0g ` R ) ) )
62		iffalse 3910	. . . . . . . . . . 11 |- ( -. i = j -> if ( i = j , ( 1r ` R ) , ( 0g ` R ) ) = ( 0g ` R ) )
63	62	oveq1d 6218	. . . . . . . . . 10 |- ( -. i = j -> ( if ( i = j , ( 1r ` R ) , ( 0g ` R ) ) ( .r ` R ) ( Y ` j ) ) = ( ( 0g ` R ) ( .r ` R ) ( Y ` j ) ) )
64	63	adantr 465	. . . . . . . . 9 |- ( ( -. i = j /\ ( ( ph /\ i e. N ) /\ j e. N ) ) -> ( if ( i = j , ( 1r ` R ) , ( 0g ` R ) ) ( .r ` R ) ( Y ` j ) ) = ( ( 0g ` R ) ( .r ` R ) ( Y ` j ) ) )
65	3, 4, 14	rnglz 16814	. . . . . . . . . . 11 |- ( ( R e. Ring /\ ( Y ` j ) e. B ) -> ( ( 0g ` R ) ( .r ` R ) ( Y ` j ) ) = ( 0g ` R ) )
66	39, 50, 65	syl2anc 661	. . . . . . . . . 10 |- ( ( ( ph /\ i e. N ) /\ j e. N ) -> ( ( 0g ` R ) ( .r ` R ) ( Y ` j ) ) = ( 0g ` R ) )
67	66	adantl 466	. . . . . . . . 9 |- ( ( -. i = j /\ ( ( ph /\ i e. N ) /\ j e. N ) ) -> ( ( 0g ` R ) ( .r ` R ) ( Y ` j ) ) = ( 0g ` R ) )
68		eqcom 2463	. . . . . . . . . . . 12 |- ( i = j <-> j = i )
69		iffalse 3910	. . . . . . . . . . . 12 |- ( -. j = i -> if ( j = i , ( Y ` i ) , ( 0g ` R ) ) = ( 0g ` R ) )
70	68, 69	sylnbi 306	. . . . . . . . . . 11 |- ( -. i = j -> if ( j = i , ( Y ` i ) , ( 0g ` R ) ) = ( 0g ` R ) )
71	70	eqcomd 2462	. . . . . . . . . 10 |- ( -. i = j -> ( 0g ` R ) = if ( j = i , ( Y ` i ) , ( 0g ` R ) ) )
72	71	adantr 465	. . . . . . . . 9 |- ( ( -. i = j /\ ( ( ph /\ i e. N ) /\ j e. N ) ) -> ( 0g ` R ) = if ( j = i , ( Y ` i ) , ( 0g ` R ) ) )
73	64, 67, 72	3eqtrd 2499	. . . . . . . 8 |- ( ( -. i = j /\ ( ( ph /\ i e. N ) /\ j e. N ) ) -> ( if ( i = j , ( 1r ` R ) , ( 0g ` R ) ) ( .r ` R ) ( Y ` j ) ) = if ( j = i , ( Y ` i ) , ( 0g ` R ) ) )
74	61, 73	pm2.61ian 788	. . . . . . 7 |- ( ( ( ph /\ i e. N ) /\ j e. N ) -> ( if ( i = j , ( 1r ` R ) , ( 0g ` R ) ) ( .r ` R ) ( Y ` j ) ) = if ( j = i , ( Y ` i ) , ( 0g ` R ) ) )
75	34, 74	eqtrd 2495	. . . . . 6 |- ( ( ( ph /\ i e. N ) /\ j e. N ) -> ( ( i ( x e. N , y e. N |-> if ( x = y , ( 1r ` R ) , ( 0g ` R ) ) ) j ) ( .r ` R ) ( Y ` j ) ) = if ( j = i , ( Y ` i ) , ( 0g ` R ) ) )
76	75	mpteq2dva 4489	. . . . 5 |- ( ( ph /\ i e. N ) -> ( j e. N |-> ( ( i ( x e. N , y e. N |-> if ( x = y , ( 1r ` R ) , ( 0g ` R ) ) ) j ) ( .r ` R ) ( Y ` j ) ) ) = ( j e. N |-> if ( j = i , ( Y ` i ) , ( 0g ` R ) ) ) )
77	76	oveq2d 6219	. . . 4 |- ( ( ph /\ i e. N ) -> ( R gsumg ( j e. N |-> ( ( i ( x e. N , y e. N |-> if ( x = y , ( 1r ` R ) , ( 0g ` R ) ) ) j ) ( .r ` R ) ( Y ` j ) ) ) ) = ( R gsumg ( j e. N |-> if ( j = i , ( Y ` i ) , ( 0g ` R ) ) ) ) )
78		rngmnd 16787	. . . . . . 7 |- ( R e. Ring -> R e. Mnd )
79	5, 78	syl 16	. . . . . 6 |- ( ph -> R e. Mnd )
80	79	adantr 465	. . . . 5 |- ( ( ph /\ i e. N ) -> R e. Mnd )
81	6	adantr 465	. . . . 5 |- ( ( ph /\ i e. N ) -> N e. Fin )
82		eqid 2454	. . . . 5 |- ( j e. N |-> if ( j = i , ( Y ` i ) , ( 0g ` R ) ) ) = ( j e. N |-> if ( j = i , ( Y ` i ) , ( 0g ` R ) ) )
83		ffvelrn 5953	. . . . . . . . . 10 |- ( ( Y : N --> B /\ i e. N ) -> ( Y ` i ) e. B )
84	83, 3	syl6eleq 2552	. . . . . . . . 9 |- ( ( Y : N --> B /\ i e. N ) -> ( Y ` i ) e. ( Base ` R ) )
85	84	ex 434	. . . . . . . 8 |- ( Y : N --> B -> ( i e. N -> ( Y ` i ) e. ( Base ` R ) ) )
86	44, 85	syl6bi 228	. . . . . . 7 |- ( ph -> ( Y e. ( B ^m N ) -> ( i e. N -> ( Y ` i ) e. ( Base ` R ) ) ) )
87	11, 86	mpd 15	. . . . . 6 |- ( ph -> ( i e. N -> ( Y ` i ) e. ( Base ` R ) ) )
88	87	imp 429	. . . . 5 |- ( ( ph /\ i e. N ) -> ( Y ` i ) e. ( Base ` R ) )
89	14, 80, 81, 25, 82, 88	gsummptif1n0 16589	. . . 4 |- ( ( ph /\ i e. N ) -> ( R gsumg ( j e. N |-> if ( j = i , ( Y ` i ) , ( 0g ` R ) ) ) ) = ( Y ` i ) )
90	20, 77, 89	3eqtrd 2499	. . 3 |- ( ( ph /\ i e. N ) -> ( R gsumg ( j e. N |-> ( ( i ( 1r ` A ) j ) ( .r ` R ) ( Y ` j ) ) ) ) = ( Y ` i ) )
91	90	mpteq2dva 4489	. 2 |- ( ph -> ( i e. N |-> ( R gsumg ( j e. N |-> ( ( i ( 1r ` A ) j ) ( .r ` R ) ( Y ` j ) ) ) ) ) = ( i e. N |-> ( Y ` i ) ) )
92		ffn 5670	. . . . 5 |- ( Y : N --> B -> Y Fn N )
93	44, 92	syl6bi 228	. . . 4 |- ( ph -> ( Y e. ( B ^m N ) -> Y Fn N ) )
94	11, 93	mpd 15	. . 3 |- ( ph -> Y Fn N )
95		eqcom 2463	. . . 4 |- ( ( i e. N |-> ( Y ` i ) ) = Y <-> Y = ( i e. N |-> ( Y ` i ) ) )
96		dffn5 5849	. . . 4 |- ( Y Fn N <-> Y = ( i e. N |-> ( Y ` i ) ) )
97	95, 96	bitr4i 252	. . 3 |- ( ( i e. N |-> ( Y ` i ) ) = Y <-> Y Fn N )
98	94, 97	sylibr 212	. 2 |- ( ph -> ( i e. N |-> ( Y ` i ) ) = Y )
99	12, 91, 98	3eqtrd 2499	1 |- ( ph -> ( ( 1r ` A ) .x. Y ) = Y )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 184   /\ wa 369   = wceq 1370   e. wcel 1758   _Vcvv 3078   ifcif 3902   <.cop 3994   |-> cmpt 4461   Fn wfn 5524   -->wf 5525   ` cfv 5529  (class class class)co 6203   |-> cmpt2 6205   ^m cmap 7327   Fincfn 7423   Basecbs 14296   .rcmulr 14362   0gc0g 14501   gsum_g cgsu 14502   Mndcmnd 15532   1rcur 16735   Ringcrg 16778   Mat cmat 18415   maVecMul cmvmul 18488

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-8 1760  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432  ax-rep 4514  ax-sep 4524  ax-nul 4532  ax-pow 4581  ax-pr 4642  ax-un 6485  ax-inf2 7962  ax-cnex 9453  ax-resscn 9454  ax-1cn 9455  ax-icn 9456  ax-addcl 9457  ax-addrcl 9458  ax-mulcl 9459  ax-mulrcl 9460  ax-mulcom 9461  ax-addass 9462  ax-mulass 9463  ax-distr 9464  ax-i2m1 9465  ax-1ne0 9466  ax-1rid 9467  ax-rnegex 9468  ax-rrecex 9469  ax-cnre 9470  ax-pre-lttri 9471  ax-pre-lttrn 9472  ax-pre-ltadd 9473  ax-pre-mulgt0 9474

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1373  df-fal 1376  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2266  df-mo 2267  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2650  df-nel 2651  df-ral 2804  df-rex 2805  df-reu 2806  df-rmo 2807  df-rab 2808  df-v 3080  df-sbc 3295  df-csb 3399  df-dif 3442  df-un 3444  df-in 3446  df-ss 3453  df-pss 3455  df-nul 3749  df-if 3903  df-pw 3973  df-sn 3989  df-pr 3991  df-tp 3993  df-op 3995  df-ot 3997  df-uni 4203  df-int 4240  df-iun 4284  df-iin 4285  df-br 4404  df-opab 4462  df-mpt 4463  df-tr 4497  df-eprel 4743  df-id 4747  df-po 4752  df-so 4753  df-fr 4790  df-se 4791  df-we 4792  df-ord 4833  df-on 4834  df-lim 4835  df-suc 4836  df-xp 4957  df-rel 4958  df-cnv 4959  df-co 4960  df-dm 4961  df-rn 4962  df-res 4963  df-ima 4964  df-iota 5492  df-fun 5531  df-fn 5532  df-f 5533  df-f1 5534  df-fo 5535  df-f1o 5536  df-fv 5537  df-isom 5538  df-riota 6164  df-ov 6206  df-oprab 6207  df-mpt2 6208  df-of 6433  df-om 6590  df-1st 6690  df-2nd 6691  df-supp 6804  df-recs 6945  df-rdg 6979  df-1o 7033  df-oadd 7037  df-er 7214  df-map 7329  df-ixp 7377  df-en 7424  df-dom 7425  df-sdom 7426  df-fin 7427  df-fsupp 7735  df-sup 7806  df-oi 7839  df-card 8224  df-pnf 9535  df-mnf 9536  df-xr 9537  df-ltxr 9538  df-le 9539  df-sub 9712  df-neg 9713  df-nn 10438  df-2 10495  df-3 10496  df-4 10497  df-5 10498  df-6 10499  df-7 10500  df-8 10501  df-9 10502  df-10 10503  df-n0 10695  df-z 10762  df-dec 10871  df-uz 10977  df-fz 11559  df-fzo 11670  df-seq 11928  df-hash 12225  df-struct 14298  df-ndx 14299  df-slot 14300  df-base 14301  df-sets 14302  df-ress 14303  df-plusg 14374  df-mulr 14375  df-sca 14377  df-vsca 14378  df-ip 14379  df-tset 14380  df-ple 14381  df-ds 14383  df-hom 14385  df-cco 14386  df-0g 14503  df-gsum 14504  df-prds 14509  df-pws 14511  df-mre 14647  df-mrc 14648  df-acs 14650  df-mnd 15538  df-mhm 15587  df-submnd 15588  df-grp 15668  df-minusg 15669  df-sbg 15670  df-mulg 15671  df-subg 15801  df-ghm 15868  df-cntz 15958  df-cmn 16404  df-abl 16405  df-mgp 16724  df-ur 16736  df-rng 16780  df-subrg 16996  df-lmod 17083  df-lss 17147  df-sra 17386  df-rgmod 17387  df-dsmm 18292  df-frlm 18307  df-mamu 18416  df-mat 18417  df-mvmul 18489

This theorem is referenced by:  slesolinv  18628  slesolinvbi  18629