Metamath Proof Explorer

Theorem llnexchb2

Description: Line exchange property (compare cvlatexchb2 for atoms). (Contributed by NM, 17-Nov-2012)

Ref Expression
Hypotheses llnexch.l 
|- .<_ = ( le ` K )
llnexch.j 
|- .\/ = ( join ` K )
llnexch.m 
|- ./\ = ( meet ` K )
llnexch.a 
|- A = ( Atoms ` K )
llnexch.n 
|- N = ( LLines ` K )
Assertion llnexchb2 
|- ( ( K e. HL /\ ( X e. N /\ Y e. N /\ Z e. N ) /\ ( ( X ./\ Y ) e. A /\ X =/= Z ) ) -> ( ( X ./\ Y ) .<_ Z <-> ( X ./\ Y ) = ( X ./\ Z ) ) )

Proof

Step Hyp Ref Expression
1 llnexch.l 
 |-  .<_ = ( le ` K )
2 llnexch.j 
 |-  .\/ = ( join ` K )
3 llnexch.m 
 |-  ./\ = ( meet ` K )
4 llnexch.a 
 |-  A = ( Atoms ` K )
5 llnexch.n 
 |-  N = ( LLines ` K )
6 simp23 
 |-  ( ( K e. HL /\ ( X e. N /\ Y e. N /\ Z e. N ) /\ ( ( X ./\ Y ) e. A /\ X =/= Z ) ) -> Z e. N )
7 simp1 
 |-  ( ( K e. HL /\ ( X e. N /\ Y e. N /\ Z e. N ) /\ ( ( X ./\ Y ) e. A /\ X =/= Z ) ) -> K e. HL )
8 eqid 
 |-  ( Base ` K ) = ( Base ` K )
9 8 5 llnbase 
 |-  ( Z e. N -> Z e. ( Base ` K ) )
10 6 9 syl 
 |-  ( ( K e. HL /\ ( X e. N /\ Y e. N /\ Z e. N ) /\ ( ( X ./\ Y ) e. A /\ X =/= Z ) ) -> Z e. ( Base ` K ) )
