Metamath Proof Explorer

Theorem hlsupr2

Description: A Hilbert lattice has the superposition property. (Contributed by NM, 25-Nov-2012)

Ref Expression
Hypotheses hlsupr2.j ⊢ ∨ = ( join ‘ 𝐾 )
hlsupr2.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
Assertion hlsupr2 ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) → ∃ 𝑟 ∈ 𝐴 ( 𝑃 ∨ 𝑟 ) = ( 𝑄 ∨ 𝑟 ) )

Proof

Step Hyp Ref Expression
1 hlsupr2.j ⊢ ∨ = ( join ‘ 𝐾 )
2 hlsupr2.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
3 eqid ⊢ ( le ‘ 𝐾 ) = ( le ‘ 𝐾 )
4 3 1 2 hlsupr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑃 ≠ 𝑄 ) → ∃ 𝑟 ∈ 𝐴 ( 𝑟 ≠ 𝑃 ∧ 𝑟 ≠ 𝑄 ∧ 𝑟 ( le ‘ 𝐾 ) ( 𝑃 ∨ 𝑄 ) ) )
5 4 ex ⊢ ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) → ( 𝑃 ≠ 𝑄 → ∃ 𝑟 ∈ 𝐴 ( 𝑟 ≠ 𝑃 ∧ 𝑟 ≠ 𝑄 ∧ 𝑟 ( le ‘ 𝐾 ) ( 𝑃 ∨ 𝑄 ) ) ) )
6 simpl1 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑟 ∈ 𝐴 ) → 𝐾 ∈ HL )
7 hlcvl ⊢ ( 𝐾 ∈ HL → 𝐾 ∈ CvLat )
8 6 7 syl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑟 ∈ 𝐴 ) → 𝐾 ∈ CvLat )
9 simpl2 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑟 ∈ 𝐴 ) → 𝑃 ∈ 𝐴 )
10 simpl3 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑟 ∈ 𝐴 ) → 𝑄 ∈ 𝐴 )
11 simpr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑟 ∈ 𝐴 ) → 𝑟 ∈ 𝐴 )
12 2 3 1 cvlsupr3 ⊢ ( ( 𝐾 ∈ CvLat ∧ ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ) → ( ( 𝑃 ∨ 𝑟 ) = ( 𝑄 ∨ 𝑟 ) ↔ ( 𝑃 ≠ 𝑄 → ( 𝑟 ≠ 𝑃 ∧ 𝑟 ≠ 𝑄 ∧ 𝑟 ( le ‘ 𝐾 ) ( 𝑃 ∨ 𝑄 ) ) ) ) )
13 8 9 10 11 12 syl13anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) ∧ 𝑟 ∈ 𝐴 ) → ( ( 𝑃 ∨ 𝑟 ) = ( 𝑄 ∨ 𝑟 ) ↔ ( 𝑃 ≠ 𝑄 → ( 𝑟 ≠ 𝑃 ∧ 𝑟 ≠ 𝑄 ∧ 𝑟 ( le ‘ 𝐾 ) ( 𝑃 ∨ 𝑄 ) ) ) ) )
14 13 rexbidva ⊢ ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) → ( ∃ 𝑟 ∈ 𝐴 ( 𝑃 ∨ 𝑟 ) = ( 𝑄 ∨ 𝑟 ) ↔ ∃ 𝑟 ∈ 𝐴 ( 𝑃 ≠ 𝑄 → ( 𝑟 ≠ 𝑃 ∧ 𝑟 ≠ 𝑄 ∧ 𝑟 ( le ‘ 𝐾 ) ( 𝑃 ∨ 𝑄 ) ) ) ) )
15 ne0i ⊢ ( 𝑃 ∈ 𝐴 → 𝐴 ≠ ∅ )
16 15 3ad2ant2 ⊢ ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) → 𝐴 ≠ ∅ )
17 r19.37zv ⊢ ( 𝐴 ≠ ∅ → ( ∃ 𝑟 ∈ 𝐴 ( 𝑃 ≠ 𝑄 → ( 𝑟 ≠ 𝑃 ∧ 𝑟 ≠ 𝑄 ∧ 𝑟 ( le ‘ 𝐾 ) ( 𝑃 ∨ 𝑄 ) ) ) ↔ ( 𝑃 ≠ 𝑄 → ∃ 𝑟 ∈ 𝐴 ( 𝑟 ≠ 𝑃 ∧ 𝑟 ≠ 𝑄 ∧ 𝑟 ( le ‘ 𝐾 ) ( 𝑃 ∨ 𝑄 ) ) ) ) )
18 16 17 syl ⊢ ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) → ( ∃ 𝑟 ∈ 𝐴 ( 𝑃 ≠ 𝑄 → ( 𝑟 ≠ 𝑃 ∧ 𝑟 ≠ 𝑄 ∧ 𝑟 ( le ‘ 𝐾 ) ( 𝑃 ∨ 𝑄 ) ) ) ↔ ( 𝑃 ≠ 𝑄 → ∃ 𝑟 ∈ 𝐴 ( 𝑟 ≠ 𝑃 ∧ 𝑟 ≠ 𝑄 ∧ 𝑟 ( le ‘ 𝐾 ) ( 𝑃 ∨ 𝑄 ) ) ) ) )
19 14 18 bitrd ⊢ ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) → ( ∃ 𝑟 ∈ 𝐴 ( 𝑃 ∨ 𝑟 ) = ( 𝑄 ∨ 𝑟 ) ↔ ( 𝑃 ≠ 𝑄 → ∃ 𝑟 ∈ 𝐴 ( 𝑟 ≠ 𝑃 ∧ 𝑟 ≠ 𝑄 ∧ 𝑟 ( le ‘ 𝐾 ) ( 𝑃 ∨ 𝑄 ) ) ) ) )
20 5 19 mpbird ⊢ ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) → ∃ 𝑟 ∈ 𝐴 ( 𝑃 ∨ 𝑟 ) = ( 𝑄 ∨ 𝑟 ) )