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

Metamath Proof Explorer

Theorem islvol5

Description: The predicate "is a 3-dim lattice volume" in terms of atoms. (Contributed by NM, 1-Jul-2012)

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

Proof

Step Hyp Ref Expression
1 islvol5.b 
 |-  B = ( Base ` K )
2 islvol5.l 
 |-  .<_ = ( le ` K )
3 islvol5.j 
 |-  .\/ = ( join ` K )
4 islvol5.a 
 |-  A = ( Atoms ` K )
5 islvol5.v 
 |-  V = ( LVols ` K )
6 eqid 
 |-  ( LPlanes ` K ) = ( LPlanes ` K )
7 1 2 3 4 6 5 islvol3 
 |-  ( ( K e. HL /\ X e. B ) -> ( X e. V <-> E. y e. ( LPlanes ` K ) E. s e. A ( -. s .<_ y /\ X = ( y .\/ s ) ) ) )
8 df-rex 
 |-  ( E. y e. ( LPlanes ` K ) E. s e. A ( -. s .<_ y /\ X = ( y .\/ s ) ) <-> E. y ( y e. ( LPlanes ` K ) /\ E. s e. A ( -. s .<_ y /\ X = ( y .\/ s ) ) ) )
9 r19.41v 
 |-  ( E. s e. A ( ( y e. B /\ ( -. s .<_ y /\ X = ( y .\/ s ) ) ) /\ ( p =/= q /\ -. r .<_ ( p .\/ q ) /\ y = ( ( p .\/ q ) .\/ r ) ) ) <-> ( E. s e. A ( y e. B /\ ( -. s .<_ y /\ X = ( y .\/ s ) ) ) /\ ( p =/= q /\ -. r .<_ ( p .\/ q ) /\ y = ( ( p .\/ q ) .\/ r ) ) ) )
10 df-3an 
 |-  ( ( p =/= q /\ -. r .<_ ( p .\/ q ) /\ y = ( ( p .\/ q ) .\/ r ) ) <-> ( ( p =/= q /\ -. r .<_ ( p .\/ q ) ) /\ y = ( ( p .\/ q ) .\/ r ) ) )
11 10 anbi2i 
 |-  ( ( E. s e. A ( y e. B /\ ( -. s .<_ y /\ X = ( y .\/ s ) ) ) /\ ( p =/= q /\ -. r .<_ ( p .\/ q ) /\ y = ( ( p .\/ q ) .\/ r ) ) ) <-> ( E. s e. A ( y e. B /\ ( -. s .<_ y /\ X = ( y .\/ s ) ) ) /\ ( ( p =/= q /\ -. r .<_ ( p .\/ q ) ) /\ y = ( ( p .\/ q ) .\/ r ) ) ) )
12 an13 
 |-  ( ( E. s e. A ( y e. B /\ ( -. s .<_ y /\ X = ( y .\/ s ) ) ) /\ ( ( p =/= q /\ -. r .<_ ( p .\/ q ) ) /\ y = ( ( p .\/ q ) .\/ r ) ) ) <-> ( y = ( ( p .\/ q ) .\/ r ) /\ ( ( p =/= q /\ -. r .<_ ( p .\/ q ) ) /\ E. s e. A ( y e. B /\ ( -. s .<_ y /\ X = ( y .\/ s ) ) ) ) ) )
13 11 12 bitri 
 |-  ( ( E. s e. A ( y e. B /\ ( -. s .<_ y /\ X = ( y .\/ s ) ) ) /\ ( p =/= q /\ -. r .<_ ( p .\/ q ) /\ y = ( ( p .\/ q ) .\/ r ) ) ) <-> ( y = ( ( p .\/ q ) .\/ r ) /\ ( ( p =/= q /\ -. r .<_ ( p .\/ q ) ) /\ E. s e. A ( y e. B /\ ( -. s .<_ y /\ X = ( y .\/ s ) ) ) ) ) )
14 9 13 bitri 
 |-  ( E. s e. A ( ( y e. B /\ ( -. s .<_ y /\ X = ( y .\/ s ) ) ) /\ ( p =/= q /\ -. r .<_ ( p .\/ q ) /\ y = ( ( p .\/ q ) .\/ r ) ) ) <-> ( y = ( ( p .\/ q ) .\/ r ) /\ ( ( p =/= q /\ -. r .<_ ( p .\/ q ) ) /\ E. s e. A ( y e. B /\ ( -. s .<_ y /\ X = ( y .\/ s ) ) ) ) ) )
15 14 exbii 
 |-  ( E. y E. s e. A ( ( y e. B /\ ( -. s .<_ y /\ X = ( y .\/ s ) ) ) /\ ( p =/= q /\ -. r .<_ ( p .\/ q ) /\ y = ( ( p .\/ q ) .\/ r ) ) ) <-> E. y ( y = ( ( p .\/ q ) .\/ r ) /\ ( ( p =/= q /\ -. r .<_ ( p .\/ q ) ) /\ E. s e. A ( y e. B /\ ( -. s .<_ y /\ X = ( y .\/ s ) ) ) ) ) )