11 8 2 4 5 islln3 
 |-  ( ( K e. HL /\ Z e. ( Base ` K ) ) -> ( Z e. N <-> E. p e. A E. q e. A ( p =/= q /\ Z = ( p .\/ q ) ) ) )
12 7 10 11 syl2anc 
 |-  ( ( K e. HL /\ ( X e. N /\ Y e. N /\ Z e. N ) /\ ( ( X ./\ Y ) e. A /\ X =/= Z ) ) -> ( Z e. N <-> E. p e. A E. q e. A ( p =/= q /\ Z = ( p .\/ q ) ) ) )
13 6 12 mpbid 
 |-  ( ( K e. HL /\ ( X e. N /\ Y e. N /\ Z e. N ) /\ ( ( X ./\ Y ) e. A /\ X =/= Z ) ) -> E. p e. A E. q e. A ( p =/= q /\ Z = ( p .\/ q ) ) )
14 simp3r 
 |-  ( ( K e. HL /\ ( X e. N /\ Y e. N /\ Z e. N ) /\ ( ( X ./\ Y ) e. A /\ X =/= Z ) ) -> X =/= Z )
15 14 necomd 
 |-  ( ( K e. HL /\ ( X e. N /\ Y e. N /\ Z e. N ) /\ ( ( X ./\ Y ) e. A /\ X =/= Z ) ) -> Z =/= X )
16 simp11 
 |-  ( ( ( K e. HL /\ ( X e. N /\ Y e. N /\ Z e. N ) /\ ( ( X ./\ Y ) e. A /\ X =/= Z ) ) /\ ( p e. A /\ q e. A ) /\ p =/= q ) -> K e. HL )
17 16 hllatd 
 |-  ( ( ( K e. HL /\ ( X e. N /\ Y e. N /\ Z e. N ) /\ ( ( X ./\ Y ) e. A /\ X =/= Z ) ) /\ ( p e. A /\ q e. A ) /\ p =/= q ) -> K e. Lat )
18 simp2l 
 |-  ( ( ( K e. HL /\ ( X e. N /\ Y e. N /\ Z e. N ) /\ ( ( X ./\ Y ) e. A /\ X =/= Z ) ) /\ ( p e. A /\ q e. A ) /\ p =/= q ) -> p e. A )
19 8 4 atbase 
 |-  ( p e. A -> p e. ( Base ` K ) )
20 18 19 syl 
 |-  ( ( ( K e. HL /\ ( X e. N /\ Y e. N /\ Z e. N ) /\ ( ( X ./\ Y ) e. A /\ X =/= Z ) ) /\ ( p e. A /\ q e. A ) /\ p =/= q ) -> p e. ( Base ` K ) )
21 simp2r 
 |-  ( ( ( K e. HL /\ ( X e. N /\ Y e. N /\ Z e. N ) /\ ( ( X ./\ Y ) e. A /\ X =/= Z ) ) /\ ( p e. A /\ q e. A ) /\ p =/= q ) -> q e. A )
22 8 4 atbase 
 |-  ( q e. A -> q e. ( Base ` K ) )
23 21 22 syl 
 |-  ( ( ( K e. HL /\ ( X e. N /\ Y e. N /\ Z e. N ) /\ ( ( X ./\ Y ) e. A /\ X =/= Z ) ) /\ ( p e. A /\ q e. A ) /\ p =/= q ) -> q e. ( Base ` K ) )
24 simp121 
 |-  ( ( ( K e. HL /\ ( X e. N /\ Y e. N /\ Z e. N ) /\ ( ( X ./\ Y ) e. A /\ X =/= Z ) ) /\ ( p e. A /\ q e. A ) /\ p =/= q ) -> X e. N )
25 8 5 llnbase 
 |-  ( X e. N -> X e. ( Base ` K ) )
26 24 25 syl 
 |-  ( ( ( K e. HL /\ ( X e. N /\ Y e. N /\ Z e. N ) /\ ( ( X ./\ Y ) e. A /\ X =/= Z ) ) /\ ( p e. A /\ q e. A ) /\ p =/= q ) -> X e. ( Base ` K ) )
27 8 1 2 latjle12 
 |-  ( ( K e. Lat /\ ( p e. ( Base ` K ) /\ q e. ( Base ` K ) /\ X e. ( Base ` K ) ) ) -> ( ( p .<_ X /\ q .<_ X ) <-> ( p .\/ q ) .<_ X ) )
28 17 20 23 26 27 syl13anc 
 |-  ( ( ( K e. HL /\ ( X e. N /\ Y e. N /\ Z e. N ) /\ ( ( X ./\ Y ) e. A /\ X =/= Z ) ) /\ ( p e. A /\ q e. A ) /\ p =/= q ) -> ( ( p .<_ X /\ q .<_ X ) <-> ( p .\/ q ) .<_ X ) )
29 simp3 
 |-  ( ( ( K e. HL /\ ( X e. N /\ Y e. N /\ Z e. N ) /\ ( ( X ./\ Y ) e. A /\ X =/= Z ) ) /\ ( p e. A /\ q e. A ) /\ p =/= q ) -> p =/= q )
30 2 4 5 llni2 
 |-  ( ( ( K e. HL /\ p e. A /\ q e. A ) /\ p =/= q ) -> ( p .\/ q ) e. N )
31 16 18 21 29 30 syl31anc 
 |-  ( ( ( K e. HL /\ ( X e. N /\ Y e. N /\ Z e. N ) /\ ( ( X ./\ Y ) e. A /\ X =/= Z ) ) /\ ( p e. A /\ q e. A ) /\ p =/= q ) -> ( p .\/ q ) e. N )
32 1 5 llncmp 
 |-  ( ( K e. HL /\ ( p .\/ q ) e. N /\ X e. N ) -> ( ( p .\/ q ) .<_ X <-> ( p .\/ q ) = X ) )
33 16 31 24 32 syl3anc 
 |-  ( ( ( K e. HL /\ ( X e. N /\ Y e. N /\ Z e. N ) /\ ( ( X ./\ Y ) e. A /\ X =/= Z ) ) /\ ( p e. A /\ q e. A ) /\ p =/= q ) -> ( ( p .\/ q ) .<_ X <-> ( p .\/ q ) = X ) )
