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 ∧ 𝑃𝐴 ) → ∃ 𝑞𝐴𝑟𝐴 ( 𝑃 𝐶 ( 𝑃 𝑞 ) ∧ ( 𝑃 𝑞 ) 𝐶 ( ( 𝑃 𝑞 ) 𝑟 ) ) )