Metamath Proof Explorer


Theorem 4noncolr3

Description: A way to express 4 non-colinear atoms (rotated right 3 places). (Contributed by NM, 11-Jul-2012)

Ref Expression
Hypotheses 3noncol.l = ( le ‘ 𝐾 )
3noncol.j = ( join ‘ 𝐾 )
3noncol.a 𝐴 = ( Atoms ‘ 𝐾 )
Assertion 4noncolr3 ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) ∧ ( 𝑅𝐴𝑆𝐴 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑆 ( ( 𝑃 𝑄 ) 𝑅 ) ) ) → ( 𝑄𝑅 ∧ ¬ 𝑆 ( 𝑄 𝑅 ) ∧ ¬ 𝑃 ( ( 𝑄 𝑅 ) 𝑆 ) ) )

Proof

Step Hyp Ref Expression
1 3noncol.l = ( le ‘ 𝐾 )
2 3noncol.j = ( join ‘ 𝐾 )
3 3noncol.a 𝐴 = ( Atoms ‘ 𝐾 )
4 simp11 ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) ∧ ( 𝑅𝐴𝑆𝐴 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑆 ( ( 𝑃 𝑄 ) 𝑅 ) ) ) → 𝐾 ∈ HL )
5 4 hllatd ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) ∧ ( 𝑅𝐴𝑆𝐴 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑆 ( ( 𝑃 𝑄 ) 𝑅 ) ) ) → 𝐾 ∈ Lat )
6 simp2l ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) ∧ ( 𝑅𝐴𝑆𝐴 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑆 ( ( 𝑃 𝑄 ) 𝑅 ) ) ) → 𝑅𝐴 )
7 eqid ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
8 7 3 atbase ( 𝑅𝐴𝑅 ∈ ( Base ‘ 𝐾 ) )
9 6 8 syl ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) ∧ ( 𝑅𝐴𝑆𝐴 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑆 ( ( 𝑃 𝑄 ) 𝑅 ) ) ) → 𝑅 ∈ ( Base ‘ 𝐾 ) )
10 simp12 ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) ∧ ( 𝑅𝐴𝑆𝐴 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑆 ( ( 𝑃 𝑄 ) 𝑅 ) ) ) → 𝑃𝐴 )
11 7 3 atbase ( 𝑃𝐴𝑃 ∈ ( Base ‘ 𝐾 ) )
12 10 11 syl ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) ∧ ( 𝑅𝐴𝑆𝐴 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑆 ( ( 𝑃 𝑄 ) 𝑅 ) ) ) → 𝑃 ∈ ( Base ‘ 𝐾 ) )
13 simp13 ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) ∧ ( 𝑅𝐴𝑆𝐴 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑆 ( ( 𝑃 𝑄 ) 𝑅 ) ) ) → 𝑄𝐴 )
14 7 3 atbase ( 𝑄𝐴𝑄 ∈ ( Base ‘ 𝐾 ) )
15 13 14 syl ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) ∧ ( 𝑅𝐴𝑆𝐴 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑆 ( ( 𝑃 𝑄 ) 𝑅 ) ) ) → 𝑄 ∈ ( Base ‘ 𝐾 ) )
16 simp32 ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) ∧ ( 𝑅𝐴𝑆𝐴 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑆 ( ( 𝑃 𝑄 ) 𝑅 ) ) ) → ¬ 𝑅 ( 𝑃 𝑄 ) )
17 7 1 2 latnlej1r ( ( 𝐾 ∈ Lat ∧ ( 𝑅 ∈ ( Base ‘ 𝐾 ) ∧ 𝑃 ∈ ( Base ‘ 𝐾 ) ∧ 𝑄 ∈ ( Base ‘ 𝐾 ) ) ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ) → 𝑅𝑄 )
18 5 9 12 15 16 17 syl131anc ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) ∧ ( 𝑅𝐴𝑆𝐴 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑆 ( ( 𝑃 𝑄 ) 𝑅 ) ) ) → 𝑅𝑄 )
19 18 necomd ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) ∧ ( 𝑅𝐴𝑆𝐴 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑆 ( ( 𝑃 𝑄 ) 𝑅 ) ) ) → 𝑄𝑅 )
20 simp2r ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) ∧ ( 𝑅𝐴𝑆𝐴 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑆 ( ( 𝑃 𝑄 ) 𝑅 ) ) ) → 𝑆𝐴 )
21 7 3 atbase ( 𝑆𝐴𝑆 ∈ ( Base ‘ 𝐾 ) )
22 20 21 syl ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) ∧ ( 𝑅𝐴𝑆𝐴 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑆 ( ( 𝑃 𝑄 ) 𝑅 ) ) ) → 𝑆 ∈ ( Base ‘ 𝐾 ) )
23 7 2 latjcl ( ( 𝐾 ∈ Lat ∧ 𝑄 ∈ ( Base ‘ 𝐾 ) ∧ 𝑅 ∈ ( Base ‘ 𝐾 ) ) → ( 𝑄 𝑅 ) ∈ ( Base ‘ 𝐾 ) )
24 5 15 9 23 syl3anc ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) ∧ ( 𝑅𝐴𝑆𝐴 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑆 ( ( 𝑃 𝑄 ) 𝑅 ) ) ) → ( 𝑄 𝑅 ) ∈ ( Base ‘ 𝐾 ) )
25 simp33 ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) ∧ ( 𝑅𝐴𝑆𝐴 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑆 ( ( 𝑃 𝑄 ) 𝑅 ) ) ) → ¬ 𝑆 ( ( 𝑃 𝑄 ) 𝑅 ) )
26 2 3 hlatjass ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑄𝐴𝑅𝐴 ) ) → ( ( 𝑃 𝑄 ) 𝑅 ) = ( 𝑃 ( 𝑄 𝑅 ) ) )
27 4 10 13 6 26 syl13anc ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) ∧ ( 𝑅𝐴𝑆𝐴 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑆 ( ( 𝑃 𝑄 ) 𝑅 ) ) ) → ( ( 𝑃 𝑄 ) 𝑅 ) = ( 𝑃 ( 𝑄 𝑅 ) ) )
28 27 breq2d ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) ∧ ( 𝑅𝐴𝑆𝐴 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑆 ( ( 𝑃 𝑄 ) 𝑅 ) ) ) → ( 𝑆 ( ( 𝑃 𝑄 ) 𝑅 ) ↔ 𝑆 ( 𝑃 ( 𝑄 𝑅 ) ) ) )
29 25 28 mtbid ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) ∧ ( 𝑅𝐴𝑆𝐴 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑆 ( ( 𝑃 𝑄 ) 𝑅 ) ) ) → ¬ 𝑆 ( 𝑃 ( 𝑄 𝑅 ) ) )
30 7 1 2 latnlej2r ( ( 𝐾 ∈ Lat ∧ ( 𝑆 ∈ ( Base ‘ 𝐾 ) ∧ 𝑃 ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑄 𝑅 ) ∈ ( Base ‘ 𝐾 ) ) ∧ ¬ 𝑆 ( 𝑃 ( 𝑄 𝑅 ) ) ) → ¬ 𝑆 ( 𝑄 𝑅 ) )
31 5 22 12 24 29 30 syl131anc ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) ∧ ( 𝑅𝐴𝑆𝐴 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑆 ( ( 𝑃 𝑄 ) 𝑅 ) ) ) → ¬ 𝑆 ( 𝑄 𝑅 ) )
32 simp31 ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) ∧ ( 𝑅𝐴𝑆𝐴 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑆 ( ( 𝑃 𝑄 ) 𝑅 ) ) ) → 𝑃𝑄 )
33 1 2 3 hlatexch1 ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑅𝐴𝑄𝐴 ) ∧ 𝑃𝑄 ) → ( 𝑃 ( 𝑄 𝑅 ) → 𝑅 ( 𝑄 𝑃 ) ) )
34 4 10 6 13 32 33 syl131anc ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) ∧ ( 𝑅𝐴𝑆𝐴 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑆 ( ( 𝑃 𝑄 ) 𝑅 ) ) ) → ( 𝑃 ( 𝑄 𝑅 ) → 𝑅 ( 𝑄 𝑃 ) ) )
35 7 2 latjcom ( ( 𝐾 ∈ Lat ∧ 𝑃 ∈ ( Base ‘ 𝐾 ) ∧ 𝑄 ∈ ( Base ‘ 𝐾 ) ) → ( 𝑃 𝑄 ) = ( 𝑄 𝑃 ) )
36 5 12 15 35 syl3anc ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) ∧ ( 𝑅𝐴𝑆𝐴 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑆 ( ( 𝑃 𝑄 ) 𝑅 ) ) ) → ( 𝑃 𝑄 ) = ( 𝑄 𝑃 ) )
37 36 breq2d ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) ∧ ( 𝑅𝐴𝑆𝐴 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑆 ( ( 𝑃 𝑄 ) 𝑅 ) ) ) → ( 𝑅 ( 𝑃 𝑄 ) ↔ 𝑅 ( 𝑄 𝑃 ) ) )
38 34 37 sylibrd ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) ∧ ( 𝑅𝐴𝑆𝐴 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑆 ( ( 𝑃 𝑄 ) 𝑅 ) ) ) → ( 𝑃 ( 𝑄 𝑅 ) → 𝑅 ( 𝑃 𝑄 ) ) )
39 16 38 mtod ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) ∧ ( 𝑅𝐴𝑆𝐴 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑆 ( ( 𝑃 𝑄 ) 𝑅 ) ) ) → ¬ 𝑃 ( 𝑄 𝑅 ) )
40 7 1 2 3 hlexch1 ( ( 𝐾 ∈ HL ∧ ( 𝑃𝐴𝑆𝐴 ∧ ( 𝑄 𝑅 ) ∈ ( Base ‘ 𝐾 ) ) ∧ ¬ 𝑃 ( 𝑄 𝑅 ) ) → ( 𝑃 ( ( 𝑄 𝑅 ) 𝑆 ) → 𝑆 ( ( 𝑄 𝑅 ) 𝑃 ) ) )
41 4 10 20 24 39 40 syl131anc ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) ∧ ( 𝑅𝐴𝑆𝐴 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑆 ( ( 𝑃 𝑄 ) 𝑅 ) ) ) → ( 𝑃 ( ( 𝑄 𝑅 ) 𝑆 ) → 𝑆 ( ( 𝑄 𝑅 ) 𝑃 ) ) )
42 7 2 latjcom ( ( 𝐾 ∈ Lat ∧ 𝑄 ∈ ( Base ‘ 𝐾 ) ∧ 𝑅 ∈ ( Base ‘ 𝐾 ) ) → ( 𝑄 𝑅 ) = ( 𝑅 𝑄 ) )
43 5 15 9 42 syl3anc ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) ∧ ( 𝑅𝐴𝑆𝐴 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑆 ( ( 𝑃 𝑄 ) 𝑅 ) ) ) → ( 𝑄 𝑅 ) = ( 𝑅 𝑄 ) )
44 43 oveq1d ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) ∧ ( 𝑅𝐴𝑆𝐴 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑆 ( ( 𝑃 𝑄 ) 𝑅 ) ) ) → ( ( 𝑄 𝑅 ) 𝑃 ) = ( ( 𝑅 𝑄 ) 𝑃 ) )
45 7 2 latj31 ( ( 𝐾 ∈ Lat ∧ ( 𝑅 ∈ ( Base ‘ 𝐾 ) ∧ 𝑄 ∈ ( Base ‘ 𝐾 ) ∧ 𝑃 ∈ ( Base ‘ 𝐾 ) ) ) → ( ( 𝑅 𝑄 ) 𝑃 ) = ( ( 𝑃 𝑄 ) 𝑅 ) )
46 5 9 15 12 45 syl13anc ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) ∧ ( 𝑅𝐴𝑆𝐴 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑆 ( ( 𝑃 𝑄 ) 𝑅 ) ) ) → ( ( 𝑅 𝑄 ) 𝑃 ) = ( ( 𝑃 𝑄 ) 𝑅 ) )
47 44 46 eqtrd ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) ∧ ( 𝑅𝐴𝑆𝐴 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑆 ( ( 𝑃 𝑄 ) 𝑅 ) ) ) → ( ( 𝑄 𝑅 ) 𝑃 ) = ( ( 𝑃 𝑄 ) 𝑅 ) )
48 47 breq2d ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) ∧ ( 𝑅𝐴𝑆𝐴 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑆 ( ( 𝑃 𝑄 ) 𝑅 ) ) ) → ( 𝑆 ( ( 𝑄 𝑅 ) 𝑃 ) ↔ 𝑆 ( ( 𝑃 𝑄 ) 𝑅 ) ) )
49 41 48 sylibd ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) ∧ ( 𝑅𝐴𝑆𝐴 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑆 ( ( 𝑃 𝑄 ) 𝑅 ) ) ) → ( 𝑃 ( ( 𝑄 𝑅 ) 𝑆 ) → 𝑆 ( ( 𝑃 𝑄 ) 𝑅 ) ) )
50 25 49 mtod ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) ∧ ( 𝑅𝐴𝑆𝐴 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑆 ( ( 𝑃 𝑄 ) 𝑅 ) ) ) → ¬ 𝑃 ( ( 𝑄 𝑅 ) 𝑆 ) )
51 19 31 50 3jca ( ( ( 𝐾 ∈ HL ∧ 𝑃𝐴𝑄𝐴 ) ∧ ( 𝑅𝐴𝑆𝐴 ) ∧ ( 𝑃𝑄 ∧ ¬ 𝑅 ( 𝑃 𝑄 ) ∧ ¬ 𝑆 ( ( 𝑃 𝑄 ) 𝑅 ) ) ) → ( 𝑄𝑅 ∧ ¬ 𝑆 ( 𝑄 𝑅 ) ∧ ¬ 𝑃 ( ( 𝑄 𝑅 ) 𝑆 ) ) )