34 28 33 bitr2d 
 |-  ( ( ( K e. HL /\ ( X e. N /\ Y e. N /\ Z e. N ) /\ ( ( X ./\ Y ) e. A /\ X =/= Z ) ) /\ ( p e. A /\ q e. A ) /\ p =/= q ) -> ( ( p .\/ q ) = X <-> ( p .<_ X /\ q .<_ X ) ) )
35 34 necon3abid 
 |-  ( ( ( K e. HL /\ ( X e. N /\ Y e. N /\ Z e. N ) /\ ( ( X ./\ Y ) e. A /\ X =/= Z ) ) /\ ( p e. A /\ q e. A ) /\ p =/= q ) -> ( ( p .\/ q ) =/= X <-> -. ( p .<_ X /\ q .<_ X ) ) )
36 ianor 
 |-  ( -. ( p .<_ X /\ q .<_ X ) <-> ( -. p .<_ X \/ -. q .<_ X ) )
37 35 36 bitrdi 
 |-  ( ( ( K e. HL /\ ( X e. N /\ Y e. N /\ Z e. N ) /\ ( ( X ./\ Y ) e. A /\ X =/= Z ) ) /\ ( p e. A /\ q e. A ) /\ p =/= q ) -> ( ( p .\/ q ) =/= X <-> ( -. p .<_ X \/ -. q .<_ X ) ) )
38 simpl11 
 |-  ( ( ( ( K e. HL /\ ( X e. N /\ Y e. N /\ Z e. N ) /\ ( ( X ./\ Y ) e. A /\ X =/= Z ) ) /\ ( p e. A /\ q e. A ) /\ p =/= q ) /\ -. p .<_ X ) -> K e. HL )
39 24 adantr 
 |-  ( ( ( ( K e. HL /\ ( X e. N /\ Y e. N /\ Z e. N ) /\ ( ( X ./\ Y ) e. A /\ X =/= Z ) ) /\ ( p e. A /\ q e. A ) /\ p =/= q ) /\ -. p .<_ X ) -> X e. N )
40 simp122 
 |-  ( ( ( K e. HL /\ ( X e. N /\ Y e. N /\ Z e. N ) /\ ( ( X ./\ Y ) e. A /\ X =/= Z ) ) /\ ( p e. A /\ q e. A ) /\ p =/= q ) -> Y e. N )
41 40 adantr 
 |-  ( ( ( ( K e. HL /\ ( X e. N /\ Y e. N /\ Z e. N ) /\ ( ( X ./\ Y ) e. A /\ X =/= Z ) ) /\ ( p e. A /\ q e. A ) /\ p =/= q ) /\ -. p .<_ X ) -> Y e. N )
42 simpl2l 
 |-  ( ( ( ( K e. HL /\ ( X e. N /\ Y e. N /\ Z e. N ) /\ ( ( X ./\ Y ) e. A /\ X =/= Z ) ) /\ ( p e. A /\ q e. A ) /\ p =/= q ) /\ -. p .<_ X ) -> p e. A )
43 simpl2r 
 |-  ( ( ( ( K e. HL /\ ( X e. N /\ Y e. N /\ Z e. N ) /\ ( ( X ./\ Y ) e. A /\ X =/= Z ) ) /\ ( p e. A /\ q e. A ) /\ p =/= q ) /\ -. p .<_ X ) -> q e. A )
44 simpr 
 |-  ( ( ( ( K e. HL /\ ( X e. N /\ Y e. N /\ Z e. N ) /\ ( ( X ./\ Y ) e. A /\ X =/= Z ) ) /\ ( p e. A /\ q e. A ) /\ p =/= q ) /\ -. p .<_ X ) -> -. p .<_ X )
45 simp13l 
 |-  ( ( ( K e. HL /\ ( X e. N /\ Y e. N /\ Z e. N ) /\ ( ( X ./\ Y ) e. A /\ X =/= Z ) ) /\ ( p e. A /\ q e. A ) /\ p =/= q ) -> ( X ./\ Y ) e. A )
46 45 adantr 
 |-  ( ( ( ( K e. HL /\ ( X e. N /\ Y e. N /\ Z e. N ) /\ ( ( X ./\ Y ) e. A /\ X =/= Z ) ) /\ ( p e. A /\ q e. A ) /\ p =/= q ) /\ -. p .<_ X ) -> ( X ./\ Y ) e. A )
