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 = ( le ‘ 𝐾 )
2atm.j = ( join ‘ 𝐾 )
2atm.m = ( meet ‘ 𝐾 )
2atm.a 𝐴 = ( Atoms ‘ 𝐾 )
Assertion ps-2c ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) ∧ ( 𝑅𝐴𝑆𝐴𝑇𝐴 ) ∧ ( ( ¬ 𝑃 ( 𝑄 𝑅 ) ∧ 𝑆𝑇 ) ∧ ( 𝑃 𝑅 ) ≠ ( 𝑆 𝑇 ) ∧ ( 𝑆 ( 𝑃 𝑄 ) ∧ 𝑇 ( 𝑄 𝑅 ) ) ) ) → ( ( 𝑃 𝑅 ) ( 𝑆 𝑇 ) ) ∈ 𝐴 )

Proof

Step Hyp Ref Expression
1 2atm.l = ( le ‘ 𝐾 )
2 2atm.j = ( join ‘ 𝐾 )
3 2atm.m = ( meet ‘ 𝐾 )
4 2atm.a 𝐴 = ( Atoms ‘ 𝐾 )
5 simp11 ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) ∧ ( 𝑅𝐴𝑆𝐴𝑇𝐴 ) ∧ ( ( ¬ 𝑃 ( 𝑄 𝑅 ) ∧ 𝑆𝑇 ) ∧ ( 𝑃 𝑅 ) ≠ ( 𝑆 𝑇 ) ∧ ( 𝑆 ( 𝑃 𝑄 ) ∧ 𝑇 ( 𝑄 𝑅 ) ) ) ) → 𝐾 ∈ HL )
6 simp12 ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) ∧ ( 𝑅𝐴𝑆𝐴𝑇𝐴 ) ∧ ( ( ¬ 𝑃 ( 𝑄 𝑅 ) ∧ 𝑆𝑇 ) ∧ ( 𝑃 𝑅 ) ≠ ( 𝑆 𝑇 ) ∧ ( 𝑆 ( 𝑃 𝑄 ) ∧ 𝑇 ( 𝑄 𝑅 ) ) ) ) → 𝑃𝐴 )
7 simp21 ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) ∧ ( 𝑅𝐴𝑆𝐴𝑇𝐴 ) ∧ ( ( ¬ 𝑃 ( 𝑄 𝑅 ) ∧ 𝑆𝑇 ) ∧ ( 𝑃 𝑅 ) ≠ ( 𝑆 𝑇 ) ∧ ( 𝑆 ( 𝑃 𝑄 ) ∧ 𝑇 ( 𝑄 𝑅 ) ) ) ) → 𝑅𝐴 )
8 5 hllatd ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) ∧ ( 𝑅𝐴𝑆𝐴𝑇𝐴 ) ∧ ( ( ¬ 𝑃 ( 𝑄 𝑅 ) ∧ 𝑆𝑇 ) ∧ ( 𝑃 𝑅 ) ≠ ( 𝑆 𝑇 ) ∧ ( 𝑆 ( 𝑃 𝑄 ) ∧ 𝑇 ( 𝑄 𝑅 ) ) ) ) → 𝐾 ∈ Lat )
9 eqid ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
10 9 4 atbase ( 𝑃𝐴𝑃 ∈ ( Base ‘ 𝐾 ) )
11 6 10 syl ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) ∧ ( 𝑅𝐴𝑆𝐴𝑇𝐴 ) ∧ ( ( ¬ 𝑃 ( 𝑄 𝑅 ) ∧ 𝑆𝑇 ) ∧ ( 𝑃 𝑅 ) ≠ ( 𝑆 𝑇 ) ∧ ( 𝑆 ( 𝑃 𝑄 ) ∧ 𝑇 ( 𝑄 𝑅 ) ) ) ) → 𝑃 ∈ ( Base ‘ 𝐾 ) )
12 simp13 ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) ∧ ( 𝑅𝐴𝑆𝐴𝑇𝐴 ) ∧ ( ( ¬ 𝑃 ( 𝑄 𝑅 ) ∧ 𝑆𝑇 ) ∧ ( 𝑃 𝑅 ) ≠ ( 𝑆 𝑇 ) ∧ ( 𝑆 ( 𝑃 𝑄 ) ∧ 𝑇 ( 𝑄 𝑅 ) ) ) ) → 𝑄𝐴 )
13 9 4 atbase ( 𝑄𝐴𝑄 ∈ ( Base ‘ 𝐾 ) )
14 12 13 syl ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) ∧ ( 𝑅𝐴𝑆𝐴𝑇𝐴 ) ∧ ( ( ¬ 𝑃 ( 𝑄 𝑅 ) ∧ 𝑆𝑇 ) ∧ ( 𝑃 𝑅 ) ≠ ( 𝑆 𝑇 ) ∧ ( 𝑆 ( 𝑃 𝑄 ) ∧ 𝑇 ( 𝑄 𝑅 ) ) ) ) → 𝑄 ∈ ( Base ‘ 𝐾 ) )
15 9 4 atbase ( 𝑅𝐴𝑅 ∈ ( Base ‘ 𝐾 ) )
16 7 15 syl ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) ∧ ( 𝑅𝐴𝑆𝐴𝑇𝐴 ) ∧ ( ( ¬ 𝑃 ( 𝑄 𝑅 ) ∧ 𝑆𝑇 ) ∧ ( 𝑃 𝑅 ) ≠ ( 𝑆 𝑇 ) ∧ ( 𝑆 ( 𝑃 𝑄 ) ∧ 𝑇 ( 𝑄 𝑅 ) ) ) ) → 𝑅 ∈ ( Base ‘ 𝐾 ) )
17 simp31l ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) ∧ ( 𝑅𝐴𝑆𝐴𝑇𝐴 ) ∧ ( ( ¬ 𝑃 ( 𝑄 𝑅 ) ∧ 𝑆𝑇 ) ∧ ( 𝑃 𝑅 ) ≠ ( 𝑆 𝑇 ) ∧ ( 𝑆 ( 𝑃 𝑄 ) ∧ 𝑇 ( 𝑄 𝑅 ) ) ) ) → ¬ 𝑃 ( 𝑄 𝑅 ) )
18 9 1 2 latnlej1r ( ( 𝐾 ∈ Lat ∧ ( 𝑃 ∈ ( Base ‘ 𝐾 ) ∧ 𝑄 ∈ ( Base ‘ 𝐾 ) ∧ 𝑅 ∈ ( Base ‘ 𝐾 ) ) ∧ ¬ 𝑃 ( 𝑄 𝑅 ) ) → 𝑃𝑅 )
19 8 11 14 16 17 18 syl131anc ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) ∧ ( 𝑅𝐴𝑆𝐴𝑇𝐴 ) ∧ ( ( ¬ 𝑃 ( 𝑄 𝑅 ) ∧ 𝑆𝑇 ) ∧ ( 𝑃 𝑅 ) ≠ ( 𝑆 𝑇 ) ∧ ( 𝑆 ( 𝑃 𝑄 ) ∧ 𝑇 ( 𝑄 𝑅 ) ) ) ) → 𝑃𝑅 )
20 eqid ( LLines ‘ 𝐾 ) = ( LLines ‘ 𝐾 )
21 2 4 20 llni2 ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑅𝐴 ) ∧ 𝑃𝑅 ) → ( 𝑃 𝑅 ) ∈ ( LLines ‘ 𝐾 ) )
22 5 6 7 19 21 syl31anc ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) ∧ ( 𝑅𝐴𝑆𝐴𝑇𝐴 ) ∧ ( ( ¬ 𝑃 ( 𝑄 𝑅 ) ∧ 𝑆𝑇 ) ∧ ( 𝑃 𝑅 ) ≠ ( 𝑆 𝑇 ) ∧ ( 𝑆 ( 𝑃 𝑄 ) ∧ 𝑇 ( 𝑄 𝑅 ) ) ) ) → ( 𝑃 𝑅 ) ∈ ( LLines ‘ 𝐾 ) )
23 simp22 ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) ∧ ( 𝑅𝐴𝑆𝐴𝑇𝐴 ) ∧ ( ( ¬ 𝑃 ( 𝑄 𝑅 ) ∧ 𝑆𝑇 ) ∧ ( 𝑃 𝑅 ) ≠ ( 𝑆 𝑇 ) ∧ ( 𝑆 ( 𝑃 𝑄 ) ∧ 𝑇 ( 𝑄 𝑅 ) ) ) ) → 𝑆𝐴 )
24 simp23 ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) ∧ ( 𝑅𝐴𝑆𝐴𝑇𝐴 ) ∧ ( ( ¬ 𝑃 ( 𝑄 𝑅 ) ∧ 𝑆𝑇 ) ∧ ( 𝑃 𝑅 ) ≠ ( 𝑆 𝑇 ) ∧ ( 𝑆 ( 𝑃 𝑄 ) ∧ 𝑇 ( 𝑄 𝑅 ) ) ) ) → 𝑇𝐴 )
25 simp31r ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) ∧ ( 𝑅𝐴𝑆𝐴𝑇𝐴 ) ∧ ( ( ¬ 𝑃 ( 𝑄 𝑅 ) ∧ 𝑆𝑇 ) ∧ ( 𝑃 𝑅 ) ≠ ( 𝑆 𝑇 ) ∧ ( 𝑆 ( 𝑃 𝑄 ) ∧ 𝑇 ( 𝑄 𝑅 ) ) ) ) → 𝑆𝑇 )
26 2 4 20 llni2 ( ( ( 𝐾 ∈ HL ∧ 𝑆𝐴𝑇𝐴 ) ∧ 𝑆𝑇 ) → ( 𝑆 𝑇 ) ∈ ( LLines ‘ 𝐾 ) )
27 5 23 24 25 26 syl31anc ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) ∧ ( 𝑅𝐴𝑆𝐴𝑇𝐴 ) ∧ ( ( ¬ 𝑃 ( 𝑄 𝑅 ) ∧ 𝑆𝑇 ) ∧ ( 𝑃 𝑅 ) ≠ ( 𝑆 𝑇 ) ∧ ( 𝑆 ( 𝑃 𝑄 ) ∧ 𝑇 ( 𝑄 𝑅 ) ) ) ) → ( 𝑆 𝑇 ) ∈ ( LLines ‘ 𝐾 ) )
28 simp32 ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) ∧ ( 𝑅𝐴𝑆𝐴𝑇𝐴 ) ∧ ( ( ¬ 𝑃 ( 𝑄 𝑅 ) ∧ 𝑆𝑇 ) ∧ ( 𝑃 𝑅 ) ≠ ( 𝑆 𝑇 ) ∧ ( 𝑆 ( 𝑃 𝑄 ) ∧ 𝑇 ( 𝑄 𝑅 ) ) ) ) → ( 𝑃 𝑅 ) ≠ ( 𝑆 𝑇 ) )
29 simp33 ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) ∧ ( 𝑅𝐴𝑆𝐴𝑇𝐴 ) ∧ ( ( ¬ 𝑃 ( 𝑄 𝑅 ) ∧ 𝑆𝑇 ) ∧ ( 𝑃 𝑅 ) ≠ ( 𝑆 𝑇 ) ∧ ( 𝑆 ( 𝑃 𝑄 ) ∧ 𝑇 ( 𝑄 𝑅 ) ) ) ) → ( 𝑆 ( 𝑃 𝑄 ) ∧ 𝑇 ( 𝑄 𝑅 ) ) )
30 eqid ( 0. ‘ 𝐾 ) = ( 0. ‘ 𝐾 )
31 1 2 3 30 4 ps-2b ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) ∧ ( 𝑅𝐴𝑆𝐴𝑇𝐴 ) ∧ ( ¬ 𝑃 ( 𝑄 𝑅 ) ∧ 𝑆𝑇 ∧ ( 𝑆 ( 𝑃 𝑄 ) ∧ 𝑇 ( 𝑄 𝑅 ) ) ) ) → ( ( 𝑃 𝑅 ) ( 𝑆 𝑇 ) ) ≠ ( 0. ‘ 𝐾 ) )
32 5 6 12 7 23 24 17 25 29 31 syl333anc ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) ∧ ( 𝑅𝐴𝑆𝐴𝑇𝐴 ) ∧ ( ( ¬ 𝑃 ( 𝑄 𝑅 ) ∧ 𝑆𝑇 ) ∧ ( 𝑃 𝑅 ) ≠ ( 𝑆 𝑇 ) ∧ ( 𝑆 ( 𝑃 𝑄 ) ∧ 𝑇 ( 𝑄 𝑅 ) ) ) ) → ( ( 𝑃 𝑅 ) ( 𝑆 𝑇 ) ) ≠ ( 0. ‘ 𝐾 ) )
33 3 30 4 20 2llnmat ( ( ( 𝐾 ∈ HL ∧ ( 𝑃 𝑅 ) ∈ ( LLines ‘ 𝐾 ) ∧ ( 𝑆 𝑇 ) ∈ ( LLines ‘ 𝐾 ) ) ∧ ( ( 𝑃 𝑅 ) ≠ ( 𝑆 𝑇 ) ∧ ( ( 𝑃 𝑅 ) ( 𝑆 𝑇 ) ) ≠ ( 0. ‘ 𝐾 ) ) ) → ( ( 𝑃 𝑅 ) ( 𝑆 𝑇 ) ) ∈ 𝐴 )
34 5 22 27 28 32 33 syl32anc ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) ∧ ( 𝑅𝐴𝑆𝐴𝑇𝐴 ) ∧ ( ( ¬ 𝑃 ( 𝑄 𝑅 ) ∧ 𝑆𝑇 ) ∧ ( 𝑃 𝑅 ) ≠ ( 𝑆 𝑇 ) ∧ ( 𝑆 ( 𝑃 𝑄 ) ∧ 𝑇 ( 𝑄 𝑅 ) ) ) ) → ( ( 𝑃 𝑅 ) ( 𝑆 𝑇 ) ) ∈ 𝐴 )