16 ovex 
 |-  ( ( p .\/ q ) .\/ r ) e. _V
17 an12 
 |-  ( ( ( p =/= q /\ -. r .<_ ( p .\/ q ) ) /\ ( y e. B /\ ( -. s .<_ y /\ X = ( y .\/ s ) ) ) ) <-> ( y e. B /\ ( ( p =/= q /\ -. r .<_ ( p .\/ q ) ) /\ ( -. s .<_ y /\ X = ( y .\/ s ) ) ) ) )
18 eleq1 
 |-  ( y = ( ( p .\/ q ) .\/ r ) -> ( y e. B <-> ( ( p .\/ q ) .\/ r ) e. B ) )
19 breq2 
 |-  ( y = ( ( p .\/ q ) .\/ r ) -> ( s .<_ y <-> s .<_ ( ( p .\/ q ) .\/ r ) ) )
20 19 notbid 
 |-  ( y = ( ( p .\/ q ) .\/ r ) -> ( -. s .<_ y <-> -. s .<_ ( ( p .\/ q ) .\/ r ) ) )
21 oveq1 
 |-  ( y = ( ( p .\/ q ) .\/ r ) -> ( y .\/ s ) = ( ( ( p .\/ q ) .\/ r ) .\/ s ) )
22 21 eqeq2d 
 |-  ( y = ( ( p .\/ q ) .\/ r ) -> ( X = ( y .\/ s ) <-> X = ( ( ( p .\/ q ) .\/ r ) .\/ s ) ) )
23 20 22 anbi12d 
 |-  ( y = ( ( p .\/ q ) .\/ r ) -> ( ( -. s .<_ y /\ X = ( y .\/ s ) ) <-> ( -. s .<_ ( ( p .\/ q ) .\/ r ) /\ X = ( ( ( p .\/ q ) .\/ r ) .\/ s ) ) ) )
24 23 anbi2d 
 |-  ( y = ( ( p .\/ q ) .\/ r ) -> ( ( ( p =/= q /\ -. r .<_ ( p .\/ q ) ) /\ ( -. s .<_ y /\ X = ( y .\/ s ) ) ) <-> ( ( p =/= q /\ -. r .<_ ( p .\/ q ) ) /\ ( -. s .<_ ( ( p .\/ q ) .\/ r ) /\ X = ( ( ( p .\/ q ) .\/ r ) .\/ s ) ) ) ) )
25 anass 
 |-  ( ( ( ( p =/= q /\ -. r .<_ ( p .\/ q ) ) /\ -. s .<_ ( ( p .\/ q ) .\/ r ) ) /\ X = ( ( ( p .\/ q ) .\/ r ) .\/ s ) ) <-> ( ( p =/= q /\ -. r .<_ ( p .\/ q ) ) /\ ( -. s .<_ ( ( p .\/ q ) .\/ r ) /\ X = ( ( ( p .\/ q ) .\/ r ) .\/ s ) ) ) )
26 df-3an 
 |-  ( ( p =/= q /\ -. r .<_ ( p .\/ q ) /\ -. s .<_ ( ( p .\/ q ) .\/ r ) ) <-> ( ( p =/= q /\ -. r .<_ ( p .\/ q ) ) /\ -. s .<_ ( ( p .\/ q ) .\/ r ) ) )
27 26 bicomi 
 |-  ( ( ( p =/= q /\ -. r .<_ ( p .\/ q ) ) /\ -. s .<_ ( ( p .\/ q ) .\/ r ) ) <-> ( p =/= q /\ -. r .<_ ( p .\/ q ) /\ -. s .<_ ( ( p .\/ q ) .\/ r ) ) )
28 27 anbi1i 
 |-  ( ( ( ( p =/= q /\ -. r .<_ ( p .\/ q ) ) /\ -. s .<_ ( ( p .\/ q ) .\/ r ) ) /\ X = ( ( ( p .\/ q ) .\/ r ) .\/ s ) ) <-> ( ( p =/= q /\ -. r .<_ ( p .\/ q ) /\ -. s .<_ ( ( p .\/ q ) .\/ r ) ) /\ X = ( ( ( p .\/ q ) .\/ r ) .\/ s ) ) )
29 25 28 bitr3i 
 |-  ( ( ( p =/= q /\ -. r .<_ ( p .\/ q ) ) /\ ( -. s .<_ ( ( p .\/ q ) .\/ r ) /\ X = ( ( ( p .\/ q ) .\/ r ) .\/ s ) ) ) <-> ( ( p =/= q /\ -. r .<_ ( p .\/ q ) /\ -. s .<_ ( ( p .\/ q ) .\/ r ) ) /\ X = ( ( ( p .\/ q ) .\/ r ) .\/ s ) ) )
30 24 29 bitrdi 
 |-  ( y = ( ( p .\/ q ) .\/ r ) -> ( ( ( p =/= q /\ -. r .<_ ( p .\/ q ) ) /\ ( -. s .<_ y /\ X = ( y .\/ s ) ) ) <-> ( ( p =/= q /\ -. r .<_ ( p .\/ q ) /\ -. s .<_ ( ( p .\/ q ) .\/ r ) ) /\ X = ( ( ( p .\/ q ) .\/ r ) .\/ s ) ) ) )