47 1 2 3 4 5 llnexchb2lem 
 |-  ( ( ( K e. HL /\ X e. N /\ Y e. N ) /\ ( p e. A /\ q e. A /\ -. p .<_ X ) /\ ( X ./\ Y ) e. A ) -> ( ( X ./\ Y ) .<_ ( p .\/ q ) <-> ( X ./\ Y ) = ( X ./\ ( p .\/ q ) ) ) )
48 38 39 41 42 43 44 46 47 syl331anc 
 |-  ( ( ( ( K e. HL /\ ( X e. N /\ Y e. N /\ Z e. N ) /\ ( ( X ./\ Y ) e. A /\ X =/= Z ) ) /\ ( p e. A /\ q e. A ) /\ p =/= q ) /\ -. p .<_ X ) -> ( ( X ./\ Y ) .<_ ( p .\/ q ) <-> ( X ./\ Y ) = ( X ./\ ( p .\/ q ) ) ) )
49 48 ex 
 |-  ( ( ( K e. HL /\ ( X e. N /\ Y e. N /\ Z e. N ) /\ ( ( X ./\ Y ) e. A /\ X =/= Z ) ) /\ ( p e. A /\ q e. A ) /\ p =/= q ) -> ( -. p .<_ X -> ( ( X ./\ Y ) .<_ ( p .\/ q ) <-> ( X ./\ Y ) = ( X ./\ ( p .\/ q ) ) ) ) )
50 simpl11 
 |-  ( ( ( ( K e. HL /\ ( X e. N /\ Y e. N /\ Z e. N ) /\ ( ( X ./\ Y ) e. A /\ X =/= Z ) ) /\ ( p e. A /\ q e. A ) /\ p =/= q ) /\ -. q .<_ X ) -> K e. HL )
51 24 adantr 
 |-  ( ( ( ( K e. HL /\ ( X e. N /\ Y e. N /\ Z e. N ) /\ ( ( X ./\ Y ) e. A /\ X =/= Z ) ) /\ ( p e. A /\ q e. A ) /\ p =/= q ) /\ -. q .<_ X ) -> X e. N )
52 40 adantr 
 |-  ( ( ( ( K e. HL /\ ( X e. N /\ Y e. N /\ Z e. N ) /\ ( ( X ./\ Y ) e. A /\ X =/= Z ) ) /\ ( p e. A /\ q e. A ) /\ p =/= q ) /\ -. q .<_ X ) -> Y e. N )
53 simpl2r 
 |-  ( ( ( ( K e. HL /\ ( X e. N /\ Y e. N /\ Z e. N ) /\ ( ( X ./\ Y ) e. A /\ X =/= Z ) ) /\ ( p e. A /\ q e. A ) /\ p =/= q ) /\ -. q .<_ X ) -> q e. A )
54 simpl2l 
 |-  ( ( ( ( K e. HL /\ ( X e. N /\ Y e. N /\ Z e. N ) /\ ( ( X ./\ Y ) e. A /\ X =/= Z ) ) /\ ( p e. A /\ q e. A ) /\ p =/= q ) /\ -. q .<_ X ) -> p e. A )
55 simpr 
 |-  ( ( ( ( K e. HL /\ ( X e. N /\ Y e. N /\ Z e. N ) /\ ( ( X ./\ Y ) e. A /\ X =/= Z ) ) /\ ( p e. A /\ q e. A ) /\ p =/= q ) /\ -. q .<_ X ) -> -. q .<_ X )
56 45 adantr 
 |-  ( ( ( ( K e. HL /\ ( X e. N /\ Y e. N /\ Z e. N ) /\ ( ( X ./\ Y ) e. A /\ X =/= Z ) ) /\ ( p e. A /\ q e. A ) /\ p =/= q ) /\ -. q .<_ X ) -> ( X ./\ Y ) e. A )
57 1 2 3 4 5 llnexchb2lem 
 |-  ( ( ( K e. HL /\ X e. N /\ Y e. N ) /\ ( q e. A /\ p e. A /\ -. q .<_ X ) /\ ( X ./\ Y ) e. A ) -> ( ( X ./\ Y ) .<_ ( q .\/ p ) <-> ( X ./\ Y ) = ( X ./\ ( q .\/ p ) ) ) )
