Metamath Proof Explorer

Theorem islpln5

Description: The predicate "is a lattice plane" in terms of atoms. (Contributed by NM, 24-Jun-2012)

Ref Expression
Hypotheses islpln5.b 
|- B = ( Base ` K )
islpln5.l 
|- .<_ = ( le ` K )
islpln5.j 
|- .\/ = ( join ` K )
islpln5.a 
|- A = ( Atoms ` K )
islpln5.p 
|- P = ( LPlanes ` K )
Assertion islpln5 
|- ( ( K e. HL /\ X e. B ) -> ( X e. P <-> E. p e. A E. q e. A E. r e. A ( p =/= q /\ -. r .<_ ( p .\/ q ) /\ X = ( ( p .\/ q ) .\/ r ) ) ) )

Proof

Step Hyp Ref Expression
1 islpln5.b 
 |-  B = ( Base ` K )
2 islpln5.l 
 |-  .<_ = ( le ` K )
3 islpln5.j 
 |-  .\/ = ( join ` K )
4 islpln5.a 
 |-  A = ( Atoms ` K )
5 islpln5.p 
 |-  P = ( LPlanes ` K )
6 eqid 
 |-  ( LLines ` K ) = ( LLines ` K )
7 1 2 3 4 6 5 islpln3 
 |-  ( ( K e. HL /\ X e. B ) -> ( X e. P <-> E. y e. ( LLines ` K ) E. r e. A ( -. r .<_ y /\ X = ( y .\/ r ) ) ) )
8 df-rex 
 |-  ( E. y e. ( LLines ` K ) E. r e. A ( -. r .<_ y /\ X = ( y .\/ r ) ) <-> E. y ( y e. ( LLines ` K ) /\ E. r e. A ( -. r .<_ y /\ X = ( y .\/ r ) ) ) )
9 r19.41v 
 |-  ( E. r e. A ( ( y e. B /\ ( -. r .<_ y /\ X = ( y .\/ r ) ) ) /\ ( p =/= q /\ y = ( p .\/ q ) ) ) <-> ( E. r e. A ( y e. B /\ ( -. r .<_ y /\ X = ( y .\/ r ) ) ) /\ ( p =/= q /\ y = ( p .\/ q ) ) ) )
10 an13 
 |-  ( ( E. r e. A ( y e. B /\ ( -. r .<_ y /\ X = ( y .\/ r ) ) ) /\ ( p =/= q /\ y = ( p .\/ q ) ) ) <-> ( y = ( p .\/ q ) /\ ( p =/= q /\ E. r e. A ( y e. B /\ ( -. r .<_ y /\ X = ( y .\/ r ) ) ) ) ) )
11 9 10 bitri 
 |-  ( E. r e. A ( ( y e. B /\ ( -. r .<_ y /\ X = ( y .\/ r ) ) ) /\ ( p =/= q /\ y = ( p .\/ q ) ) ) <-> ( y = ( p .\/ q ) /\ ( p =/= q /\ E. r e. A ( y e. B /\ ( -. r .<_ y /\ X = ( y .\/ r ) ) ) ) ) )
12 11 exbii 
 |-  ( E. y E. r e. A ( ( y e. B /\ ( -. r .<_ y /\ X = ( y .\/ r ) ) ) /\ ( p =/= q /\ y = ( p .\/ q ) ) ) <-> E. y ( y = ( p .\/ q ) /\ ( p =/= q /\ E. r e. A ( y e. B /\ ( -. r .<_ y /\ X = ( y .\/ r ) ) ) ) ) )
13 ovex 
 |-  ( p .\/ q ) e. _V
14 an12 
 |-  ( ( p =/= q /\ ( y e. B /\ ( -. r .<_ y /\ X = ( y .\/ r ) ) ) ) <-> ( y e. B /\ ( p =/= q /\ ( -. r .<_ y /\ X = ( y .\/ r ) ) ) ) )
15 eleq1 
 |-  ( y = ( p .\/ q ) -> ( y e. B <-> ( p .\/ q ) e. B ) )
16 breq2 
 |-  ( y = ( p .\/ q ) -> ( r .<_ y <-> r .<_ ( p .\/ q ) ) )
17 16 notbid 
 |-  ( y = ( p .\/ q ) -> ( -. r .<_ y <-> -. r .<_ ( p .\/ q ) ) )
18 oveq1 
 |-  ( y = ( p .\/ q ) -> ( y .\/ r ) = ( ( p .\/ q ) .\/ r ) )
19 18 eqeq2d 
 |-  ( y = ( p .\/ q ) -> ( X = ( y .\/ r ) <-> X = ( ( p .\/ q ) .\/ r ) ) )
20 17 19 anbi12d 
 |-  ( y = ( p .\/ q ) -> ( ( -. r .<_ y /\ X = ( y .\/ r ) ) <-> ( -. r .<_ ( p .\/ q ) /\ X = ( ( p .\/ q ) .\/ r ) ) ) )
21 20 anbi2d 
 |-  ( y = ( p .\/ q ) -> ( ( p =/= q /\ ( -. r .<_ y /\ X = ( y .\/ r ) ) ) <-> ( p =/= q /\ ( -. r .<_ ( p .\/ q ) /\ X = ( ( p .\/ q ) .\/ r ) ) ) ) )
22 3anass 
 |-  ( ( p =/= q /\ -. r .<_ ( p .\/ q ) /\ X = ( ( p .\/ q ) .\/ r ) ) <-> ( p =/= q /\ ( -. r .<_ ( p .\/ q ) /\ X = ( ( p .\/ q ) .\/ r ) ) ) )
23 21 22 bitr4di 
 |-  ( y = ( p .\/ q ) -> ( ( p =/= q /\ ( -. r .<_ y /\ X = ( y .\/ r ) ) ) <-> ( p =/= q /\ -. r .<_ ( p .\/ q ) /\ X = ( ( p .\/ q ) .\/ r ) ) ) )
24 15 23 anbi12d 
 |-  ( y = ( p .\/ q ) -> ( ( y e. B /\ ( p =/= q /\ ( -. r .<_ y /\ X = ( y .\/ r ) ) ) ) <-> ( ( p .\/ q ) e. B /\ ( p =/= q /\ -. r .<_ ( p .\/ q ) /\ X = ( ( p .\/ q ) .\/ r ) ) ) ) )
25 14 24 syl5bb 
 |-  ( y = ( p .\/ q ) -> ( ( p =/= q /\ ( y e. B /\ ( -. r .<_ y /\ X = ( y .\/ r ) ) ) ) <-> ( ( p .\/ q ) e. B /\ ( p =/= q /\ -. r .<_ ( p .\/ q ) /\ X = ( ( p .\/ q ) .\/ r ) ) ) ) )
26 25 rexbidv 
 |-  ( y = ( p .\/ q ) -> ( E. r e. A ( p =/= q /\ ( y e. B /\ ( -. r .<_ y /\ X = ( y .\/ r ) ) ) ) <-> E. r e. A ( ( p .\/ q ) e. B /\ ( p =/= q /\ -. r .<_ ( p .\/ q ) /\ X = ( ( p .\/ q ) .\/ r ) ) ) ) )
27 r19.42v 
 |-  ( E. r e. A ( p =/= q /\ ( y e. B /\ ( -. r .<_ y /\ X = ( y .\/ r ) ) ) ) <-> ( p =/= q /\ E. r e. A ( y e. B /\ ( -. r .<_ y /\ X = ( y .\/ r ) ) ) ) )
28 r19.42v 
 |-  ( E. r e. A ( ( p .\/ q ) e. B /\ ( p =/= q /\ -. r .<_ ( p .\/ q ) /\ X = ( ( p .\/ q ) .\/ r ) ) ) <-> ( ( p .\/ q ) e. B /\ E. r e. A ( p =/= q /\ -. r .<_ ( p .\/ q ) /\ X = ( ( p .\/ q ) .\/ r ) ) ) )
29 26 27 28 3bitr3g 
 |-  ( y = ( p .\/ q ) -> ( ( p =/= q /\ E. r e. A ( y e. B /\ ( -. r .<_ y /\ X = ( y .\/ r ) ) ) ) <-> ( ( p .\/ q ) e. B /\ E. r e. A ( p =/= q /\ -. r .<_ ( p .\/ q ) /\ X = ( ( p .\/ q ) .\/ r ) ) ) ) )
30 13 29 ceqsexv 
 |-  ( E. y ( y = ( p .\/ q ) /\ ( p =/= q /\ E. r e. A ( y e. B /\ ( -. r .<_ y /\ X = ( y .\/ r ) ) ) ) ) <-> ( ( p .\/ q ) e. B /\ E. r e. A ( p =/= q /\ -. r .<_ ( p .\/ q ) /\ X = ( ( p .\/ q ) .\/ r ) ) ) )
31 12 30 bitri 
 |-  ( E. y E. r e. A ( ( y e. B /\ ( -. r .<_ y /\ X = ( y .\/ r ) ) ) /\ ( p =/= q /\ y = ( p .\/ q ) ) ) <-> ( ( p .\/ q ) e. B /\ E. r e. A ( p =/= q /\ -. r .<_ ( p .\/ q ) /\ X = ( ( p .\/ q ) .\/ r ) ) ) )
32 simpll 
 |-  ( ( ( K e. HL /\ X e. B ) /\ ( p e. A /\ q e. A ) ) -> K e. HL )
33 simprl 
 |-  ( ( ( K e. HL /\ X e. B ) /\ ( p e. A /\ q e. A ) ) -> p e. A )
34 simprr 
 |-  ( ( ( K e. HL /\ X e. B ) /\ ( p e. A /\ q e. A ) ) -> q e. A )
35 1 3 4 hlatjcl 
 |-  ( ( K e. HL /\ p e. A /\ q e. A ) -> ( p .\/ q ) e. B )
36 32 33 34 35 syl3anc 
 |-  ( ( ( K e. HL /\ X e. B ) /\ ( p e. A /\ q e. A ) ) -> ( p .\/ q ) e. B )
37 36 biantrurd 
 |-  ( ( ( K e. HL /\ X e. B ) /\ ( p e. A /\ q e. A ) ) -> ( E. r e. A ( p =/= q /\ -. r .<_ ( p .\/ q ) /\ X = ( ( p .\/ q ) .\/ r ) ) <-> ( ( p .\/ q ) e. B /\ E. r e. A ( p =/= q /\ -. r .<_ ( p .\/ q ) /\ X = ( ( p .\/ q ) .\/ r ) ) ) ) )
38 31 37 bitr4id 
 |-  ( ( ( K e. HL /\ X e. B ) /\ ( p e. A /\ q e. A ) ) -> ( E. y E. r e. A ( ( y e. B /\ ( -. r .<_ y /\ X = ( y .\/ r ) ) ) /\ ( p =/= q /\ y = ( p .\/ q ) ) ) <-> E. r e. A ( p =/= q /\ -. r .<_ ( p .\/ q ) /\ X = ( ( p .\/ q ) .\/ r ) ) ) )
39 38 2rexbidva 
 |-  ( ( K e. HL /\ X e. B ) -> ( E. p e. A E. q e. A E. y E. r e. A ( ( y e. B /\ ( -. r .<_ y /\ X = ( y .\/ r ) ) ) /\ ( p =/= q /\ y = ( p .\/ q ) ) ) <-> E. p e. A E. q e. A E. r e. A ( p =/= q /\ -. r .<_ ( p .\/ q ) /\ X = ( ( p .\/ q ) .\/ r ) ) ) )
40 rexcom4 
 |-  ( E. q e. A E. y E. r e. A ( ( y e. B /\ ( -. r .<_ y /\ X = ( y .\/ r ) ) ) /\ ( p =/= q /\ y = ( p .\/ q ) ) ) <-> E. y E. q e. A E. r e. A ( ( y e. B /\ ( -. r .<_ y /\ X = ( y .\/ r ) ) ) /\ ( p =/= q /\ y = ( p .\/ q ) ) ) )
41 40 rexbii 
 |-  ( E. p e. A E. q e. A E. y E. r e. A ( ( y e. B /\ ( -. r .<_ y /\ X = ( y .\/ r ) ) ) /\ ( p =/= q /\ y = ( p .\/ q ) ) ) <-> E. p e. A E. y E. q e. A E. r e. A ( ( y e. B /\ ( -. r .<_ y /\ X = ( y .\/ r ) ) ) /\ ( p =/= q /\ y = ( p .\/ q ) ) ) )
42 rexcom4 
 |-  ( E. p e. A E. y E. q e. A E. r e. A ( ( y e. B /\ ( -. r .<_ y /\ X = ( y .\/ r ) ) ) /\ ( p =/= q /\ y = ( p .\/ q ) ) ) <-> E. y E. p e. A E. q e. A E. r e. A ( ( y e. B /\ ( -. r .<_ y /\ X = ( y .\/ r ) ) ) /\ ( p =/= q /\ y = ( p .\/ q ) ) ) )
43 41 42 bitri 
 |-  ( E. p e. A E. q e. A E. y E. r e. A ( ( y e. B /\ ( -. r .<_ y /\ X = ( y .\/ r ) ) ) /\ ( p =/= q /\ y = ( p .\/ q ) ) ) <-> E. y E. p e. A E. q e. A E. r e. A ( ( y e. B /\ ( -. r .<_ y /\ X = ( y .\/ r ) ) ) /\ ( p =/= q /\ y = ( p .\/ q ) ) ) )
44 39 43 bitr3di 
 |-  ( ( K e. HL /\ X e. B ) -> ( E. p e. A E. q e. A E. r e. A ( p =/= q /\ -. r .<_ ( p .\/ q ) /\ X = ( ( p .\/ q ) .\/ r ) ) <-> E. y E. p e. A E. q e. A E. r e. A ( ( y e. B /\ ( -. r .<_ y /\ X = ( y .\/ r ) ) ) /\ ( p =/= q /\ y = ( p .\/ q ) ) ) ) )
45 rexcom 
 |-  ( E. q e. A E. r e. A ( ( y e. B /\ ( -. r .<_ y /\ X = ( y .\/ r ) ) ) /\ ( p =/= q /\ y = ( p .\/ q ) ) ) <-> E. r e. A E. q e. A ( ( y e. B /\ ( -. r .<_ y /\ X = ( y .\/ r ) ) ) /\ ( p =/= q /\ y = ( p .\/ q ) ) ) )
46 45 rexbii 
 |-  ( E. p e. A E. q e. A E. r e. A ( ( y e. B /\ ( -. r .<_ y /\ X = ( y .\/ r ) ) ) /\ ( p =/= q /\ y = ( p .\/ q ) ) ) <-> E. p e. A E. r e. A E. q e. A ( ( y e. B /\ ( -. r .<_ y /\ X = ( y .\/ r ) ) ) /\ ( p =/= q /\ y = ( p .\/ q ) ) ) )
47 rexcom 
 |-  ( E. p e. A E. r e. A E. q e. A ( ( y e. B /\ ( -. r .<_ y /\ X = ( y .\/ r ) ) ) /\ ( p =/= q /\ y = ( p .\/ q ) ) ) <-> E. r e. A E. p e. A E. q e. A ( ( y e. B /\ ( -. r .<_ y /\ X = ( y .\/ r ) ) ) /\ ( p =/= q /\ y = ( p .\/ q ) ) ) )
48 46 47 bitri 
 |-  ( E. p e. A E. q e. A E. r e. A ( ( y e. B /\ ( -. r .<_ y /\ X = ( y .\/ r ) ) ) /\ ( p =/= q /\ y = ( p .\/ q ) ) ) <-> E. r e. A E. p e. A E. q e. A ( ( y e. B /\ ( -. r .<_ y /\ X = ( y .\/ r ) ) ) /\ ( p =/= q /\ y = ( p .\/ q ) ) ) )
49 1 3 4 6 islln2 
 |-  ( K e. HL -> ( y e. ( LLines ` K ) <-> ( y e. B /\ E. p e. A E. q e. A ( p =/= q /\ y = ( p .\/ q ) ) ) ) )
50 49 adantr 
 |-  ( ( K e. HL /\ X e. B ) -> ( y e. ( LLines ` K ) <-> ( y e. B /\ E. p e. A E. q e. A ( p =/= q /\ y = ( p .\/ q ) ) ) ) )
51 50 anbi1d 
 |-  ( ( K e. HL /\ X e. B ) -> ( ( y e. ( LLines ` K ) /\ ( -. r .<_ y /\ X = ( y .\/ r ) ) ) <-> ( ( y e. B /\ E. p e. A E. q e. A ( p =/= q /\ y = ( p .\/ q ) ) ) /\ ( -. r .<_ y /\ X = ( y .\/ r ) ) ) ) )