31 18 30 anbi12d 
 |-  ( y = ( ( p .\/ q ) .\/ r ) -> ( ( y e. B /\ ( ( p =/= q /\ -. r .<_ ( p .\/ q ) ) /\ ( -. s .<_ y /\ X = ( y .\/ s ) ) ) ) <-> ( ( ( p .\/ q ) .\/ r ) e. B /\ ( ( p =/= q /\ -. r .<_ ( p .\/ q ) /\ -. s .<_ ( ( p .\/ q ) .\/ r ) ) /\ X = ( ( ( p .\/ q ) .\/ r ) .\/ s ) ) ) ) )
32 17 31 bitrid 
 |-  ( y = ( ( p .\/ q ) .\/ r ) -> ( ( ( p =/= q /\ -. r .<_ ( p .\/ q ) ) /\ ( y e. B /\ ( -. s .<_ y /\ X = ( y .\/ s ) ) ) ) <-> ( ( ( p .\/ q ) .\/ r ) e. B /\ ( ( p =/= q /\ -. r .<_ ( p .\/ q ) /\ -. s .<_ ( ( p .\/ q ) .\/ r ) ) /\ X = ( ( ( p .\/ q ) .\/ r ) .\/ s ) ) ) ) )
33 32 rexbidv 
 |-  ( y = ( ( p .\/ q ) .\/ r ) -> ( E. s e. A ( ( p =/= q /\ -. r .<_ ( p .\/ q ) ) /\ ( y e. B /\ ( -. s .<_ y /\ X = ( y .\/ s ) ) ) ) <-> E. s e. A ( ( ( p .\/ q ) .\/ r ) e. B /\ ( ( p =/= q /\ -. r .<_ ( p .\/ q ) /\ -. s .<_ ( ( p .\/ q ) .\/ r ) ) /\ X = ( ( ( p .\/ q ) .\/ r ) .\/ s ) ) ) ) )
34 r19.42v 
 |-  ( E. s e. A ( ( p =/= q /\ -. r .<_ ( p .\/ q ) ) /\ ( y e. B /\ ( -. s .<_ y /\ X = ( y .\/ s ) ) ) ) <-> ( ( p =/= q /\ -. r .<_ ( p .\/ q ) ) /\ E. s e. A ( y e. B /\ ( -. s .<_ y /\ X = ( y .\/ s ) ) ) ) )
35 r19.42v 
 |-  ( E. s e. A ( ( ( p .\/ q ) .\/ r ) e. B /\ ( ( p =/= q /\ -. r .<_ ( p .\/ q ) /\ -. s .<_ ( ( p .\/ q ) .\/ r ) ) /\ X = ( ( ( p .\/ q ) .\/ r ) .\/ s ) ) ) <-> ( ( ( p .\/ q ) .\/ r ) e. B /\ E. s e. A ( ( p =/= q /\ -. r .<_ ( p .\/ q ) /\ -. s .<_ ( ( p .\/ q ) .\/ r ) ) /\ X = ( ( ( p .\/ q ) .\/ r ) .\/ s ) ) ) )
36 33 34 35 3bitr3g 
 |-  ( y = ( ( p .\/ q ) .\/ r ) -> ( ( ( p =/= q /\ -. r .<_ ( p .\/ q ) ) /\ E. s e. A ( y e. B /\ ( -. s .<_ y /\ X = ( y .\/ s ) ) ) ) <-> ( ( ( p .\/ q ) .\/ r ) e. B /\ E. s e. A ( ( p =/= q /\ -. r .<_ ( p .\/ q ) /\ -. s .<_ ( ( p .\/ q ) .\/ r ) ) /\ X = ( ( ( p .\/ q ) .\/ r ) .\/ s ) ) ) ) )
37 16 36 ceqsexv 
 |-  ( E. y ( y = ( ( p .\/ q ) .\/ r ) /\ ( ( p =/= q /\ -. r .<_ ( p .\/ q ) ) /\ E. s e. A ( y e. B /\ ( -. s .<_ y /\ X = ( y .\/ s ) ) ) ) ) <-> ( ( ( p .\/ q ) .\/ r ) e. B /\ E. s e. A ( ( p =/= q /\ -. r .<_ ( p .\/ q ) /\ -. s .<_ ( ( p .\/ q ) .\/ r ) ) /\ X = ( ( ( p .\/ q ) .\/ r ) .\/ s ) ) ) )
38 15 37 bitri 
 |-  ( E. y E. s e. A ( ( y e. B /\ ( -. s .<_ y /\ X = ( y .\/ s ) ) ) /\ ( p =/= q /\ -. r .<_ ( p .\/ q ) /\ y = ( ( p .\/ q ) .\/ r ) ) ) <-> ( ( ( p .\/ q ) .\/ r ) e. B /\ E. s e. A ( ( p =/= q /\ -. r .<_ ( p .\/ q ) /\ -. s .<_ ( ( p .\/ q ) .\/ r ) ) /\ X = ( ( ( p .\/ q ) .\/ r ) .\/ s ) ) ) )
