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

Metamath Proof Explorer

Theorem llni2

Description: The join of two different atoms is a lattice line. (Contributed by NM, 26-Jun-2012)

Ref Expression
Hypotheses llni2.j 
|- .\/ = ( join ` K )
llni2.a 
|- A = ( Atoms ` K )
llni2.n 
|- N = ( LLines ` K )
Assertion llni2 
|- ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ P =/= Q ) -> ( P .\/ Q ) e. N )

Proof

Step Hyp Ref Expression
1 llni2.j 
 |-  .\/ = ( join ` K )
2 llni2.a 
 |-  A = ( Atoms ` K )
3 llni2.n 
 |-  N = ( LLines ` K )
4 simpl2 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ P =/= Q ) -> P e. A )
5 simpl3 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ P =/= Q ) -> Q e. A )
6 simpr 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ P =/= Q ) -> P =/= Q )
7 eqidd 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ P =/= Q ) -> ( P .\/ Q ) = ( P .\/ Q ) )
8 neeq1 
 |-  ( r = P -> ( r =/= s <-> P =/= s ) )
9 oveq1 
 |-  ( r = P -> ( r .\/ s ) = ( P .\/ s ) )
10 9 eqeq2d 
 |-  ( r = P -> ( ( P .\/ Q ) = ( r .\/ s ) <-> ( P .\/ Q ) = ( P .\/ s ) ) )
11 8 10 anbi12d 
 |-  ( r = P -> ( ( r =/= s /\ ( P .\/ Q ) = ( r .\/ s ) ) <-> ( P =/= s /\ ( P .\/ Q ) = ( P .\/ s ) ) ) )
12 neeq2 
 |-  ( s = Q -> ( P =/= s <-> P =/= Q ) )
13 oveq2 
 |-  ( s = Q -> ( P .\/ s ) = ( P .\/ Q ) )
14 13 eqeq2d 
 |-  ( s = Q -> ( ( P .\/ Q ) = ( P .\/ s ) <-> ( P .\/ Q ) = ( P .\/ Q ) ) )
15 12 14 anbi12d 
 |-  ( s = Q -> ( ( P =/= s /\ ( P .\/ Q ) = ( P .\/ s ) ) <-> ( P =/= Q /\ ( P .\/ Q ) = ( P .\/ Q ) ) ) )
16 11 15 rspc2ev 
 |-  ( ( P e. A /\ Q e. A /\ ( P =/= Q /\ ( P .\/ Q ) = ( P .\/ Q ) ) ) -> E. r e. A E. s e. A ( r =/= s /\ ( P .\/ Q ) = ( r .\/ s ) ) )
17 4 5 6 7 16 syl112anc 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ P =/= Q ) -> E. r e. A E. s e. A ( r =/= s /\ ( P .\/ Q ) = ( r .\/ s ) ) )
18 simpl1 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ P =/= Q ) -> K e. HL )
19 eqid 
 |-  ( Base ` K ) = ( Base ` K )
20 19 1 2 hlatjcl 
 |-  ( ( K e. HL /\ P e. A /\ Q e. A ) -> ( P .\/ Q ) e. ( Base ` K ) )
21 20 adantr 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ P =/= Q ) -> ( P .\/ Q ) e. ( Base ` K ) )
22 19 1 2 3 islln3 
 |-  ( ( K e. HL /\ ( P .\/ Q ) e. ( Base ` K ) ) -> ( ( P .\/ Q ) e. N <-> E. r e. A E. s e. A ( r =/= s /\ ( P .\/ Q ) = ( r .\/ s ) ) ) )
23 18 21 22 syl2anc 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ P =/= Q ) -> ( ( P .\/ Q ) e. N <-> E. r e. A E. s e. A ( r =/= s /\ ( P .\/ Q ) = ( r .\/ s ) ) ) )
24 17 23 mpbird 
 |-  ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ P =/= Q ) -> ( P .\/ Q ) e. N )