52 r19.42v 
 |-  ( E. p e. A ( ( y e. B /\ ( -. r .<_ y /\ X = ( y .\/ r ) ) ) /\ E. q e. A ( p =/= q /\ y = ( p .\/ q ) ) ) <-> ( ( y e. B /\ ( -. r .<_ y /\ X = ( y .\/ r ) ) ) /\ E. p e. A E. q e. A ( p =/= q /\ y = ( p .\/ q ) ) ) )
53 r19.42v 
 |-  ( E. q e. A ( ( y e. B /\ ( -. r .<_ y /\ X = ( y .\/ r ) ) ) /\ ( p =/= q /\ y = ( p .\/ q ) ) ) <-> ( ( y e. B /\ ( -. r .<_ y /\ X = ( y .\/ r ) ) ) /\ E. q e. A ( p =/= q /\ y = ( p .\/ q ) ) ) )
54 53 rexbii 
 |-  ( E. p e. A E. q e. A ( ( y e. B /\ ( -. r .<_ y /\ X = ( y .\/ r ) ) ) /\ ( p =/= q /\ y = ( p .\/ q ) ) ) <-> E. p e. A ( ( y e. B /\ ( -. r .<_ y /\ X = ( y .\/ r ) ) ) /\ E. q e. A ( p =/= q /\ y = ( p .\/ q ) ) ) )
