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

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 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ 𝑋 𝐶 ( 𝑃 ∨ 𝑄 ) ) ) → 𝑋 ∈ 𝐴 )