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 )