Theorem cdleme42ke 34141

Description: Part of proof of Lemma E in [Crawley] p. 113. Remove R =/= S condition. TODO: FIX COMMENT (Contributed by NM, 2-Apr-2013.)

Hypotheses

Ref	Expression
cdleme41.b	|- B = ( Base ` K )
cdleme41.l	|- .<_ = ( le ` K )
cdleme41.j	|- .\/ = ( join ` K )
cdleme41.m	|- ./\ = ( meet ` K )
cdleme41.a	|- A = ( Atoms ` K )
cdleme41.h	|- H = ( LHyp ` K )
cdleme41.u	|- U = ( ( P .\/ Q ) ./\ W )
cdleme41.d	|- D = ( ( s .\/ U ) ./\ ( Q .\/ ( ( P .\/ s ) ./\ W ) ) )
cdleme41.e	|- E = ( ( t .\/ U ) ./\ ( Q .\/ ( ( P .\/ t ) ./\ W ) ) )
cdleme41.g	|- G = ( ( P .\/ Q ) ./\ ( E .\/ ( ( s .\/ t ) ./\ W ) ) )
cdleme41.i	|- I = ( iota_ y e. B A. t e. A ( ( -. t .<_ W /\ -. t .<_ ( P .\/ Q ) ) -> y = G ) )
cdleme41.n	|- N = if ( s .<_ ( P .\/ Q ) , I , D )
cdleme41.o	|- O = ( iota_ z e. B A. s e. A ( ( -. s .<_ W /\ ( s .\/ ( x ./\ W ) ) = x ) -> z = ( N .\/ ( x ./\ W ) ) ) )
cdleme41.f	|- F = ( x e. B |-> if ( ( P =/= Q /\ -. x .<_ W ) , O , x ) )
cdleme34e.v	|- V = ( ( R .\/ S ) ./\ W )

Assertion

