Metamath Proof Explorer

Theorem 2llnjN

Description: The join of two different lattice lines in a lattice plane equals the plane. (Contributed by NM, 4-Jul-2012) (New usage is discouraged.)

Ref Expression
Hypotheses 2llnj.l 
|- .<_ = ( le ` K )
2llnj.j 
|- .\/ = ( join ` K )
2llnj.n 
|- N = ( LLines ` K )
2llnj.p 
|- P = ( LPlanes ` K )
Assertion 2llnjN 
|- ( ( K e. HL /\ ( X e. N /\ Y e. N /\ W e. P ) /\ ( X .<_ W /\ Y .<_ W /\ X =/= Y ) ) -> ( X .\/ Y ) = W )

Proof

Step Hyp Ref Expression
1 2llnj.l 
 |-  .<_ = ( le ` K )
2 2llnj.j 
 |-  .\/ = ( join ` K )
3 2llnj.n 
 |-  N = ( LLines ` K )
4 2llnj.p 
 |-  P = ( LPlanes ` K )
5 eqid 
 |-  ( Base ` K ) = ( Base ` K )
6 eqid 
 |-  ( Atoms ` K ) = ( Atoms ` K )
7 5 2 6 3 islln2 
 |-  ( K e. HL -> ( X e. N <-> ( X e. ( Base ` K ) /\ E. q e. ( Atoms ` K ) E. r e. ( Atoms ` K ) ( q =/= r /\ X = ( q .\/ r ) ) ) ) )
8 simpr 
 |-  ( ( X e. ( Base ` K ) /\ E. q e. ( Atoms ` K ) E. r e. ( Atoms ` K ) ( q =/= r /\ X = ( q .\/ r ) ) ) -> E. q e. ( Atoms ` K ) E. r e. ( Atoms ` K ) ( q =/= r /\ X = ( q .\/ r ) ) )
9 7 8 syl6bi 
 |-  ( K e. HL -> ( X e. N -> E. q e. ( Atoms ` K ) E. r e. ( Atoms ` K ) ( q =/= r /\ X = ( q .\/ r ) ) ) )
10 5 2 6 3 islln2 
 |-  ( K e. HL -> ( Y e. N <-> ( Y e. ( Base ` K ) /\ E. s e. ( Atoms ` K ) E. t e. ( Atoms ` K ) ( s =/= t /\ Y = ( s .\/ t ) ) ) ) )
11 simpr 
 |-  ( ( Y e. ( Base ` K ) /\ E. s e. ( Atoms ` K ) E. t e. ( Atoms ` K ) ( s =/= t /\ Y = ( s .\/ t ) ) ) -> E. s e. ( Atoms ` K ) E. t e. ( Atoms ` K ) ( s =/= t /\ Y = ( s .\/ t ) ) )
12 10 11 syl6bi 
 |-  ( K e. HL -> ( Y e. N -> E. s e. ( Atoms ` K ) E. t e. ( Atoms ` K ) ( s =/= t /\ Y = ( s .\/ t ) ) ) )
13 9 12 anim12d 
 |-  ( K e. HL -> ( ( X e. N /\ Y e. N ) -> ( E. q e. ( Atoms ` K ) E. r e. ( Atoms ` K ) ( q =/= r /\ X = ( q .\/ r ) ) /\ E. s e. ( Atoms ` K ) E. t e. ( Atoms ` K ) ( s =/= t /\ Y = ( s .\/ t ) ) ) ) )
14 13 imp 
 |-  ( ( K e. HL /\ ( X e. N /\ Y e. N ) ) -> ( E. q e. ( Atoms ` K ) E. r e. ( Atoms ` K ) ( q =/= r /\ X = ( q .\/ r ) ) /\ E. s e. ( Atoms ` K ) E. t e. ( Atoms ` K ) ( s =/= t /\ Y = ( s .\/ t ) ) ) )
15 14 3adantr3 
 |-  ( ( K e. HL /\ ( X e. N /\ Y e. N /\ W e. P ) ) -> ( E. q e. ( Atoms ` K ) E. r e. ( Atoms ` K ) ( q =/= r /\ X = ( q .\/ r ) ) /\ E. s e. ( Atoms ` K ) E. t e. ( Atoms ` K ) ( s =/= t /\ Y = ( s .\/ t ) ) ) )
16 15 3adant3 
 |-  ( ( K e. HL /\ ( X e. N /\ Y e. N /\ W e. P ) /\ ( X .<_ W /\ Y .<_ W /\ X =/= Y ) ) -> ( E. q e. ( Atoms ` K ) E. r e. ( Atoms ` K ) ( q =/= r /\ X = ( q .\/ r ) ) /\ E. s e. ( Atoms ` K ) E. t e. ( Atoms ` K ) ( s =/= t /\ Y = ( s .\/ t ) ) ) )
17 simp2rr 
 |-  ( ( ( K e. HL /\ ( X e. N /\ Y e. N /\ W e. P ) /\ ( X .<_ W /\ Y .<_ W /\ X =/= Y ) ) /\ ( ( q e. ( Atoms ` K ) /\ r e. ( Atoms ` K ) ) /\ ( q =/= r /\ X = ( q .\/ r ) ) ) /\ ( ( s e. ( Atoms ` K ) /\ t e. ( Atoms ` K ) ) /\ ( s =/= t /\ Y = ( s .\/ t ) ) ) ) -> X = ( q .\/ r ) )
18 simp3rr 
 |-  ( ( ( K e. HL /\ ( X e. N /\ Y e. N /\ W e. P ) /\ ( X .<_ W /\ Y .<_ W /\ X =/= Y ) ) /\ ( ( q e. ( Atoms ` K ) /\ r e. ( Atoms ` K ) ) /\ ( q =/= r /\ X = ( q .\/ r ) ) ) /\ ( ( s e. ( Atoms ` K ) /\ t e. ( Atoms ` K ) ) /\ ( s =/= t /\ Y = ( s .\/ t ) ) ) ) -> Y = ( s .\/ t ) )
19 17 18 oveq12d 
 |-  ( ( ( K e. HL /\ ( X e. N /\ Y e. N /\ W e. P ) /\ ( X .<_ W /\ Y .<_ W /\ X =/= Y ) ) /\ ( ( q e. ( Atoms ` K ) /\ r e. ( Atoms ` K ) ) /\ ( q =/= r /\ X = ( q .\/ r ) ) ) /\ ( ( s e. ( Atoms ` K ) /\ t e. ( Atoms ` K ) ) /\ ( s =/= t /\ Y = ( s .\/ t ) ) ) ) -> ( X .\/ Y ) = ( ( q .\/ r ) .\/ ( s .\/ t ) ) )
20 simp13 
 |-  ( ( ( K e. HL /\ ( X e. N /\ Y e. N /\ W e. P ) /\ ( X .<_ W /\ Y .<_ W /\ X =/= Y ) ) /\ ( ( q e. ( Atoms ` K ) /\ r e. ( Atoms ` K ) ) /\ ( q =/= r /\ X = ( q .\/ r ) ) ) /\ ( ( s e. ( Atoms ` K ) /\ t e. ( Atoms ` K ) ) /\ ( s =/= t /\ Y = ( s .\/ t ) ) ) ) -> ( X .<_ W /\ Y .<_ W /\ X =/= Y ) )
21 breq1 
 |-  ( X = ( q .\/ r ) -> ( X .<_ W <-> ( q .\/ r ) .<_ W ) )
22 neeq1 
 |-  ( X = ( q .\/ r ) -> ( X =/= Y <-> ( q .\/ r ) =/= Y ) )
23 21 22 3anbi13d 
 |-  ( X = ( q .\/ r ) -> ( ( X .<_ W /\ Y .<_ W /\ X =/= Y ) <-> ( ( q .\/ r ) .<_ W /\ Y .<_ W /\ ( q .\/ r ) =/= Y ) ) )
24 breq1 
 |-  ( Y = ( s .\/ t ) -> ( Y .<_ W <-> ( s .\/ t ) .<_ W ) )
25 neeq2 
 |-  ( Y = ( s .\/ t ) -> ( ( q .\/ r ) =/= Y <-> ( q .\/ r ) =/= ( s .\/ t ) ) )
26 24 25 3anbi23d 
 |-  ( Y = ( s .\/ t ) -> ( ( ( q .\/ r ) .<_ W /\ Y .<_ W /\ ( q .\/ r ) =/= Y ) <-> ( ( q .\/ r ) .<_ W /\ ( s .\/ t ) .<_ W /\ ( q .\/ r ) =/= ( s .\/ t ) ) ) )
27 23 26 sylan9bb 
 |-  ( ( X = ( q .\/ r ) /\ Y = ( s .\/ t ) ) -> ( ( X .<_ W /\ Y .<_ W /\ X =/= Y ) <-> ( ( q .\/ r ) .<_ W /\ ( s .\/ t ) .<_ W /\ ( q .\/ r ) =/= ( s .\/ t ) ) ) )
28 17 18 27 syl2anc 
 |-  ( ( ( K e. HL /\ ( X e. N /\ Y e. N /\ W e. P ) /\ ( X .<_ W /\ Y .<_ W /\ X =/= Y ) ) /\ ( ( q e. ( Atoms ` K ) /\ r e. ( Atoms ` K ) ) /\ ( q =/= r /\ X = ( q .\/ r ) ) ) /\ ( ( s e. ( Atoms ` K ) /\ t e. ( Atoms ` K ) ) /\ ( s =/= t /\ Y = ( s .\/ t ) ) ) ) -> ( ( X .<_ W /\ Y .<_ W /\ X =/= Y ) <-> ( ( q .\/ r ) .<_ W /\ ( s .\/ t ) .<_ W /\ ( q .\/ r ) =/= ( s .\/ t ) ) ) )
29 20 28 mpbid 
 |-  ( ( ( K e. HL /\ ( X e. N /\ Y e. N /\ W e. P ) /\ ( X .<_ W /\ Y .<_ W /\ X =/= Y ) ) /\ ( ( q e. ( Atoms ` K ) /\ r e. ( Atoms ` K ) ) /\ ( q =/= r /\ X = ( q .\/ r ) ) ) /\ ( ( s e. ( Atoms ` K ) /\ t e. ( Atoms ` K ) ) /\ ( s =/= t /\ Y = ( s .\/ t ) ) ) ) -> ( ( q .\/ r ) .<_ W /\ ( s .\/ t ) .<_ W /\ ( q .\/ r ) =/= ( s .\/ t ) ) )
30 simp11 
 |-  ( ( ( K e. HL /\ ( X e. N /\ Y e. N /\ W e. P ) /\ ( X .<_ W /\ Y .<_ W /\ X =/= Y ) ) /\ ( ( q e. ( Atoms ` K ) /\ r e. ( Atoms ` K ) ) /\ ( q =/= r /\ X = ( q .\/ r ) ) ) /\ ( ( s e. ( Atoms ` K ) /\ t e. ( Atoms ` K ) ) /\ ( s =/= t /\ Y = ( s .\/ t ) ) ) ) -> K e. HL )
31 simp123 
 |-  ( ( ( K e. HL /\ ( X e. N /\ Y e. N /\ W e. P ) /\ ( X .<_ W /\ Y .<_ W /\ X =/= Y ) ) /\ ( ( q e. ( Atoms ` K ) /\ r e. ( Atoms ` K ) ) /\ ( q =/= r /\ X = ( q .\/ r ) ) ) /\ ( ( s e. ( Atoms ` K ) /\ t e. ( Atoms ` K ) ) /\ ( s =/= t /\ Y = ( s .\/ t ) ) ) ) -> W e. P )
32 simp2ll 
 |-  ( ( ( K e. HL /\ ( X e. N /\ Y e. N /\ W e. P ) /\ ( X .<_ W /\ Y .<_ W /\ X =/= Y ) ) /\ ( ( q e. ( Atoms ` K ) /\ r e. ( Atoms ` K ) ) /\ ( q =/= r /\ X = ( q .\/ r ) ) ) /\ ( ( s e. ( Atoms ` K ) /\ t e. ( Atoms ` K ) ) /\ ( s =/= t /\ Y = ( s .\/ t ) ) ) ) -> q e. ( Atoms ` K ) )
33 simp2lr 
 |-  ( ( ( K e. HL /\ ( X e. N /\ Y e. N /\ W e. P ) /\ ( X .<_ W /\ Y .<_ W /\ X =/= Y ) ) /\ ( ( q e. ( Atoms ` K ) /\ r e. ( Atoms ` K ) ) /\ ( q =/= r /\ X = ( q .\/ r ) ) ) /\ ( ( s e. ( Atoms ` K ) /\ t e. ( Atoms ` K ) ) /\ ( s =/= t /\ Y = ( s .\/ t ) ) ) ) -> r e. ( Atoms ` K ) )
34 simp2rl 
 |-  ( ( ( K e. HL /\ ( X e. N /\ Y e. N /\ W e. P ) /\ ( X .<_ W /\ Y .<_ W /\ X =/= Y ) ) /\ ( ( q e. ( Atoms ` K ) /\ r e. ( Atoms ` K ) ) /\ ( q =/= r /\ X = ( q .\/ r ) ) ) /\ ( ( s e. ( Atoms ` K ) /\ t e. ( Atoms ` K ) ) /\ ( s =/= t /\ Y = ( s .\/ t ) ) ) ) -> q =/= r )
35 simp3ll 
 |-  ( ( ( K e. HL /\ ( X e. N /\ Y e. N /\ W e. P ) /\ ( X .<_ W /\ Y .<_ W /\ X =/= Y ) ) /\ ( ( q e. ( Atoms ` K ) /\ r e. ( Atoms ` K ) ) /\ ( q =/= r /\ X = ( q .\/ r ) ) ) /\ ( ( s e. ( Atoms ` K ) /\ t e. ( Atoms ` K ) ) /\ ( s =/= t /\ Y = ( s .\/ t ) ) ) ) -> s e. ( Atoms ` K ) )
36 simp3lr 
 |-  ( ( ( K e. HL /\ ( X e. N /\ Y e. N /\ W e. P ) /\ ( X .<_ W /\ Y .<_ W /\ X =/= Y ) ) /\ ( ( q e. ( Atoms ` K ) /\ r e. ( Atoms ` K ) ) /\ ( q =/= r /\ X = ( q .\/ r ) ) ) /\ ( ( s e. ( Atoms ` K ) /\ t e. ( Atoms ` K ) ) /\ ( s =/= t /\ Y = ( s .\/ t ) ) ) ) -> t e. ( Atoms ` K ) )
37 simp3rl 
 |-  ( ( ( K e. HL /\ ( X e. N /\ Y e. N /\ W e. P ) /\ ( X .<_ W /\ Y .<_ W /\ X =/= Y ) ) /\ ( ( q e. ( Atoms ` K ) /\ r e. ( Atoms ` K ) ) /\ ( q =/= r /\ X = ( q .\/ r ) ) ) /\ ( ( s e. ( Atoms ` K ) /\ t e. ( Atoms ` K ) ) /\ ( s =/= t /\ Y = ( s .\/ t ) ) ) ) -> s =/= t )
38 1 2 6 3 4 2llnjaN 
 |-  ( ( ( ( K e. HL /\ W e. P ) /\ ( q e. ( Atoms ` K ) /\ r e. ( Atoms ` K ) /\ q =/= r ) /\ ( s e. ( Atoms ` K ) /\ t e. ( Atoms ` K ) /\ s =/= t ) ) /\ ( ( q .\/ r ) .<_ W /\ ( s .\/ t ) .<_ W /\ ( q .\/ r ) =/= ( s .\/ t ) ) ) -> ( ( q .\/ r ) .\/ ( s .\/ t ) ) = W )
39 38 ex 
 |-  ( ( ( K e. HL /\ W e. P ) /\ ( q e. ( Atoms ` K ) /\ r e. ( Atoms ` K ) /\ q =/= r ) /\ ( s e. ( Atoms ` K ) /\ t e. ( Atoms ` K ) /\ s =/= t ) ) -> ( ( ( q .\/ r ) .<_ W /\ ( s .\/ t ) .<_ W /\ ( q .\/ r ) =/= ( s .\/ t ) ) -> ( ( q .\/ r ) .\/ ( s .\/ t ) ) = W ) )
40 30 31 32 33 34 35 36 37 39 syl233anc 
 |-  ( ( ( K e. HL /\ ( X e. N /\ Y e. N /\ W e. P ) /\ ( X .<_ W /\ Y .<_ W /\ X =/= Y ) ) /\ ( ( q e. ( Atoms ` K ) /\ r e. ( Atoms ` K ) ) /\ ( q =/= r /\ X = ( q .\/ r ) ) ) /\ ( ( s e. ( Atoms ` K ) /\ t e. ( Atoms ` K ) ) /\ ( s =/= t /\ Y = ( s .\/ t ) ) ) ) -> ( ( ( q .\/ r ) .<_ W /\ ( s .\/ t ) .<_ W /\ ( q .\/ r ) =/= ( s .\/ t ) ) -> ( ( q .\/ r ) .\/ ( s .\/ t ) ) = W ) )
41 29 40 mpd 
 |-  ( ( ( K e. HL /\ ( X e. N /\ Y e. N /\ W e. P ) /\ ( X .<_ W /\ Y .<_ W /\ X =/= Y ) ) /\ ( ( q e. ( Atoms ` K ) /\ r e. ( Atoms ` K ) ) /\ ( q =/= r /\ X = ( q .\/ r ) ) ) /\ ( ( s e. ( Atoms ` K ) /\ t e. ( Atoms ` K ) ) /\ ( s =/= t /\ Y = ( s .\/ t ) ) ) ) -> ( ( q .\/ r ) .\/ ( s .\/ t ) ) = W )
42 19 41 eqtrd 
 |-  ( ( ( K e. HL /\ ( X e. N /\ Y e. N /\ W e. P ) /\ ( X .<_ W /\ Y .<_ W /\ X =/= Y ) ) /\ ( ( q e. ( Atoms ` K ) /\ r e. ( Atoms ` K ) ) /\ ( q =/= r /\ X = ( q .\/ r ) ) ) /\ ( ( s e. ( Atoms ` K ) /\ t e. ( Atoms ` K ) ) /\ ( s =/= t /\ Y = ( s .\/ t ) ) ) ) -> ( X .\/ Y ) = W )
43 42 3exp 
 |-  ( ( K e. HL /\ ( X e. N /\ Y e. N /\ W e. P ) /\ ( X .<_ W /\ Y .<_ W /\ X =/= Y ) ) -> ( ( ( q e. ( Atoms ` K ) /\ r e. ( Atoms ` K ) ) /\ ( q =/= r /\ X = ( q .\/ r ) ) ) -> ( ( ( s e. ( Atoms ` K ) /\ t e. ( Atoms ` K ) ) /\ ( s =/= t /\ Y = ( s .\/ t ) ) ) -> ( X .\/ Y ) = W ) ) )
44 43 3impib 
 |-  ( ( ( K e. HL /\ ( X e. N /\ Y e. N /\ W e. P ) /\ ( X .<_ W /\ Y .<_ W /\ X =/= Y ) ) /\ ( q e. ( Atoms ` K ) /\ r e. ( Atoms ` K ) ) /\ ( q =/= r /\ X = ( q .\/ r ) ) ) -> ( ( ( s e. ( Atoms ` K ) /\ t e. ( Atoms ` K ) ) /\ ( s =/= t /\ Y = ( s .\/ t ) ) ) -> ( X .\/ Y ) = W ) )
45 44 expd 
 |-  ( ( ( K e. HL /\ ( X e. N /\ Y e. N /\ W e. P ) /\ ( X .<_ W /\ Y .<_ W /\ X =/= Y ) ) /\ ( q e. ( Atoms ` K ) /\ r e. ( Atoms ` K ) ) /\ ( q =/= r /\ X = ( q .\/ r ) ) ) -> ( ( s e. ( Atoms ` K ) /\ t e. ( Atoms ` K ) ) -> ( ( s =/= t /\ Y = ( s .\/ t ) ) -> ( X .\/ Y ) = W ) ) )
46 45 rexlimdvv 
 |-  ( ( ( K e. HL /\ ( X e. N /\ Y e. N /\ W e. P ) /\ ( X .<_ W /\ Y .<_ W /\ X =/= Y ) ) /\ ( q e. ( Atoms ` K ) /\ r e. ( Atoms ` K ) ) /\ ( q =/= r /\ X = ( q .\/ r ) ) ) -> ( E. s e. ( Atoms ` K ) E. t e. ( Atoms ` K ) ( s =/= t /\ Y = ( s .\/ t ) ) -> ( X .\/ Y ) = W ) )
47 46 3exp 
 |-  ( ( K e. HL /\ ( X e. N /\ Y e. N /\ W e. P ) /\ ( X .<_ W /\ Y .<_ W /\ X =/= Y ) ) -> ( ( q e. ( Atoms ` K ) /\ r e. ( Atoms ` K ) ) -> ( ( q =/= r /\ X = ( q .\/ r ) ) -> ( E. s e. ( Atoms ` K ) E. t e. ( Atoms ` K ) ( s =/= t /\ Y = ( s .\/ t ) ) -> ( X .\/ Y ) = W ) ) ) )
48 47 rexlimdvv 
 |-  ( ( K e. HL /\ ( X e. N /\ Y e. N /\ W e. P ) /\ ( X .<_ W /\ Y .<_ W /\ X =/= Y ) ) -> ( E. q e. ( Atoms ` K ) E. r e. ( Atoms ` K ) ( q =/= r /\ X = ( q .\/ r ) ) -> ( E. s e. ( Atoms ` K ) E. t e. ( Atoms ` K ) ( s =/= t /\ Y = ( s .\/ t ) ) -> ( X .\/ Y ) = W ) ) )
49 48 impd 
 |-  ( ( K e. HL /\ ( X e. N /\ Y e. N /\ W e. P ) /\ ( X .<_ W /\ Y .<_ W /\ X =/= Y ) ) -> ( ( E. q e. ( Atoms ` K ) E. r e. ( Atoms ` K ) ( q =/= r /\ X = ( q .\/ r ) ) /\ E. s e. ( Atoms ` K ) E. t e. ( Atoms ` K ) ( s =/= t /\ Y = ( s .\/ t ) ) ) -> ( X .\/ Y ) = W ) )
50 16 49 mpd 
 |-  ( ( K e. HL /\ ( X e. N /\ Y e. N /\ W e. P ) /\ ( X .<_ W /\ Y .<_ W /\ X =/= Y ) ) -> ( X .\/ Y ) = W )