55 an32 
 |-  ( ( ( y e. B /\ E. p e. A E. q e. A ( p =/= q /\ y = ( p .\/ q ) ) ) /\ ( -. r .<_ y /\ X = ( y .\/ r ) ) ) <-> ( ( y e. B /\ ( -. r .<_ y /\ X = ( y .\/ r ) ) ) /\ E. p e. A E. q e. A ( p =/= q /\ y = ( p .\/ q ) ) ) )
56 52 54 55 3bitr4ri 
 |-  ( ( ( y e. B /\ E. p e. A E. q e. A ( p =/= q /\ y = ( p .\/ q ) ) ) /\ ( -. r .<_ y /\ X = ( y .\/ r ) ) ) <-> E. p e. A E. q e. A ( ( y e. B /\ ( -. r .<_ y /\ X = ( y .\/ r ) ) ) /\ ( p =/= q /\ y = ( p .\/ q ) ) ) )
57 51 56 bitrdi 
 |-  ( ( K e. HL /\ X e. B ) -> ( ( y e. ( LLines ` K ) /\ ( -. r .<_ y /\ X = ( y .\/ r ) ) ) <-> E. p e. A E. q e. A ( ( y e. B /\ ( -. r .<_ y /\ X = ( y .\/ r ) ) ) /\ ( p =/= q /\ y = ( p .\/ q ) ) ) ) )
58 57 rexbidv 
 |-  ( ( K e. HL /\ X e. B ) -> ( E. r e. A ( y e. ( LLines ` K ) /\ ( -. r .<_ y /\ X = ( y .\/ r ) ) ) <-> E. r e. A E. p e. A E. q e. A ( ( y e. B /\ ( -. r .<_ y /\ X = ( y .\/ r ) ) ) /\ ( p =/= q /\ y = ( p .\/ q ) ) ) ) )