Ref	Expression
cdleme42ke	|- ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( P =/= Q /\ ( R e. A /\ -. R .<_ W ) /\ ( S e. A /\ -. S .<_ W ) ) ) -> ( ( F ` R ) .\/ ( F ` S ) ) = ( ( F ` R ) .\/ V ) )

Distinct variable groups:   A, s   .\/ , s   .<_ , s   ./\ , s   P, s   Q, s   R, s   S, s   U, s   W, s   y, t, A, s   B, s, t, y   y, D   y, G   E, s, y   H, s, t, y   t, .\/ , y   K, s, t, y   t, .<_ , y   t, ./\ , y   t, P, y   t, Q, y   t, R, y   t, S, y   t, U, y   t, W, y   x, z, A   x, B, z   z, E, s   z, H   x, .\/ , z   z, K   x, .<_ , z   x, ./\ , z   x, N, z   x, P, z   x, Q, z   x, R, z   x, S, z   x, U, z   x, W, z, s, t, y   V, s, t, x, z

Allowed substitution hints:   D( x, z, t, s)   E( x, t)   F( x, y, z, t, s)   G( x, z, t, s)   H( x)   I( x, y, z, t, s)   K( x)   N( y, t, s)   O( x, y, z, t, s)   V( y)

Proof of Theorem cdleme42ke

Step	Hyp	Ref	Expression
1		simpl1l 1039	. . . . 5 |- ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( P =/= Q /\ ( R e. A /\ -. R .<_ W ) /\ ( S e. A /\ -. S .<_ W ) ) ) -> K e. HL )
2		simpr2 995	. . . . . . 7 |- ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( P =/= Q /\ ( R e. A /\ -. R .<_ W ) /\ ( S e. A /\ -. S .<_ W ) ) ) -> ( R e. A /\ -. R .<_ W ) )
3		cdleme41.b	. . . . . . . 8 |- B = ( Base ` K )
4		cdleme41.l	. . . . . . . 8 |- .<_ = ( le ` K )
5		cdleme41.j	. . . . . . . 8 |- .\/ = ( join ` K )
6		cdleme41.m	. . . . . . . 8 |- ./\ = ( meet ` K )
7		cdleme41.a	. . . . . . . 8 |- A = ( Atoms ` K )
8		cdleme41.h	. . . . . . . 8 |- H = ( LHyp ` K )
9		cdleme41.u	. . . . . . . 8 |- U = ( ( P .\/ Q ) ./\ W )
10		cdleme41.d	. . . . . . . 8 |- D = ( ( s .\/ U ) ./\ ( Q .\/ ( ( P .\/ s ) ./\ W ) ) )
11		cdleme41.e	. . . . . . . 8 |- E = ( ( t .\/ U ) ./\ ( Q .\/ ( ( P .\/ t ) ./\ W ) ) )
12		cdleme41.g	. . . . . . . 8 |- G = ( ( P .\/ Q ) ./\ ( E .\/ ( ( s .\/ t ) ./\ W ) ) )
13		cdleme41.i	. . . . . . . 8 |- I = ( iota_ y e. B A. t e. A ( ( -. t .<_ W /\ -. t .<_ ( P .\/ Q ) ) -> y = G ) )
14		cdleme41.n	. . . . . . . 8 |- N = if ( s .<_ ( P .\/ Q ) , I , D )
15		cdleme41.o	. . . . . . . 8 |- O = ( iota_ z e. B A. s e. A ( ( -. s .<_ W /\ ( s .\/ ( x ./\ W ) ) = x ) -> z = ( N .\/ ( x ./\ W ) ) ) )
16		cdleme41.f	. . . . . . . 8 |- F = ( x e. B |-> if ( ( P =/= Q /\ -. x .<_ W ) , O , x ) )
17	3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16	cdleme32fvaw 34095	. . . . . . 7 |- ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( R e. A /\ -. R .<_ W ) ) -> ( ( F ` R ) e. A /\ -. ( F ` R ) .<_ W ) )
18	2, 17	syldan 470	. . . . . 6 |- ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( P =/= Q /\ ( R e. A /\ -. R .<_ W ) /\ ( S e. A /\ -. S .<_ W ) ) ) -> ( ( F ` R ) e. A /\ -. ( F ` R ) .<_ W ) )
19	18	simpld 459	. . . . 5 |- ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( P =/= Q /\ ( R e. A /\ -. R .<_ W ) /\ ( S e. A /\ -. S .<_ W ) ) ) -> ( F ` R ) e. A )
20	5, 7	hlatjidm 33025	. . . . 5 |- ( ( K e. HL /\ ( F ` R ) e. A ) -> ( ( F ` R ) .\/ ( F ` R ) ) = ( F ` R ) )
21	1, 19, 20	syl2anc 661	. . . 4 |- ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( P =/= Q /\ ( R e. A /\ -. R .<_ W ) /\ ( S e. A /\ -. S .<_ W ) ) ) -> ( ( F ` R ) .\/ ( F ` R ) ) = ( F ` R ) )
22		fveq2 5703	. . . . 5 |- ( R = S -> ( F ` R ) = ( F ` S ) )
23	22	oveq2d 6119	. . . 4 |- ( R = S -> ( ( F ` R ) .\/ ( F ` R ) ) = ( ( F ` R ) .\/ ( F ` S ) ) )
24	21, 23	sylan9req 2496	. . 3 |- ( ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( P =/= Q /\ ( R e. A /\ -. R .<_ W ) /\ ( S e. A /\ -. S .<_ W ) ) ) /\ R = S ) -> ( F ` R ) = ( ( F ` R ) .\/ ( F ` S ) ) )
25		simpr2l 1047	. . . . . . . . 9 |- ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( P =/= Q /\ ( R e. A /\ -. R .<_ W ) /\ ( S e. A /\ -. S .<_ W ) ) ) -> R e. A )
26	5, 7	hlatjidm 33025	. . . . . . . . 9 |- ( ( K e. HL /\ R e. A ) -> ( R .\/ R ) = R )
27	1, 25, 26	syl2anc 661	. . . . . . . 8 |- ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( P =/= Q /\ ( R e. A /\ -. R .<_ W ) /\ ( S e. A /\ -. S .<_ W ) ) ) -> ( R .\/ R ) = R )
28	27	oveq1d 6118	. . . . . . 7 |- ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( P =/= Q /\ ( R e. A /\ -. R .<_ W ) /\ ( S e. A /\ -. S .<_ W ) ) ) -> ( ( R .\/ R ) ./\ W ) = ( R ./\ W ) )
29		simpl1 991	. . . . . . . 8 |- ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( P =/= Q /\ ( R e. A /\ -. R .<_ W ) /\ ( S e. A /\ -. S .<_ W ) ) ) -> ( K e. HL /\ W e. H ) )
30		eqid 2443	. . . . . . . . 9 |- ( 0. ` K ) = ( 0. ` K )
31	4, 6, 30, 7, 8	lhpmat 33686	. . . . . . . 8 |- ( ( ( K e. HL /\ W e. H ) /\ ( R e. A /\ -. R .<_ W ) ) -> ( R ./\ W ) = ( 0. ` K ) )
32	29, 2, 31	syl2anc 661	. . . . . . 7 |- ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( P =/= Q /\ ( R e. A /\ -. R .<_ W ) /\ ( S e. A /\ -. S .<_ W ) ) ) -> ( R ./\ W ) = ( 0. ` K ) )
33	28, 32	eqtrd 2475	. . . . . 6 |- ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( P =/= Q /\ ( R e. A /\ -. R .<_ W ) /\ ( S e. A /\ -. S .<_ W ) ) ) -> ( ( R .\/ R ) ./\ W ) = ( 0. ` K ) )
34	33	oveq2d 6119	. . . . 5 |- ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( P =/= Q /\ ( R e. A /\ -. R .<_ W ) /\ ( S e. A /\ -. S .<_ W ) ) ) -> ( ( F ` R ) .\/ ( ( R .\/ R ) ./\ W ) ) = ( ( F ` R ) .\/ ( 0. ` K ) ) )
35		hlol 33018	. . . . . . 7 |- ( K e. HL -> K e. OL )
36	1, 35	syl 16	. . . . . 6 |- ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( P =/= Q /\ ( R e. A /\ -. R .<_ W ) /\ ( S e. A /\ -. S .<_ W ) ) ) -> K e. OL )
37	3, 7	atbase 32946	. . . . . . 7 |- ( ( F ` R ) e. A -> ( F ` R ) e. B )
38	19, 37	syl 16	. . . . . 6 |- ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( P =/= Q /\ ( R e. A /\ -. R .<_ W ) /\ ( S e. A /\ -. S .<_ W ) ) ) -> ( F ` R ) e. B )
39	3, 5, 30	olj01 32882	. . . . . 6 |- ( ( K e. OL /\ ( F ` R ) e. B ) -> ( ( F ` R ) .\/ ( 0. ` K ) ) = ( F ` R ) )
40	36, 38, 39	syl2anc 661	. . . . 5 |- ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( P =/= Q /\ ( R e. A /\ -. R .<_ W ) /\ ( S e. A /\ -. S .<_ W ) ) ) -> ( ( F ` R ) .\/ ( 0. ` K ) ) = ( F ` R ) )
41	34, 40	eqtrd 2475	. . . 4 |- ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( P =/= Q /\ ( R e. A /\ -. R .<_ W ) /\ ( S e. A /\ -. S .<_ W ) ) ) -> ( ( F ` R ) .\/ ( ( R .\/ R ) ./\ W ) ) = ( F ` R ) )
42		oveq2 6111	. . . . . . 7 |- ( R = S -> ( R .\/ R ) = ( R .\/ S ) )
43	42	oveq1d 6118	. . . . . 6 |- ( R = S -> ( ( R .\/ R ) ./\ W ) = ( ( R .\/ S ) ./\ W ) )
44		cdleme34e.v	. . . . . 6 |- V = ( ( R .\/ S ) ./\ W )
45	43, 44	syl6eqr 2493	. . . . 5 |- ( R = S -> ( ( R .\/ R ) ./\ W ) = V )
46	45	oveq2d 6119	. . . 4 |- ( R = S -> ( ( F ` R ) .\/ ( ( R .\/ R ) ./\ W ) ) = ( ( F ` R ) .\/ V ) )
47	41, 46	sylan9req 2496	. . 3 |- ( ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( P =/= Q /\ ( R e. A /\ -. R .<_ W ) /\ ( S e. A /\ -. S .<_ W ) ) ) /\ R = S ) -> ( F ` R ) = ( ( F ` R ) .\/ V ) )
48	24, 47	eqtr3d 2477	. 2 |- ( ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( P =/= Q /\ ( R e. A /\ -. R .<_ W ) /\ ( S e. A /\ -. S .<_ W ) ) ) /\ R = S ) -> ( ( F ` R ) .\/ ( F ` S ) ) = ( ( F ` R ) .\/ V ) )
49	3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 44	cdleme42k 34140	. . 3 |- ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( P =/= Q /\ ( R e. A /\ -. R .<_ W ) /\ ( S e. A /\ -. S .<_ W ) ) /\ R =/= S ) -> ( ( F ` R ) .\/ ( F ` S ) ) = ( ( F ` R ) .\/ V ) )
50	49	3expa 1187	. 2 |- ( ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( P =/= Q /\ ( R e. A /\ -. R .<_ W ) /\ ( S e. A /\ -. S .<_ W ) ) ) /\ R =/= S ) -> ( ( F ` R ) .\/ ( F ` S ) ) = ( ( F ` R ) .\/ V ) )
51	48, 50	pm2.61dane 2701	1 |- ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( P =/= Q /\ ( R e. A /\ -. R .<_ W ) /\ ( S e. A /\ -. S .<_ W ) ) ) -> ( ( F ` R ) .\/ ( F ` S ) ) = ( ( F ` R ) .\/ V ) )

