Metamath Proof Explorer

Theorem 4atex2

Description: More general version of 4atex for a line S .\/ T not necessarily connected to P .\/ Q . (Contributed by NM, 27-May-2013)

Ref Expression
Hypotheses 4that.l 
|- .<_ = ( le ` K )
4that.j 
|- .\/ = ( join ` K )
4that.a 
|- A = ( Atoms ` K )
4that.h 
|- H = ( LHyp ` K )
Assertion 4atex2 
|- ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ -. S .<_ W ) ) /\ ( P =/= Q /\ T e. A /\ E. r e. A ( -. r .<_ W /\ ( P .\/ r ) = ( Q .\/ r ) ) ) ) -> E. z e. A ( -. z .<_ W /\ ( S .\/ z ) = ( T .\/ z ) ) )

Proof

Step Hyp Ref Expression
1 4that.l 
 |-  .<_ = ( le ` K )
2 4that.j 
 |-  .\/ = ( join ` K )
3 4that.a 
 |-  A = ( Atoms ` K )
4 4that.h 
 |-  H = ( LHyp ` K )
5 oveq1 
 |-  ( S = P -> ( S .\/ z ) = ( P .\/ z ) )
6 5 eqeq1d 
 |-  ( S = P -> ( ( S .\/ z ) = ( T .\/ z ) <-> ( P .\/ z ) = ( T .\/ z ) ) )
7 6 anbi2d 
 |-  ( S = P -> ( ( -. z .<_ W /\ ( S .\/ z ) = ( T .\/ z ) ) <-> ( -. z .<_ W /\ ( P .\/ z ) = ( T .\/ z ) ) ) )
8 7 rexbidv 
 |-  ( S = P -> ( E. z e. A ( -. z .<_ W /\ ( S .\/ z ) = ( T .\/ z ) ) <-> E. z e. A ( -. z .<_ W /\ ( P .\/ z ) = ( T .\/ z ) ) ) )
9 simpl1 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ -. S .<_ W ) ) /\ ( P =/= Q /\ T e. A /\ E. r e. A ( -. r .<_ W /\ ( P .\/ r ) = ( Q .\/ r ) ) ) ) /\ S =/= P ) -> ( K e. HL /\ W e. H ) )
10 simpl23 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ -. S .<_ W ) ) /\ ( P =/= Q /\ T e. A /\ E. r e. A ( -. r .<_ W /\ ( P .\/ r ) = ( Q .\/ r ) ) ) ) /\ S =/= P ) -> ( S e. A /\ -. S .<_ W ) )
11 simpl21 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ -. S .<_ W ) ) /\ ( P =/= Q /\ T e. A /\ E. r e. A ( -. r .<_ W /\ ( P .\/ r ) = ( Q .\/ r ) ) ) ) /\ S =/= P ) -> ( P e. A /\ -. P .<_ W ) )
12 simpl32 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ -. S .<_ W ) ) /\ ( P =/= Q /\ T e. A /\ E. r e. A ( -. r .<_ W /\ ( P .\/ r ) = ( Q .\/ r ) ) ) ) /\ S =/= P ) -> T e. A )
13 simpr 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ -. S .<_ W ) ) /\ ( P =/= Q /\ T e. A /\ E. r e. A ( -. r .<_ W /\ ( P .\/ r ) = ( Q .\/ r ) ) ) ) /\ S =/= P ) -> S =/= P )
14 simpl22 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ -. S .<_ W ) ) /\ ( P =/= Q /\ T e. A /\ E. r e. A ( -. r .<_ W /\ ( P .\/ r ) = ( Q .\/ r ) ) ) ) /\ S =/= P ) -> ( Q e. A /\ -. Q .<_ W ) )
15 simp23l 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ -. S .<_ W ) ) /\ ( P =/= Q /\ T e. A /\ E. r e. A ( -. r .<_ W /\ ( P .\/ r ) = ( Q .\/ r ) ) ) ) -> S e. A )
16 15 adantr 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ -. S .<_ W ) ) /\ ( P =/= Q /\ T e. A /\ E. r e. A ( -. r .<_ W /\ ( P .\/ r ) = ( Q .\/ r ) ) ) ) /\ S =/= P ) -> S e. A )
17 simpl31 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ -. S .<_ W ) ) /\ ( P =/= Q /\ T e. A /\ E. r e. A ( -. r .<_ W /\ ( P .\/ r ) = ( Q .\/ r ) ) ) ) /\ S =/= P ) -> P =/= Q )
18 simpl33 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ -. S .<_ W ) ) /\ ( P =/= Q /\ T e. A /\ E. r e. A ( -. r .<_ W /\ ( P .\/ r ) = ( Q .\/ r ) ) ) ) /\ S =/= P ) -> E. r e. A ( -. r .<_ W /\ ( P .\/ r ) = ( Q .\/ r ) ) )
19 1 2 3 4 4atex 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ S e. A ) /\ ( P =/= Q /\ E. r e. A ( -. r .<_ W /\ ( P .\/ r ) = ( Q .\/ r ) ) ) ) -> E. y e. A ( -. y .<_ W /\ ( P .\/ y ) = ( S .\/ y ) ) )
20 9 11 14 16 17 18 19 syl132anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ -. S .<_ W ) ) /\ ( P =/= Q /\ T e. A /\ E. r e. A ( -. r .<_ W /\ ( P .\/ r ) = ( Q .\/ r ) ) ) ) /\ S =/= P ) -> E. y e. A ( -. y .<_ W /\ ( P .\/ y ) = ( S .\/ y ) ) )
21 eqcom 
 |-  ( ( P .\/ y ) = ( S .\/ y ) <-> ( S .\/ y ) = ( P .\/ y ) )
