Theorem cdlemk53 34909

Description: Part of proof of Lemma K of [Crawley] p. 118. Line 7, p. 120. G, I stand for g, h. X represents tau. (Contributed by NM, 26-Jul-2013.)

Hypotheses

Ref	Expression
cdlemk5.b	|- B = ( Base ` K )
cdlemk5.l	|- .<_ = ( le ` K )
cdlemk5.j	|- .\/ = ( join ` K )
cdlemk5.m	|- ./\ = ( meet ` K )
cdlemk5.a	|- A = ( Atoms ` K )
cdlemk5.h	|- H = ( LHyp ` K )
cdlemk5.t	|- T = ( ( LTrn ` K ) ` W )
cdlemk5.r	|- R = ( ( trL ` K ) ` W )
cdlemk5.z	|- Z = ( ( P .\/ ( R ` b ) ) ./\ ( ( N ` P ) .\/ ( R ` ( b o. `' F ) ) ) )
cdlemk5.y	|- Y = ( ( P .\/ ( R ` g ) ) ./\ ( Z .\/ ( R ` ( g o. `' b ) ) ) )
cdlemk5.x	|- X = ( iota_ z e. T A. b e. T ( ( b =/= ( _I |` B ) /\ ( R ` b ) =/= ( R ` F ) /\ ( R ` b ) =/= ( R ` g ) ) -> ( z ` P ) = Y ) )

Assertion

Ref	Expression
cdlemk53	|- ( ( ( ( K e. HL /\ W e. H ) /\ ( R ` F ) = ( R ` N ) ) /\ ( ( F e. T /\ F =/= ( _I |` B ) /\ N e. T ) /\ G e. T /\ ( P e. A /\ -. P .<_ W ) ) /\ ( I e. T /\ ( R ` G ) =/= ( R ` I ) ) ) -> [_ ( G o. I ) / g ]_ X = ( [_ G / g ]_ X o. [_ I / g ]_ X ) )

Distinct variable groups:   ./\ , g   .\/ , g   B, g   P, g   R, g   T, g   g, Z   g, b, G, z   ./\ , b, z   .<_ , b   z, g, .<_   .\/ , b, z   A, b, g, z   B, b, z   F, b, g, z   z, G   H, b, g, z   K, b, g, z   N, b, g, z   P, b, z   R, b, z   T, b, z   W, b, g, z   z, Y   G, b   I, b, g, z

Allowed substitution hints:   X( z, g, b)   Y( g, b)   Z( z, b)

Proof of Theorem cdlemk53

Step	Hyp	Ref	Expression
1		simp1l 1012	. . . . . 6 |- ( ( ( ( K e. HL /\ W e. H ) /\ ( R ` F ) = ( R ` N ) ) /\ ( ( F e. T /\ F =/= ( _I |` B ) /\ N e. T ) /\ G e. T /\ ( P e. A /\ -. P .<_ W ) ) /\ ( I e. T /\ ( R ` G ) =/= ( R ` I ) ) ) -> ( K e. HL /\ W e. H ) )
2		simp211 1126	. . . . . . . 8 |- ( ( ( ( K e. HL /\ W e. H ) /\ ( R ` F ) = ( R ` N ) ) /\ ( ( F e. T /\ F =/= ( _I |` B ) /\ N e. T ) /\ G e. T /\ ( P e. A /\ -. P .<_ W ) ) /\ ( I e. T /\ ( R ` G ) =/= ( R ` I ) ) ) -> F e. T )
3		simp212 1127	. . . . . . . 8 |- ( ( ( ( K e. HL /\ W e. H ) /\ ( R ` F ) = ( R ` N ) ) /\ ( ( F e. T /\ F =/= ( _I |` B ) /\ N e. T ) /\ G e. T /\ ( P e. A /\ -. P .<_ W ) ) /\ ( I e. T /\ ( R ` G ) =/= ( R ` I ) ) ) -> F =/= ( _I |` B ) )
4	2, 3	jca 532	. . . . . . 7 |- ( ( ( ( K e. HL /\ W e. H ) /\ ( R ` F ) = ( R ` N ) ) /\ ( ( F e. T /\ F =/= ( _I |` B ) /\ N e. T ) /\ G e. T /\ ( P e. A /\ -. P .<_ W ) ) /\ ( I e. T /\ ( R ` G ) =/= ( R ` I ) ) ) -> ( F e. T /\ F =/= ( _I |` B ) ) )
5		simp22 1022	. . . . . . 7 |- ( ( ( ( K e. HL /\ W e. H ) /\ ( R ` F ) = ( R ` N ) ) /\ ( ( F e. T /\ F =/= ( _I |` B ) /\ N e. T ) /\ G e. T /\ ( P e. A /\ -. P .<_ W ) ) /\ ( I e. T /\ ( R ` G ) =/= ( R ` I ) ) ) -> G e. T )
6		simp213 1128	. . . . . . 7 |- ( ( ( ( K e. HL /\ W e. H ) /\ ( R ` F ) = ( R ` N ) ) /\ ( ( F e. T /\ F =/= ( _I |` B ) /\ N e. T ) /\ G e. T /\ ( P e. A /\ -. P .<_ W ) ) /\ ( I e. T /\ ( R ` G ) =/= ( R ` I ) ) ) -> N e. T )
7		simp23 1023	. . . . . . 7 |- ( ( ( ( K e. HL /\ W e. H ) /\ ( R ` F ) = ( R ` N ) ) /\ ( ( F e. T /\ F =/= ( _I |` B ) /\ N e. T ) /\ G e. T /\ ( P e. A /\ -. P .<_ W ) ) /\ ( I e. T /\ ( R ` G ) =/= ( R ` I ) ) ) -> ( P e. A /\ -. P .<_ W ) )
8		simp1r 1013	. . . . . . 7 |- ( ( ( ( K e. HL /\ W e. H ) /\ ( R ` F ) = ( R ` N ) ) /\ ( ( F e. T /\ F =/= ( _I |` B ) /\ N e. T ) /\ G e. T /\ ( P e. A /\ -. P .<_ W ) ) /\ ( I e. T /\ ( R ` G ) =/= ( R ` I ) ) ) -> ( R ` F ) = ( R ` N ) )
9		cdlemk5.b	. . . . . . . 8 |- B = ( Base ` K )
10		cdlemk5.l	. . . . . . . 8 |- .<_ = ( le ` K )
11		cdlemk5.j	. . . . . . . 8 |- .\/ = ( join ` K )
12		cdlemk5.m	. . . . . . . 8 |- ./\ = ( meet ` K )
13		cdlemk5.a	. . . . . . . 8 |- A = ( Atoms ` K )
14		cdlemk5.h	. . . . . . . 8 |- H = ( LHyp ` K )
15		cdlemk5.t	. . . . . . . 8 |- T = ( ( LTrn ` K ) ` W )
16		cdlemk5.r	. . . . . . . 8 |- R = ( ( trL ` K ) ` W )
17		cdlemk5.z	. . . . . . . 8 |- Z = ( ( P .\/ ( R ` b ) ) ./\ ( ( N ` P ) .\/ ( R ` ( b o. `' F ) ) ) )
18		cdlemk5.y	. . . . . . . 8 |- Y = ( ( P .\/ ( R ` g ) ) ./\ ( Z .\/ ( R ` ( g o. `' b ) ) ) )
19		cdlemk5.x	. . . . . . . 8 |- X = ( iota_ z e. T A. b e. T ( ( b =/= ( _I |` B ) /\ ( R ` b ) =/= ( R ` F ) /\ ( R ` b ) =/= ( R ` g ) ) -> ( z ` P ) = Y ) )
20	9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19	cdlemk35s-id 34890	. . . . . . 7 |- ( ( ( K e. HL /\ W e. H ) /\ ( ( F e. T /\ F =/= ( _I |` B ) ) /\ G e. T /\ N e. T ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( R ` F ) = ( R ` N ) ) ) -> [_ G / g ]_ X e. T )
21	1, 4, 5, 6, 7, 8, 20	syl132anc 1237	. . . . . 6 |- ( ( ( ( K e. HL /\ W e. H ) /\ ( R ` F ) = ( R ` N ) ) /\ ( ( F e. T /\ F =/= ( _I |` B ) /\ N e. T ) /\ G e. T /\ ( P e. A /\ -. P .<_ W ) ) /\ ( I e. T /\ ( R ` G ) =/= ( R ` I ) ) ) -> [_ G / g ]_ X e. T )
22	9, 14, 15	ltrn1o 34076	. . . . . 6 |- ( ( ( K e. HL /\ W e. H ) /\ [_ G / g ]_ X e. T ) -> [_ G / g ]_ X : B -1-1-onto-> B )
23	1, 21, 22	syl2anc 661	. . . . 5 |- ( ( ( ( K e. HL /\ W e. H ) /\ ( R ` F ) = ( R ` N ) ) /\ ( ( F e. T /\ F =/= ( _I |` B ) /\ N e. T ) /\ G e. T /\ ( P e. A /\ -. P .<_ W ) ) /\ ( I e. T /\ ( R ` G ) =/= ( R ` I ) ) ) -> [_ G / g ]_ X : B -1-1-onto-> B )
24		f1of 5741	. . . . 5 |- ( [_ G / g ]_ X : B -1-1-onto-> B -> [_ G / g ]_ X : B --> B )
25		fcoi1 5685	. . . . 5 |- ( [_ G / g ]_ X : B --> B -> ( [_ G / g ]_ X o. ( _I |` B ) ) = [_ G / g ]_ X )
26	23, 24, 25	3syl 20	. . . 4 |- ( ( ( ( K e. HL /\ W e. H ) /\ ( R ` F ) = ( R ` N ) ) /\ ( ( F e. T /\ F =/= ( _I |` B ) /\ N e. T ) /\ G e. T /\ ( P e. A /\ -. P .<_ W ) ) /\ ( I e. T /\ ( R ` G ) =/= ( R ` I ) ) ) -> ( [_ G / g ]_ X o. ( _I |` B ) ) = [_ G / g ]_ X )
27	26	adantr 465	. . 3 |- ( ( ( ( ( K e. HL /\ W e. H ) /\ ( R ` F ) = ( R ` N ) ) /\ ( ( F e. T /\ F =/= ( _I |` B ) /\ N e. T ) /\ G e. T /\ ( P e. A /\ -. P .<_ W ) ) /\ ( I e. T /\ ( R ` G ) =/= ( R ` I ) ) ) /\ I = ( _I |` B ) ) -> ( [_ G / g ]_ X o. ( _I |` B ) ) = [_ G / g ]_ X )
28		simpl1l 1039	. . . . 5 |- ( ( ( ( ( K e. HL /\ W e. H ) /\ ( R ` F ) = ( R ` N ) ) /\ ( ( F e. T /\ F =/= ( _I |` B ) /\ N e. T ) /\ G e. T /\ ( P e. A /\ -. P .<_ W ) ) /\ ( I e. T /\ ( R ` G ) =/= ( R ` I ) ) ) /\ I = ( _I |` B ) ) -> ( K e. HL /\ W e. H ) )
29	2, 6, 8	3jca 1168	. . . . . 6 |- ( ( ( ( K e. HL /\ W e. H ) /\ ( R ` F ) = ( R ` N ) ) /\ ( ( F e. T /\ F =/= ( _I |` B ) /\ N e. T ) /\ G e. T /\ ( P e. A /\ -. P .<_ W ) ) /\ ( I e. T /\ ( R ` G ) =/= ( R ` I ) ) ) -> ( F e. T /\ N e. T /\ ( R ` F ) = ( R ` N ) ) )
30	29	adantr 465	. . . . 5 |- ( ( ( ( ( K e. HL /\ W e. H ) /\ ( R ` F ) = ( R ` N ) ) /\ ( ( F e. T /\ F =/= ( _I |` B ) /\ N e. T ) /\ G e. T /\ ( P e. A /\ -. P .<_ W ) ) /\ ( I e. T /\ ( R ` G ) =/= ( R ` I ) ) ) /\ I = ( _I |` B ) ) -> ( F e. T /\ N e. T /\ ( R ` F ) = ( R ` N ) ) )
31		simpl23 1068	. . . . 5 |- ( ( ( ( ( K e. HL /\ W e. H ) /\ ( R ` F ) = ( R ` N ) ) /\ ( ( F e. T /\ F =/= ( _I |` B ) /\ N e. T ) /\ G e. T /\ ( P e. A /\ -. P .<_ W ) ) /\ ( I e. T /\ ( R ` G ) =/= ( R ` I ) ) ) /\ I = ( _I |` B ) ) -> ( P e. A /\ -. P .<_ W ) )
32		simpr 461	. . . . 5 |- ( ( ( ( ( K e. HL /\ W e. H ) /\ ( R ` F ) = ( R ` N ) ) /\ ( ( F e. T /\ F =/= ( _I |` B ) /\ N e. T ) /\ G e. T /\ ( P e. A /\ -. P .<_ W ) ) /\ ( I e. T /\ ( R ` G ) =/= ( R ` I ) ) ) /\ I = ( _I |` B ) ) -> I = ( _I |` B ) )
33	9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19	cdlemkid 34888	. . . . 5 |- ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ N e. T /\ ( R ` F ) = ( R ` N ) ) /\ ( ( P e. A /\ -. P .<_ W ) /\ I = ( _I |` B ) ) ) -> [_ I / g ]_ X = ( _I |` B ) )
34	28, 30, 31, 32, 33	syl112anc 1223	. . . 4 |- ( ( ( ( ( K e. HL /\ W e. H ) /\ ( R ` F ) = ( R ` N ) ) /\ ( ( F e. T /\ F =/= ( _I |` B ) /\ N e. T ) /\ G e. T /\ ( P e. A /\ -. P .<_ W ) ) /\ ( I e. T /\ ( R ` G ) =/= ( R ` I ) ) ) /\ I = ( _I |` B ) ) -> [_ I / g ]_ X = ( _I |` B ) )
35	34	coeq2d 5102	. . 3 |- ( ( ( ( ( K e. HL /\ W e. H ) /\ ( R ` F ) = ( R ` N ) ) /\ ( ( F e. T /\ F =/= ( _I |` B ) /\ N e. T ) /\ G e. T /\ ( P e. A /\ -. P .<_ W ) ) /\ ( I e. T /\ ( R ` G ) =/= ( R ` I ) ) ) /\ I = ( _I |` B ) ) -> ( [_ G / g ]_ X o. [_ I / g ]_ X ) = ( [_ G / g ]_ X o. ( _I |` B ) ) )
36	32	coeq2d 5102	. . . . 5 |- ( ( ( ( ( K e. HL /\ W e. H ) /\ ( R ` F ) = ( R ` N ) ) /\ ( ( F e. T /\ F =/= ( _I |` B ) /\ N e. T ) /\ G e. T /\ ( P e. A /\ -. P .<_ W ) ) /\ ( I e. T /\ ( R ` G ) =/= ( R ` I ) ) ) /\ I = ( _I |` B ) ) -> ( G o. I ) = ( G o. ( _I |` B ) ) )
37	9, 14, 15	ltrn1o 34076	. . . . . . . 8 |- ( ( ( K e. HL /\ W e. H ) /\ G e. T ) -> G : B -1-1-onto-> B )
38	1, 5, 37	syl2anc 661	. . . . . . 7 |- ( ( ( ( K e. HL /\ W e. H ) /\ ( R ` F ) = ( R ` N ) ) /\ ( ( F e. T /\ F =/= ( _I |` B ) /\ N e. T ) /\ G e. T /\ ( P e. A /\ -. P .<_ W ) ) /\ ( I e. T /\ ( R ` G ) =/= ( R ` I ) ) ) -> G : B -1-1-onto-> B )
39		f1of 5741	. . . . . . 7 |- ( G : B -1-1-onto-> B -> G : B --> B )
40		fcoi1 5685	. . . . . . 7 |- ( G : B --> B -> ( G o. ( _I |` B ) ) = G )
41	38, 39, 40	3syl 20	. . . . . 6 |- ( ( ( ( K e. HL /\ W e. H ) /\ ( R ` F ) = ( R ` N ) ) /\ ( ( F e. T /\ F =/= ( _I |` B ) /\ N e. T ) /\ G e. T /\ ( P e. A /\ -. P .<_ W ) ) /\ ( I e. T /\ ( R ` G ) =/= ( R ` I ) ) ) -> ( G o. ( _I |` B ) ) = G )
42	41	adantr 465	. . . . 5 |- ( ( ( ( ( K e. HL /\ W e. H ) /\ ( R ` F ) = ( R ` N ) ) /\ ( ( F e. T /\ F =/= ( _I |` B ) /\ N e. T ) /\ G e. T /\ ( P e. A /\ -. P .<_ W ) ) /\ ( I e. T /\ ( R ` G ) =/= ( R ` I ) ) ) /\ I = ( _I |` B ) ) -> ( G o. ( _I |` B ) ) = G )
43	36, 42	eqtrd 2492	. . . 4 |- ( ( ( ( ( K e. HL /\ W e. H ) /\ ( R ` F ) = ( R ` N ) ) /\ ( ( F e. T /\ F =/= ( _I |` B ) /\ N e. T ) /\ G e. T /\ ( P e. A /\ -. P .<_ W ) ) /\ ( I e. T /\ ( R ` G ) =/= ( R ` I ) ) ) /\ I = ( _I |` B ) ) -> ( G o. I ) = G )
44	43	csbeq1d 3395	. . 3 |- ( ( ( ( ( K e. HL /\ W e. H ) /\ ( R ` F ) = ( R ` N ) ) /\ ( ( F e. T /\ F =/= ( _I |` B ) /\ N e. T ) /\ G e. T /\ ( P e. A /\ -. P .<_ W ) ) /\ ( I e. T /\ ( R ` G ) =/= ( R ` I ) ) ) /\ I = ( _I |` B ) ) -> [_ ( G o. I ) / g ]_ X = [_ G / g ]_ X )
45	27, 35, 44	3eqtr4rd 2503	. 2 |- ( ( ( ( ( K e. HL /\ W e. H ) /\ ( R ` F ) = ( R ` N ) ) /\ ( ( F e. T /\ F =/= ( _I |` B ) /\ N e. T ) /\ G e. T /\ ( P e. A /\ -. P .<_ W ) ) /\ ( I e. T /\ ( R ` G ) =/= ( R ` I ) ) ) /\ I = ( _I |` B ) ) -> [_ ( G o. I ) / g ]_ X = ( [_ G / g ]_ X o. [_ I / g ]_ X ) )
46		simpl1 991	. . 3 |- ( ( ( ( ( K e. HL /\ W e. H ) /\ ( R ` F ) = ( R ` N ) ) /\ ( ( F e. T /\ F =/= ( _I |` B ) /\ N e. T ) /\ G e. T /\ ( P e. A /\ -. P .<_ W ) ) /\ ( I e. T /\ ( R ` G ) =/= ( R ` I ) ) ) /\ I =/= ( _I |` B ) ) -> ( ( K e. HL /\ W e. H ) /\ ( R ` F ) = ( R ` N ) ) )
47		simpl2 992	. . 3 |- ( ( ( ( ( K e. HL /\ W e. H ) /\ ( R ` F ) = ( R ` N ) ) /\ ( ( F e. T /\ F =/= ( _I |` B ) /\ N e. T ) /\ G e. T /\ ( P e. A /\ -. P .<_ W ) ) /\ ( I e. T /\ ( R ` G ) =/= ( R ` I ) ) ) /\ I =/= ( _I |` B ) ) -> ( ( F e. T /\ F =/= ( _I |` B ) /\ N e. T ) /\ G e. T /\ ( P e. A /\ -. P .<_ W ) ) )
48		simpl3l 1043	. . 3 |- ( ( ( ( ( K e. HL /\ W e. H ) /\ ( R ` F ) = ( R ` N ) ) /\ ( ( F e. T /\ F =/= ( _I |` B ) /\ N e. T ) /\ G e. T /\ ( P e. A /\ -. P .<_ W ) ) /\ ( I e. T /\ ( R ` G ) =/= ( R ` I ) ) ) /\ I =/= ( _I |` B ) ) -> I e. T )
49		simpr 461	. . 3 |- ( ( ( ( ( K e. HL /\ W e. H ) /\ ( R ` F ) = ( R ` N ) ) /\ ( ( F e. T /\ F =/= ( _I |` B ) /\ N e. T ) /\ G e. T /\ ( P e. A /\ -. P .<_ W ) ) /\ ( I e. T /\ ( R ` G ) =/= ( R ` I ) ) ) /\ I =/= ( _I |` B ) ) -> I =/= ( _I |` B ) )
50		simpl3r 1044	. . 3 |- ( ( ( ( ( K e. HL /\ W e. H ) /\ ( R ` F ) = ( R ` N ) ) /\ ( ( F e. T /\ F =/= ( _I |` B ) /\ N e. T ) /\ G e. T /\ ( P e. A /\ -. P .<_ W ) ) /\ ( I e. T /\ ( R ` G ) =/= ( R ` I ) ) ) /\ I =/= ( _I |` B ) ) -> ( R ` G ) =/= ( R ` I ) )
51	9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19	cdlemk53b 34908	. . 3 |- ( ( ( ( K e. HL /\ W e. H ) /\ ( R ` F ) = ( R ` N ) ) /\ ( ( F e. T /\ F =/= ( _I |` B ) /\ N e. T ) /\ G e. T /\ ( P e. A /\ -. P .<_ W ) ) /\ ( I e. T /\ I =/= ( _I |` B ) /\ ( R ` G ) =/= ( R ` I ) ) ) -> [_ ( G o. I ) / g ]_ X = ( [_ G / g ]_ X o. [_ I / g ]_ X ) )
52	46, 47, 48, 49, 50, 51	syl113anc 1231	. 2 |- ( ( ( ( ( K e. HL /\ W e. H ) /\ ( R ` F ) = ( R ` N ) ) /\ ( ( F e. T /\ F =/= ( _I |` B ) /\ N e. T ) /\ G e. T /\ ( P e. A /\ -. P .<_ W ) ) /\ ( I e. T /\ ( R ` G ) =/= ( R ` I ) ) ) /\ I =/= ( _I |` B ) ) -> [_ ( G o. I ) / g ]_ X = ( [_ G / g ]_ X o. [_ I / g ]_ X ) )
53	45, 52	pm2.61dane 2766	1 |- ( ( ( ( K e. HL /\ W e. H ) /\ ( R ` F ) = ( R ` N ) ) /\ ( ( F e. T /\ F =/= ( _I |` B ) /\ N e. T ) /\ G e. T /\ ( P e. A /\ -. P .<_ W ) ) /\ ( I e. T /\ ( R ` G ) =/= ( R ` I ) ) ) -> [_ ( G o. I ) / g ]_ X = ( [_ G / g ]_ X o. [_ I / g ]_ X ) )

Syntax hints:   -. wn 3   -> wi 4   /\ wa 369   /\ w3a 965   = wceq 1370   e. wcel 1758   =/= wne 2644   A.wral 2795   [_csb 3388   class class class wbr 4392   _I cid 4731   `'ccnv 4939   |` cres 4942   o. ccom 4944   -->wf 5514   -1-1-onto->wf1o 5517   ` cfv 5518   iota_crio 6152  (class class class)co 6192   Basecbs 14278   lecple 14349   joincjn 15218   meetcmee 15219   Atomscatm 33216   HLchlt 33303   LHypclh 33936   LTrncltrn 34053   trLctrl 34110

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 1952  ax-ext 2430  ax-rep 4503  ax-sep 4513  ax-nul 4521  ax-pow 4570  ax-pr 4631  ax-un 6474  ax-riotaBAD 32912

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 2264  df-mo 2265  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2601  df-ne 2646  df-nel 2647  df-ral 2800  df-rex 2801  df-reu 2802  df-rmo 2803  df-rab 2804  df-v 3072  df-sbc 3287  df-csb 3389  df-dif 3431  df-un 3433  df-in 3435  df-ss 3442  df-nul 3738  df-if 3892  df-pw 3962  df-sn 3978  df-pr 3980  df-op 3984  df-uni 4192  df-iun 4273  df-iin 4274  df-br 4393  df-opab 4451  df-mpt 4452  df-id 4736  df-xp 4946  df-rel 4947  df-cnv 4948  df-co 4949  df-dm 4950  df-rn 4951  df-res 4952  df-ima 4953  df-iota 5481  df-fun 5520  df-fn 5521  df-f 5522  df-f1 5523  df-fo 5524  df-f1o 5525  df-fv 5526  df-riota 6153  df-ov 6195  df-oprab 6196  df-mpt2 6197  df-1st 6679  df-2nd 6680  df-undef 6894  df-map 7318  df-poset 15220  df-plt 15232  df-lub 15248  df-glb 15249  df-join 15250  df-meet 15251  df-p0 15313  df-p1 15314  df-lat 15320  df-clat 15382  df-oposet 33129  df-ol 33131  df-oml 33132  df-covers 33219  df-ats 33220  df-atl 33251  df-cvlat 33275  df-hlat 33304  df-llines 33450  df-lplanes 33451  df-lvols 33452  df-lines 33453  df-psubsp 33455  df-pmap 33456  df-padd 33748  df-lhyp 33940  df-laut 33941  df-ldil 34056  df-ltrn 34057  df-trl 34111

This theorem is referenced by:  cdlemk54  34910  cdlemk55  34913