59 48 58 bitr4id 
 |-  ( ( K e. HL /\ X e. B ) -> ( E. p e. A E. q e. A E. r e. A ( ( y e. B /\ ( -. r .<_ y /\ X = ( y .\/ r ) ) ) /\ ( p =/= q /\ y = ( p .\/ q ) ) ) <-> E. r e. A ( y e. ( LLines ` K ) /\ ( -. r .<_ y /\ X = ( y .\/ r ) ) ) ) )
60 r19.42v 
 |-  ( E. r e. A ( y e. ( LLines ` K ) /\ ( -. r .<_ y /\ X = ( y .\/ r ) ) ) <-> ( y e. ( LLines ` K ) /\ E. r e. A ( -. r .<_ y /\ X = ( y .\/ r ) ) ) )
61 59 60 bitrdi 
 |-  ( ( K e. HL /\ X e. B ) -> ( E. p e. A E. q e. A E. r e. A ( ( y e. B /\ ( -. r .<_ y /\ X = ( y .\/ r ) ) ) /\ ( p =/= q /\ y = ( p .\/ q ) ) ) <-> ( y e. ( LLines ` K ) /\ E. r e. A ( -. r .<_ y /\ X = ( y .\/ r ) ) ) ) )
62 61 exbidv 
 |-  ( ( K e. HL /\ X e. B ) -> ( E. y E. p e. A E. q e. A E. r e. A ( ( y e. B /\ ( -. r .<_ y /\ X = ( y .\/ r ) ) ) /\ ( p =/= q /\ y = ( p .\/ q ) ) ) <-> E. y ( y e. ( LLines ` K ) /\ E. r e. A ( -. r .<_ y /\ X = ( y .\/ r ) ) ) ) )
63 44 62 bitrd 
 |-  ( ( K e. HL /\ X e. B ) -> ( E. p e. A E. q e. A E. r e. A ( p =/= q /\ -. r .<_ ( p .\/ q ) /\ X = ( ( p .\/ q ) .\/ r ) ) <-> E. y ( y e. ( LLines ` K ) /\ E. r e. A ( -. r .<_ y /\ X = ( y .\/ r ) ) ) ) )
64 8 63 bitr4id 
 |-  ( ( K e. HL /\ X e. B ) -> ( E. y e. ( LLines ` K ) E. r e. A ( -. r .<_ y /\ X = ( y .\/ r ) ) <-> E. p e. A E. q e. A E. r e. A ( p =/= q /\ -. r .<_ ( p .\/ q ) /\ X = ( ( p .\/ q ) .\/ r ) ) ) )
65 7 64 bitrd 
 |-  ( ( K e. HL /\ X e. B ) -> ( X e. P <-> E. p e. A E. q e. A E. r e. A ( p =/= q /\ -. r .<_ ( p .\/ q ) /\ X = ( ( p .\/ q ) .\/ r ) ) ) )