22 21 anbi2i 
 |-  ( ( -. y .<_ W /\ ( P .\/ y ) = ( S .\/ y ) ) <-> ( -. y .<_ W /\ ( S .\/ y ) = ( P .\/ y ) ) )
23 22 rexbii 
 |-  ( E. y e. A ( -. y .<_ W /\ ( P .\/ y ) = ( S .\/ y ) ) <-> E. y e. A ( -. y .<_ W /\ ( S .\/ y ) = ( P .\/ y ) ) )
24 20 23 sylib 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ -. S .<_ W ) ) /\ ( P =/= Q /\ T e. A /\ E. r e. A ( -. r .<_ W /\ ( P .\/ r ) = ( Q .\/ r ) ) ) ) /\ S =/= P ) -> E. y e. A ( -. y .<_ W /\ ( S .\/ y ) = ( P .\/ y ) ) )
25 1 2 3 4 4atex 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( S e. A /\ -. S .<_ W ) /\ ( P e. A /\ -. P .<_ W ) /\ T e. A ) /\ ( S =/= P /\ E. y e. A ( -. y .<_ W /\ ( S .\/ y ) = ( P .\/ y ) ) ) ) -> E. z e. A ( -. z .<_ W /\ ( S .\/ z ) = ( T .\/ z ) ) )
26 9 10 11 12 13 24 25 syl132anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ -. S .<_ W ) ) /\ ( P =/= Q /\ T e. A /\ E. r e. A ( -. r .<_ W /\ ( P .\/ r ) = ( Q .\/ r ) ) ) ) /\ S =/= P ) -> E. z e. A ( -. z .<_ W /\ ( S .\/ z ) = ( T .\/ z ) ) )
27 simp1 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ -. S .<_ W ) ) /\ ( P =/= Q /\ T e. A /\ E. r e. A ( -. r .<_ W /\ ( P .\/ r ) = ( Q .\/ r ) ) ) ) -> ( K e. HL /\ W e. H ) )
28 simp21 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ -. S .<_ W ) ) /\ ( P =/= Q /\ T e. A /\ E. r e. A ( -. r .<_ W /\ ( P .\/ r ) = ( Q .\/ r ) ) ) ) -> ( P e. A /\ -. P .<_ W ) )
29 simp22 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ -. S .<_ W ) ) /\ ( P =/= Q /\ T e. A /\ E. r e. A ( -. r .<_ W /\ ( P .\/ r ) = ( Q .\/ r ) ) ) ) -> ( Q e. A /\ -. Q .<_ W ) )
30 simp32 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ -. S .<_ W ) ) /\ ( P =/= Q /\ T e. A /\ E. r e. A ( -. r .<_ W /\ ( P .\/ r ) = ( Q .\/ r ) ) ) ) -> T e. A )
31 simp31 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ -. S .<_ W ) ) /\ ( P =/= Q /\ T e. A /\ E. r e. A ( -. r .<_ W /\ ( P .\/ r ) = ( Q .\/ r ) ) ) ) -> P =/= Q )
32 simp33 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ -. S .<_ W ) ) /\ ( P =/= Q /\ T e. A /\ E. r e. A ( -. r .<_ W /\ ( P .\/ r ) = ( Q .\/ r ) ) ) ) -> E. r e. A ( -. r .<_ W /\ ( P .\/ r ) = ( Q .\/ r ) ) )
33 1 2 3 4 4atex 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ T e. A ) /\ ( P =/= Q /\ E. r e. A ( -. r .<_ W /\ ( P .\/ r ) = ( Q .\/ r ) ) ) ) -> E. z e. A ( -. z .<_ W /\ ( P .\/ z ) = ( T .\/ z ) ) )
34 27 28 29 30 31 32 33 syl132anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ -. S .<_ W ) ) /\ ( P =/= Q /\ T e. A /\ E. r e. A ( -. r .<_ W /\ ( P .\/ r ) = ( Q .\/ r ) ) ) ) -> E. z e. A ( -. z .<_ W /\ ( P .\/ z ) = ( T .\/ z ) ) )
35 8 26 34 pm2.61ne 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ -. S .<_ W ) ) /\ ( P =/= Q /\ T e. A /\ E. r e. A ( -. r .<_ W /\ ( P .\/ r ) = ( Q .\/ r ) ) ) ) -> E. z e. A ( -. z .<_ W /\ ( S .\/ z ) = ( T .\/ z ) ) )