Metamath Proof Explorer


Theorem lneq2at

Description: A line equals the join of any two of its distinct points (atoms). (Contributed by NM, 29-Apr-2012)

Ref Expression
Hypotheses lneq2at.b B = Base K
lneq2at.l ˙ = K
lneq2at.j ˙ = join K
lneq2at.a A = Atoms K
lneq2at.n N = Lines K
lneq2at.m M = pmap K
Assertion lneq2at K HL X B M X N P A Q A P Q P ˙ X Q ˙ X X = P ˙ Q

Proof

Step Hyp Ref Expression
1 lneq2at.b B = Base K
2 lneq2at.l ˙ = K
3 lneq2at.j ˙ = join K
4 lneq2at.a A = Atoms K
5 lneq2at.n N = Lines K
6 lneq2at.m M = pmap K
7 simp11 K HL X B M X N P A Q A P Q P ˙ X Q ˙ X K HL
8 simp12 K HL X B M X N P A Q A P Q P ˙ X Q ˙ X X B
9 7 8 jca K HL X B M X N P A Q A P Q P ˙ X Q ˙ X K HL X B
10 simp13 K HL X B M X N P A Q A P Q P ˙ X Q ˙ X M X N
11 1 3 4 5 6 isline3 K HL X B M X N r A s A r s X = r ˙ s
12 11 biimpd K HL X B M X N r A s A r s X = r ˙ s
13 9 10 12 sylc K HL X B M X N P A Q A P Q P ˙ X Q ˙ X r A s A r s X = r ˙ s
14 simp3r K HL X B M X N P A Q A P Q P ˙ X Q ˙ X r A s A r s X = r ˙ s X = r ˙ s
15 simp111 K HL X B M X N P A Q A P Q P ˙ X Q ˙ X r A s A r s X = r ˙ s K HL
16 simp121 K HL X B M X N P A Q A P Q P ˙ X Q ˙ X r A s A r s X = r ˙ s P A
17 simp122 K HL X B M X N P A Q A P Q P ˙ X Q ˙ X r A s A r s X = r ˙ s Q A
18 16 17 jca K HL X B M X N P A Q A P Q P ˙ X Q ˙ X r A s A r s X = r ˙ s P A Q A
19 simp2 K HL X B M X N P A Q A P Q P ˙ X Q ˙ X r A s A r s X = r ˙ s r A s A
20 15 18 19 3jca K HL X B M X N P A Q A P Q P ˙ X Q ˙ X r A s A r s X = r ˙ s K HL P A Q A r A s A
21 simp123 K HL X B M X N P A Q A P Q P ˙ X Q ˙ X r A s A r s X = r ˙ s P Q
22 20 21 jca K HL X B M X N P A Q A P Q P ˙ X Q ˙ X r A s A r s X = r ˙ s K HL P A Q A r A s A P Q
23 7 hllatd K HL X B M X N P A Q A P Q P ˙ X Q ˙ X K Lat
24 simp21 K HL X B M X N P A Q A P Q P ˙ X Q ˙ X P A
25 1 4 atbase P A P B
26 24 25 syl K HL X B M X N P A Q A P Q P ˙ X Q ˙ X P B
27 simp22 K HL X B M X N P A Q A P Q P ˙ X Q ˙ X Q A
28 1 4 atbase Q A Q B
29 27 28 syl K HL X B M X N P A Q A P Q P ˙ X Q ˙ X Q B
30 26 29 8 3jca K HL X B M X N P A Q A P Q P ˙ X Q ˙ X P B Q B X B
31 23 30 jca K HL X B M X N P A Q A P Q P ˙ X Q ˙ X K Lat P B Q B X B
32 simp3 K HL X B M X N P A Q A P Q P ˙ X Q ˙ X P ˙ X Q ˙ X
33 1 2 3 latjle12 K Lat P B Q B X B P ˙ X Q ˙ X P ˙ Q ˙ X
34 33 biimpd K Lat P B Q B X B P ˙ X Q ˙ X P ˙ Q ˙ X
35 31 32 34 sylc K HL X B M X N P A Q A P Q P ˙ X Q ˙ X P ˙ Q ˙ X
36 35 3ad2ant1 K HL X B M X N P A Q A P Q P ˙ X Q ˙ X r A s A r s X = r ˙ s P ˙ Q ˙ X
37 36 14 breqtrd K HL X B M X N P A Q A P Q P ˙ X Q ˙ X r A s A r s X = r ˙ s P ˙ Q ˙ r ˙ s
38 simpl1 K HL P A Q A r A s A P Q K HL
39 simpl2l K HL P A Q A r A s A P Q P A
40 simpl2r K HL P A Q A r A s A P Q Q A
41 simpr K HL P A Q A r A s A P Q P Q
42 simpl3 K HL P A Q A r A s A P Q r A s A
43 2 3 4 ps-1 K HL P A Q A P Q r A s A P ˙ Q ˙ r ˙ s P ˙ Q = r ˙ s
44 38 39 40 41 42 43 syl131anc K HL P A Q A r A s A P Q P ˙ Q ˙ r ˙ s P ˙ Q = r ˙ s
45 44 biimpd K HL P A Q A r A s A P Q P ˙ Q ˙ r ˙ s P ˙ Q = r ˙ s
46 22 37 45 sylc K HL X B M X N P A Q A P Q P ˙ X Q ˙ X r A s A r s X = r ˙ s P ˙ Q = r ˙ s
47 14 46 eqtr4d K HL X B M X N P A Q A P Q P ˙ X Q ˙ X r A s A r s X = r ˙ s X = P ˙ Q
48 47 3exp K HL X B M X N P A Q A P Q P ˙ X Q ˙ X r A s A r s X = r ˙ s X = P ˙ Q
49 48 rexlimdvv K HL X B M X N P A Q A P Q P ˙ X Q ˙ X r A s A r s X = r ˙ s X = P ˙ Q
50 13 49 mpd K HL X B M X N P A Q A P Q P ˙ X Q ˙ X X = P ˙ Q