39 hllat 
 |-  ( K e. HL -> K e. Lat )
40 39 ad3antrrr 
 |-  ( ( ( ( K e. HL /\ X e. B ) /\ ( p e. A /\ q e. A ) ) /\ r e. A ) -> K e. Lat )
41 simplll 
 |-  ( ( ( ( K e. HL /\ X e. B ) /\ ( p e. A /\ q e. A ) ) /\ r e. A ) -> K e. HL )
42 simplrl 
 |-  ( ( ( ( K e. HL /\ X e. B ) /\ ( p e. A /\ q e. A ) ) /\ r e. A ) -> p e. A )
43 simplrr 
 |-  ( ( ( ( K e. HL /\ X e. B ) /\ ( p e. A /\ q e. A ) ) /\ r e. A ) -> q e. A )
44 1 3 4 hlatjcl 
 |-  ( ( K e. HL /\ p e. A /\ q e. A ) -> ( p .\/ q ) e. B )
45 41 42 43 44 syl3anc 
 |-  ( ( ( ( K e. HL /\ X e. B ) /\ ( p e. A /\ q e. A ) ) /\ r e. A ) -> ( p .\/ q ) e. B )
46 1 4 atbase 
 |-  ( r e. A -> r e. B )
47 46 adantl 
 |-  ( ( ( ( K e. HL /\ X e. B ) /\ ( p e. A /\ q e. A ) ) /\ r e. A ) -> r e. B )
48 1 3 latjcl 
 |-  ( ( K e. Lat /\ ( p .\/ q ) e. B /\ r e. B ) -> ( ( p .\/ q ) .\/ r ) e. B )
49 40 45 47 48 syl3anc 
 |-  ( ( ( ( K e. HL /\ X e. B ) /\ ( p e. A /\ q e. A ) ) /\ r e. A ) -> ( ( p .\/ q ) .\/ r ) e. B )
50 49 biantrurd 
 |-  ( ( ( ( K e. HL /\ X e. B ) /\ ( p e. A /\ q e. A ) ) /\ r e. A ) -> ( E. s e. A ( ( p =/= q /\ -. r .<_ ( p .\/ q ) /\ -. s .<_ ( ( p .\/ q ) .\/ r ) ) /\ X = ( ( ( p .\/ q ) .\/ r ) .\/ s ) ) <-> ( ( ( p .\/ q ) .\/ r ) e. B /\ E. s e. A ( ( p =/= q /\ -. r .<_ ( p .\/ q ) /\ -. s .<_ ( ( p .\/ q ) .\/ r ) ) /\ X = ( ( ( p .\/ q ) .\/ r ) .\/ s ) ) ) ) )
51 38 50 bitr4id 
 |-  ( ( ( ( K e. HL /\ X e. B ) /\ ( p e. A /\ q e. A ) ) /\ r e. A ) -> ( E. y E. s e. A ( ( y e. B /\ ( -. s .<_ y /\ X = ( y .\/ s ) ) ) /\ ( p =/= q /\ -. r .<_ ( p .\/ q ) /\ y = ( ( p .\/ q ) .\/ r ) ) ) <-> E. s e. A ( ( p =/= q /\ -. r .<_ ( p .\/ q ) /\ -. s .<_ ( ( p .\/ q ) .\/ r ) ) /\ X = ( ( ( p .\/ q ) .\/ r ) .\/ s ) ) ) )
52 51 rexbidva 
 |-  ( ( ( K e. HL /\ X e. B ) /\ ( p e. A /\ q e. A ) ) -> ( E. r e. A E. y E. s e. A ( ( y e. B /\ ( -. s .<_ y /\ X = ( y .\/ s ) ) ) /\ ( p =/= q /\ -. r .<_ ( p .\/ q ) /\ y = ( ( p .\/ q ) .\/ r ) ) ) <-> E. r e. A E. s e. A ( ( p =/= q /\ -. r .<_ ( p .\/ q ) /\ -. s .<_ ( ( p .\/ q ) .\/ r ) ) /\ X = ( ( ( p .\/ q ) .\/ r ) .\/ s ) ) ) )
53 52 2rexbidva 
 |-  ( ( K e. HL /\ X e. B ) -> ( E. p e. A E. q e. A E. r e. A E. y E. s e. A ( ( y e. B /\ ( -. s .<_ y /\ X = ( y .\/ s ) ) ) /\ ( p =/= q /\ -. r .<_ ( p .\/ q ) /\ y = ( ( p .\/ q ) .\/ r ) ) ) <-> E. p e. A E. q e. A E. r e. A E. s e. A ( ( p =/= q /\ -. r .<_ ( p .\/ q ) /\ -. s .<_ ( ( p .\/ q ) .\/ r ) ) /\ X = ( ( ( p .\/ q ) .\/ r ) .\/ s ) ) ) )
