Step |
Hyp |
Ref |
Expression |
1 |
|
isline.l |
|- .<_ = ( le ` K ) |
2 |
|
isline.j |
|- .\/ = ( join ` K ) |
3 |
|
isline.a |
|- A = ( Atoms ` K ) |
4 |
|
isline.n |
|- N = ( Lines ` K ) |
5 |
|
simpl2 |
|- ( ( ( K e. D /\ Q e. A /\ R e. A ) /\ ( Q =/= R /\ X = { p e. A | p .<_ ( Q .\/ R ) } ) ) -> Q e. A ) |
6 |
|
simpl3 |
|- ( ( ( K e. D /\ Q e. A /\ R e. A ) /\ ( Q =/= R /\ X = { p e. A | p .<_ ( Q .\/ R ) } ) ) -> R e. A ) |
7 |
|
simpr |
|- ( ( ( K e. D /\ Q e. A /\ R e. A ) /\ ( Q =/= R /\ X = { p e. A | p .<_ ( Q .\/ R ) } ) ) -> ( Q =/= R /\ X = { p e. A | p .<_ ( Q .\/ R ) } ) ) |
8 |
|
neeq1 |
|- ( q = Q -> ( q =/= r <-> Q =/= r ) ) |
9 |
|
oveq1 |
|- ( q = Q -> ( q .\/ r ) = ( Q .\/ r ) ) |
10 |
9
|
breq2d |
|- ( q = Q -> ( p .<_ ( q .\/ r ) <-> p .<_ ( Q .\/ r ) ) ) |
11 |
10
|
rabbidv |
|- ( q = Q -> { p e. A | p .<_ ( q .\/ r ) } = { p e. A | p .<_ ( Q .\/ r ) } ) |
12 |
11
|
eqeq2d |
|- ( q = Q -> ( X = { p e. A | p .<_ ( q .\/ r ) } <-> X = { p e. A | p .<_ ( Q .\/ r ) } ) ) |
13 |
8 12
|
anbi12d |
|- ( q = Q -> ( ( q =/= r /\ X = { p e. A | p .<_ ( q .\/ r ) } ) <-> ( Q =/= r /\ X = { p e. A | p .<_ ( Q .\/ r ) } ) ) ) |
14 |
|
neeq2 |
|- ( r = R -> ( Q =/= r <-> Q =/= R ) ) |
15 |
|
oveq2 |
|- ( r = R -> ( Q .\/ r ) = ( Q .\/ R ) ) |
16 |
15
|
breq2d |
|- ( r = R -> ( p .<_ ( Q .\/ r ) <-> p .<_ ( Q .\/ R ) ) ) |
17 |
16
|
rabbidv |
|- ( r = R -> { p e. A | p .<_ ( Q .\/ r ) } = { p e. A | p .<_ ( Q .\/ R ) } ) |
18 |
17
|
eqeq2d |
|- ( r = R -> ( X = { p e. A | p .<_ ( Q .\/ r ) } <-> X = { p e. A | p .<_ ( Q .\/ R ) } ) ) |
19 |
14 18
|
anbi12d |
|- ( r = R -> ( ( Q =/= r /\ X = { p e. A | p .<_ ( Q .\/ r ) } ) <-> ( Q =/= R /\ X = { p e. A | p .<_ ( Q .\/ R ) } ) ) ) |
20 |
13 19
|
rspc2ev |
|- ( ( Q e. A /\ R e. A /\ ( Q =/= R /\ X = { p e. A | p .<_ ( Q .\/ R ) } ) ) -> E. q e. A E. r e. A ( q =/= r /\ X = { p e. A | p .<_ ( q .\/ r ) } ) ) |
21 |
5 6 7 20
|
syl3anc |
|- ( ( ( K e. D /\ Q e. A /\ R e. A ) /\ ( Q =/= R /\ X = { p e. A | p .<_ ( Q .\/ R ) } ) ) -> E. q e. A E. r e. A ( q =/= r /\ X = { p e. A | p .<_ ( q .\/ r ) } ) ) |
22 |
|
simpl1 |
|- ( ( ( K e. D /\ Q e. A /\ R e. A ) /\ ( Q =/= R /\ X = { p e. A | p .<_ ( Q .\/ R ) } ) ) -> K e. D ) |
23 |
1 2 3 4
|
isline |
|- ( K e. D -> ( X e. N <-> E. q e. A E. r e. A ( q =/= r /\ X = { p e. A | p .<_ ( q .\/ r ) } ) ) ) |
24 |
22 23
|
syl |
|- ( ( ( K e. D /\ Q e. A /\ R e. A ) /\ ( Q =/= R /\ X = { p e. A | p .<_ ( Q .\/ R ) } ) ) -> ( X e. N <-> E. q e. A E. r e. A ( q =/= r /\ X = { p e. A | p .<_ ( q .\/ r ) } ) ) ) |
25 |
21 24
|
mpbird |
|- ( ( ( K e. D /\ Q e. A /\ R e. A ) /\ ( Q =/= R /\ X = { p e. A | p .<_ ( Q .\/ R ) } ) ) -> X e. N ) |