Metamath Proof Explorer

Theorem cdlemk56w

Description: Use a fixed element to eliminate P in cdlemk56 . (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 ) )
cdlemk6.e 
|- E = ( ( TEndo ` K ) ` W )
Assertion cdlemk56w 
|- ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ N e. T ) /\ ( R ` F ) = ( R ` N ) ) -> ( U e. E /\ ( 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 cdlemk6.e 
 |-  E = ( ( TEndo ` K ) ` W )
15 simp1 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ N e. T ) /\ ( R ` F ) = ( R ` N ) ) -> ( K e. HL /\ W e. H ) )
16 simp2l 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ N e. T ) /\ ( R ` F ) = ( R ` N ) ) -> F e. T )
17 simp2r 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ N e. T ) /\ ( R ` F ) = ( R ` N ) ) -> N e. T )
18 simp3 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ N e. T ) /\ ( R ` F ) = ( R ` N ) ) -> ( R ` F ) = ( R ` N ) )
19 eqid 
 |-  ( le ` K ) = ( le ` K )
20 4 fveq1i 
 |-  ( ._|_ ` W ) = ( ( oc ` K ) ` W )
21 9 20 eqtri 
 |-  P = ( ( oc ` K ) ` W )
22 19 5 6 21 lhpocnel2 
 |-  ( ( K e. HL /\ W e. H ) -> ( P e. A /\ -. P ( le ` K ) W ) )
23 22 3ad2ant1 
 |-  ( ( ( 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 19 2 3 5 6 7 8 10 11 12 13 14 cdlemk56 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ N e. T ) /\ ( R ` F ) = ( R ` N ) /\ ( P e. A /\ -. P ( le ` K ) W ) ) -> U e. E )
25 15 16 17 18 23 24 syl311anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ N e. T ) /\ ( R ` F ) = ( R ` N ) ) -> U e. E )
26 1 2 3 4 5 6 7 8 9 10 11 12 13 cdlemk19w 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ N e. T ) /\ ( R ` F ) = ( R ` N ) ) -> ( U ` F ) = N )
27 25 26 jca 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ N e. T ) /\ ( R ` F ) = ( R ` N ) ) -> ( U e. E /\ ( U ` F ) = N ) )