54 rexcom4 
 |-  ( E. r e. A E. y E. s e. A ( ( y e. B /\ ( -. s .<_ y /\ X = ( y .\/ s ) ) ) /\ ( p =/= q /\ -. r .<_ ( p .\/ q ) /\ y = ( ( p .\/ q ) .\/ r ) ) ) <-> E. y E. r e. A E. s e. A ( ( y e. B /\ ( -. s .<_ y /\ X = ( y .\/ s ) ) ) /\ ( p =/= q /\ -. r .<_ ( p .\/ q ) /\ y = ( ( p .\/ q ) .\/ r ) ) ) )
55 54 rexbii 
 |-  ( E. q e. A E. r e. A E. y E. s e. A ( ( y e. B /\ ( -. s .<_ y /\ X = ( y .\/ s ) ) ) /\ ( p =/= q /\ -. r .<_ ( p .\/ q ) /\ y = ( ( p .\/ q ) .\/ r ) ) ) <-> E. q e. A E. y E. r e. A E. s e. A ( ( y e. B /\ ( -. s .<_ y /\ X = ( y .\/ s ) ) ) /\ ( p =/= q /\ -. r .<_ ( p .\/ q ) /\ y = ( ( p .\/ q ) .\/ r ) ) ) )
56 rexcom4 
 |-  ( E. q e. A E. y E. r e. A E. s e. A ( ( y e. B /\ ( -. s .<_ y /\ X = ( y .\/ s ) ) ) /\ ( p =/= q /\ -. r .<_ ( p .\/ q ) /\ y = ( ( p .\/ q ) .\/ r ) ) ) <-> E. y E. q e. A E. r e. A E. s e. A ( ( y e. B /\ ( -. s .<_ y /\ X = ( y .\/ s ) ) ) /\ ( p =/= q /\ -. r .<_ ( p .\/ q ) /\ y = ( ( p .\/ q ) .\/ r ) ) ) )
57 55 56 bitri 
 |-  ( E. q e. A E. r e. A E. y E. s e. A ( ( y e. B /\ ( -. s .<_ y /\ X = ( y .\/ s ) ) ) /\ ( p =/= q /\ -. r .<_ ( p .\/ q ) /\ y = ( ( p .\/ q ) .\/ r ) ) ) <-> E. y E. q e. A E. r e. A E. s e. A ( ( y e. B /\ ( -. s .<_ y /\ X = ( y .\/ s ) ) ) /\ ( p =/= q /\ -. r .<_ ( p .\/ q ) /\ y = ( ( p .\/ q ) .\/ r ) ) ) )
58 57 rexbii 
 |-  ( E. p e. A E. q e. A E. r e. A E. y E. s e. A ( ( y e. B /\ ( -. s .<_ y /\ X = ( y .\/ s ) ) ) /\ ( p =/= q /\ -. r .<_ ( p .\/ q ) /\ y = ( ( p .\/ q ) .\/ r ) ) ) <-> E. p e. A E. y E. q e. A E. r e. A E. s e. A ( ( y e. B /\ ( -. s .<_ y /\ X = ( y .\/ s ) ) ) /\ ( p =/= q /\ -. r .<_ ( p .\/ q ) /\ y = ( ( p .\/ q ) .\/ r ) ) ) )
59 rexcom4 
 |-  ( E. p e. A E. y E. q e. A E. r e. A E. s e. A ( ( y e. B /\ ( -. s .<_ y /\ X = ( y .\/ s ) ) ) /\ ( p =/= q /\ -. r .<_ ( p .\/ q ) /\ y = ( ( p .\/ q ) .\/ r ) ) ) <-> E. y E. p e. A E. q e. A E. r e. A E. s e. A ( ( y e. B /\ ( -. s .<_ y /\ X = ( y .\/ s ) ) ) /\ ( p =/= q /\ -. r .<_ ( p .\/ q ) /\ y = ( ( p .\/ q ) .\/ r ) ) ) )
60 58 59 bitri 
 |-  ( E. p e. A E. q e. A E. r e. A E. y E. s e. A ( ( y e. B /\ ( -. s .<_ y /\ X = ( y .\/ s ) ) ) /\ ( p =/= q /\ -. r .<_ ( p .\/ q ) /\ y = ( ( p .\/ q ) .\/ r ) ) ) <-> E. y E. p e. A E. q e. A E. r e. A E. s e. A ( ( y e. B /\ ( -. s .<_ y /\ X = ( y .\/ s ) ) ) /\ ( p =/= q /\ -. r .<_ ( p .\/ q ) /\ y = ( ( p .\/ q ) .\/ r ) ) ) )
61 53 60 bitr3di 
 |-  ( ( K e. HL /\ X e. B ) -> ( E. p e. A E. q e. A E. r e. A E. s e. A ( ( p =/= q /\ -. r .<_ ( p .\/ q ) /\ -. s .<_ ( ( p .\/ q ) .\/ r ) ) /\ X = ( ( ( p .\/ q ) .\/ r ) .\/ s ) ) <-> E. y E. p e. A E. q e. A E. r e. A E. s e. A ( ( y e. B /\ ( -. s .<_ y /\ X = ( y .\/ s ) ) ) /\ ( p =/= q /\ -. r .<_ ( p .\/ q ) /\ y = ( ( p .\/ q ) .\/ r ) ) ) ) )
