Metamath Proof Explorer


Theorem ps-2c

Description: Variation of projective geometry axiom ps-2 . (Contributed by NM, 3-Jul-2012)

Ref Expression
Hypotheses 2atm.l ˙ = K
2atm.j ˙ = join K
2atm.m ˙ = meet K
2atm.a A = Atoms K
Assertion ps-2c K HL P A Q A R A S A T A ¬ P ˙ Q ˙ R S T P ˙ R S ˙ T S ˙ P ˙ Q T ˙ Q ˙ R P ˙ R ˙ S ˙ T A

Proof

Step Hyp Ref Expression
1 2atm.l ˙ = K
2 2atm.j ˙ = join K
3 2atm.m ˙ = meet K
4 2atm.a A = Atoms K
5 simp11 K HL P A Q A R A S A T A ¬ P ˙ Q ˙ R S T P ˙ R S ˙ T S ˙ P ˙ Q T ˙ Q ˙ R K HL
6 simp12 K HL P A Q A R A S A T A ¬ P ˙ Q ˙ R S T P ˙ R S ˙ T S ˙ P ˙ Q T ˙ Q ˙ R P A
7 simp21 K HL P A Q A R A S A T A ¬ P ˙ Q ˙ R S T P ˙ R S ˙ T S ˙ P ˙ Q T ˙ Q ˙ R R A
8 5 hllatd K HL P A Q A R A S A T A ¬ P ˙ Q ˙ R S T P ˙ R S ˙ T S ˙ P ˙ Q T ˙ Q ˙ R K Lat
9 eqid Base K = Base K
10 9 4 atbase P A P Base K
11 6 10 syl K HL P A Q A R A S A T A ¬ P ˙ Q ˙ R S T P ˙ R S ˙ T S ˙ P ˙ Q T ˙ Q ˙ R P Base K
12 simp13 K HL P A Q A R A S A T A ¬ P ˙ Q ˙ R S T P ˙ R S ˙ T S ˙ P ˙ Q T ˙ Q ˙ R Q A
13 9 4 atbase Q A Q Base K
14 12 13 syl K HL P A Q A R A S A T A ¬ P ˙ Q ˙ R S T P ˙ R S ˙ T S ˙ P ˙ Q T ˙ Q ˙ R Q Base K
15 9 4 atbase R A R Base K
16 7 15 syl K HL P A Q A R A S A T A ¬ P ˙ Q ˙ R S T P ˙ R S ˙ T S ˙ P ˙ Q T ˙ Q ˙ R R Base K
17 simp31l K HL P A Q A R A S A T A ¬ P ˙ Q ˙ R S T P ˙ R S ˙ T S ˙ P ˙ Q T ˙ Q ˙ R ¬ P ˙ Q ˙ R
18 9 1 2 latnlej1r K Lat P Base K Q Base K R Base K ¬ P ˙ Q ˙ R P R
19 8 11 14 16 17 18 syl131anc K HL P A Q A R A S A T A ¬ P ˙ Q ˙ R S T P ˙ R S ˙ T S ˙ P ˙ Q T ˙ Q ˙ R P R
20 eqid LLines K = LLines K
21 2 4 20 llni2 K HL P A R A P R P ˙ R LLines K
22 5 6 7 19 21 syl31anc K HL P A Q A R A S A T A ¬ P ˙ Q ˙ R S T P ˙ R S ˙ T S ˙ P ˙ Q T ˙ Q ˙ R P ˙ R LLines K
23 simp22 K HL P A Q A R A S A T A ¬ P ˙ Q ˙ R S T P ˙ R S ˙ T S ˙ P ˙ Q T ˙ Q ˙ R S A
24 simp23 K HL P A Q A R A S A T A ¬ P ˙ Q ˙ R S T P ˙ R S ˙ T S ˙ P ˙ Q T ˙ Q ˙ R T A
25 simp31r K HL P A Q A R A S A T A ¬ P ˙ Q ˙ R S T P ˙ R S ˙ T S ˙ P ˙ Q T ˙ Q ˙ R S T
26 2 4 20 llni2 K HL S A T A S T S ˙ T LLines K
27 5 23 24 25 26 syl31anc K HL P A Q A R A S A T A ¬ P ˙ Q ˙ R S T P ˙ R S ˙ T S ˙ P ˙ Q T ˙ Q ˙ R S ˙ T LLines K
28 simp32 K HL P A Q A R A S A T A ¬ P ˙ Q ˙ R S T P ˙ R S ˙ T S ˙ P ˙ Q T ˙ Q ˙ R P ˙ R S ˙ T
29 simp33 K HL P A Q A R A S A T A ¬ P ˙ Q ˙ R S T P ˙ R S ˙ T S ˙ P ˙ Q T ˙ Q ˙ R S ˙ P ˙ Q T ˙ Q ˙ R
30 eqid 0. K = 0. K
31 1 2 3 30 4 ps-2b K HL P A Q A R A S A T A ¬ P ˙ Q ˙ R S T S ˙ P ˙ Q T ˙ Q ˙ R P ˙ R ˙ S ˙ T 0. K
32 5 6 12 7 23 24 17 25 29 31 syl333anc K HL P A Q A R A S A T A ¬ P ˙ Q ˙ R S T P ˙ R S ˙ T S ˙ P ˙ Q T ˙ Q ˙ R P ˙ R ˙ S ˙ T 0. K
33 3 30 4 20 2llnmat K HL P ˙ R LLines K S ˙ T LLines K P ˙ R S ˙ T P ˙ R ˙ S ˙ T 0. K P ˙ R ˙ S ˙ T A
34 5 22 27 28 32 33 syl32anc K HL P A Q A R A S A T A ¬ P ˙ Q ˙ R S T P ˙ R S ˙ T S ˙ P ˙ Q T ˙ Q ˙ R P ˙ R ˙ S ˙ T A