Metamath Proof Explorer

Theorem cdlemf

Description: Lemma F in Crawley p. 116. If u is an atom under w, there exists a translation whose trace is u. (Contributed by NM, 12-Apr-2013)

Ref Expression
Hypotheses cdlemf.l 
|- .<_ = ( le ` K )
cdlemf.a 
|- A = ( Atoms ` K )
cdlemf.h 
|- H = ( LHyp ` K )
cdlemf.t 
|- T = ( ( LTrn ` K ) ` W )
cdlemf.r 
|- R = ( ( trL ` K ) ` W )
Assertion cdlemf 
|- ( ( ( K e. HL /\ W e. H ) /\ ( U e. A /\ U .<_ W ) ) -> E. f e. T ( R ` f ) = U )

Proof

Step Hyp Ref Expression
1 cdlemf.l 
 |-  .<_ = ( le ` K )
2 cdlemf.a 
 |-  A = ( Atoms ` K )
3 cdlemf.h 
 |-  H = ( LHyp ` K )
4 cdlemf.t 
 |-  T = ( ( LTrn ` K ) ` W )
5 cdlemf.r 
 |-  R = ( ( trL ` K ) ` W )
6 eqid 
 |-  ( join ` K ) = ( join ` K )
7 eqid 
 |-  ( meet ` K ) = ( meet ` K )
8 1 6 2 3 7 cdlemf2 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( U e. A /\ U .<_ W ) ) -> E. p e. A E. q e. A ( ( -. p .<_ W /\ -. q .<_ W ) /\ U = ( ( p ( join ` K ) q ) ( meet ` K ) W ) ) )
9 simp1l 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. A /\ U .<_ W ) ) /\ ( p e. A /\ q e. A ) /\ ( ( -. p .<_ W /\ -. q .<_ W ) /\ U = ( ( p ( join ` K ) q ) ( meet ` K ) W ) ) ) -> ( K e. HL /\ W e. H ) )
10 simp2l 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. A /\ U .<_ W ) ) /\ ( p e. A /\ q e. A ) /\ ( ( -. p .<_ W /\ -. q .<_ W ) /\ U = ( ( p ( join ` K ) q ) ( meet ` K ) W ) ) ) -> p e. A )
11 simp3ll 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. A /\ U .<_ W ) ) /\ ( p e. A /\ q e. A ) /\ ( ( -. p .<_ W /\ -. q .<_ W ) /\ U = ( ( p ( join ` K ) q ) ( meet ` K ) W ) ) ) -> -. p .<_ W )
12 simp2r 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. A /\ U .<_ W ) ) /\ ( p e. A /\ q e. A ) /\ ( ( -. p .<_ W /\ -. q .<_ W ) /\ U = ( ( p ( join ` K ) q ) ( meet ` K ) W ) ) ) -> q e. A )
13 simp3lr 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. A /\ U .<_ W ) ) /\ ( p e. A /\ q e. A ) /\ ( ( -. p .<_ W /\ -. q .<_ W ) /\ U = ( ( p ( join ` K ) q ) ( meet ` K ) W ) ) ) -> -. q .<_ W )
14 1 2 3 4 cdleme50ex 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( p e. A /\ -. p .<_ W ) /\ ( q e. A /\ -. q .<_ W ) ) -> E. f e. T ( f ` p ) = q )
15 9 10 11 12 13 14 syl122anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. A /\ U .<_ W ) ) /\ ( p e. A /\ q e. A ) /\ ( ( -. p .<_ W /\ -. q .<_ W ) /\ U = ( ( p ( join ` K ) q ) ( meet ` K ) W ) ) ) -> E. f e. T ( f ` p ) = q )
16 simp3r 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. A /\ U .<_ W ) /\ ( p e. A /\ q e. A ) ) /\ ( ( -. p .<_ W /\ -. q .<_ W ) /\ U = ( ( p ( join ` K ) q ) ( meet ` K ) W ) ) /\ ( f e. T /\ ( f ` p ) = q ) ) -> ( f ` p ) = q )
17 16 oveq2d 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. A /\ U .<_ W ) /\ ( p e. A /\ q e. A ) ) /\ ( ( -. p .<_ W /\ -. q .<_ W ) /\ U = ( ( p ( join ` K ) q ) ( meet ` K ) W ) ) /\ ( f e. T /\ ( f ` p ) = q ) ) -> ( p ( join ` K ) ( f ` p ) ) = ( p ( join ` K ) q ) )
18 17 oveq1d 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. A /\ U .<_ W ) /\ ( p e. A /\ q e. A ) ) /\ ( ( -. p .<_ W /\ -. q .<_ W ) /\ U = ( ( p ( join ` K ) q ) ( meet ` K ) W ) ) /\ ( f e. T /\ ( f ` p ) = q ) ) -> ( ( p ( join ` K ) ( f ` p ) ) ( meet ` K ) W ) = ( ( p ( join ` K ) q ) ( meet ` K ) W ) )
19 simp11 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. A /\ U .<_ W ) /\ ( p e. A /\ q e. A ) ) /\ ( ( -. p .<_ W /\ -. q .<_ W ) /\ U = ( ( p ( join ` K ) q ) ( meet ` K ) W ) ) /\ ( f e. T /\ ( f ` p ) = q ) ) -> ( K e. HL /\ W e. H ) )
20 simp3l 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. A /\ U .<_ W ) /\ ( p e. A /\ q e. A ) ) /\ ( ( -. p .<_ W /\ -. q .<_ W ) /\ U = ( ( p ( join ` K ) q ) ( meet ` K ) W ) ) /\ ( f e. T /\ ( f ` p ) = q ) ) -> f e. T )
21 simp13l 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. A /\ U .<_ W ) /\ ( p e. A /\ q e. A ) ) /\ ( ( -. p .<_ W /\ -. q .<_ W ) /\ U = ( ( p ( join ` K ) q ) ( meet ` K ) W ) ) /\ ( f e. T /\ ( f ` p ) = q ) ) -> p e. A )
22 simp2ll 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. A /\ U .<_ W ) /\ ( p e. A /\ q e. A ) ) /\ ( ( -. p .<_ W /\ -. q .<_ W ) /\ U = ( ( p ( join ` K ) q ) ( meet ` K ) W ) ) /\ ( f e. T /\ ( f ` p ) = q ) ) -> -. p .<_ W )
23 1 6 7 2 3 4 5 trlval2 
 |-  ( ( ( K e. HL /\ W e. H ) /\ f e. T /\ ( p e. A /\ -. p .<_ W ) ) -> ( R ` f ) = ( ( p ( join ` K ) ( f ` p ) ) ( meet ` K ) W ) )
24 19 20 21 22 23 syl112anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. A /\ U .<_ W ) /\ ( p e. A /\ q e. A ) ) /\ ( ( -. p .<_ W /\ -. q .<_ W ) /\ U = ( ( p ( join ` K ) q ) ( meet ` K ) W ) ) /\ ( f e. T /\ ( f ` p ) = q ) ) -> ( R ` f ) = ( ( p ( join ` K ) ( f ` p ) ) ( meet ` K ) W ) )
25 simp2r 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. A /\ U .<_ W ) /\ ( p e. A /\ q e. A ) ) /\ ( ( -. p .<_ W /\ -. q .<_ W ) /\ U = ( ( p ( join ` K ) q ) ( meet ` K ) W ) ) /\ ( f e. T /\ ( f ` p ) = q ) ) -> U = ( ( p ( join ` K ) q ) ( meet ` K ) W ) )
26 18 24 25 3eqtr4d 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. A /\ U .<_ W ) /\ ( p e. A /\ q e. A ) ) /\ ( ( -. p .<_ W /\ -. q .<_ W ) /\ U = ( ( p ( join ` K ) q ) ( meet ` K ) W ) ) /\ ( f e. T /\ ( f ` p ) = q ) ) -> ( R ` f ) = U )
27 26 3exp 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( U e. A /\ U .<_ W ) /\ ( p e. A /\ q e. A ) ) -> ( ( ( -. p .<_ W /\ -. q .<_ W ) /\ U = ( ( p ( join ` K ) q ) ( meet ` K ) W ) ) -> ( ( f e. T /\ ( f ` p ) = q ) -> ( R ` f ) = U ) ) )
28 27 3expia 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( U e. A /\ U .<_ W ) ) -> ( ( p e. A /\ q e. A ) -> ( ( ( -. p .<_ W /\ -. q .<_ W ) /\ U = ( ( p ( join ` K ) q ) ( meet ` K ) W ) ) -> ( ( f e. T /\ ( f ` p ) = q ) -> ( R ` f ) = U ) ) ) )
29 28 3imp 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. A /\ U .<_ W ) ) /\ ( p e. A /\ q e. A ) /\ ( ( -. p .<_ W /\ -. q .<_ W ) /\ U = ( ( p ( join ` K ) q ) ( meet ` K ) W ) ) ) -> ( ( f e. T /\ ( f ` p ) = q ) -> ( R ` f ) = U ) )
30 29 expd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. A /\ U .<_ W ) ) /\ ( p e. A /\ q e. A ) /\ ( ( -. p .<_ W /\ -. q .<_ W ) /\ U = ( ( p ( join ` K ) q ) ( meet ` K ) W ) ) ) -> ( f e. T -> ( ( f ` p ) = q -> ( R ` f ) = U ) ) )
31 30 reximdvai 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. A /\ U .<_ W ) ) /\ ( p e. A /\ q e. A ) /\ ( ( -. p .<_ W /\ -. q .<_ W ) /\ U = ( ( p ( join ` K ) q ) ( meet ` K ) W ) ) ) -> ( E. f e. T ( f ` p ) = q -> E. f e. T ( R ` f ) = U ) )
32 15 31 mpd 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. A /\ U .<_ W ) ) /\ ( p e. A /\ q e. A ) /\ ( ( -. p .<_ W /\ -. q .<_ W ) /\ U = ( ( p ( join ` K ) q ) ( meet ` K ) W ) ) ) -> E. f e. T ( R ` f ) = U )
33 32 3exp 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( U e. A /\ U .<_ W ) ) -> ( ( p e. A /\ q e. A ) -> ( ( ( -. p .<_ W /\ -. q .<_ W ) /\ U = ( ( p ( join ` K ) q ) ( meet ` K ) W ) ) -> E. f e. T ( R ` f ) = U ) ) )
34 33 rexlimdvv 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( U e. A /\ U .<_ W ) ) -> ( E. p e. A E. q e. A ( ( -. p .<_ W /\ -. q .<_ W ) /\ U = ( ( p ( join ` K ) q ) ( meet ` K ) W ) ) -> E. f e. T ( R ` f ) = U ) )
35 8 34 mpd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( U e. A /\ U .<_ W ) ) -> E. f e. T ( R ` f ) = U )