Metamath Proof Explorer

Theorem isline3

Description: Definition of line in terms of original lattice elements. (Contributed by NM, 29-Apr-2012)

Ref Expression
Hypotheses isline3.b 
|- B = ( Base ` K )
isline3.j 
|- .\/ = ( join ` K )
isline3.a 
|- A = ( Atoms ` K )
isline3.n 
|- N = ( Lines ` K )
isline3.m 
|- M = ( pmap ` K )
Assertion isline3 
|- ( ( K e. HL /\ X e. B ) -> ( ( M ` X ) e. N <-> E. p e. A E. q e. A ( p =/= q /\ X = ( p .\/ q ) ) ) )

Proof

Step Hyp Ref Expression
1 isline3.b 
 |-  B = ( Base ` K )
2 isline3.j 
 |-  .\/ = ( join ` K )
3 isline3.a 
 |-  A = ( Atoms ` K )
4 isline3.n 
 |-  N = ( Lines ` K )
5 isline3.m 
 |-  M = ( pmap ` K )
6 hllat 
 |-  ( K e. HL -> K e. Lat )
7 6 adantr 
 |-  ( ( K e. HL /\ X e. B ) -> K e. Lat )
8 2 3 4 5 isline2 
 |-  ( K e. Lat -> ( ( M ` X ) e. N <-> E. p e. A E. q e. A ( p =/= q /\ ( M ` X ) = ( M ` ( p .\/ q ) ) ) ) )
9 7 8 syl 
 |-  ( ( K e. HL /\ X e. B ) -> ( ( M ` X ) e. N <-> E. p e. A E. q e. A ( p =/= q /\ ( M ` X ) = ( M ` ( p .\/ q ) ) ) ) )
10 simpll 
 |-  ( ( ( K e. HL /\ X e. B ) /\ ( p e. A /\ q e. A ) ) -> K e. HL )
11 simplr 
 |-  ( ( ( K e. HL /\ X e. B ) /\ ( p e. A /\ q e. A ) ) -> X e. B )
12 6 ad2antrr 
 |-  ( ( ( K e. HL /\ X e. B ) /\ ( p e. A /\ q e. A ) ) -> K e. Lat )
13 1 3 atbase 
 |-  ( p e. A -> p e. B )
14 13 ad2antrl 
 |-  ( ( ( K e. HL /\ X e. B ) /\ ( p e. A /\ q e. A ) ) -> p e. B )
15 1 3 atbase 
 |-  ( q e. A -> q e. B )
16 15 ad2antll 
 |-  ( ( ( K e. HL /\ X e. B ) /\ ( p e. A /\ q e. A ) ) -> q e. B )
17 1 2 latjcl 
 |-  ( ( K e. Lat /\ p e. B /\ q e. B ) -> ( p .\/ q ) e. B )
18 12 14 16 17 syl3anc 
 |-  ( ( ( K e. HL /\ X e. B ) /\ ( p e. A /\ q e. A ) ) -> ( p .\/ q ) e. B )
19 1 5 pmap11 
 |-  ( ( K e. HL /\ X e. B /\ ( p .\/ q ) e. B ) -> ( ( M ` X ) = ( M ` ( p .\/ q ) ) <-> X = ( p .\/ q ) ) )
20 10 11 18 19 syl3anc 
 |-  ( ( ( K e. HL /\ X e. B ) /\ ( p e. A /\ q e. A ) ) -> ( ( M ` X ) = ( M ` ( p .\/ q ) ) <-> X = ( p .\/ q ) ) )
21 20 anbi2d 
 |-  ( ( ( K e. HL /\ X e. B ) /\ ( p e. A /\ q e. A ) ) -> ( ( p =/= q /\ ( M ` X ) = ( M ` ( p .\/ q ) ) ) <-> ( p =/= q /\ X = ( p .\/ q ) ) ) )
22 21 2rexbidva 
 |-  ( ( K e. HL /\ X e. B ) -> ( E. p e. A E. q e. A ( p =/= q /\ ( M ` X ) = ( M ` ( p .\/ q ) ) ) <-> E. p e. A E. q e. A ( p =/= q /\ X = ( p .\/ q ) ) ) )
23 9 22 bitrd 
 |-  ( ( K e. HL /\ X e. B ) -> ( ( M ` X ) e. N <-> E. p e. A E. q e. A ( p =/= q /\ X = ( p .\/ q ) ) ) )