Metamath Proof Explorer

Theorem 2atmat

Description: The meet of two intersecting lines (expressed as joins of atoms) is an atom. (Contributed by NM, 21-Nov-2012)

Ref Expression
Hypotheses 2atmat.l 
|- .<_ = ( le ` K )
2atmat.j 
|- .\/ = ( join ` K )
2atmat.m 
|- ./\ = ( meet ` K )
2atmat.a 
|- A = ( Atoms ` K )
Assertion 2atmat 
|- ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ P =/= Q ) /\ ( R =/= S /\ -. R .<_ ( P .\/ Q ) /\ S .<_ ( ( P .\/ Q ) .\/ R ) ) ) -> ( ( P .\/ Q ) ./\ ( R .\/ S ) ) e. A )

Proof

Step Hyp Ref Expression
1 2atmat.l 
 |-  .<_ = ( le ` K )
2 2atmat.j 
 |-  .\/ = ( join ` K )
3 2atmat.m 
 |-  ./\ = ( meet ` K )
4 2atmat.a 
 |-  A = ( Atoms ` K )
5 simp11 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ P =/= Q ) /\ ( R =/= S /\ -. R .<_ ( P .\/ Q ) /\ S .<_ ( ( P .\/ Q ) .\/ R ) ) ) -> K e. HL )
6 5 hllatd 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ P =/= Q ) /\ ( R =/= S /\ -. R .<_ ( P .\/ Q ) /\ S .<_ ( ( P .\/ Q ) .\/ R ) ) ) -> K e. Lat )
7 eqid 
 |-  ( Base ` K ) = ( Base ` K )
8 7 2 4 hlatjcl 
 |-  ( ( K e. HL /\ P e. A /\ Q e. A ) -> ( P .\/ Q ) e. ( Base ` K ) )
9 8 3ad2ant1 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ P =/= Q ) /\ ( R =/= S /\ -. R .<_ ( P .\/ Q ) /\ S .<_ ( ( P .\/ Q ) .\/ R ) ) ) -> ( P .\/ Q ) e. ( Base ` K ) )
10 simp21 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ P =/= Q ) /\ ( R =/= S /\ -. R .<_ ( P .\/ Q ) /\ S .<_ ( ( P .\/ Q ) .\/ R ) ) ) -> R e. A )
11 7 4 atbase 
 |-  ( R e. A -> R e. ( Base ` K ) )
12 10 11 syl 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ P =/= Q ) /\ ( R =/= S /\ -. R .<_ ( P .\/ Q ) /\ S .<_ ( ( P .\/ Q ) .\/ R ) ) ) -> R e. ( Base ` K ) )
13 simp22 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ P =/= Q ) /\ ( R =/= S /\ -. R .<_ ( P .\/ Q ) /\ S .<_ ( ( P .\/ Q ) .\/ R ) ) ) -> S e. A )
14 7 4 atbase 
 |-  ( S e. A -> S e. ( Base ` K ) )
15 13 14 syl 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ P =/= Q ) /\ ( R =/= S /\ -. R .<_ ( P .\/ Q ) /\ S .<_ ( ( P .\/ Q ) .\/ R ) ) ) -> S e. ( Base ` K ) )
16 7 2 latjass 
 |-  ( ( K e. Lat /\ ( ( P .\/ Q ) e. ( Base ` K ) /\ R e. ( Base ` K ) /\ S e. ( Base ` K ) ) ) -> ( ( ( P .\/ Q ) .\/ R ) .\/ S ) = ( ( P .\/ Q ) .\/ ( R .\/ S ) ) )
17 6 9 12 15 16 syl13anc 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ P =/= Q ) /\ ( R =/= S /\ -. R .<_ ( P .\/ Q ) /\ S .<_ ( ( P .\/ Q ) .\/ R ) ) ) -> ( ( ( P .\/ Q ) .\/ R ) .\/ S ) = ( ( P .\/ Q ) .\/ ( R .\/ S ) ) )
18 simp33 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ P =/= Q ) /\ ( R =/= S /\ -. R .<_ ( P .\/ Q ) /\ S .<_ ( ( P .\/ Q ) .\/ R ) ) ) -> S .<_ ( ( P .\/ Q ) .\/ R ) )
19 7 2 latjcl 
 |-  ( ( K e. Lat /\ ( P .\/ Q ) e. ( Base ` K ) /\ R e. ( Base ` K ) ) -> ( ( P .\/ Q ) .\/ R ) e. ( Base ` K ) )
20 6 9 12 19 syl3anc 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ P =/= Q ) /\ ( R =/= S /\ -. R .<_ ( P .\/ Q ) /\ S .<_ ( ( P .\/ Q ) .\/ R ) ) ) -> ( ( P .\/ Q ) .\/ R ) e. ( Base ` K ) )
21 7 1 2 latleeqj2 
 |-  ( ( K e. Lat /\ S e. ( Base ` K ) /\ ( ( P .\/ Q ) .\/ R ) e. ( Base ` K ) ) -> ( S .<_ ( ( P .\/ Q ) .\/ R ) <-> ( ( ( P .\/ Q ) .\/ R ) .\/ S ) = ( ( P .\/ Q ) .\/ R ) ) )
22 6 15 20 21 syl3anc 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ P =/= Q ) /\ ( R =/= S /\ -. R .<_ ( P .\/ Q ) /\ S .<_ ( ( P .\/ Q ) .\/ R ) ) ) -> ( S .<_ ( ( P .\/ Q ) .\/ R ) <-> ( ( ( P .\/ Q ) .\/ R ) .\/ S ) = ( ( P .\/ Q ) .\/ R ) ) )
23 18 22 mpbid 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ P =/= Q ) /\ ( R =/= S /\ -. R .<_ ( P .\/ Q ) /\ S .<_ ( ( P .\/ Q ) .\/ R ) ) ) -> ( ( ( P .\/ Q ) .\/ R ) .\/ S ) = ( ( P .\/ Q ) .\/ R ) )
24 17 23 eqtr3d 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ P =/= Q ) /\ ( R =/= S /\ -. R .<_ ( P .\/ Q ) /\ S .<_ ( ( P .\/ Q ) .\/ R ) ) ) -> ( ( P .\/ Q ) .\/ ( R .\/ S ) ) = ( ( P .\/ Q ) .\/ R ) )
25 simp23 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ P =/= Q ) /\ ( R =/= S /\ -. R .<_ ( P .\/ Q ) /\ S .<_ ( ( P .\/ Q ) .\/ R ) ) ) -> P =/= Q )
26 simp32 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ P =/= Q ) /\ ( R =/= S /\ -. R .<_ ( P .\/ Q ) /\ S .<_ ( ( P .\/ Q ) .\/ R ) ) ) -> -. R .<_ ( P .\/ Q ) )
27 simp12 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ P =/= Q ) /\ ( R =/= S /\ -. R .<_ ( P .\/ Q ) /\ S .<_ ( ( P .\/ Q ) .\/ R ) ) ) -> P e. A )
28 simp13 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ P =/= Q ) /\ ( R =/= S /\ -. R .<_ ( P .\/ Q ) /\ S .<_ ( ( P .\/ Q ) .\/ R ) ) ) -> Q e. A )
29 eqid 
 |-  ( LPlanes ` K ) = ( LPlanes ` K )
30 1 2 4 29 islpln2a 
 |-  ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) ) -> ( ( ( P .\/ Q ) .\/ R ) e. ( LPlanes ` K ) <-> ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) )
