Theorem f1lindf 19373

Description: Rearranging and deleting elements from an independent family gives an independent family. (Contributed by Stefan O'Rear, 24-Feb-2015.)

Assertion

Ref	Expression
f1lindf	|- ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) -> ( F o. G ) LIndF W )

Proof of Theorem f1lindf

Dummy variables k x are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		eqid 2450	. . . . . . 7 |- ( Base ` W ) = ( Base ` W )
2	1	lindff 19366	. . . . . 6 |- ( ( F LIndF W /\ W e. LMod ) -> F : dom F --> ( Base ` W ) )
3	2	ancoms 455	. . . . 5 |- ( ( W e. LMod /\ F LIndF W ) -> F : dom F --> ( Base ` W ) )
4	3	3adant3 1027	. . . 4 |- ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) -> F : dom F --> ( Base ` W ) )
5		f1f 5777	. . . . 5 |- ( G : K -1-1-> dom F -> G : K --> dom F )
6	5	3ad2ant3 1030	. . . 4 |- ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) -> G : K --> dom F )
7		fco 5737	. . . 4 |- ( ( F : dom F --> ( Base ` W ) /\ G : K --> dom F ) -> ( F o. G ) : K --> ( Base ` W ) )
8	4, 6, 7	syl2anc 666	. . 3 |- ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) -> ( F o. G ) : K --> ( Base ` W ) )
9		ffdm 5741	. . . 4 |- ( ( F o. G ) : K --> ( Base ` W ) -> ( ( F o. G ) : dom ( F o. G ) --> ( Base ` W ) /\ dom ( F o. G ) C_ K ) )
10	9	simpld 461	. . 3 |- ( ( F o. G ) : K --> ( Base ` W ) -> ( F o. G ) : dom ( F o. G ) --> ( Base ` W ) )
11	8, 10	syl 17	. 2 |- ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) -> ( F o. G ) : dom ( F o. G ) --> ( Base ` W ) )
12		simpl2 1011	. . . . 5 |- ( ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) /\ ( x e. dom ( F o. G ) /\ k e. ( ( Base ` (Scalar ` W ) ) \ { ( 0g ` (Scalar ` W ) ) } ) ) ) -> F LIndF W )
13	6	adantr 467	. . . . . . 7 |- ( ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) /\ x e. dom ( F o. G ) ) -> G : K --> dom F )
14		fdm 5731	. . . . . . . . . 10 |- ( ( F o. G ) : K --> ( Base ` W ) -> dom ( F o. G ) = K )
15	8, 14	syl 17	. . . . . . . . 9 |- ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) -> dom ( F o. G ) = K )
16	15	eleq2d 2513	. . . . . . . 8 |- ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) -> ( x e. dom ( F o. G ) <-> x e. K ) )
17	16	biimpa 487	. . . . . . 7 |- ( ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) /\ x e. dom ( F o. G ) ) -> x e. K )
18	13, 17	ffvelrnd 6021	. . . . . 6 |- ( ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) /\ x e. dom ( F o. G ) ) -> ( G ` x ) e. dom F )
19	18	adantrr 722	. . . . 5 |- ( ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) /\ ( x e. dom ( F o. G ) /\ k e. ( ( Base ` (Scalar ` W ) ) \ { ( 0g ` (Scalar ` W ) ) } ) ) ) -> ( G ` x ) e. dom F )
20		eldifi 3554	. . . . . 6 |- ( k e. ( ( Base ` (Scalar ` W ) ) \ { ( 0g ` (Scalar ` W ) ) } ) -> k e. ( Base ` (Scalar ` W ) ) )
21	20	ad2antll 734	. . . . 5 |- ( ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) /\ ( x e. dom ( F o. G ) /\ k e. ( ( Base ` (Scalar ` W ) ) \ { ( 0g ` (Scalar ` W ) ) } ) ) ) -> k e. ( Base ` (Scalar ` W ) ) )
22		eldifsni 4097	. . . . . 6 |- ( k e. ( ( Base ` (Scalar ` W ) ) \ { ( 0g ` (Scalar ` W ) ) } ) -> k =/= ( 0g ` (Scalar ` W ) ) )
23	22	ad2antll 734	. . . . 5 |- ( ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) /\ ( x e. dom ( F o. G ) /\ k e. ( ( Base ` (Scalar ` W ) ) \ { ( 0g ` (Scalar ` W ) ) } ) ) ) -> k =/= ( 0g ` (Scalar ` W ) ) )
24		eqid 2450	. . . . . 6 |- ( .s ` W ) = ( .s ` W )
25		eqid 2450	. . . . . 6 |- ( LSpan ` W ) = ( LSpan ` W )
26		eqid 2450	. . . . . 6 |- (Scalar ` W ) = (Scalar ` W )
27		eqid 2450	. . . . . 6 |- ( 0g ` (Scalar ` W ) ) = ( 0g ` (Scalar ` W ) )
28		eqid 2450	. . . . . 6 |- ( Base ` (Scalar ` W ) ) = ( Base ` (Scalar ` W ) )
29	24, 25, 26, 27, 28	lindfind 19367	. . . . 5 |- ( ( ( F LIndF W /\ ( G ` x ) e. dom F ) /\ ( k e. ( Base ` (Scalar ` W ) ) /\ k =/= ( 0g ` (Scalar ` W ) ) ) ) -> -. ( k ( .s ` W ) ( F ` ( G ` x ) ) ) e. ( ( LSpan ` W ) ` ( F " ( dom F \ { ( G ` x ) } ) ) ) )
30	12, 19, 21, 23, 29	syl22anc 1268	. . . 4 |- ( ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) /\ ( x e. dom ( F o. G ) /\ k e. ( ( Base ` (Scalar ` W ) ) \ { ( 0g ` (Scalar ` W ) ) } ) ) ) -> -. ( k ( .s ` W ) ( F ` ( G ` x ) ) ) e. ( ( LSpan ` W ) ` ( F " ( dom F \ { ( G ` x ) } ) ) ) )
31		f1fn 5778	. . . . . . . . . . 11 |- ( G : K -1-1-> dom F -> G Fn K )
32	31	3ad2ant3 1030	. . . . . . . . . 10 |- ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) -> G Fn K )
33	32	adantr 467	. . . . . . . . 9 |- ( ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) /\ x e. dom ( F o. G ) ) -> G Fn K )
34		fvco2 5938	. . . . . . . . 9 |- ( ( G Fn K /\ x e. K ) -> ( ( F o. G ) ` x ) = ( F ` ( G ` x ) ) )
35	33, 17, 34	syl2anc 666	. . . . . . . 8 |- ( ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) /\ x e. dom ( F o. G ) ) -> ( ( F o. G ) ` x ) = ( F ` ( G ` x ) ) )
36	35	oveq2d 6304	. . . . . . 7 |- ( ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) /\ x e. dom ( F o. G ) ) -> ( k ( .s ` W ) ( ( F o. G ) ` x ) ) = ( k ( .s ` W ) ( F ` ( G ` x ) ) ) )
37	36	eleq1d 2512	. . . . . 6 |- ( ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) /\ x e. dom ( F o. G ) ) -> ( ( k ( .s ` W ) ( ( F o. G ) ` x ) ) e. ( ( LSpan ` W ) ` ( ( F o. G ) " ( dom ( F o. G ) \ { x } ) ) ) <-> ( k ( .s ` W ) ( F ` ( G ` x ) ) ) e. ( ( LSpan ` W ) ` ( ( F o. G ) " ( dom ( F o. G ) \ { x } ) ) ) ) )
38		simpl1 1010	. . . . . . . . 9 |- ( ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) /\ x e. K ) -> W e. LMod )
39		imassrn 5178	. . . . . . . . . . 11 |- ( F " ( dom F \ { ( G ` x ) } ) ) C_ ran F
40		frn 5733	. . . . . . . . . . . 12 |- ( F : dom F --> ( Base ` W ) -> ran F C_ ( Base ` W ) )
41	4, 40	syl 17	. . . . . . . . . . 11 |- ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) -> ran F C_ ( Base ` W ) )
42	39, 41	syl5ss 3442	. . . . . . . . . 10 |- ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) -> ( F " ( dom F \ { ( G ` x ) } ) ) C_ ( Base ` W ) )
43	42	adantr 467	. . . . . . . . 9 |- ( ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) /\ x e. K ) -> ( F " ( dom F \ { ( G ` x ) } ) ) C_ ( Base ` W ) )
44		imaco 5339	. . . . . . . . . 10 |- ( ( F o. G ) " ( dom ( F o. G ) \ { x } ) ) = ( F " ( G " ( dom ( F o. G ) \ { x } ) ) )
45	15	difeq1d 3549	. . . . . . . . . . . . . . 15 |- ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) -> ( dom ( F o. G ) \ { x } ) = ( K \ { x } ) )
46	45	imaeq2d 5167	. . . . . . . . . . . . . 14 |- ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) -> ( G " ( dom ( F o. G ) \ { x } ) ) = ( G " ( K \ { x } ) ) )
47		df-f1 5586	. . . . . . . . . . . . . . . . 17 |- ( G : K -1-1-> dom F <-> ( G : K --> dom F /\ Fun `' G ) )
48	47	simprbi 466	. . . . . . . . . . . . . . . 16 |- ( G : K -1-1-> dom F -> Fun `' G )
49	48	3ad2ant3 1030	. . . . . . . . . . . . . . 15 |- ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) -> Fun `' G )
50		imadif 5656	. . . . . . . . . . . . . . 15 |- ( Fun `' G -> ( G " ( K \ { x } ) ) = ( ( G " K ) \ ( G " { x } ) ) )
51	49, 50	syl 17	. . . . . . . . . . . . . 14 |- ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) -> ( G " ( K \ { x } ) ) = ( ( G " K ) \ ( G " { x } ) ) )
52	46, 51	eqtrd 2484	. . . . . . . . . . . . 13 |- ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) -> ( G " ( dom ( F o. G ) \ { x } ) ) = ( ( G " K ) \ ( G " { x } ) ) )
53	52	adantr 467	. . . . . . . . . . . 12 |- ( ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) /\ x e. K ) -> ( G " ( dom ( F o. G ) \ { x } ) ) = ( ( G " K ) \ ( G " { x } ) ) )
54		fnsnfv 5923	. . . . . . . . . . . . . . 15 |- ( ( G Fn K /\ x e. K ) -> { ( G ` x ) } = ( G " { x } ) )
55	32, 54	sylan 474	. . . . . . . . . . . . . 14 |- ( ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) /\ x e. K ) -> { ( G ` x ) } = ( G " { x } ) )
56	55	difeq2d 3550	. . . . . . . . . . . . 13 |- ( ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) /\ x e. K ) -> ( ( G " K ) \ { ( G ` x ) } ) = ( ( G " K ) \ ( G " { x } ) ) )
57		imassrn 5178	. . . . . . . . . . . . . . 15 |- ( G " K ) C_ ran G
58	6	adantr 467	. . . . . . . . . . . . . . . 16 |- ( ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) /\ x e. K ) -> G : K --> dom F )
59		frn 5733	. . . . . . . . . . . . . . . 16 |- ( G : K --> dom F -> ran G C_ dom F )
60	58, 59	syl 17	. . . . . . . . . . . . . . 15 |- ( ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) /\ x e. K ) -> ran G C_ dom F )
61	57, 60	syl5ss 3442	. . . . . . . . . . . . . 14 |- ( ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) /\ x e. K ) -> ( G " K ) C_ dom F )
62	61	ssdifd 3568	. . . . . . . . . . . . 13 |- ( ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) /\ x e. K ) -> ( ( G " K ) \ { ( G ` x ) } ) C_ ( dom F \ { ( G ` x ) } ) )
63	56, 62	eqsstr3d 3466	. . . . . . . . . . . 12 |- ( ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) /\ x e. K ) -> ( ( G " K ) \ ( G " { x } ) ) C_ ( dom F \ { ( G ` x ) } ) )
64	53, 63	eqsstrd 3465	. . . . . . . . . . 11 |- ( ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) /\ x e. K ) -> ( G " ( dom ( F o. G ) \ { x } ) ) C_ ( dom F \ { ( G ` x ) } ) )
65		imass2 5203	. . . . . . . . . . 11 |- ( ( G " ( dom ( F o. G ) \ { x } ) ) C_ ( dom F \ { ( G ` x ) } ) -> ( F " ( G " ( dom ( F o. G ) \ { x } ) ) ) C_ ( F " ( dom F \ { ( G ` x ) } ) ) )
66	64, 65	syl 17	. . . . . . . . . 10 |- ( ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) /\ x e. K ) -> ( F " ( G " ( dom ( F o. G ) \ { x } ) ) ) C_ ( F " ( dom F \ { ( G ` x ) } ) ) )
67	44, 66	syl5eqss 3475	. . . . . . . . 9 |- ( ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) /\ x e. K ) -> ( ( F o. G ) " ( dom ( F o. G ) \ { x } ) ) C_ ( F " ( dom F \ { ( G ` x ) } ) ) )
68	1, 25	lspss 18200	. . . . . . . . 9 |- ( ( W e. LMod /\ ( F " ( dom F \ { ( G ` x ) } ) ) C_ ( Base ` W ) /\ ( ( F o. G ) " ( dom ( F o. G ) \ { x } ) ) C_ ( F " ( dom F \ { ( G ` x ) } ) ) ) -> ( ( LSpan ` W ) ` ( ( F o. G ) " ( dom ( F o. G ) \ { x } ) ) ) C_ ( ( LSpan ` W ) ` ( F " ( dom F \ { ( G ` x ) } ) ) ) )
69	38, 43, 67, 68	syl3anc 1267	. . . . . . . 8 |- ( ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) /\ x e. K ) -> ( ( LSpan ` W ) ` ( ( F o. G ) " ( dom ( F o. G ) \ { x } ) ) ) C_ ( ( LSpan ` W ) ` ( F " ( dom F \ { ( G ` x ) } ) ) ) )
70	17, 69	syldan 473	. . . . . . 7 |- ( ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) /\ x e. dom ( F o. G ) ) -> ( ( LSpan ` W ) ` ( ( F o. G ) " ( dom ( F o. G ) \ { x } ) ) ) C_ ( ( LSpan ` W ) ` ( F " ( dom F \ { ( G ` x ) } ) ) ) )
71	70	sseld 3430	. . . . . 6 |- ( ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) /\ x e. dom ( F o. G ) ) -> ( ( k ( .s ` W ) ( F ` ( G ` x ) ) ) e. ( ( LSpan ` W ) ` ( ( F o. G ) " ( dom ( F o. G ) \ { x } ) ) ) -> ( k ( .s ` W ) ( F ` ( G ` x ) ) ) e. ( ( LSpan ` W ) ` ( F " ( dom F \ { ( G ` x ) } ) ) ) ) )
72	37, 71	sylbid 219	. . . . 5 |- ( ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) /\ x e. dom ( F o. G ) ) -> ( ( k ( .s ` W ) ( ( F o. G ) ` x ) ) e. ( ( LSpan ` W ) ` ( ( F o. G ) " ( dom ( F o. G ) \ { x } ) ) ) -> ( k ( .s ` W ) ( F ` ( G ` x ) ) ) e. ( ( LSpan ` W ) ` ( F " ( dom F \ { ( G ` x ) } ) ) ) ) )
73	72	adantrr 722	. . . 4 |- ( ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) /\ ( x e. dom ( F o. G ) /\ k e. ( ( Base ` (Scalar ` W ) ) \ { ( 0g ` (Scalar ` W ) ) } ) ) ) -> ( ( k ( .s ` W ) ( ( F o. G ) ` x ) ) e. ( ( LSpan ` W ) ` ( ( F o. G ) " ( dom ( F o. G ) \ { x } ) ) ) -> ( k ( .s ` W ) ( F ` ( G ` x ) ) ) e. ( ( LSpan ` W ) ` ( F " ( dom F \ { ( G ` x ) } ) ) ) ) )
74	30, 73	mtod 181	. . 3 |- ( ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) /\ ( x e. dom ( F o. G ) /\ k e. ( ( Base ` (Scalar ` W ) ) \ { ( 0g ` (Scalar ` W ) ) } ) ) ) -> -. ( k ( .s ` W ) ( ( F o. G ) ` x ) ) e. ( ( LSpan ` W ) ` ( ( F o. G ) " ( dom ( F o. G ) \ { x } ) ) ) )
75	74	ralrimivva 2808	. 2 |- ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) -> A. x e. dom ( F o. G ) A. k e. ( ( Base ` (Scalar ` W ) ) \ { ( 0g ` (Scalar ` W ) ) } ) -. ( k ( .s ` W ) ( ( F o. G ) ` x ) ) e. ( ( LSpan ` W ) ` ( ( F o. G ) " ( dom ( F o. G ) \ { x } ) ) ) )
76		simp1 1007	. . 3 |- ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) -> W e. LMod )
77		rellindf 19359	. . . . . 6 |- Rel LIndF
78	77	brrelexi 4874	. . . . 5 |- ( F LIndF W -> F e. _V )
79	78	3ad2ant2 1029	. . . 4 |- ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) -> F e. _V )
80		simp3 1009	. . . . . 6 |- ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) -> G : K -1-1-> dom F )
81		dmexg 6721	. . . . . . 7 |- ( F e. _V -> dom F e. _V )
82	79, 81	syl 17	. . . . . 6 |- ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) -> dom F e. _V )
83		f1dmex 6760	. . . . . 6 |- ( ( G : K -1-1-> dom F /\ dom F e. _V ) -> K e. _V )
84	80, 82, 83	syl2anc 666	. . . . 5 |- ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) -> K e. _V )
85		fex 6136	. . . . 5 |- ( ( G : K --> dom F /\ K e. _V ) -> G e. _V )
86	6, 84, 85	syl2anc 666	. . . 4 |- ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) -> G e. _V )
87		coexg 6741	. . . 4 |- ( ( F e. _V /\ G e. _V ) -> ( F o. G ) e. _V )
88	79, 86, 87	syl2anc 666	. . 3 |- ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) -> ( F o. G ) e. _V )
89	1, 24, 25, 26, 28, 27	islindf 19363	. . 3 |- ( ( W e. LMod /\ ( F o. G ) e. _V ) -> ( ( F o. G ) LIndF W <-> ( ( F o. G ) : dom ( F o. G ) --> ( Base ` W ) /\ A. x e. dom ( F o. G ) A. k e. ( ( Base ` (Scalar ` W ) ) \ { ( 0g ` (Scalar ` W ) ) } ) -. ( k ( .s ` W ) ( ( F o. G ) ` x ) ) e. ( ( LSpan ` W ) ` ( ( F o. G ) " ( dom ( F o. G ) \ { x } ) ) ) ) ) )
90	76, 88, 89	syl2anc 666	. 2 |- ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) -> ( ( F o. G ) LIndF W <-> ( ( F o. G ) : dom ( F o. G ) --> ( Base ` W ) /\ A. x e. dom ( F o. G ) A. k e. ( ( Base ` (Scalar ` W ) ) \ { ( 0g ` (Scalar ` W ) ) } ) -. ( k ( .s ` W ) ( ( F o. G ) ` x ) ) e. ( ( LSpan ` W ) ` ( ( F o. G ) " ( dom ( F o. G ) \ { x } ) ) ) ) ) )
91	11, 75, 90	mpbir2and 932	1 |- ( ( W e. LMod /\ F LIndF W /\ G : K -1-1-> dom F ) -> ( F o. G ) LIndF W )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 188   /\ wa 371   /\ w3a 984   = wceq 1443   e. wcel 1886   =/= wne 2621   A.wral 2736   _Vcvv 3044   \ cdif 3400   C_ wss 3403   {csn 3967   class class class wbr 4401   `'ccnv 4832   dom cdm 4833   ran crn 4834   "cima 4836   o. ccom 4837   Fun wfun 5575   Fn wfn 5576   -->wf 5577   -1-1->wf1 5578   ` cfv 5581  (class class class)co 6288   Basecbs 15114  Scalarcsca 15186   .scvsca 15187   0gc0g 15331   LModclmod 18084   LSpanclspn 18187   LIndF clindf 19355

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1668  ax-4 1681  ax-5 1757  ax-6 1804  ax-7 1850  ax-8 1888  ax-9 1895  ax-10 1914  ax-11 1919  ax-12 1932  ax-13 2090  ax-ext 2430  ax-rep 4514  ax-sep 4524  ax-nul 4533  ax-pow 4580  ax-pr 4638  ax-un 6580

This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 986  df-tru 1446  df-ex 1663  df-nf 1667  df-sb 1797  df-eu 2302  df-mo 2303  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2580  df-ne 2623  df-ral 2741  df-rex 2742  df-reu 2743  df-rmo 2744  df-rab 2745  df-v 3046  df-sbc 3267  df-csb 3363  df-dif 3406  df-un 3408  df-in 3410  df-ss 3417  df-nul 3731  df-if 3881  df-pw 3952  df-sn 3968  df-pr 3970  df-op 3974  df-uni 4198  df-int 4234  df-iun 4279  df-br 4402  df-opab 4461  df-mpt 4462  df-id 4748  df-xp 4839  df-rel 4840  df-cnv 4841  df-co 4842  df-dm 4843  df-rn 4844  df-res 4845  df-ima 4846  df-iota 5545  df-fun 5583  df-fn 5584  df-f 5585  df-f1 5586  df-fo 5587  df-f1o 5588  df-fv 5589  df-riota 6250  df-ov 6291  df-slot 15118  df-base 15119  df-0g 15333  df-mgm 16481  df-sgrp 16520  df-mnd 16530  df-grp 16666  df-lmod 18086  df-lss 18149  df-lsp 18188  df-lindf 19357

This theorem is referenced by:  lindfres  19374  f1linds  19376