62 rexcom 
 |-  ( E. r e. A E. s e. A ( ( y e. B /\ ( -. s .<_ y /\ X = ( y .\/ s ) ) ) /\ ( p =/= q /\ -. r .<_ ( p .\/ q ) /\ y = ( ( p .\/ q ) .\/ r ) ) ) <-> E. s e. A E. r e. A ( ( y e. B /\ ( -. s .<_ y /\ X = ( y .\/ s ) ) ) /\ ( p =/= q /\ -. r .<_ ( p .\/ q ) /\ y = ( ( p .\/ q ) .\/ r ) ) ) )
63 62 rexbii 
 |-  ( E. q e. A E. r e. A E. s e. A ( ( y e. B /\ ( -. s .<_ y /\ X = ( y .\/ s ) ) ) /\ ( p =/= q /\ -. r .<_ ( p .\/ q ) /\ y = ( ( p .\/ q ) .\/ r ) ) ) <-> E. q e. A E. s e. A E. r e. A ( ( y e. B /\ ( -. s .<_ y /\ X = ( y .\/ s ) ) ) /\ ( p =/= q /\ -. r .<_ ( p .\/ q ) /\ y = ( ( p .\/ q ) .\/ r ) ) ) )
64 rexcom 
 |-  ( E. q e. A E. s e. A E. r e. A ( ( y e. B /\ ( -. s .<_ y /\ X = ( y .\/ s ) ) ) /\ ( p =/= q /\ -. r .<_ ( p .\/ q ) /\ y = ( ( p .\/ q ) .\/ r ) ) ) <-> E. s e. A E. q e. A E. r e. A ( ( y e. B /\ ( -. s .<_ y /\ X = ( y .\/ s ) ) ) /\ ( p =/= q /\ -. r .<_ ( p .\/ q ) /\ y = ( ( p .\/ q ) .\/ r ) ) ) )
65 63 64 bitri 
 |-  ( E. q e. A E. r e. A E. s e. A ( ( y e. B /\ ( -. s .<_ y /\ X = ( y .\/ s ) ) ) /\ ( p =/= q /\ -. r .<_ ( p .\/ q ) /\ y = ( ( p .\/ q ) .\/ r ) ) ) <-> E. s e. A E. q e. A E. r e. A ( ( y e. B /\ ( -. s .<_ y /\ X = ( y .\/ s ) ) ) /\ ( p =/= q /\ -. r .<_ ( p .\/ q ) /\ y = ( ( p .\/ q ) .\/ r ) ) ) )
66 65 rexbii 
 |-  ( E. p e. A E. q e. A E. r e. A E. s e. A ( ( y e. B /\ ( -. s .<_ y /\ X = ( y .\/ s ) ) ) /\ ( p =/= q /\ -. r .<_ ( p .\/ q ) /\ y = ( ( p .\/ q ) .\/ r ) ) ) <-> E. p e. A E. s e. A E. q e. A E. r e. A ( ( y e. B /\ ( -. s .<_ y /\ X = ( y .\/ s ) ) ) /\ ( p =/= q /\ -. r .<_ ( p .\/ q ) /\ y = ( ( p .\/ q ) .\/ r ) ) ) )
67 rexcom 
 |-  ( E. p e. A E. s e. A E. q e. A E. r e. A ( ( y e. B /\ ( -. s .<_ y /\ X = ( y .\/ s ) ) ) /\ ( p =/= q /\ -. r .<_ ( p .\/ q ) /\ y = ( ( p .\/ q ) .\/ r ) ) ) <-> E. s e. A E. p e. A E. q e. A E. r e. A ( ( y e. B /\ ( -. s .<_ y /\ X = ( y .\/ s ) ) ) /\ ( p =/= q /\ -. r .<_ ( p .\/ q ) /\ y = ( ( p .\/ q ) .\/ r ) ) ) )
68 66 67 bitri 
 |-  ( E. p e. A E. q e. A E. r e. A E. s e. A ( ( y e. B /\ ( -. s .<_ y /\ X = ( y .\/ s ) ) ) /\ ( p =/= q /\ -. r .<_ ( p .\/ q ) /\ y = ( ( p .\/ q ) .\/ r ) ) ) <-> E. s e. A E. p e. A E. q e. A E. r e. A ( ( y e. B /\ ( -. s .<_ y /\ X = ( y .\/ s ) ) ) /\ ( p =/= q /\ -. r .<_ ( p .\/ q ) /\ y = ( ( p .\/ q ) .\/ r ) ) ) )
69 1 2 3 4 6 islpln2 
 |-  ( K e. HL -> ( y e. ( LPlanes ` K ) <-> ( y e. B /\ E. p e. A E. q e. A E. r e. A ( p =/= q /\ -. r .<_ ( p .\/ q ) /\ y = ( ( p .\/ q ) .\/ r ) ) ) ) )
70 69 adantr 
 |-  ( ( K e. HL /\ X e. B ) -> ( y e. ( LPlanes ` K ) <-> ( y e. B /\ E. p e. A E. q e. A E. r e. A ( p =/= q /\ -. r .<_ ( p .\/ q ) /\ y = ( ( p .\/ q ) .\/ r ) ) ) ) )
