Step |
Hyp |
Ref |
Expression |
1 |
|
2lplnm.j |
|- .\/ = ( join ` K ) |
2 |
|
2lplnm.m |
|- ./\ = ( meet ` K ) |
3 |
|
2lplnm.c |
|- C = ( |
4 |
|
2lplnm.n |
|- N = ( LLines ` K ) |
5 |
|
2lplnm.p |
|- P = ( LPlanes ` K ) |
6 |
|
simpl3 |
|- ( ( ( K e. HL /\ X e. P /\ Y e. P ) /\ X C ( X .\/ Y ) ) -> Y e. P ) |
7 |
|
simpl1 |
|- ( ( ( K e. HL /\ X e. P /\ Y e. P ) /\ X C ( X .\/ Y ) ) -> K e. HL ) |
8 |
|
hllat |
|- ( K e. HL -> K e. Lat ) |
9 |
|
eqid |
|- ( Base ` K ) = ( Base ` K ) |
10 |
9 5
|
lplnbase |
|- ( X e. P -> X e. ( Base ` K ) ) |
11 |
9 5
|
lplnbase |
|- ( Y e. P -> Y e. ( Base ` K ) ) |
12 |
9 2
|
latmcl |
|- ( ( K e. Lat /\ X e. ( Base ` K ) /\ Y e. ( Base ` K ) ) -> ( X ./\ Y ) e. ( Base ` K ) ) |
13 |
8 10 11 12
|
syl3an |
|- ( ( K e. HL /\ X e. P /\ Y e. P ) -> ( X ./\ Y ) e. ( Base ` K ) ) |
14 |
13
|
adantr |
|- ( ( ( K e. HL /\ X e. P /\ Y e. P ) /\ X C ( X .\/ Y ) ) -> ( X ./\ Y ) e. ( Base ` K ) ) |
15 |
11
|
3ad2ant3 |
|- ( ( K e. HL /\ X e. P /\ Y e. P ) -> Y e. ( Base ` K ) ) |
16 |
15
|
adantr |
|- ( ( ( K e. HL /\ X e. P /\ Y e. P ) /\ X C ( X .\/ Y ) ) -> Y e. ( Base ` K ) ) |
17 |
|
simp1 |
|- ( ( K e. HL /\ X e. P /\ Y e. P ) -> K e. HL ) |
18 |
10
|
3ad2ant2 |
|- ( ( K e. HL /\ X e. P /\ Y e. P ) -> X e. ( Base ` K ) ) |
19 |
9 1 2 3
|
cvrexch |
|- ( ( K e. HL /\ X e. ( Base ` K ) /\ Y e. ( Base ` K ) ) -> ( ( X ./\ Y ) C Y <-> X C ( X .\/ Y ) ) ) |
20 |
17 18 15 19
|
syl3anc |
|- ( ( K e. HL /\ X e. P /\ Y e. P ) -> ( ( X ./\ Y ) C Y <-> X C ( X .\/ Y ) ) ) |
21 |
20
|
biimpar |
|- ( ( ( K e. HL /\ X e. P /\ Y e. P ) /\ X C ( X .\/ Y ) ) -> ( X ./\ Y ) C Y ) |
22 |
9 3 4 5
|
llncvrlpln |
|- ( ( ( K e. HL /\ ( X ./\ Y ) e. ( Base ` K ) /\ Y e. ( Base ` K ) ) /\ ( X ./\ Y ) C Y ) -> ( ( X ./\ Y ) e. N <-> Y e. P ) ) |
23 |
7 14 16 21 22
|
syl31anc |
|- ( ( ( K e. HL /\ X e. P /\ Y e. P ) /\ X C ( X .\/ Y ) ) -> ( ( X ./\ Y ) e. N <-> Y e. P ) ) |
24 |
6 23
|
mpbird |
|- ( ( ( K e. HL /\ X e. P /\ Y e. P ) /\ X C ( X .\/ Y ) ) -> ( X ./\ Y ) e. N ) |