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

Metamath Proof Explorer

Theorem lnjatN

Description: Given an atom in a line, there is another atom which when joined equals the line. (Contributed by NM, 30-Apr-2012) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 lnjat.b 
 |-  B = ( Base ` K )
2 lnjat.l 
 |-  .<_ = ( le ` K )
3 lnjat.j 
 |-  .\/ = ( join ` K )
4 lnjat.a 
 |-  A = ( Atoms ` K )
5 lnjat.n 
 |-  N = ( Lines ` K )
6 lnjat.m 
 |-  M = ( pmap ` K )
7 simpl1 
 |-  ( ( ( K e. HL /\ X e. B /\ P e. A ) /\ ( ( M ` X ) e. N /\ P .<_ X ) ) -> K e. HL )
8 simpl2 
 |-  ( ( ( K e. HL /\ X e. B /\ P e. A ) /\ ( ( M ` X ) e. N /\ P .<_ X ) ) -> X e. B )
9 simprl 
 |-  ( ( ( K e. HL /\ X e. B /\ P e. A ) /\ ( ( M ` X ) e. N /\ P .<_ X ) ) -> ( M ` X ) e. N )
10 1 2 4 5 6 lnatexN 
 |-  ( ( K e. HL /\ X e. B /\ ( M ` X ) e. N ) -> E. q e. A ( q =/= P /\ q .<_ X ) )
11 7 8 9 10 syl3anc 
 |-  ( ( ( K e. HL /\ X e. B /\ P e. A ) /\ ( ( M ` X ) e. N /\ P .<_ X ) ) -> E. q e. A ( q =/= P /\ q .<_ X ) )
12 simp3l 
 |-  ( ( ( ( K e. HL /\ X e. B /\ P e. A ) /\ ( ( M ` X ) e. N /\ P .<_ X ) ) /\ q e. A /\ ( q =/= P /\ q .<_ X ) ) -> q =/= P )
13 simp1l1 
 |-  ( ( ( ( K e. HL /\ X e. B /\ P e. A ) /\ ( ( M ` X ) e. N /\ P .<_ X ) ) /\ q e. A /\ ( q =/= P /\ q .<_ X ) ) -> K e. HL )
14 simp1l2 
 |-  ( ( ( ( K e. HL /\ X e. B /\ P e. A ) /\ ( ( M ` X ) e. N /\ P .<_ X ) ) /\ q e. A /\ ( q =/= P /\ q .<_ X ) ) -> X e. B )
15 simp1rl 
 |-  ( ( ( ( K e. HL /\ X e. B /\ P e. A ) /\ ( ( M ` X ) e. N /\ P .<_ X ) ) /\ q e. A /\ ( q =/= P /\ q .<_ X ) ) -> ( M ` X ) e. N )
16 simp1l3 
 |-  ( ( ( ( K e. HL /\ X e. B /\ P e. A ) /\ ( ( M ` X ) e. N /\ P .<_ X ) ) /\ q e. A /\ ( q =/= P /\ q .<_ X ) ) -> P e. A )
17 simp2 
 |-  ( ( ( ( K e. HL /\ X e. B /\ P e. A ) /\ ( ( M ` X ) e. N /\ P .<_ X ) ) /\ q e. A /\ ( q =/= P /\ q .<_ X ) ) -> q e. A )
18 12 necomd 
 |-  ( ( ( ( K e. HL /\ X e. B /\ P e. A ) /\ ( ( M ` X ) e. N /\ P .<_ X ) ) /\ q e. A /\ ( q =/= P /\ q .<_ X ) ) -> P =/= q )
19 simp1rr 
 |-  ( ( ( ( K e. HL /\ X e. B /\ P e. A ) /\ ( ( M ` X ) e. N /\ P .<_ X ) ) /\ q e. A /\ ( q =/= P /\ q .<_ X ) ) -> P .<_ X )
20 simp3r 
 |-  ( ( ( ( K e. HL /\ X e. B /\ P e. A ) /\ ( ( M ` X ) e. N /\ P .<_ X ) ) /\ q e. A /\ ( q =/= P /\ q .<_ X ) ) -> q .<_ X )
21 1 2 3 4 5 6 lneq2at 
 |-  ( ( ( K e. HL /\ X e. B /\ ( M ` X ) e. N ) /\ ( P e. A /\ q e. A /\ P =/= q ) /\ ( P .<_ X /\ q .<_ X ) ) -> X = ( P .\/ q ) )
22 13 14 15 16 17 18 19 20 21 syl332anc 
 |-  ( ( ( ( K e. HL /\ X e. B /\ P e. A ) /\ ( ( M ` X ) e. N /\ P .<_ X ) ) /\ q e. A /\ ( q =/= P /\ q .<_ X ) ) -> X = ( P .\/ q ) )
23 12 22 jca 
 |-  ( ( ( ( K e. HL /\ X e. B /\ P e. A ) /\ ( ( M ` X ) e. N /\ P .<_ X ) ) /\ q e. A /\ ( q =/= P /\ q .<_ X ) ) -> ( q =/= P /\ X = ( P .\/ q ) ) )
24 23 3exp 
 |-  ( ( ( K e. HL /\ X e. B /\ P e. A ) /\ ( ( M ` X ) e. N /\ P .<_ X ) ) -> ( q e. A -> ( ( q =/= P /\ q .<_ X ) -> ( q =/= P /\ X = ( P .\/ q ) ) ) ) )
25 24 reximdvai 
 |-  ( ( ( K e. HL /\ X e. B /\ P e. A ) /\ ( ( M ` X ) e. N /\ P .<_ X ) ) -> ( E. q e. A ( q =/= P /\ q .<_ X ) -> E. q e. A ( q =/= P /\ X = ( P .\/ q ) ) ) )
26 11 25 mpd 
 |-  ( ( ( K e. HL /\ X e. B /\ P e. A ) /\ ( ( M ` X ) e. N /\ P .<_ X ) ) -> E. q e. A ( q =/= P /\ X = ( P .\/ q ) ) )