71 70 anbi1d 
 |-  ( ( K e. HL /\ X e. B ) -> ( ( y e. ( LPlanes ` K ) /\ ( -. s .<_ y /\ X = ( y .\/ s ) ) ) <-> ( ( y e. B /\ E. p e. A E. q e. A E. r e. A ( p =/= q /\ -. r .<_ ( p .\/ q ) /\ y = ( ( p .\/ q ) .\/ r ) ) ) /\ ( -. s .<_ y /\ X = ( y .\/ s ) ) ) ) )
72 r19.42v 
 |-  ( E. p e. A ( ( y e. B /\ ( -. s .<_ y /\ X = ( y .\/ s ) ) ) /\ E. q e. A E. r e. A ( p =/= q /\ -. r .<_ ( p .\/ q ) /\ y = ( ( p .\/ q ) .\/ r ) ) ) <-> ( ( y e. B /\ ( -. s .<_ y /\ X = ( y .\/ s ) ) ) /\ E. p e. A E. q e. A E. r e. A ( p =/= q /\ -. r .<_ ( p .\/ q ) /\ y = ( ( p .\/ q ) .\/ r ) ) ) )
73 r19.42v 
 |-  ( E. r e. A ( ( y e. B /\ ( -. s .<_ y /\ X = ( y .\/ s ) ) ) /\ ( p =/= q /\ -. r .<_ ( p .\/ q ) /\ y = ( ( p .\/ q ) .\/ r ) ) ) <-> ( ( y e. B /\ ( -. s .<_ y /\ X = ( y .\/ s ) ) ) /\ E. r e. A ( p =/= q /\ -. r .<_ ( p .\/ q ) /\ y = ( ( p .\/ q ) .\/ r ) ) ) )
74 73 rexbii 
 |-  ( E. q e. A E. r e. A ( ( y e. B /\ ( -. s .<_ y /\ X = ( y .\/ s ) ) ) /\ ( p =/= q /\ -. r .<_ ( p .\/ q ) /\ y = ( ( p .\/ q ) .\/ r ) ) ) <-> E. q e. A ( ( y e. B /\ ( -. s .<_ y /\ X = ( y .\/ s ) ) ) /\ E. r e. A ( p =/= q /\ -. r .<_ ( p .\/ q ) /\ y = ( ( p .\/ q ) .\/ r ) ) ) )
75 r19.42v 
 |-  ( E. q e. A ( ( y e. B /\ ( -. s .<_ y /\ X = ( y .\/ s ) ) ) /\ E. r e. A ( p =/= q /\ -. r .<_ ( p .\/ q ) /\ y = ( ( p .\/ q ) .\/ r ) ) ) <-> ( ( y e. B /\ ( -. s .<_ y /\ X = ( y .\/ s ) ) ) /\ E. q e. A E. r e. A ( p =/= q /\ -. r .<_ ( p .\/ q ) /\ y = ( ( p .\/ q ) .\/ r ) ) ) )
76 74 75 bitri 
 |-  ( E. q e. A E. r e. A ( ( y e. B /\ ( -. s .<_ y /\ X = ( y .\/ s ) ) ) /\ ( p =/= q /\ -. r .<_ ( p .\/ q ) /\ y = ( ( p .\/ q ) .\/ r ) ) ) <-> ( ( y e. B /\ ( -. s .<_ y /\ X = ( y .\/ s ) ) ) /\ E. q e. A E. r e. A ( p =/= q /\ -. r .<_ ( p .\/ q ) /\ y = ( ( p .\/ q ) .\/ r ) ) ) )
77 76 rexbii 
 |-  ( E. p e. A E. q e. A E. r e. A ( ( y e. B /\ ( -. s .<_ y /\ X = ( y .\/ s ) ) ) /\ ( p =/= q /\ -. r .<_ ( p .\/ q ) /\ y = ( ( p .\/ q ) .\/ r ) ) ) <-> E. p e. A ( ( y e. B /\ ( -. s .<_ y /\ X = ( y .\/ s ) ) ) /\ E. q e. A E. r e. A ( p =/= q /\ -. r .<_ ( p .\/ q ) /\ y = ( ( p .\/ q ) .\/ r ) ) ) )
78 an32 
 |-  ( ( ( y e. B /\ E. p e. A E. q e. A E. r e. A ( p =/= q /\ -. r .<_ ( p .\/ q ) /\ y = ( ( p .\/ q ) .\/ r ) ) ) /\ ( -. s .<_ y /\ X = ( y .\/ s ) ) ) <-> ( ( y e. B /\ ( -. s .<_ y /\ X = ( y .\/ s ) ) ) /\ E. p e. A E. q e. A E. r e. A ( p =/= q /\ -. r .<_ ( p .\/ q ) /\ y = ( ( p .\/ q ) .\/ r ) ) ) )
79 72 77 78 3bitr4ri 
 |-  ( ( ( y e. B /\ E. p e. A E. q e. A E. r e. A ( p =/= q /\ -. r .<_ ( p .\/ q ) /\ y = ( ( p .\/ q ) .\/ r ) ) ) /\ ( -. s .<_ y /\ X = ( y .\/ s ) ) ) <-> E. p e. A E. q e. A E. r e. A ( ( y e. B /\ ( -. s .<_ y /\ X = ( y .\/ s ) ) ) /\ ( p =/= q /\ -. r .<_ ( p .\/ q ) /\ y = ( ( p .\/ q ) .\/ r ) ) ) )
80 71 79 bitrdi 
 |-  ( ( K e. HL /\ X e. B ) -> ( ( y e. ( LPlanes ` K ) /\ ( -. s .<_ y /\ X = ( y .\/ s ) ) ) <-> E. p e. A E. q e. A E. r e. A ( ( y e. B /\ ( -. s .<_ y /\ X = ( y .\/ s ) ) ) /\ ( p =/= q /\ -. r .<_ ( p .\/ q ) /\ y = ( ( p .\/ q ) .\/ r ) ) ) ) )
