This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cdlemk19w

Description: Use a fixed element to eliminate P in cdlemk19u . (Contributed by NM, 1-Aug-2013)

Ref Expression
Hypotheses cdlemk6.b 
|- B = ( Base ` K )
cdlemk6.j 
|- .\/ = ( join ` K )
cdlemk6.m 
|- ./\ = ( meet ` K )
cdlemk6.o 
|- ._|_ = ( oc ` K )
cdlemk6.a 
|- A = ( Atoms ` K )
cdlemk6.h 
|- H = ( LHyp ` K )
cdlemk6.t 
|- T = ( ( LTrn ` K ) ` W )
cdlemk6.r 
|- R = ( ( trL ` K ) ` W )
cdlemk6.p 
|- P = ( ._|_ ` W )
cdlemk6.z 
|- Z = ( ( P .\/ ( R ` b ) ) ./\ ( ( N ` P ) .\/ ( R ` ( b o. `' F ) ) ) )
cdlemk6.y 
|- Y = ( ( P .\/ ( R ` g ) ) ./\ ( Z .\/ ( R ` ( g o. `' b ) ) ) )
cdlemk6.x 
|- X = ( iota_ z e. T A. b e. T ( ( b =/= ( _I |` B ) /\ ( R ` b ) =/= ( R ` F ) /\ ( R ` b ) =/= ( R ` g ) ) -> ( z ` P ) = Y ) )
cdlemk6.u 
|- U = ( g e. T |-> if ( F = N , g , X ) )
Assertion cdlemk19w 
|- ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ N e. T ) /\ ( R ` F ) = ( R ` N ) ) -> ( U ` F ) = N )

Proof

Step Hyp Ref Expression
1 cdlemk6.b 
 |-  B = ( Base ` K )
2 cdlemk6.j 
 |-  .\/ = ( join ` K )
3 cdlemk6.m 
 |-  ./\ = ( meet ` K )
4 cdlemk6.o 
 |-  ._|_ = ( oc ` K )
5 cdlemk6.a 
 |-  A = ( Atoms ` K )
6 cdlemk6.h 
 |-  H = ( LHyp ` K )
7 cdlemk6.t 
 |-  T = ( ( LTrn ` K ) ` W )
8 cdlemk6.r 
 |-  R = ( ( trL ` K ) ` W )
9 cdlemk6.p 
 |-  P = ( ._|_ ` W )
10 cdlemk6.z 
 |-  Z = ( ( P .\/ ( R ` b ) ) ./\ ( ( N ` P ) .\/ ( R ` ( b o. `' F ) ) ) )
11 cdlemk6.y 
 |-  Y = ( ( P .\/ ( R ` g ) ) ./\ ( Z .\/ ( R ` ( g o. `' b ) ) ) )
12 cdlemk6.x 
 |-  X = ( iota_ z e. T A. b e. T ( ( b =/= ( _I |` B ) /\ ( R ` b ) =/= ( R ` F ) /\ ( R ` b ) =/= ( R ` g ) ) -> ( z ` P ) = Y ) )
13 cdlemk6.u 
 |-  U = ( g e. T |-> if ( F = N , g , X ) )
14 3simpb 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ N e. T ) /\ ( R ` F ) = ( R ` N ) ) -> ( ( K e. HL /\ W e. H ) /\ ( R ` F ) = ( R ` N ) ) )
15 simp2 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ N e. T ) /\ ( R ` F ) = ( R ` N ) ) -> ( F e. T /\ N e. T ) )
16 eqid 
 |-  ( le ` K ) = ( le ` K )
17 16 4 5 6 lhpocnel 
 |-  ( ( K e. HL /\ W e. H ) -> ( ( ._|_ ` W ) e. A /\ -. ( ._|_ ` W ) ( le ` K ) W ) )
18 17 3ad2ant1 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ N e. T ) /\ ( R ` F ) = ( R ` N ) ) -> ( ( ._|_ ` W ) e. A /\ -. ( ._|_ ` W ) ( le ` K ) W ) )
19 9 eleq1i 
 |-  ( P e. A <-> ( ._|_ ` W ) e. A )
20 9 breq1i 
 |-  ( P ( le ` K ) W <-> ( ._|_ ` W ) ( le ` K ) W )
21 20 notbii 
 |-  ( -. P ( le ` K ) W <-> -. ( ._|_ ` W ) ( le ` K ) W )
22 19 21 anbi12i 
 |-  ( ( P e. A /\ -. P ( le ` K ) W ) <-> ( ( ._|_ ` W ) e. A /\ -. ( ._|_ ` W ) ( le ` K ) W ) )
23 18 22 sylibr 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ N e. T ) /\ ( R ` F ) = ( R ` N ) ) -> ( P e. A /\ -. P ( le ` K ) W ) )
24 1 16 2 3 5 6 7 8 10 11 12 13 cdlemk19u 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( R ` F ) = ( R ` N ) ) /\ ( F e. T /\ N e. T ) /\ ( P e. A /\ -. P ( le ` K ) W ) ) -> ( U ` F ) = N )
25 14 15 23 24 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ N e. T ) /\ ( R ` F ) = ( R ` N ) ) -> ( U ` F ) = N )