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 )