81 80 rexbidv 
 |-  ( ( K e. HL /\ X e. B ) -> ( E. s e. A ( y e. ( LPlanes ` K ) /\ ( -. s .<_ y /\ X = ( y .\/ s ) ) ) <-> E. s e. A E. p e. A E. q e. A E. r e. A ( ( y e. B /\ ( -. s .<_ y /\ X = ( y .\/ s ) ) ) /\ ( p =/= q /\ -. r .<_ ( p .\/ q ) /\ y = ( ( p .\/ q ) .\/ r ) ) ) ) )
82 68 81 bitr4id 
 |-  ( ( K e. HL /\ X e. B ) -> ( E. p e. A E. q e. A E. r e. A E. s e. A ( ( y e. B /\ ( -. s .<_ y /\ X = ( y .\/ s ) ) ) /\ ( p =/= q /\ -. r .<_ ( p .\/ q ) /\ y = ( ( p .\/ q ) .\/ r ) ) ) <-> E. s e. A ( y e. ( LPlanes ` K ) /\ ( -. s .<_ y /\ X = ( y .\/ s ) ) ) ) )
83 r19.42v 
 |-  ( E. s e. A ( y e. ( LPlanes ` K ) /\ ( -. s .<_ y /\ X = ( y .\/ s ) ) ) <-> ( y e. ( LPlanes ` K ) /\ E. s e. A ( -. s .<_ y /\ X = ( y .\/ s ) ) ) )
84 82 83 bitrdi 
 |-  ( ( K e. HL /\ X e. B ) -> ( E. p e. A E. q e. A E. r e. A E. s e. A ( ( y e. B /\ ( -. s .<_ y /\ X = ( y .\/ s ) ) ) /\ ( p =/= q /\ -. r .<_ ( p .\/ q ) /\ y = ( ( p .\/ q ) .\/ r ) ) ) <-> ( y e. ( LPlanes ` K ) /\ E. s e. A ( -. s .<_ y /\ X = ( y .\/ s ) ) ) ) )
85 84 exbidv 
 |-  ( ( K e. HL /\ X e. B ) -> ( E. y E. p e. A E. q e. A E. r e. A E. s e. A ( ( y e. B /\ ( -. s .<_ y /\ X = ( y .\/ s ) ) ) /\ ( p =/= q /\ -. r .<_ ( p .\/ q ) /\ y = ( ( p .\/ q ) .\/ r ) ) ) <-> E. y ( y e. ( LPlanes ` K ) /\ E. s e. A ( -. s .<_ y /\ X = ( y .\/ s ) ) ) ) )
86 61 85 bitrd 
 |-  ( ( K e. HL /\ X e. B ) -> ( E. p e. A E. q e. A E. r e. A E. s e. A ( ( p =/= q /\ -. r .<_ ( p .\/ q ) /\ -. s .<_ ( ( p .\/ q ) .\/ r ) ) /\ X = ( ( ( p .\/ q ) .\/ r ) .\/ s ) ) <-> E. y ( y e. ( LPlanes ` K ) /\ E. s e. A ( -. s .<_ y /\ X = ( y .\/ s ) ) ) ) )
87 8 86 bitr4id 
 |-  ( ( K e. HL /\ X e. B ) -> ( E. y e. ( LPlanes ` K ) E. s e. A ( -. s .<_ y /\ X = ( y .\/ s ) ) <-> E. p e. A E. q e. A E. r e. A E. s e. A ( ( p =/= q /\ -. r .<_ ( p .\/ q ) /\ -. s .<_ ( ( p .\/ q ) .\/ r ) ) /\ X = ( ( ( p .\/ q ) .\/ r ) .\/ s ) ) ) )
88 7 87 bitrd 
 |-  ( ( K e. HL /\ X e. B ) -> ( X e. V <-> E. p e. A E. q e. A E. r e. A E. s e. A ( ( p =/= q /\ -. r .<_ ( p .\/ q ) /\ -. s .<_ ( ( p .\/ q ) .\/ r ) ) /\ X = ( ( ( p .\/ q ) .\/ r ) .\/ s ) ) ) )