Theorem cdleme42ke 30967

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 1008	. . . . 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 964	. . . . . . 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 30921	. . . . . . 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 457	. . . . . 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 446	. . . . 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 29851	. . . . 5 |- ( ( K e. HL /\ ( F ` R ) e. A ) -> ( ( F ` R ) .\/ ( F ` R ) ) = ( F ` R ) )
21	1, 19, 20	syl2anc 643	. . . 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 5687	. . . . 5 |- ( R = S -> ( F ` R ) = ( F ` S ) )
23	22	oveq2d 6056	. . . 4 |- ( R = S -> ( ( F ` R ) .\/ ( F ` R ) ) = ( ( F ` R ) .\/ ( F ` S ) ) )
24	21, 23	sylan9req 2457	. . 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 1016	. . . . . . . . 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 29851	. . . . . . . . 9 |- ( ( K e. HL /\ R e. A ) -> ( R .\/ R ) = R )
27	1, 25, 26	syl2anc 643	. . . . . . . 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 6055	. . . . . . 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 960	. . . . . . . 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 2404	. . . . . . . . 9 |- ( 0. ` K ) = ( 0. ` K )
31	4, 6, 30, 7, 8	lhpmat 30512	. . . . . . . 8 |- ( ( ( K e. HL /\ W e. H ) /\ ( R e. A /\ -. R .<_ W ) ) -> ( R ./\ W ) = ( 0. ` K ) )
32	29, 2, 31	syl2anc 643	. . . . . . 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 2436	. . . . . 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 6056	. . . . 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 29844	. . . . . . 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 29772	. . . . . . 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 29708	. . . . . 6 |- ( ( K e. OL /\ ( F ` R ) e. B ) -> ( ( F ` R ) .\/ ( 0. ` K ) ) = ( F ` R ) )
40	36, 38, 39	syl2anc 643	. . . . 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 2436	. . . 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 6048	. . . . . . 7 |- ( R = S -> ( R .\/ R ) = ( R .\/ S ) )
43	42	oveq1d 6055	. . . . . 6 |- ( R = S -> ( ( R .\/ R ) ./\ W ) = ( ( R .\/ S ) ./\ W ) )
44		cdleme34e.v	. . . . . 6 |- V = ( ( R .\/ S ) ./\ W )
45	43, 44	syl6eqr 2454	. . . . 5 |- ( R = S -> ( ( R .\/ R ) ./\ W ) = V )
46	45	oveq2d 6056	. . . 4 |- ( R = S -> ( ( F ` R ) .\/ ( ( R .\/ R ) ./\ W ) ) = ( ( F ` R ) .\/ V ) )
47	41, 46	sylan9req 2457	. . 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 2438	. 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 30966	. . 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 1153	. 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 2645	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 359   /\ w3a 936   = wceq 1649   e. wcel 1721   =/= wne 2567   A.wral 2666   ifcif 3699   class class class wbr 4172   e. cmpt 4226   ` cfv 5413  (class class class)co 6040   iota_crio 6501   Basecbs 13424   lecple 13491   joincjn 14356   meetcmee 14357   0.cp0 14421   OLcol 29657   Atomscatm 29746   HLchlt 29833   LHypclh 30466

This theorem is referenced by:  cdleme42keg  30968  cdleme42mN  30969  cdlemeg46fjv  31005

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

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-nul 3589  df-if 3700  df-pw 3761  df-sn 3780  df-pr 3781  df-op 3783  df-uni 3976  df-iun 4055  df-iin 4056  df-br 4173  df-opab 4227  df-mpt 4228  df-id 4458  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-1st 6308  df-2nd 6309  df-undef 6502  df-riota 6508  df-poset 14358  df-plt 14370  df-lub 14386  df-glb 14387  df-join 14388  df-meet 14389  df-p0 14423  df-p1 14424  df-lat 14430  df-clat 14492  df-oposet 29659  df-ol 29661  df-oml 29662  df-covers 29749  df-ats 29750  df-atl 29781  df-cvlat 29805  df-hlat 29834  df-llines 29980  df-lplanes 29981  df-lvols 29982  df-lines 29983  df-psubsp 29985  df-pmap 29986  df-padd 30278  df-lhyp 30470