31 5 27 28 10 30 syl13anc 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ P =/= Q ) /\ ( R =/= S /\ -. R .<_ ( P .\/ Q ) /\ S .<_ ( ( P .\/ Q ) .\/ R ) ) ) -> ( ( ( P .\/ Q ) .\/ R ) e. ( LPlanes ` K ) <-> ( P =/= Q /\ -. R .<_ ( P .\/ Q ) ) ) )
32 25 26 31 mpbir2and 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ P =/= Q ) /\ ( R =/= S /\ -. R .<_ ( P .\/ Q ) /\ S .<_ ( ( P .\/ Q ) .\/ R ) ) ) -> ( ( P .\/ Q ) .\/ R ) e. ( LPlanes ` K ) )
33 24 32 eqeltrd 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ P =/= Q ) /\ ( R =/= S /\ -. R .<_ ( P .\/ Q ) /\ S .<_ ( ( P .\/ Q ) .\/ R ) ) ) -> ( ( P .\/ Q ) .\/ ( R .\/ S ) ) e. ( LPlanes ` K ) )
34 eqid 
 |-  ( LLines ` K ) = ( LLines ` K )
35 2 4 34 llni2 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ P =/= Q ) -> ( P .\/ Q ) e. ( LLines ` K ) )
36 5 27 28 25 35 syl31anc 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ P =/= Q ) /\ ( R =/= S /\ -. R .<_ ( P .\/ Q ) /\ S .<_ ( ( P .\/ Q ) .\/ R ) ) ) -> ( P .\/ Q ) e. ( LLines ` K ) )
37 simp31 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ P =/= Q ) /\ ( R =/= S /\ -. R .<_ ( P .\/ Q ) /\ S .<_ ( ( P .\/ Q ) .\/ R ) ) ) -> R =/= S )
38 2 4 34 llni2 
 |-  ( ( ( K e. HL /\ R e. A /\ S e. A ) /\ R =/= S ) -> ( R .\/ S ) e. ( LLines ` K ) )
39 5 10 13 37 38 syl31anc 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ P =/= Q ) /\ ( R =/= S /\ -. R .<_ ( P .\/ Q ) /\ S .<_ ( ( P .\/ Q ) .\/ R ) ) ) -> ( R .\/ S ) e. ( LLines ` K ) )
40 2 3 4 34 29 2llnmj 
 |-  ( ( K e. HL /\ ( P .\/ Q ) e. ( LLines ` K ) /\ ( R .\/ S ) e. ( LLines ` K ) ) -> ( ( ( P .\/ Q ) ./\ ( R .\/ S ) ) e. A <-> ( ( P .\/ Q ) .\/ ( R .\/ S ) ) e. ( LPlanes ` K ) ) )
41 5 36 39 40 syl3anc 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ P =/= Q ) /\ ( R =/= S /\ -. R .<_ ( P .\/ Q ) /\ S .<_ ( ( P .\/ Q ) .\/ R ) ) ) -> ( ( ( P .\/ Q ) ./\ ( R .\/ S ) ) e. A <-> ( ( P .\/ Q ) .\/ ( R .\/ S ) ) e. ( LPlanes ` K ) ) )
42 33 41 mpbird 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A /\ P =/= Q ) /\ ( R =/= S /\ -. R .<_ ( P .\/ Q ) /\ S .<_ ( ( P .\/ Q ) .\/ R ) ) ) -> ( ( P .\/ Q ) ./\ ( R .\/ S ) ) e. A )