Metamath Proof Explorer

Theorem 2dim

Description: Generate a height-3 element (2-dimensional plane) from an atom. (Contributed by NM, 3-May-2012)

Ref Expression
Hypotheses 2dim.j ⊢ ∨ = ( join ‘ 𝐾 )
2dim.c ⊢ 𝐶 = ( ⋖ ‘ 𝐾 )
2dim.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
Assertion 2dim ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ) → ∃ 𝑞 ∈ 𝐴 ∃ 𝑟 ∈ 𝐴 ( 𝑃 𝐶 ( 𝑃 ∨ 𝑞 ) ∧ ( 𝑃 ∨ 𝑞 ) 𝐶 ( ( 𝑃 ∨ 𝑞 ) ∨ 𝑟 ) ) )

Proof

Step Hyp Ref Expression
1 2dim.j ⊢ ∨ = ( join ‘ 𝐾 )
2 2dim.c ⊢ 𝐶 = ( ⋖ ‘ 𝐾 )
3 2dim.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
4 eqid ⊢ ( le ‘ 𝐾 ) = ( le ‘ 𝐾 )
5 1 4 3 3dim1 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ) → ∃ 𝑞 ∈ 𝐴 ∃ 𝑟 ∈ 𝐴 ∃ 𝑠 ∈ 𝐴 ( 𝑃 ≠ 𝑞 ∧ ¬ 𝑟 ( le ‘ 𝐾 ) ( 𝑃 ∨ 𝑞 ) ∧ ¬ 𝑠 ( le ‘ 𝐾 ) ( ( 𝑃 ∨ 𝑞 ) ∨ 𝑟 ) ) )
6 df-3an ⊢ ( ( 𝑃 ≠ 𝑞 ∧ ¬ 𝑟 ( le ‘ 𝐾 ) ( 𝑃 ∨ 𝑞 ) ∧ ¬ 𝑠 ( le ‘ 𝐾 ) ( ( 𝑃 ∨ 𝑞 ) ∨ 𝑟 ) ) ↔ ( ( 𝑃 ≠ 𝑞 ∧ ¬ 𝑟 ( le ‘ 𝐾 ) ( 𝑃 ∨ 𝑞 ) ) ∧ ¬ 𝑠 ( le ‘ 𝐾 ) ( ( 𝑃 ∨ 𝑞 ) ∨ 𝑟 ) ) )
7 6 rexbii ⊢ ( ∃ 𝑠 ∈ 𝐴 ( 𝑃 ≠ 𝑞 ∧ ¬ 𝑟 ( le ‘ 𝐾 ) ( 𝑃 ∨ 𝑞 ) ∧ ¬ 𝑠 ( le ‘ 𝐾 ) ( ( 𝑃 ∨ 𝑞 ) ∨ 𝑟 ) ) ↔ ∃ 𝑠 ∈ 𝐴 ( ( 𝑃 ≠ 𝑞 ∧ ¬ 𝑟 ( le ‘ 𝐾 ) ( 𝑃 ∨ 𝑞 ) ) ∧ ¬ 𝑠 ( le ‘ 𝐾 ) ( ( 𝑃 ∨ 𝑞 ) ∨ 𝑟 ) ) )
8 r19.42v ⊢ ( ∃ 𝑠 ∈ 𝐴 ( ( 𝑃 ≠ 𝑞 ∧ ¬ 𝑟 ( le ‘ 𝐾 ) ( 𝑃 ∨ 𝑞 ) ) ∧ ¬ 𝑠 ( le ‘ 𝐾 ) ( ( 𝑃 ∨ 𝑞 ) ∨ 𝑟 ) ) ↔ ( ( 𝑃 ≠ 𝑞 ∧ ¬ 𝑟 ( le ‘ 𝐾 ) ( 𝑃 ∨ 𝑞 ) ) ∧ ∃ 𝑠 ∈ 𝐴 ¬ 𝑠 ( le ‘ 𝐾 ) ( ( 𝑃 ∨ 𝑞 ) ∨ 𝑟 ) ) )
9 7 8 bitri ⊢ ( ∃ 𝑠 ∈ 𝐴 ( 𝑃 ≠ 𝑞 ∧ ¬ 𝑟 ( le ‘ 𝐾 ) ( 𝑃 ∨ 𝑞 ) ∧ ¬ 𝑠 ( le ‘ 𝐾 ) ( ( 𝑃 ∨ 𝑞 ) ∨ 𝑟 ) ) ↔ ( ( 𝑃 ≠ 𝑞 ∧ ¬ 𝑟 ( le ‘ 𝐾 ) ( 𝑃 ∨ 𝑞 ) ) ∧ ∃ 𝑠 ∈ 𝐴 ¬ 𝑠 ( le ‘ 𝐾 ) ( ( 𝑃 ∨ 𝑞 ) ∨ 𝑟 ) ) )
10 9 simplbi ⊢ ( ∃ 𝑠 ∈ 𝐴 ( 𝑃 ≠ 𝑞 ∧ ¬ 𝑟 ( le ‘ 𝐾 ) ( 𝑃 ∨ 𝑞 ) ∧ ¬ 𝑠 ( le ‘ 𝐾 ) ( ( 𝑃 ∨ 𝑞 ) ∨ 𝑟 ) ) → ( 𝑃 ≠ 𝑞 ∧ ¬ 𝑟 ( le ‘ 𝐾 ) ( 𝑃 ∨ 𝑞 ) ) )
11 simplll ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ) ∧ 𝑞 ∈ 𝐴 ) ∧ 𝑟 ∈ 𝐴 ) → 𝐾 ∈ HL )
12 hlatl ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ AtLat )
13 11 12 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ) ∧ 𝑞 ∈ 𝐴 ) ∧ 𝑟 ∈ 𝐴 ) → 𝐾 ∈ AtLat )
14 simplr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ) ∧ 𝑞 ∈ 𝐴 ) ∧ 𝑟 ∈ 𝐴 ) → 𝑞 ∈ 𝐴 )
15 simpllr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ) ∧ 𝑞 ∈ 𝐴 ) ∧ 𝑟 ∈ 𝐴 ) → 𝑃 ∈ 𝐴 )
16 4 3 atncmp ⊢ ( ( 𝐾 ∈ AtLat ∧ 𝑞 ∈ 𝐴 ∧ 𝑃 ∈ 𝐴 ) → ( ¬ 𝑞 ( le ‘ 𝐾 ) 𝑃 ↔ 𝑞 ≠ 𝑃 ) )
17 13 14 15 16 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ) ∧ 𝑞 ∈ 𝐴 ) ∧ 𝑟 ∈ 𝐴 ) → ( ¬ 𝑞 ( le ‘ 𝐾 ) 𝑃 ↔ 𝑞 ≠ 𝑃 ) )
18 necom ⊢ ( 𝑞 ≠ 𝑃 ↔ 𝑃 ≠ 𝑞 )
19 17 18 bitr2di ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ) ∧ 𝑞 ∈ 𝐴 ) ∧ 𝑟 ∈ 𝐴 ) → ( 𝑃 ≠ 𝑞 ↔ ¬ 𝑞 ( le ‘ 𝐾 ) 𝑃 ) )
20 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
21 20 3 atbase ⊢ ( 𝑃 ∈ 𝐴 → 𝑃 ∈ ( Base ‘ 𝐾 ) )
22 15 21 syl ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ) ∧ 𝑞 ∈ 𝐴 ) ∧ 𝑟 ∈ 𝐴 ) → 𝑃 ∈ ( Base ‘ 𝐾 ) )
23 20 4 1 2 3 cvr1 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ ( Base ‘ 𝐾 ) ∧ 𝑞 ∈ 𝐴 ) → ( ¬ 𝑞 ( le ‘ 𝐾 ) 𝑃 ↔ 𝑃 𝐶 ( 𝑃 ∨ 𝑞 ) ) )
24 11 22 14 23 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ) ∧ 𝑞 ∈ 𝐴 ) ∧ 𝑟 ∈ 𝐴 ) → ( ¬ 𝑞 ( le ‘ 𝐾 ) 𝑃 ↔ 𝑃 𝐶 ( 𝑃 ∨ 𝑞 ) ) )
25 19 24 bitrd ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ) ∧ 𝑞 ∈ 𝐴 ) ∧ 𝑟 ∈ 𝐴 ) → ( 𝑃 ≠ 𝑞 ↔ 𝑃 𝐶 ( 𝑃 ∨ 𝑞 ) ) )
26 20 1 3 hlatjcl ⊢ ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑞 ∈ 𝐴 ) → ( 𝑃 ∨ 𝑞 ) ∈ ( Base ‘ 𝐾 ) )
27 11 15 14 26 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ) ∧ 𝑞 ∈ 𝐴 ) ∧ 𝑟 ∈ 𝐴 ) → ( 𝑃 ∨ 𝑞 ) ∈ ( Base ‘ 𝐾 ) )
28 simpr ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ) ∧ 𝑞 ∈ 𝐴 ) ∧ 𝑟 ∈ 𝐴 ) → 𝑟 ∈ 𝐴 )
29 20 4 1 2 3 cvr1 ⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑃 ∨ 𝑞 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑟 ∈ 𝐴 ) → ( ¬ 𝑟 ( le ‘ 𝐾 ) ( 𝑃 ∨ 𝑞 ) ↔ ( 𝑃 ∨ 𝑞 ) 𝐶 ( ( 𝑃 ∨ 𝑞 ) ∨ 𝑟 ) ) )
30 11 27 28 29 syl3anc ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ) ∧ 𝑞 ∈ 𝐴 ) ∧ 𝑟 ∈ 𝐴 ) → ( ¬ 𝑟 ( le ‘ 𝐾 ) ( 𝑃 ∨ 𝑞 ) ↔ ( 𝑃 ∨ 𝑞 ) 𝐶 ( ( 𝑃 ∨ 𝑞 ) ∨ 𝑟 ) ) )
31 25 30 anbi12d ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ) ∧ 𝑞 ∈ 𝐴 ) ∧ 𝑟 ∈ 𝐴 ) → ( ( 𝑃 ≠ 𝑞 ∧ ¬ 𝑟 ( le ‘ 𝐾 ) ( 𝑃 ∨ 𝑞 ) ) ↔ ( 𝑃 𝐶 ( 𝑃 ∨ 𝑞 ) ∧ ( 𝑃 ∨ 𝑞 ) 𝐶 ( ( 𝑃 ∨ 𝑞 ) ∨ 𝑟 ) ) ) )
32 10 31 syl5ib ⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ) ∧ 𝑞 ∈ 𝐴 ) ∧ 𝑟 ∈ 𝐴 ) → ( ∃ 𝑠 ∈ 𝐴 ( 𝑃 ≠ 𝑞 ∧ ¬ 𝑟 ( le ‘ 𝐾 ) ( 𝑃 ∨ 𝑞 ) ∧ ¬ 𝑠 ( le ‘ 𝐾 ) ( ( 𝑃 ∨ 𝑞 ) ∨ 𝑟 ) ) → ( 𝑃 𝐶 ( 𝑃 ∨ 𝑞 ) ∧ ( 𝑃 ∨ 𝑞 ) 𝐶 ( ( 𝑃 ∨ 𝑞 ) ∨ 𝑟 ) ) ) )
33 32 reximdva ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ) ∧ 𝑞 ∈ 𝐴 ) → ( ∃ 𝑟 ∈ 𝐴 ∃ 𝑠 ∈ 𝐴 ( 𝑃 ≠ 𝑞 ∧ ¬ 𝑟 ( le ‘ 𝐾 ) ( 𝑃 ∨ 𝑞 ) ∧ ¬ 𝑠 ( le ‘ 𝐾 ) ( ( 𝑃 ∨ 𝑞 ) ∨ 𝑟 ) ) → ∃ 𝑟 ∈ 𝐴 ( 𝑃 𝐶 ( 𝑃 ∨ 𝑞 ) ∧ ( 𝑃 ∨ 𝑞 ) 𝐶 ( ( 𝑃 ∨ 𝑞 ) ∨ 𝑟 ) ) ) )
34 33 reximdva ⊢ ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ) → ( ∃ 𝑞 ∈ 𝐴 ∃ 𝑟 ∈ 𝐴 ∃ 𝑠 ∈ 𝐴 ( 𝑃 ≠ 𝑞 ∧ ¬ 𝑟 ( le ‘ 𝐾 ) ( 𝑃 ∨ 𝑞 ) ∧ ¬ 𝑠 ( le ‘ 𝐾 ) ( ( 𝑃 ∨ 𝑞 ) ∨ 𝑟 ) ) → ∃ 𝑞 ∈ 𝐴 ∃ 𝑟 ∈ 𝐴 ( 𝑃 𝐶 ( 𝑃 ∨ 𝑞 ) ∧ ( 𝑃 ∨ 𝑞 ) 𝐶 ( ( 𝑃 ∨ 𝑞 ) ∨ 𝑟 ) ) ) )
35 5 34 mpd ⊢ ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ) → ∃ 𝑞 ∈ 𝐴 ∃ 𝑟 ∈ 𝐴 ( 𝑃 𝐶 ( 𝑃 ∨ 𝑞 ) ∧ ( 𝑃 ∨ 𝑞 ) 𝐶 ( ( 𝑃 ∨ 𝑞 ) ∨ 𝑟 ) ) )