Metamath Proof Explorer


Theorem cvrat2

Description: A Hilbert lattice element covered by the join of two distinct atoms is an atom. ( atcvat2i analog.) (Contributed by NM, 30-Nov-2011)

Ref Expression
Hypotheses cvrat2.b 𝐵 = ( Base ‘ 𝐾 )
cvrat2.j = ( join ‘ 𝐾 )
cvrat2.c 𝐶 = ( ⋖ ‘ 𝐾 )
cvrat2.a 𝐴 = ( Atoms ‘ 𝐾 )
Assertion cvrat2 ( ( 𝐾 ∈ HL ∧ ( 𝑋𝐵𝑃𝐴𝑄𝐴 ) ∧ ( 𝑃𝑄𝑋 𝐶 ( 𝑃 𝑄 ) ) ) → 𝑋𝐴 )

Proof

Step Hyp Ref Expression
1 cvrat2.b 𝐵 = ( Base ‘ 𝐾 )
2 cvrat2.j = ( join ‘ 𝐾 )
3 cvrat2.c 𝐶 = ( ⋖ ‘ 𝐾 )
4 cvrat2.a 𝐴 = ( Atoms ‘ 𝐾 )
5 eqid ( 0. ‘ 𝐾 ) = ( 0. ‘ 𝐾 )
6 1 2 5 3 4 atcvrj0 ( ( 𝐾 ∈ HL ∧ ( 𝑋𝐵𝑃𝐴𝑄𝐴 ) ∧ 𝑋 𝐶 ( 𝑃 𝑄 ) ) → ( 𝑋 = ( 0. ‘ 𝐾 ) ↔ 𝑃 = 𝑄 ) )
7 6 3expa ( ( ( 𝐾 ∈ HL ∧ ( 𝑋𝐵𝑃𝐴𝑄𝐴 ) ) ∧ 𝑋 𝐶 ( 𝑃 𝑄 ) ) → ( 𝑋 = ( 0. ‘ 𝐾 ) ↔ 𝑃 = 𝑄 ) )
8 7 necon3bid ( ( ( 𝐾 ∈ HL ∧ ( 𝑋𝐵𝑃𝐴𝑄𝐴 ) ) ∧ 𝑋 𝐶 ( 𝑃 𝑄 ) ) → ( 𝑋 ≠ ( 0. ‘ 𝐾 ) ↔ 𝑃𝑄 ) )
9 simpl ( ( 𝐾 ∈ HL ∧ ( 𝑋𝐵𝑃𝐴𝑄𝐴 ) ) → 𝐾 ∈ HL )
10 simpr1 ( ( 𝐾 ∈ HL ∧ ( 𝑋𝐵𝑃𝐴𝑄𝐴 ) ) → 𝑋𝐵 )
11 hllat ( 𝐾 ∈ HL → 𝐾 ∈ Lat )
12 11 adantr ( ( 𝐾 ∈ HL ∧ ( 𝑋𝐵𝑃𝐴𝑄𝐴 ) ) → 𝐾 ∈ Lat )
13 simpr2 ( ( 𝐾 ∈ HL ∧ ( 𝑋𝐵𝑃𝐴𝑄𝐴 ) ) → 𝑃𝐴 )
14 1 4 atbase ( 𝑃𝐴𝑃𝐵 )
15 13 14 syl ( ( 𝐾 ∈ HL ∧ ( 𝑋𝐵𝑃𝐴𝑄𝐴 ) ) → 𝑃𝐵 )
16 simpr3 ( ( 𝐾 ∈ HL ∧ ( 𝑋𝐵𝑃𝐴𝑄𝐴 ) ) → 𝑄𝐴 )
17 1 4 atbase ( 𝑄𝐴𝑄𝐵 )
18 16 17 syl ( ( 𝐾 ∈ HL ∧ ( 𝑋𝐵𝑃𝐴𝑄𝐴 ) ) → 𝑄𝐵 )
19 1 2 latjcl ( ( 𝐾 ∈ Lat ∧ 𝑃𝐵𝑄𝐵 ) → ( 𝑃 𝑄 ) ∈ 𝐵 )
20 12 15 18 19 syl3anc ( ( 𝐾 ∈ HL ∧ ( 𝑋𝐵𝑃𝐴𝑄𝐴 ) ) → ( 𝑃 𝑄 ) ∈ 𝐵 )
21 eqid ( lt ‘ 𝐾 ) = ( lt ‘ 𝐾 )
22 1 21 3 cvrlt ( ( ( 𝐾 ∈ HL ∧ 𝑋𝐵 ∧ ( 𝑃 𝑄 ) ∈ 𝐵 ) ∧ 𝑋 𝐶 ( 𝑃 𝑄 ) ) → 𝑋 ( lt ‘ 𝐾 ) ( 𝑃 𝑄 ) )
23 22 ex ( ( 𝐾 ∈ HL ∧ 𝑋𝐵 ∧ ( 𝑃 𝑄 ) ∈ 𝐵 ) → ( 𝑋 𝐶 ( 𝑃 𝑄 ) → 𝑋 ( lt ‘ 𝐾 ) ( 𝑃 𝑄 ) ) )
24 9 10 20 23 syl3anc ( ( 𝐾 ∈ HL ∧ ( 𝑋𝐵𝑃𝐴𝑄𝐴 ) ) → ( 𝑋 𝐶 ( 𝑃 𝑄 ) → 𝑋 ( lt ‘ 𝐾 ) ( 𝑃 𝑄 ) ) )
25 1 21 2 5 4 cvrat ( ( 𝐾 ∈ HL ∧ ( 𝑋𝐵𝑃𝐴𝑄𝐴 ) ) → ( ( 𝑋 ≠ ( 0. ‘ 𝐾 ) ∧ 𝑋 ( lt ‘ 𝐾 ) ( 𝑃 𝑄 ) ) → 𝑋𝐴 ) )
26 25 expcomd ( ( 𝐾 ∈ HL ∧ ( 𝑋𝐵𝑃𝐴𝑄𝐴 ) ) → ( 𝑋 ( lt ‘ 𝐾 ) ( 𝑃 𝑄 ) → ( 𝑋 ≠ ( 0. ‘ 𝐾 ) → 𝑋𝐴 ) ) )
27 24 26 syld ( ( 𝐾 ∈ HL ∧ ( 𝑋𝐵𝑃𝐴𝑄𝐴 ) ) → ( 𝑋 𝐶 ( 𝑃 𝑄 ) → ( 𝑋 ≠ ( 0. ‘ 𝐾 ) → 𝑋𝐴 ) ) )
28 27 imp ( ( ( 𝐾 ∈ HL ∧ ( 𝑋𝐵𝑃𝐴𝑄𝐴 ) ) ∧ 𝑋 𝐶 ( 𝑃 𝑄 ) ) → ( 𝑋 ≠ ( 0. ‘ 𝐾 ) → 𝑋𝐴 ) )
29 8 28 sylbird ( ( ( 𝐾 ∈ HL ∧ ( 𝑋𝐵𝑃𝐴𝑄𝐴 ) ) ∧ 𝑋 𝐶 ( 𝑃 𝑄 ) ) → ( 𝑃𝑄𝑋𝐴 ) )
30 29 ex ( ( 𝐾 ∈ HL ∧ ( 𝑋𝐵𝑃𝐴𝑄𝐴 ) ) → ( 𝑋 𝐶 ( 𝑃 𝑄 ) → ( 𝑃𝑄𝑋𝐴 ) ) )
31 30 com23 ( ( 𝐾 ∈ HL ∧ ( 𝑋𝐵𝑃𝐴𝑄𝐴 ) ) → ( 𝑃𝑄 → ( 𝑋 𝐶 ( 𝑃 𝑄 ) → 𝑋𝐴 ) ) )
32 31 impd ( ( 𝐾 ∈ HL ∧ ( 𝑋𝐵𝑃𝐴𝑄𝐴 ) ) → ( ( 𝑃𝑄𝑋 𝐶 ( 𝑃 𝑄 ) ) → 𝑋𝐴 ) )
33 32 3impia ( ( 𝐾 ∈ HL ∧ ( 𝑋𝐵𝑃𝐴𝑄𝐴 ) ∧ ( 𝑃𝑄𝑋 𝐶 ( 𝑃 𝑄 ) ) ) → 𝑋𝐴 )