58 50 51 52 53 54 55 56 57 syl331anc 
 |-  ( ( ( ( K e. HL /\ ( X e. N /\ Y e. N /\ Z e. N ) /\ ( ( X ./\ Y ) e. A /\ X =/= Z ) ) /\ ( p e. A /\ q e. A ) /\ p =/= q ) /\ -. q .<_ X ) -> ( ( X ./\ Y ) .<_ ( q .\/ p ) <-> ( X ./\ Y ) = ( X ./\ ( q .\/ p ) ) ) )
59 2 4 hlatjcom 
 |-  ( ( K e. HL /\ p e. A /\ q e. A ) -> ( p .\/ q ) = ( q .\/ p ) )
60 50 54 53 59 syl3anc 
 |-  ( ( ( ( K e. HL /\ ( X e. N /\ Y e. N /\ Z e. N ) /\ ( ( X ./\ Y ) e. A /\ X =/= Z ) ) /\ ( p e. A /\ q e. A ) /\ p =/= q ) /\ -. q .<_ X ) -> ( p .\/ q ) = ( q .\/ p ) )
61 60 breq2d 
 |-  ( ( ( ( K e. HL /\ ( X e. N /\ Y e. N /\ Z e. N ) /\ ( ( X ./\ Y ) e. A /\ X =/= Z ) ) /\ ( p e. A /\ q e. A ) /\ p =/= q ) /\ -. q .<_ X ) -> ( ( X ./\ Y ) .<_ ( p .\/ q ) <-> ( X ./\ Y ) .<_ ( q .\/ p ) ) )
62 60 oveq2d 
 |-  ( ( ( ( K e. HL /\ ( X e. N /\ Y e. N /\ Z e. N ) /\ ( ( X ./\ Y ) e. A /\ X =/= Z ) ) /\ ( p e. A /\ q e. A ) /\ p =/= q ) /\ -. q .<_ X ) -> ( X ./\ ( p .\/ q ) ) = ( X ./\ ( q .\/ p ) ) )
63 62 eqeq2d 
 |-  ( ( ( ( K e. HL /\ ( X e. N /\ Y e. N /\ Z e. N ) /\ ( ( X ./\ Y ) e. A /\ X =/= Z ) ) /\ ( p e. A /\ q e. A ) /\ p =/= q ) /\ -. q .<_ X ) -> ( ( X ./\ Y ) = ( X ./\ ( p .\/ q ) ) <-> ( X ./\ Y ) = ( X ./\ ( q .\/ p ) ) ) )
64 58 61 63 3bitr4d 
 |-  ( ( ( ( K e. HL /\ ( X e. N /\ Y e. N /\ Z e. N ) /\ ( ( X ./\ Y ) e. A /\ X =/= Z ) ) /\ ( p e. A /\ q e. A ) /\ p =/= q ) /\ -. q .<_ X ) -> ( ( X ./\ Y ) .<_ ( p .\/ q ) <-> ( X ./\ Y ) = ( X ./\ ( p .\/ q ) ) ) )
65 64 ex 
 |-  ( ( ( K e. HL /\ ( X e. N /\ Y e. N /\ Z e. N ) /\ ( ( X ./\ Y ) e. A /\ X =/= Z ) ) /\ ( p e. A /\ q e. A ) /\ p =/= q ) -> ( -. q .<_ X -> ( ( X ./\ Y ) .<_ ( p .\/ q ) <-> ( X ./\ Y ) = ( X ./\ ( p .\/ q ) ) ) ) )
66 49 65 jaod 
 |-  ( ( ( K e. HL /\ ( X e. N /\ Y e. N /\ Z e. N ) /\ ( ( X ./\ Y ) e. A /\ X =/= Z ) ) /\ ( p e. A /\ q e. A ) /\ p =/= q ) -> ( ( -. p .<_ X \/ -. q .<_ X ) -> ( ( X ./\ Y ) .<_ ( p .\/ q ) <-> ( X ./\ Y ) = ( X ./\ ( p .\/ q ) ) ) ) )
