Theorem lfl1dim 29604

Description: Equivalent expressions for a 1-dim subspace (ray) of functionals. (Contributed by NM, 24-Oct-2014.)

Hypotheses

Ref	Expression
lfl1dim.v	|- V = ( Base ` W )
lfl1dim.d	|- D = (Scalar ` W )
lfl1dim.f	|- F = (LFnl ` W )
lfl1dim.l	|- L = (LKer ` W )
lfl1dim.k	|- K = ( Base ` D )
lfl1dim.t	|- .x. = ( .r ` D )
lfl1dim.w	|- ( ph -> W e. LVec )
lfl1dim.g	|- ( ph -> G e. F )

Assertion

Ref	Expression
lfl1dim	|- ( ph -> { g e. F | ( L ` G ) C_ ( L ` g ) } = { g | E. k e. K g = ( G o F .x. ( V X. { k } ) ) } )

Distinct variable groups:   D, k   k, F   k, G   k, K   k, L   k, V   k, W   g, k, ph   .x. , k

Allowed substitution hints:   D( g)   .x. ( g)   F( g)   G( g)   K( g)   L( g)   V( g)   W( g)

Proof of Theorem lfl1dim

Step	Hyp	Ref	Expression
1		df-rab 2675	. 2 |- { g e. F | ( L ` G ) C_ ( L ` g ) } = { g | ( g e. F /\ ( L ` G ) C_ ( L ` g ) ) }
2		lfl1dim.w	. . . . . . . . . . . 12 |- ( ph -> W e. LVec )
3		lveclmod 16133	. . . . . . . . . . . 12 |- ( W e. LVec -> W e. LMod )
4	2, 3	syl 16	. . . . . . . . . . 11 |- ( ph -> W e. LMod )
5		lfl1dim.d	. . . . . . . . . . . 12 |- D = (Scalar ` W )
6		lfl1dim.k	. . . . . . . . . . . 12 |- K = ( Base ` D )
7		eqid 2404	. . . . . . . . . . . 12 |- ( 0g ` D ) = ( 0g ` D )
8	5, 6, 7	lmod0cl 15931	. . . . . . . . . . 11 |- ( W e. LMod -> ( 0g ` D ) e. K )
9	4, 8	syl 16	. . . . . . . . . 10 |- ( ph -> ( 0g ` D ) e. K )
10	9	ad2antrr 707	. . . . . . . . 9 |- ( ( ( ph /\ g e. F ) /\ g = ( V X. { ( 0g ` D ) } ) ) -> ( 0g ` D ) e. K )
11		simpr 448	. . . . . . . . . 10 |- ( ( ( ph /\ g e. F ) /\ g = ( V X. { ( 0g ` D ) } ) ) -> g = ( V X. { ( 0g ` D ) } ) )
12		lfl1dim.v	. . . . . . . . . . 11 |- V = ( Base ` W )
13		lfl1dim.f	. . . . . . . . . . 11 |- F = (LFnl ` W )
14		lfl1dim.t	. . . . . . . . . . 11 |- .x. = ( .r ` D )
15	4	ad2antrr 707	. . . . . . . . . . 11 |- ( ( ( ph /\ g e. F ) /\ g = ( V X. { ( 0g ` D ) } ) ) -> W e. LMod )
16		lfl1dim.g	. . . . . . . . . . . 12 |- ( ph -> G e. F )
17	16	ad2antrr 707	. . . . . . . . . . 11 |- ( ( ( ph /\ g e. F ) /\ g = ( V X. { ( 0g ` D ) } ) ) -> G e. F )
18	12, 5, 13, 6, 14, 7, 15, 17	lfl0sc 29565	. . . . . . . . . 10 |- ( ( ( ph /\ g e. F ) /\ g = ( V X. { ( 0g ` D ) } ) ) -> ( G o F .x. ( V X. { ( 0g ` D ) } ) ) = ( V X. { ( 0g ` D ) } ) )
19	11, 18	eqtr4d 2439	. . . . . . . . 9 |- ( ( ( ph /\ g e. F ) /\ g = ( V X. { ( 0g ` D ) } ) ) -> g = ( G o F .x. ( V X. { ( 0g ` D ) } ) ) )
20		sneq 3785	. . . . . . . . . . . . 13 |- ( k = ( 0g ` D ) -> { k } = { ( 0g ` D ) } )
21	20	xpeq2d 4861	. . . . . . . . . . . 12 |- ( k = ( 0g ` D ) -> ( V X. { k } ) = ( V X. { ( 0g ` D ) } ) )
22	21	oveq2d 6056	. . . . . . . . . . 11 |- ( k = ( 0g ` D ) -> ( G o F .x. ( V X. { k } ) ) = ( G o F .x. ( V X. { ( 0g ` D ) } ) ) )
23	22	eqeq2d 2415	. . . . . . . . . 10 |- ( k = ( 0g ` D ) -> ( g = ( G o F .x. ( V X. { k } ) ) <-> g = ( G o F .x. ( V X. { ( 0g ` D ) } ) ) ) )
24	23	rspcev 3012	. . . . . . . . 9 |- ( ( ( 0g ` D ) e. K /\ g = ( G o F .x. ( V X. { ( 0g ` D ) } ) ) ) -> E. k e. K g = ( G o F .x. ( V X. { k } ) ) )
25	10, 19, 24	syl2anc 643	. . . . . . . 8 |- ( ( ( ph /\ g e. F ) /\ g = ( V X. { ( 0g ` D ) } ) ) -> E. k e. K g = ( G o F .x. ( V X. { k } ) ) )
26	25	a1d 23	. . . . . . 7 |- ( ( ( ph /\ g e. F ) /\ g = ( V X. { ( 0g ` D ) } ) ) -> ( ( L ` G ) C_ ( L ` g ) -> E. k e. K g = ( G o F .x. ( V X. { k } ) ) ) )
27	9	ad3antrrr 711	. . . . . . . . 9 |- ( ( ( ( ph /\ g e. F ) /\ G = ( V X. { ( 0g ` D ) } ) ) /\ ( L ` G ) C_ ( L ` g ) ) -> ( 0g ` D ) e. K )
28		lfl1dim.l	. . . . . . . . . . . . 13 |- L = (LKer ` W )
29	4	ad3antrrr 711	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ g e. F ) /\ G = ( V X. { ( 0g ` D ) } ) ) /\ ( L ` G ) C_ ( L ` g ) ) -> W e. LMod )
30		simpllr 736	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ g e. F ) /\ G = ( V X. { ( 0g ` D ) } ) ) /\ ( L ` G ) C_ ( L ` g ) ) -> g e. F )
31	12, 13, 28, 29, 30	lkrssv 29579	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ g e. F ) /\ G = ( V X. { ( 0g ` D ) } ) ) /\ ( L ` G ) C_ ( L ` g ) ) -> ( L ` g ) C_ V )
32	4	adantr 452	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ g e. F ) -> W e. LMod )
33	16	adantr 452	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ g e. F ) -> G e. F )
34	5, 7, 12, 13, 28	lkr0f 29577	. . . . . . . . . . . . . . . 16 |- ( ( W e. LMod /\ G e. F ) -> ( ( L ` G ) = V <-> G = ( V X. { ( 0g ` D ) } ) ) )
35	32, 33, 34	syl2anc 643	. . . . . . . . . . . . . . 15 |- ( ( ph /\ g e. F ) -> ( ( L ` G ) = V <-> G = ( V X. { ( 0g ` D ) } ) ) )
36	35	biimpar 472	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ g e. F ) /\ G = ( V X. { ( 0g ` D ) } ) ) -> ( L ` G ) = V )
37	36	sseq1d 3335	. . . . . . . . . . . . 13 |- ( ( ( ph /\ g e. F ) /\ G = ( V X. { ( 0g ` D ) } ) ) -> ( ( L ` G ) C_ ( L ` g ) <-> V C_ ( L ` g ) ) )
38	37	biimpa 471	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ g e. F ) /\ G = ( V X. { ( 0g ` D ) } ) ) /\ ( L ` G ) C_ ( L ` g ) ) -> V C_ ( L ` g ) )
39	31, 38	eqssd 3325	. . . . . . . . . . 11 |- ( ( ( ( ph /\ g e. F ) /\ G = ( V X. { ( 0g ` D ) } ) ) /\ ( L ` G ) C_ ( L ` g ) ) -> ( L ` g ) = V )
40	5, 7, 12, 13, 28	lkr0f 29577	. . . . . . . . . . . 12 |- ( ( W e. LMod /\ g e. F ) -> ( ( L ` g ) = V <-> g = ( V X. { ( 0g ` D ) } ) ) )
41	29, 30, 40	syl2anc 643	. . . . . . . . . . 11 |- ( ( ( ( ph /\ g e. F ) /\ G = ( V X. { ( 0g ` D ) } ) ) /\ ( L ` G ) C_ ( L ` g ) ) -> ( ( L ` g ) = V <-> g = ( V X. { ( 0g ` D ) } ) ) )
42	39, 41	mpbid 202	. . . . . . . . . 10 |- ( ( ( ( ph /\ g e. F ) /\ G = ( V X. { ( 0g ` D ) } ) ) /\ ( L ` G ) C_ ( L ` g ) ) -> g = ( V X. { ( 0g ` D ) } ) )
43	16	ad3antrrr 711	. . . . . . . . . . 11 |- ( ( ( ( ph /\ g e. F ) /\ G = ( V X. { ( 0g ` D ) } ) ) /\ ( L ` G ) C_ ( L ` g ) ) -> G e. F )
44	12, 5, 13, 6, 14, 7, 29, 43	lfl0sc 29565	. . . . . . . . . 10 |- ( ( ( ( ph /\ g e. F ) /\ G = ( V X. { ( 0g ` D ) } ) ) /\ ( L ` G ) C_ ( L ` g ) ) -> ( G o F .x. ( V X. { ( 0g ` D ) } ) ) = ( V X. { ( 0g ` D ) } ) )
45	42, 44	eqtr4d 2439	. . . . . . . . 9 |- ( ( ( ( ph /\ g e. F ) /\ G = ( V X. { ( 0g ` D ) } ) ) /\ ( L ` G ) C_ ( L ` g ) ) -> g = ( G o F .x. ( V X. { ( 0g ` D ) } ) ) )
46	27, 45, 24	syl2anc 643	. . . . . . . 8 |- ( ( ( ( ph /\ g e. F ) /\ G = ( V X. { ( 0g ` D ) } ) ) /\ ( L ` G ) C_ ( L ` g ) ) -> E. k e. K g = ( G o F .x. ( V X. { k } ) ) )
47	46	ex 424	. . . . . . 7 |- ( ( ( ph /\ g e. F ) /\ G = ( V X. { ( 0g ` D ) } ) ) -> ( ( L ` G ) C_ ( L ` g ) -> E. k e. K g = ( G o F .x. ( V X. { k } ) ) ) )
48		eqid 2404	. . . . . . . . 9 |- (LSHyp ` W ) = (LSHyp ` W )
49	2	ad2antrr 707	. . . . . . . . 9 |- ( ( ( ph /\ g e. F ) /\ ( g =/= ( V X. { ( 0g ` D ) } ) /\ G =/= ( V X. { ( 0g ` D ) } ) ) ) -> W e. LVec )
50	16	ad2antrr 707	. . . . . . . . . 10 |- ( ( ( ph /\ g e. F ) /\ ( g =/= ( V X. { ( 0g ` D ) } ) /\ G =/= ( V X. { ( 0g ` D ) } ) ) ) -> G e. F )
51		simprr 734	. . . . . . . . . 10 |- ( ( ( ph /\ g e. F ) /\ ( g =/= ( V X. { ( 0g ` D ) } ) /\ G =/= ( V X. { ( 0g ` D ) } ) ) ) -> G =/= ( V X. { ( 0g ` D ) } ) )
52	12, 5, 7, 48, 13, 28	lkrshp 29588	. . . . . . . . . 10 |- ( ( W e. LVec /\ G e. F /\ G =/= ( V X. { ( 0g ` D ) } ) ) -> ( L ` G ) e. (LSHyp ` W ) )
53	49, 50, 51, 52	syl3anc 1184	. . . . . . . . 9 |- ( ( ( ph /\ g e. F ) /\ ( g =/= ( V X. { ( 0g ` D ) } ) /\ G =/= ( V X. { ( 0g ` D ) } ) ) ) -> ( L ` G ) e. (LSHyp ` W ) )
54		simplr 732	. . . . . . . . . 10 |- ( ( ( ph /\ g e. F ) /\ ( g =/= ( V X. { ( 0g ` D ) } ) /\ G =/= ( V X. { ( 0g ` D ) } ) ) ) -> g e. F )
55		simprl 733	. . . . . . . . . 10 |- ( ( ( ph /\ g e. F ) /\ ( g =/= ( V X. { ( 0g ` D ) } ) /\ G =/= ( V X. { ( 0g ` D ) } ) ) ) -> g =/= ( V X. { ( 0g ` D ) } ) )
56	12, 5, 7, 48, 13, 28	lkrshp 29588	. . . . . . . . . 10 |- ( ( W e. LVec /\ g e. F /\ g =/= ( V X. { ( 0g ` D ) } ) ) -> ( L ` g ) e. (LSHyp ` W ) )
57	49, 54, 55, 56	syl3anc 1184	. . . . . . . . 9 |- ( ( ( ph /\ g e. F ) /\ ( g =/= ( V X. { ( 0g ` D ) } ) /\ G =/= ( V X. { ( 0g ` D ) } ) ) ) -> ( L ` g ) e. (LSHyp ` W ) )
58	48, 49, 53, 57	lshpcmp 29471	. . . . . . . 8 |- ( ( ( ph /\ g e. F ) /\ ( g =/= ( V X. { ( 0g ` D ) } ) /\ G =/= ( V X. { ( 0g ` D ) } ) ) ) -> ( ( L ` G ) C_ ( L ` g ) <-> ( L ` G ) = ( L ` g ) ) )
59	2	ad3antrrr 711	. . . . . . . . . 10 |- ( ( ( ( ph /\ g e. F ) /\ ( g =/= ( V X. { ( 0g ` D ) } ) /\ G =/= ( V X. { ( 0g ` D ) } ) ) ) /\ ( L ` G ) = ( L ` g ) ) -> W e. LVec )
60	16	ad3antrrr 711	. . . . . . . . . 10 |- ( ( ( ( ph /\ g e. F ) /\ ( g =/= ( V X. { ( 0g ` D ) } ) /\ G =/= ( V X. { ( 0g ` D ) } ) ) ) /\ ( L ` G ) = ( L ` g ) ) -> G e. F )
61		simpllr 736	. . . . . . . . . 10 |- ( ( ( ( ph /\ g e. F ) /\ ( g =/= ( V X. { ( 0g ` D ) } ) /\ G =/= ( V X. { ( 0g ` D ) } ) ) ) /\ ( L ` G ) = ( L ` g ) ) -> g e. F )
62		simpr 448	. . . . . . . . . 10 |- ( ( ( ( ph /\ g e. F ) /\ ( g =/= ( V X. { ( 0g ` D ) } ) /\ G =/= ( V X. { ( 0g ` D ) } ) ) ) /\ ( L ` G ) = ( L ` g ) ) -> ( L ` G ) = ( L ` g ) )
63	5, 6, 14, 12, 13, 28	eqlkr2 29583	. . . . . . . . . 10 |- ( ( W e. LVec /\ ( G e. F /\ g e. F ) /\ ( L ` G ) = ( L ` g ) ) -> E. k e. K g = ( G o F .x. ( V X. { k } ) ) )
64	59, 60, 61, 62, 63	syl121anc 1189	. . . . . . . . 9 |- ( ( ( ( ph /\ g e. F ) /\ ( g =/= ( V X. { ( 0g ` D ) } ) /\ G =/= ( V X. { ( 0g ` D ) } ) ) ) /\ ( L ` G ) = ( L ` g ) ) -> E. k e. K g = ( G o F .x. ( V X. { k } ) ) )
65	64	ex 424	. . . . . . . 8 |- ( ( ( ph /\ g e. F ) /\ ( g =/= ( V X. { ( 0g ` D ) } ) /\ G =/= ( V X. { ( 0g ` D ) } ) ) ) -> ( ( L ` G ) = ( L ` g ) -> E. k e. K g = ( G o F .x. ( V X. { k } ) ) ) )
66	58, 65	sylbid 207	. . . . . . 7 |- ( ( ( ph /\ g e. F ) /\ ( g =/= ( V X. { ( 0g ` D ) } ) /\ G =/= ( V X. { ( 0g ` D ) } ) ) ) -> ( ( L ` G ) C_ ( L ` g ) -> E. k e. K g = ( G o F .x. ( V X. { k } ) ) ) )
67	26, 47, 66	pm2.61da2ne 2646	. . . . . 6 |- ( ( ph /\ g e. F ) -> ( ( L ` G ) C_ ( L ` g ) -> E. k e. K g = ( G o F .x. ( V X. { k } ) ) ) )
68	2	ad2antrr 707	. . . . . . . . . 10 |- ( ( ( ph /\ g e. F ) /\ k e. K ) -> W e. LVec )
69	16	ad2antrr 707	. . . . . . . . . 10 |- ( ( ( ph /\ g e. F ) /\ k e. K ) -> G e. F )
70		simpr 448	. . . . . . . . . 10 |- ( ( ( ph /\ g e. F ) /\ k e. K ) -> k e. K )
71	12, 5, 6, 14, 13, 28, 68, 69, 70	lkrscss 29581	. . . . . . . . 9 |- ( ( ( ph /\ g e. F ) /\ k e. K ) -> ( L ` G ) C_ ( L ` ( G o F .x. ( V X. { k } ) ) ) )
72	71	ex 424	. . . . . . . 8 |- ( ( ph /\ g e. F ) -> ( k e. K -> ( L ` G ) C_ ( L ` ( G o F .x. ( V X. { k } ) ) ) ) )
73		fveq2 5687	. . . . . . . . . 10 |- ( g = ( G o F .x. ( V X. { k } ) ) -> ( L ` g ) = ( L ` ( G o F .x. ( V X. { k } ) ) ) )
74	73	sseq2d 3336	. . . . . . . . 9 |- ( g = ( G o F .x. ( V X. { k } ) ) -> ( ( L ` G ) C_ ( L ` g ) <-> ( L ` G ) C_ ( L ` ( G o F .x. ( V X. { k } ) ) ) ) )
75	74	biimprcd 217	. . . . . . . 8 |- ( ( L ` G ) C_ ( L ` ( G o F .x. ( V X. { k } ) ) ) -> ( g = ( G o F .x. ( V X. { k } ) ) -> ( L ` G ) C_ ( L ` g ) ) )
76	72, 75	syl6 31	. . . . . . 7 |- ( ( ph /\ g e. F ) -> ( k e. K -> ( g = ( G o F .x. ( V X. { k } ) ) -> ( L ` G ) C_ ( L ` g ) ) ) )
77	76	rexlimdv 2789	. . . . . 6 |- ( ( ph /\ g e. F ) -> ( E. k e. K g = ( G o F .x. ( V X. { k } ) ) -> ( L ` G ) C_ ( L ` g ) ) )
78	67, 77	impbid 184	. . . . 5 |- ( ( ph /\ g e. F ) -> ( ( L ` G ) C_ ( L ` g ) <-> E. k e. K g = ( G o F .x. ( V X. { k } ) ) ) )
79	78	pm5.32da 623	. . . 4 |- ( ph -> ( ( g e. F /\ ( L ` G ) C_ ( L ` g ) ) <-> ( g e. F /\ E. k e. K g = ( G o F .x. ( V X. { k } ) ) ) ) )
80	4	adantr 452	. . . . . . . . 9 |- ( ( ph /\ k e. K ) -> W e. LMod )
81	16	adantr 452	. . . . . . . . 9 |- ( ( ph /\ k e. K ) -> G e. F )
82		simpr 448	. . . . . . . . 9 |- ( ( ph /\ k e. K ) -> k e. K )
83	12, 5, 6, 14, 13, 80, 81, 82	lflvscl 29560	. . . . . . . 8 |- ( ( ph /\ k e. K ) -> ( G o F .x. ( V X. { k } ) ) e. F )
84		eleq1a 2473	. . . . . . . 8 |- ( ( G o F .x. ( V X. { k } ) ) e. F -> ( g = ( G o F .x. ( V X. { k } ) ) -> g e. F ) )
85	83, 84	syl 16	. . . . . . 7 |- ( ( ph /\ k e. K ) -> ( g = ( G o F .x. ( V X. { k } ) ) -> g e. F ) )
86	85	pm4.71rd 617	. . . . . 6 |- ( ( ph /\ k e. K ) -> ( g = ( G o F .x. ( V X. { k } ) ) <-> ( g e. F /\ g = ( G o F .x. ( V X. { k } ) ) ) ) )
87	86	rexbidva 2683	. . . . 5 |- ( ph -> ( E. k e. K g = ( G o F .x. ( V X. { k } ) ) <-> E. k e. K ( g e. F /\ g = ( G o F .x. ( V X. { k } ) ) ) ) )
88		r19.42v 2822	. . . . 5 |- ( E. k e. K ( g e. F /\ g = ( G o F .x. ( V X. { k } ) ) ) <-> ( g e. F /\ E. k e. K g = ( G o F .x. ( V X. { k } ) ) ) )
89	87, 88	syl6rbb 254	. . . 4 |- ( ph -> ( ( g e. F /\ E. k e. K g = ( G o F .x. ( V X. { k } ) ) ) <-> E. k e. K g = ( G o F .x. ( V X. { k } ) ) ) )
90	79, 89	bitrd 245	. . 3 |- ( ph -> ( ( g e. F /\ ( L ` G ) C_ ( L ` g ) ) <-> E. k e. K g = ( G o F .x. ( V X. { k } ) ) ) )
91	90	abbidv 2518	. 2 |- ( ph -> { g | ( g e. F /\ ( L ` G ) C_ ( L ` g ) ) } = { g | E. k e. K g = ( G o F .x. ( V X. { k } ) ) } )
92	1, 91	syl5eq 2448	1 |- ( ph -> { g e. F | ( L ` G ) C_ ( L ` g ) } = { g | E. k e. K g = ( G o F .x. ( V X. { k } ) ) } )

Syntax hints:   -> wi 4   <-> wb 177   /\ wa 359   = wceq 1649   e. wcel 1721   {cab 2390   =/= wne 2567   E.wrex 2667   {crab 2670   C_ wss 3280   {csn 3774   X. cxp 4835   ` cfv 5413  (class class class)co 6040   o Fcof 6262   Basecbs 13424   .rcmulr 13485  Scalarcsca 13487   0gc0g 13678   LModclmod 15905   LVecclvec 16129  LSHypclsh 29458  LFnlclfn 29540  LKerclk 29568

This theorem is referenced by:  ldual1dim  29649

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-rep 4280  ax-sep 4290  ax-nul 4298  ax-pow 4337  ax-pr 4363  ax-un 4660  ax-cnex 9002  ax-resscn 9003  ax-1cn 9004  ax-icn 9005  ax-addcl 9006  ax-addrcl 9007  ax-mulcl 9008  ax-mulrcl 9009  ax-mulcom 9010  ax-addass 9011  ax-mulass 9012  ax-distr 9013  ax-i2m1 9014  ax-1ne0 9015  ax-1rid 9016  ax-rnegex 9017  ax-rrecex 9018  ax-cnre 9019  ax-pre-lttri 9020  ax-pre-lttrn 9021  ax-pre-ltadd 9022  ax-pre-mulgt0 9023

This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2258  df-mo 2259  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ne 2569  df-nel 2570  df-ral 2671  df-rex 2672  df-reu 2673  df-rmo 2674  df-rab 2675  df-v 2918  df-sbc 3122  df-csb 3212  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-pss 3296  df-nul 3589  df-if 3700  df-pw 3761  df-sn 3780  df-pr 3781  df-tp 3782  df-op 3783  df-uni 3976  df-int 4011  df-iun 4055  df-br 4173  df-opab 4227  df-mpt 4228  df-tr 4263  df-eprel 4454  df-id 4458  df-po 4463  df-so 4464  df-fr 4501  df-we 4503  df-ord 4544  df-on 4545  df-lim 4546  df-suc 4547  df-om 4805  df-xp 4843  df-rel 4844  df-cnv 4845  df-co 4846  df-dm 4847  df-rn 4848  df-res 4849  df-ima 4850  df-iota 5377  df-fun 5415  df-fn 5416  df-f 5417  df-f1 5418  df-fo 5419  df-f1o 5420  df-fv 5421  df-ov 6043  df-oprab 6044  df-mpt2 6045  df-of 6264  df-1st 6308  df-2nd 6309  df-tpos 6438  df-riota 6508  df-recs 6592  df-rdg 6627  df-er 6864  df-map 6979  df-en 7069  df-dom 7070  df-sdom 7071  df-pnf 9078  df-mnf 9079  df-xr 9080  df-ltxr 9081  df-le 9082  df-sub 9249  df-neg 9250  df-nn 9957  df-2 10014  df-3 10015  df-ndx 13427  df-slot 13428  df-base 13429  df-sets 13430  df-ress 13431  df-plusg 13497  df-mulr 13498  df-0g 13682  df-mnd 14645  df-submnd 14694  df-grp 14767  df-minusg 14768  df-sbg 14769  df-subg 14896  df-cntz 15071  df-lsm 15225  df-cmn 15369  df-abl 15370  df-mgp 15604  df-rng 15618  df-ur 15620  df-oppr 15683  df-dvdsr 15701  df-unit 15702  df-invr 15732  df-drng 15792  df-lmod 15907  df-lss 15964  df-lsp 16003  df-lvec 16130  df-lshyp 29460  df-lfl 29541  df-lkr 29569