Theorem cdlemk11t 36143

Description: Part of proof of Lemma K of [Crawley] p. 118. Eq. 5, line 36, p. 119. G, I stand for g, h. X represents tau. (Contributed by NM, 21-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
cdlemk11t	|- ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ F =/= ( _I |` B ) ) /\ ( G e. T /\ G =/= ( _I |` B ) ) ) /\ ( N e. T /\ ( P e. A /\ -. P .<_ W ) /\ ( R ` F ) = ( R ` N ) ) /\ ( I e. T /\ I =/= ( _I |` B ) ) ) -> ( [_ G / g ]_ X ` P ) .<_ ( ( [_ I / g ]_ X ` P ) .\/ ( R ` ( I o. `' G ) ) ) )

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 cdlemk11t

Step	Hyp	Ref	Expression
1		simp11l 1107	. . 3 |- ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ F =/= ( _I |` B ) ) /\ ( G e. T /\ G =/= ( _I |` B ) ) ) /\ ( N e. T /\ ( P e. A /\ -. P .<_ W ) /\ ( R ` F ) = ( R ` N ) ) /\ ( I e. T /\ I =/= ( _I |` B ) ) ) -> K e. HL )
2		simp11r 1108	. . 3 |- ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ F =/= ( _I |` B ) ) /\ ( G e. T /\ G =/= ( _I |` B ) ) ) /\ ( N e. T /\ ( P e. A /\ -. P .<_ W ) /\ ( R ` F ) = ( R ` N ) ) /\ ( I e. T /\ I =/= ( _I |` B ) ) ) -> W e. H )
3		cdlemk5.b	. . . 4 |- B = ( Base ` K )
4		cdlemk5.h	. . . 4 |- H = ( LHyp ` K )
5		cdlemk5.t	. . . 4 |- T = ( ( LTrn ` K ) ` W )
6		cdlemk5.r	. . . 4 |- R = ( ( trL ` K ) ` W )
7	3, 4, 5, 6	cdlemftr3 35762	. . 3 |- ( ( K e. HL /\ W e. H ) -> E. b e. T ( b =/= ( _I |` B ) /\ ( ( R ` b ) =/= ( R ` F ) /\ ( R ` b ) =/= ( R ` G ) /\ ( R ` b ) =/= ( R ` I ) ) ) )
8	1, 2, 7	syl2anc 661	. 2 |- ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ F =/= ( _I |` B ) ) /\ ( G e. T /\ G =/= ( _I |` B ) ) ) /\ ( N e. T /\ ( P e. A /\ -. P .<_ W ) /\ ( R ` F ) = ( R ` N ) ) /\ ( I e. T /\ I =/= ( _I |` B ) ) ) -> E. b e. T ( b =/= ( _I |` B ) /\ ( ( R ` b ) =/= ( R ` F ) /\ ( R ` b ) =/= ( R ` G ) /\ ( R ` b ) =/= ( R ` I ) ) ) )
9		nfv 1683	. . 3 |- F/ b ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ F =/= ( _I |` B ) ) /\ ( G e. T /\ G =/= ( _I |` B ) ) ) /\ ( N e. T /\ ( P e. A /\ -. P .<_ W ) /\ ( R ` F ) = ( R ` N ) ) /\ ( I e. T /\ I =/= ( _I |` B ) ) )
10		nfcv 2629	. . . . . 6 |- F/_ b G
11		cdlemk5.x	. . . . . . 7 |- X = ( iota_ z e. T A. b e. T ( ( b =/= ( _I |` B ) /\ ( R ` b ) =/= ( R ` F ) /\ ( R ` b ) =/= ( R ` g ) ) -> ( z ` P ) = Y ) )
12		nfra1 2848	. . . . . . . 8 |- F/ b A. b e. T ( ( b =/= ( _I |` B ) /\ ( R ` b ) =/= ( R ` F ) /\ ( R ` b ) =/= ( R ` g ) ) -> ( z ` P ) = Y )
13		nfcv 2629	. . . . . . . 8 |- F/_ b T
14	12, 13	nfriota 6265	. . . . . . 7 |- F/_ b ( iota_ z e. T A. b e. T ( ( b =/= ( _I |` B ) /\ ( R ` b ) =/= ( R ` F ) /\ ( R ` b ) =/= ( R ` g ) ) -> ( z ` P ) = Y ) )
15	11, 14	nfcxfr 2627	. . . . . 6 |- F/_ b X
16	10, 15	nfcsb 3458	. . . . 5 |- F/_ b [_ G / g ]_ X
17		nfcv 2629	. . . . 5 |- F/_ b P
18	16, 17	nffv 5879	. . . 4 |- F/_ b ( [_ G / g ]_ X ` P )
19		nfcv 2629	. . . 4 |- F/_ b .<_
20		nfcv 2629	. . . . . . 7 |- F/_ b I
21	20, 15	nfcsb 3458	. . . . . 6 |- F/_ b [_ I / g ]_ X
22	21, 17	nffv 5879	. . . . 5 |- F/_ b ( [_ I / g ]_ X ` P )
23		nfcv 2629	. . . . 5 |- F/_ b .\/
24		nfcv 2629	. . . . 5 |- F/_ b ( R ` ( I o. `' G ) )
25	22, 23, 24	nfov 6318	. . . 4 |- F/_ b ( ( [_ I / g ]_ X ` P ) .\/ ( R ` ( I o. `' G ) ) )
26	18, 19, 25	nfbr 4497	. . 3 |- F/ b ( [_ G / g ]_ X ` P ) .<_ ( ( [_ I / g ]_ X ` P ) .\/ ( R ` ( I o. `' G ) ) )
27		simp11 1026	. . . . 5 |- ( ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ F =/= ( _I |` B ) ) /\ ( G e. T /\ G =/= ( _I |` B ) ) ) /\ ( N e. T /\ ( P e. A /\ -. P .<_ W ) /\ ( R ` F ) = ( R ` N ) ) /\ ( I e. T /\ I =/= ( _I |` B ) ) ) /\ b e. T /\ ( b =/= ( _I |` B ) /\ ( ( R ` b ) =/= ( R ` F ) /\ ( R ` b ) =/= ( R ` G ) /\ ( R ` b ) =/= ( R ` I ) ) ) ) -> ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ F =/= ( _I |` B ) ) /\ ( G e. T /\ G =/= ( _I |` B ) ) ) )
28		simp12 1027	. . . . 5 |- ( ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ F =/= ( _I |` B ) ) /\ ( G e. T /\ G =/= ( _I |` B ) ) ) /\ ( N e. T /\ ( P e. A /\ -. P .<_ W ) /\ ( R ` F ) = ( R ` N ) ) /\ ( I e. T /\ I =/= ( _I |` B ) ) ) /\ b e. T /\ ( b =/= ( _I |` B ) /\ ( ( R ` b ) =/= ( R ` F ) /\ ( R ` b ) =/= ( R ` G ) /\ ( R ` b ) =/= ( R ` I ) ) ) ) -> ( N e. T /\ ( P e. A /\ -. P .<_ W ) /\ ( R ` F ) = ( R ` N ) ) )
29		simp2 997	. . . . 5 |- ( ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ F =/= ( _I |` B ) ) /\ ( G e. T /\ G =/= ( _I |` B ) ) ) /\ ( N e. T /\ ( P e. A /\ -. P .<_ W ) /\ ( R ` F ) = ( R ` N ) ) /\ ( I e. T /\ I =/= ( _I |` B ) ) ) /\ b e. T /\ ( b =/= ( _I |` B ) /\ ( ( R ` b ) =/= ( R ` F ) /\ ( R ` b ) =/= ( R ` G ) /\ ( R ` b ) =/= ( R ` I ) ) ) ) -> b e. T )
30		simp3l 1024	. . . . . 6 |- ( ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ F =/= ( _I |` B ) ) /\ ( G e. T /\ G =/= ( _I |` B ) ) ) /\ ( N e. T /\ ( P e. A /\ -. P .<_ W ) /\ ( R ` F ) = ( R ` N ) ) /\ ( I e. T /\ I =/= ( _I |` B ) ) ) /\ b e. T /\ ( b =/= ( _I |` B ) /\ ( ( R ` b ) =/= ( R ` F ) /\ ( R ` b ) =/= ( R ` G ) /\ ( R ` b ) =/= ( R ` I ) ) ) ) -> b =/= ( _I |` B ) )
31		simp3r1 1104	. . . . . 6 |- ( ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ F =/= ( _I |` B ) ) /\ ( G e. T /\ G =/= ( _I |` B ) ) ) /\ ( N e. T /\ ( P e. A /\ -. P .<_ W ) /\ ( R ` F ) = ( R ` N ) ) /\ ( I e. T /\ I =/= ( _I |` B ) ) ) /\ b e. T /\ ( b =/= ( _I |` B ) /\ ( ( R ` b ) =/= ( R ` F ) /\ ( R ` b ) =/= ( R ` G ) /\ ( R ` b ) =/= ( R ` I ) ) ) ) -> ( R ` b ) =/= ( R ` F ) )
32		simp3r2 1105	. . . . . 6 |- ( ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ F =/= ( _I |` B ) ) /\ ( G e. T /\ G =/= ( _I |` B ) ) ) /\ ( N e. T /\ ( P e. A /\ -. P .<_ W ) /\ ( R ` F ) = ( R ` N ) ) /\ ( I e. T /\ I =/= ( _I |` B ) ) ) /\ b e. T /\ ( b =/= ( _I |` B ) /\ ( ( R ` b ) =/= ( R ` F ) /\ ( R ` b ) =/= ( R ` G ) /\ ( R ` b ) =/= ( R ` I ) ) ) ) -> ( R ` b ) =/= ( R ` G ) )
33	30, 31, 32	3jca 1176	. . . . 5 |- ( ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ F =/= ( _I |` B ) ) /\ ( G e. T /\ G =/= ( _I |` B ) ) ) /\ ( N e. T /\ ( P e. A /\ -. P .<_ W ) /\ ( R ` F ) = ( R ` N ) ) /\ ( I e. T /\ I =/= ( _I |` B ) ) ) /\ b e. T /\ ( b =/= ( _I |` B ) /\ ( ( R ` b ) =/= ( R ` F ) /\ ( R ` b ) =/= ( R ` G ) /\ ( R ` b ) =/= ( R ` I ) ) ) ) -> ( b =/= ( _I |` B ) /\ ( R ` b ) =/= ( R ` F ) /\ ( R ` b ) =/= ( R ` G ) ) )
34		simp13l 1111	. . . . . 6 |- ( ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ F =/= ( _I |` B ) ) /\ ( G e. T /\ G =/= ( _I |` B ) ) ) /\ ( N e. T /\ ( P e. A /\ -. P .<_ W ) /\ ( R ` F ) = ( R ` N ) ) /\ ( I e. T /\ I =/= ( _I |` B ) ) ) /\ b e. T /\ ( b =/= ( _I |` B ) /\ ( ( R ` b ) =/= ( R ` F ) /\ ( R ` b ) =/= ( R ` G ) /\ ( R ` b ) =/= ( R ` I ) ) ) ) -> I e. T )
35		simp13r 1112	. . . . . 6 |- ( ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ F =/= ( _I |` B ) ) /\ ( G e. T /\ G =/= ( _I |` B ) ) ) /\ ( N e. T /\ ( P e. A /\ -. P .<_ W ) /\ ( R ` F ) = ( R ` N ) ) /\ ( I e. T /\ I =/= ( _I |` B ) ) ) /\ b e. T /\ ( b =/= ( _I |` B ) /\ ( ( R ` b ) =/= ( R ` F ) /\ ( R ` b ) =/= ( R ` G ) /\ ( R ` b ) =/= ( R ` I ) ) ) ) -> I =/= ( _I |` B ) )
36		simp3r3 1106	. . . . . 6 |- ( ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ F =/= ( _I |` B ) ) /\ ( G e. T /\ G =/= ( _I |` B ) ) ) /\ ( N e. T /\ ( P e. A /\ -. P .<_ W ) /\ ( R ` F ) = ( R ` N ) ) /\ ( I e. T /\ I =/= ( _I |` B ) ) ) /\ b e. T /\ ( b =/= ( _I |` B ) /\ ( ( R ` b ) =/= ( R ` F ) /\ ( R ` b ) =/= ( R ` G ) /\ ( R ` b ) =/= ( R ` I ) ) ) ) -> ( R ` b ) =/= ( R ` I ) )
37	34, 35, 36	3jca 1176	. . . . 5 |- ( ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ F =/= ( _I |` B ) ) /\ ( G e. T /\ G =/= ( _I |` B ) ) ) /\ ( N e. T /\ ( P e. A /\ -. P .<_ W ) /\ ( R ` F ) = ( R ` N ) ) /\ ( I e. T /\ I =/= ( _I |` B ) ) ) /\ b e. T /\ ( b =/= ( _I |` B ) /\ ( ( R ` b ) =/= ( R ` F ) /\ ( R ` b ) =/= ( R ` G ) /\ ( R ` b ) =/= ( R ` I ) ) ) ) -> ( I e. T /\ I =/= ( _I |` B ) /\ ( R ` b ) =/= ( R ` I ) ) )
38		cdlemk5.l	. . . . . 6 |- .<_ = ( le ` K )
39		cdlemk5.j	. . . . . 6 |- .\/ = ( join ` K )
40		cdlemk5.m	. . . . . 6 |- ./\ = ( meet ` K )
41		cdlemk5.a	. . . . . 6 |- A = ( Atoms ` K )
42		cdlemk5.z	. . . . . 6 |- Z = ( ( P .\/ ( R ` b ) ) ./\ ( ( N ` P ) .\/ ( R ` ( b o. `' F ) ) ) )
43		cdlemk5.y	. . . . . 6 |- Y = ( ( P .\/ ( R ` g ) ) ./\ ( Z .\/ ( R ` ( g o. `' b ) ) ) )
44	3, 38, 39, 40, 41, 4, 5, 6, 42, 43, 11	cdlemk11tc 36142	. . . . 5 |- ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ F =/= ( _I |` B ) ) /\ ( G e. T /\ G =/= ( _I |` B ) ) ) /\ ( N e. T /\ ( P e. A /\ -. P .<_ W ) /\ ( R ` F ) = ( R ` N ) ) /\ ( b e. T /\ ( b =/= ( _I |` B ) /\ ( R ` b ) =/= ( R ` F ) /\ ( R ` b ) =/= ( R ` G ) ) /\ ( I e. T /\ I =/= ( _I |` B ) /\ ( R ` b ) =/= ( R ` I ) ) ) ) -> ( [_ G / g ]_ X ` P ) .<_ ( ( [_ I / g ]_ X ` P ) .\/ ( R ` ( I o. `' G ) ) ) )
45	27, 28, 29, 33, 37, 44	syl113anc 1240	. . . 4 |- ( ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ F =/= ( _I |` B ) ) /\ ( G e. T /\ G =/= ( _I |` B ) ) ) /\ ( N e. T /\ ( P e. A /\ -. P .<_ W ) /\ ( R ` F ) = ( R ` N ) ) /\ ( I e. T /\ I =/= ( _I |` B ) ) ) /\ b e. T /\ ( b =/= ( _I |` B ) /\ ( ( R ` b ) =/= ( R ` F ) /\ ( R ` b ) =/= ( R ` G ) /\ ( R ` b ) =/= ( R ` I ) ) ) ) -> ( [_ G / g ]_ X ` P ) .<_ ( ( [_ I / g ]_ X ` P ) .\/ ( R ` ( I o. `' G ) ) ) )
46	45	3exp 1195	. . 3 |- ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ F =/= ( _I |` B ) ) /\ ( G e. T /\ G =/= ( _I |` B ) ) ) /\ ( N e. T /\ ( P e. A /\ -. P .<_ W ) /\ ( R ` F ) = ( R ` N ) ) /\ ( I e. T /\ I =/= ( _I |` B ) ) ) -> ( b e. T -> ( ( b =/= ( _I |` B ) /\ ( ( R ` b ) =/= ( R ` F ) /\ ( R ` b ) =/= ( R ` G ) /\ ( R ` b ) =/= ( R ` I ) ) ) -> ( [_ G / g ]_ X ` P ) .<_ ( ( [_ I / g ]_ X ` P ) .\/ ( R ` ( I o. `' G ) ) ) ) ) )
47	9, 26, 46	rexlimd 2951	. 2 |- ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ F =/= ( _I |` B ) ) /\ ( G e. T /\ G =/= ( _I |` B ) ) ) /\ ( N e. T /\ ( P e. A /\ -. P .<_ W ) /\ ( R ` F ) = ( R ` N ) ) /\ ( I e. T /\ I =/= ( _I |` B ) ) ) -> ( E. b e. T ( b =/= ( _I |` B ) /\ ( ( R ` b ) =/= ( R ` F ) /\ ( R ` b ) =/= ( R ` G ) /\ ( R ` b ) =/= ( R ` I ) ) ) -> ( [_ G / g ]_ X ` P ) .<_ ( ( [_ I / g ]_ X ` P ) .\/ ( R ` ( I o. `' G ) ) ) ) )
48	8, 47	mpd 15	1 |- ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ F =/= ( _I |` B ) ) /\ ( G e. T /\ G =/= ( _I |` B ) ) ) /\ ( N e. T /\ ( P e. A /\ -. P .<_ W ) /\ ( R ` F ) = ( R ` N ) ) /\ ( I e. T /\ I =/= ( _I |` B ) ) ) -> ( [_ G / g ]_ X ` P ) .<_ ( ( [_ I / g ]_ X ` P ) .\/ ( R ` ( I o. `' G ) ) ) )

Syntax hints:   -. wn 3   -> wi 4   /\ wa 369   /\ w3a 973   = wceq 1379   e. wcel 1767   =/= wne 2662   A.wral 2817   E.wrex 2818   [_csb 3440   class class class wbr 4453   _I cid 4796   `'ccnv 5004   |` cres 5007   o. ccom 5009   ` cfv 5594   iota_crio 6255  (class class class)co 6295   Basecbs 14507   lecple 14579   joincjn 15448   meetcmee 15449   Atomscatm 34461   HLchlt 34548   LHypclh 35181   LTrncltrn 35298   trLctrl 35355

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-8 1769  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-rep 4564  ax-sep 4574  ax-nul 4582  ax-pow 4631  ax-pr 4692  ax-un 6587  ax-riotaBAD 34157

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1382  df-fal 1385  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-nel 2665  df-ral 2822  df-rex 2823  df-reu 2824  df-rmo 2825  df-rab 2826  df-v 3120  df-sbc 3337  df-csb 3441  df-dif 3484  df-un 3486  df-in 3488  df-ss 3495  df-nul 3791  df-if 3946  df-pw 4018  df-sn 4034  df-pr 4036  df-op 4040  df-uni 4252  df-iun 4333  df-iin 4334  df-br 4454  df-opab 4512  df-mpt 4513  df-id 4801  df-xp 5011  df-rel 5012  df-cnv 5013  df-co 5014  df-dm 5015  df-rn 5016  df-res 5017  df-ima 5018  df-iota 5557  df-fun 5596  df-fn 5597  df-f 5598  df-f1 5599  df-fo 5600  df-f1o 5601  df-fv 5602  df-riota 6256  df-ov 6298  df-oprab 6299  df-mpt2 6300  df-1st 6795  df-2nd 6796  df-undef 7014  df-map 7434  df-poset 15450  df-plt 15462  df-lub 15478  df-glb 15479  df-join 15480  df-meet 15481  df-p0 15543  df-p1 15544  df-lat 15550  df-clat 15612  df-oposet 34374  df-ol 34376  df-oml 34377  df-covers 34464  df-ats 34465  df-atl 34496  df-cvlat 34520  df-hlat 34549  df-llines 34695  df-lplanes 34696  df-lvols 34697  df-lines 34698  df-psubsp 34700  df-pmap 34701  df-padd 34993  df-lhyp 35185  df-laut 35186  df-ldil 35301  df-ltrn 35302  df-trl 35356

This theorem is referenced by:  cdlemk45  36144