67 37 66 sylbid 
 |-  ( ( ( K e. HL /\ ( X e. N /\ Y e. N /\ Z e. N ) /\ ( ( X ./\ Y ) e. A /\ X =/= Z ) ) /\ ( p e. A /\ q e. A ) /\ p =/= q ) -> ( ( p .\/ q ) =/= X -> ( ( X ./\ Y ) .<_ ( p .\/ q ) <-> ( X ./\ Y ) = ( X ./\ ( p .\/ q ) ) ) ) )
68 neeq1 
 |-  ( Z = ( p .\/ q ) -> ( Z =/= X <-> ( p .\/ q ) =/= X ) )
69 breq2 
 |-  ( Z = ( p .\/ q ) -> ( ( X ./\ Y ) .<_ Z <-> ( X ./\ Y ) .<_ ( p .\/ q ) ) )
70 oveq2 
 |-  ( Z = ( p .\/ q ) -> ( X ./\ Z ) = ( X ./\ ( p .\/ q ) ) )
71 70 eqeq2d 
 |-  ( Z = ( p .\/ q ) -> ( ( X ./\ Y ) = ( X ./\ Z ) <-> ( X ./\ Y ) = ( X ./\ ( p .\/ q ) ) ) )
72 69 71 bibi12d 
 |-  ( Z = ( p .\/ q ) -> ( ( ( X ./\ Y ) .<_ Z <-> ( X ./\ Y ) = ( X ./\ Z ) ) <-> ( ( X ./\ Y ) .<_ ( p .\/ q ) <-> ( X ./\ Y ) = ( X ./\ ( p .\/ q ) ) ) ) )
73 68 72 imbi12d 
 |-  ( Z = ( p .\/ q ) -> ( ( Z =/= X -> ( ( X ./\ Y ) .<_ Z <-> ( X ./\ Y ) = ( X ./\ Z ) ) ) <-> ( ( p .\/ q ) =/= X -> ( ( X ./\ Y ) .<_ ( p .\/ q ) <-> ( X ./\ Y ) = ( X ./\ ( p .\/ q ) ) ) ) ) )
74 67 73 syl5ibrcom 
 |-  ( ( ( K e. HL /\ ( X e. N /\ Y e. N /\ Z e. N ) /\ ( ( X ./\ Y ) e. A /\ X =/= Z ) ) /\ ( p e. A /\ q e. A ) /\ p =/= q ) -> ( Z = ( p .\/ q ) -> ( Z =/= X -> ( ( X ./\ Y ) .<_ Z <-> ( X ./\ Y ) = ( X ./\ Z ) ) ) ) )
75 74 3exp 
 |-  ( ( K e. HL /\ ( X e. N /\ Y e. N /\ Z e. N ) /\ ( ( X ./\ Y ) e. A /\ X =/= Z ) ) -> ( ( p e. A /\ q e. A ) -> ( p =/= q -> ( Z = ( p .\/ q ) -> ( Z =/= X -> ( ( X ./\ Y ) .<_ Z <-> ( X ./\ Y ) = ( X ./\ Z ) ) ) ) ) ) )
76 75 imp4a 
 |-  ( ( K e. HL /\ ( X e. N /\ Y e. N /\ Z e. N ) /\ ( ( X ./\ Y ) e. A /\ X =/= Z ) ) -> ( ( p e. A /\ q e. A ) -> ( ( p =/= q /\ Z = ( p .\/ q ) ) -> ( Z =/= X -> ( ( X ./\ Y ) .<_ Z <-> ( X ./\ Y ) = ( X ./\ Z ) ) ) ) ) )
77 76 rexlimdvv 
 |-  ( ( K e. HL /\ ( X e. N /\ Y e. N /\ Z e. N ) /\ ( ( X ./\ Y ) e. A /\ X =/= Z ) ) -> ( E. p e. A E. q e. A ( p =/= q /\ Z = ( p .\/ q ) ) -> ( Z =/= X -> ( ( X ./\ Y ) .<_ Z <-> ( X ./\ Y ) = ( X ./\ Z ) ) ) ) )
78 13 15 77 mp2d 
 |-  ( ( K e. HL /\ ( X e. N /\ Y e. N /\ Z e. N ) /\ ( ( X ./\ Y ) e. A /\ X =/= Z ) ) -> ( ( X ./\ Y ) .<_ Z <-> ( X ./\ Y ) = ( X ./\ Z ) ) )