Metamath Proof Explorer

Theorem 4atexlemswapqr

Description: Lemma for 4atexlem7 . Swap Q and R , so that theorems involving C can be reused for D . Note that U must be expanded because it involves Q . (Contributed by NM, 25-Nov-2012)

Ref Expression
Hypotheses 4thatlem.ph 
|- ( ph <-> ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( S e. A /\ ( R e. A /\ -. R .<_ W /\ ( P .\/ R ) = ( Q .\/ R ) ) /\ ( T e. A /\ ( U .\/ T ) = ( V .\/ T ) ) ) /\ ( P =/= Q /\ -. S .<_ ( P .\/ Q ) ) ) )
4thatlemslps.l 
|- .<_ = ( le ` K )
4thatlemslps.j 
|- .\/ = ( join ` K )
4thatlemslps.a 
|- A = ( Atoms ` K )
4thatlemsw.u 
|- U = ( ( P .\/ Q ) ./\ W )
Assertion 4atexlemswapqr 
|- ( ph -> ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) /\ ( S e. A /\ ( Q e. A /\ -. Q .<_ W /\ ( P .\/ Q ) = ( R .\/ Q ) ) /\ ( T e. A /\ ( ( ( P .\/ R ) ./\ W ) .\/ T ) = ( V .\/ T ) ) ) /\ ( P =/= R /\ -. S .<_ ( P .\/ R ) ) ) )

Proof

Step Hyp Ref Expression
1 4thatlem.ph 
 |-  ( ph <-> ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( S e. A /\ ( R e. A /\ -. R .<_ W /\ ( P .\/ R ) = ( Q .\/ R ) ) /\ ( T e. A /\ ( U .\/ T ) = ( V .\/ T ) ) ) /\ ( P =/= Q /\ -. S .<_ ( P .\/ Q ) ) ) )
2 4thatlemslps.l 
 |-  .<_ = ( le ` K )
3 4thatlemslps.j 
 |-  .\/ = ( join ` K )
4 4thatlemslps.a 
 |-  A = ( Atoms ` K )
5 4thatlemsw.u 
 |-  U = ( ( P .\/ Q ) ./\ W )
6 simp11 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( S e. A /\ ( R e. A /\ -. R .<_ W /\ ( P .\/ R ) = ( Q .\/ R ) ) /\ ( T e. A /\ ( U .\/ T ) = ( V .\/ T ) ) ) /\ ( P =/= Q /\ -. S .<_ ( P .\/ Q ) ) ) -> ( K e. HL /\ W e. H ) )
7 1 6 sylbi 
 |-  ( ph -> ( K e. HL /\ W e. H ) )
8 1 4atexlempw 
 |-  ( ph -> ( P e. A /\ -. P .<_ W ) )
9 simp22 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( S e. A /\ ( R e. A /\ -. R .<_ W /\ ( P .\/ R ) = ( Q .\/ R ) ) /\ ( T e. A /\ ( U .\/ T ) = ( V .\/ T ) ) ) /\ ( P =/= Q /\ -. S .<_ ( P .\/ Q ) ) ) -> ( R e. A /\ -. R .<_ W /\ ( P .\/ R ) = ( Q .\/ R ) ) )
10 3simpa 
 |-  ( ( R e. A /\ -. R .<_ W /\ ( P .\/ R ) = ( Q .\/ R ) ) -> ( R e. A /\ -. R .<_ W ) )
11 9 10 syl 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( S e. A /\ ( R e. A /\ -. R .<_ W /\ ( P .\/ R ) = ( Q .\/ R ) ) /\ ( T e. A /\ ( U .\/ T ) = ( V .\/ T ) ) ) /\ ( P =/= Q /\ -. S .<_ ( P .\/ Q ) ) ) -> ( R e. A /\ -. R .<_ W ) )
12 1 11 sylbi 
 |-  ( ph -> ( R e. A /\ -. R .<_ W ) )
13 7 8 12 3jca 
 |-  ( ph -> ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) )
14 1 4atexlems 
 |-  ( ph -> S e. A )
15 1 4atexlemq 
 |-  ( ph -> Q e. A )
16 simp13r 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( S e. A /\ ( R e. A /\ -. R .<_ W /\ ( P .\/ R ) = ( Q .\/ R ) ) /\ ( T e. A /\ ( U .\/ T ) = ( V .\/ T ) ) ) /\ ( P =/= Q /\ -. S .<_ ( P .\/ Q ) ) ) -> -. Q .<_ W )
17 1 16 sylbi 
 |-  ( ph -> -. Q .<_ W )
