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

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 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( ( ¬ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ∧ 𝑆 ≠ 𝑇 ) ∧ ( 𝑃 ∨ 𝑅 ) ≠ ( 𝑆 ∨ 𝑇 ) ∧ ( 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ∧ 𝑇 ≤ ( 𝑄 ∨ 𝑅 ) ) ) ) → ( ( 𝑃 ∨ 𝑅 ) ∧ ( 𝑆 ∨ 𝑇 ) ) ∈ 𝐴 )