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