18 1 4atexlemkc 
 |-  ( ph -> K e. CvLat )
19 1 4atexlemp 
 |-  ( ph -> P e. A )
20 12 simpld 
 |-  ( ph -> R e. A )
21 1 4atexlempnq 
 |-  ( ph -> P =/= Q )
22 simp223 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( S e. A /\ ( R e. A /\ -. R .<_ W /\ ( P .\/ R ) = ( Q .\/ R ) ) /\ ( T e. A /\ ( U .\/ T ) = ( V .\/ T ) ) ) /\ ( P =/= Q /\ -. S .<_ ( P .\/ Q ) ) ) -> ( P .\/ R ) = ( Q .\/ R ) )
23 1 22 sylbi 
 |-  ( ph -> ( P .\/ R ) = ( Q .\/ R ) )
24 4 3 cvlsupr7 
 |-  ( ( K e. CvLat /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P =/= Q /\ ( P .\/ R ) = ( Q .\/ R ) ) ) -> ( P .\/ Q ) = ( R .\/ Q ) )
25 18 19 15 20 21 23 24 syl132anc 
 |-  ( ph -> ( P .\/ Q ) = ( R .\/ Q ) )
26 15 17 25 3jca 
 |-  ( ph -> ( Q e. A /\ -. Q .<_ W /\ ( P .\/ Q ) = ( R .\/ Q ) ) )
27 1 4atexlemt 
 |-  ( ph -> T e. A )
28 4 3 cvlsupr8 
 |-  ( ( K e. CvLat /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P =/= Q /\ ( P .\/ R ) = ( Q .\/ R ) ) ) -> ( P .\/ Q ) = ( P .\/ R ) )
29 18 19 15 20 21 23 28 syl132anc 
 |-  ( ph -> ( P .\/ Q ) = ( P .\/ R ) )
30 29 oveq1d 
 |-  ( ph -> ( ( P .\/ Q ) ./\ W ) = ( ( P .\/ R ) ./\ W ) )
31 5 30 syl5eq 
 |-  ( ph -> U = ( ( P .\/ R ) ./\ W ) )
32 31 oveq1d 
 |-  ( ph -> ( U .\/ T ) = ( ( ( P .\/ R ) ./\ W ) .\/ T ) )
33 1 4atexlemutvt 
 |-  ( ph -> ( U .\/ T ) = ( V .\/ T ) )
34 32 33 eqtr3d 
 |-  ( ph -> ( ( ( P .\/ R ) ./\ W ) .\/ T ) = ( V .\/ T ) )
35 27 34 jca 
 |-  ( ph -> ( T e. A /\ ( ( ( P .\/ R ) ./\ W ) .\/ T ) = ( V .\/ T ) ) )
36 14 26 35 3jca 
 |-  ( ph -> ( S e. A /\ ( Q e. A /\ -. Q .<_ W /\ ( P .\/ Q ) = ( R .\/ Q ) ) /\ ( T e. A /\ ( ( ( P .\/ R ) ./\ W ) .\/ T ) = ( V .\/ T ) ) ) )
37 4 3 cvlsupr5 
 |-  ( ( K e. CvLat /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P =/= Q /\ ( P .\/ R ) = ( Q .\/ R ) ) ) -> R =/= P )
38 37 necomd 
 |-  ( ( K e. CvLat /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P =/= Q /\ ( P .\/ R ) = ( Q .\/ R ) ) ) -> P =/= R )
39 18 19 15 20 21 23 38 syl132anc 
 |-  ( ph -> P =/= R )
40 1 4atexlemnslpq 
 |-  ( ph -> -. S .<_ ( P .\/ Q ) )
41 29 eqcomd 
 |-  ( ph -> ( P .\/ R ) = ( P .\/ Q ) )
42 41 breq2d 
 |-  ( ph -> ( S .<_ ( P .\/ R ) <-> S .<_ ( P .\/ Q ) ) )
43 40 42 mtbird 
 |-  ( ph -> -. S .<_ ( P .\/ R ) )
44 39 43 jca 
 |-  ( ph -> ( P =/= R /\ -. S .<_ ( P .\/ R ) ) )
45 13 36 44 3jca 
 |-  ( ph -> ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) /\ ( S e. A /\ ( Q e. A /\ -. Q .<_ W /\ ( P .\/ Q ) = ( R .\/ Q ) ) /\ ( T e. A /\ ( ( ( P .\/ R ) ./\ W ) .\/ T ) = ( V .\/ T ) ) ) /\ ( P =/= R /\ -. S .<_ ( P .\/ R ) ) ) )