This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 3dim1lem5

Description: Lemma for 3dim1 . (Contributed by NM, 26-Jul-2012)

Ref Expression
Hypotheses 3dim0.j 
|- .\/ = ( join ` K )
3dim0.l 
|- .<_ = ( le ` K )
3dim0.a 
|- A = ( Atoms ` K )
Assertion 3dim1lem5 
|- ( ( ( u e. A /\ v e. A /\ w e. A ) /\ ( P =/= u /\ -. v .<_ ( P .\/ u ) /\ -. w .<_ ( ( P .\/ u ) .\/ v ) ) ) -> E. q e. A E. r e. A E. s e. A ( P =/= q /\ -. r .<_ ( P .\/ q ) /\ -. s .<_ ( ( P .\/ q ) .\/ r ) ) )

Proof

Step Hyp Ref Expression
1 3dim0.j 
 |-  .\/ = ( join ` K )
2 3dim0.l 
 |-  .<_ = ( le ` K )
3 3dim0.a 
 |-  A = ( Atoms ` K )
4 neeq2 
 |-  ( q = u -> ( P =/= q <-> P =/= u ) )
5 oveq2 
 |-  ( q = u -> ( P .\/ q ) = ( P .\/ u ) )
6 5 breq2d 
 |-  ( q = u -> ( r .<_ ( P .\/ q ) <-> r .<_ ( P .\/ u ) ) )
7 6 notbid 
 |-  ( q = u -> ( -. r .<_ ( P .\/ q ) <-> -. r .<_ ( P .\/ u ) ) )
8 5 oveq1d 
 |-  ( q = u -> ( ( P .\/ q ) .\/ r ) = ( ( P .\/ u ) .\/ r ) )
9 8 breq2d 
 |-  ( q = u -> ( s .<_ ( ( P .\/ q ) .\/ r ) <-> s .<_ ( ( P .\/ u ) .\/ r ) ) )
10 9 notbid 
 |-  ( q = u -> ( -. s .<_ ( ( P .\/ q ) .\/ r ) <-> -. s .<_ ( ( P .\/ u ) .\/ r ) ) )
11 4 7 10 3anbi123d 
 |-  ( q = u -> ( ( P =/= q /\ -. r .<_ ( P .\/ q ) /\ -. s .<_ ( ( P .\/ q ) .\/ r ) ) <-> ( P =/= u /\ -. r .<_ ( P .\/ u ) /\ -. s .<_ ( ( P .\/ u ) .\/ r ) ) ) )
12 breq1 
 |-  ( r = v -> ( r .<_ ( P .\/ u ) <-> v .<_ ( P .\/ u ) ) )
13 12 notbid 
 |-  ( r = v -> ( -. r .<_ ( P .\/ u ) <-> -. v .<_ ( P .\/ u ) ) )
14 oveq2 
 |-  ( r = v -> ( ( P .\/ u ) .\/ r ) = ( ( P .\/ u ) .\/ v ) )
15 14 breq2d 
 |-  ( r = v -> ( s .<_ ( ( P .\/ u ) .\/ r ) <-> s .<_ ( ( P .\/ u ) .\/ v ) ) )
16 15 notbid 
 |-  ( r = v -> ( -. s .<_ ( ( P .\/ u ) .\/ r ) <-> -. s .<_ ( ( P .\/ u ) .\/ v ) ) )
17 13 16 3anbi23d 
 |-  ( r = v -> ( ( P =/= u /\ -. r .<_ ( P .\/ u ) /\ -. s .<_ ( ( P .\/ u ) .\/ r ) ) <-> ( P =/= u /\ -. v .<_ ( P .\/ u ) /\ -. s .<_ ( ( P .\/ u ) .\/ v ) ) ) )
18 breq1 
 |-  ( s = w -> ( s .<_ ( ( P .\/ u ) .\/ v ) <-> w .<_ ( ( P .\/ u ) .\/ v ) ) )
19 18 notbid 
 |-  ( s = w -> ( -. s .<_ ( ( P .\/ u ) .\/ v ) <-> -. w .<_ ( ( P .\/ u ) .\/ v ) ) )
20 19 3anbi3d 
 |-  ( s = w -> ( ( P =/= u /\ -. v .<_ ( P .\/ u ) /\ -. s .<_ ( ( P .\/ u ) .\/ v ) ) <-> ( P =/= u /\ -. v .<_ ( P .\/ u ) /\ -. w .<_ ( ( P .\/ u ) .\/ v ) ) ) )
21 11 17 20 rspc3ev 
 |-  ( ( ( u e. A /\ v e. A /\ w e. A ) /\ ( P =/= u /\ -. v .<_ ( P .\/ u ) /\ -. w .<_ ( ( P .\/ u ) .\/ v ) ) ) -> E. q e. A E. r e. A E. s e. A ( P =/= q /\ -. r .<_ ( P .\/ q ) /\ -. s .<_ ( ( P .\/ q ) .\/ r ) ) )