Syntax hints:   -. wn 3   -> wi 4   /\ wa 369   /\ w3a 965   = wceq 1369   e. wcel 1756   =/= wne 2618   A.wral 2727   ifcif 3803   class class class wbr 4304   e. cmpt 4362   ` cfv 5430   iota_crio 6063  (class class class)co 6103   Basecbs 14186   lecple 14257   joincjn 15126   meetcmee 15127   0.cp0 15219   OLcol 32831   Atomscatm 32920   HLchlt 33007   LHypclh 33640

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-rep 4415  ax-sep 4425  ax-nul 4433  ax-pow 4482  ax-pr 4543  ax-un 6384  ax-riotaBAD 32616

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-ne 2620  df-nel 2621  df-ral 2732  df-rex 2733  df-reu 2734  df-rmo 2735  df-rab 2736  df-v 2986  df-sbc 3199  df-csb 3301  df-dif 3343  df-un 3345  df-in 3347  df-ss 3354  df-nul 3650  df-if 3804  df-pw 3874  df-sn 3890  df-pr 3892  df-op 3896  df-uni 4104  df-iun 4185  df-iin 4186  df-br 4305  df-opab 4363  df-mpt 4364  df-id 4648  df-xp 4858  df-rel 4859  df-cnv 4860  df-co 4861  df-dm 4862  df-rn 4863  df-res 4864  df-ima 4865  df-iota 5393  df-fun 5432  df-fn 5433  df-f 5434  df-f1 5435  df-fo 5436  df-f1o 5437  df-fv 5438  df-riota 6064  df-ov 6106  df-oprab 6107  df-mpt2 6108  df-1st 6589  df-2nd 6590  df-undef 6804  df-poset 15128  df-plt 15140  df-lub 15156  df-glb 15157  df-join 15158  df-meet 15159  df-p0 15221  df-p1 15222  df-lat 15228  df-clat 15290  df-oposet 32833  df-ol 32835  df-oml 32836  df-covers 32923  df-ats 32924  df-atl 32955  df-cvlat 32979  df-hlat 33008  df-llines 33154  df-lplanes 33155  df-lvols 33156  df-lines 33157  df-psubsp 33159  df-pmap 33160  df-padd 33452  df-lhyp 33644

This theorem is referenced by:  cdleme42keg  34142  cdleme42mN  34143  cdlemeg46fjv  34179