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

Metamath Proof Explorer

Theorem paddvaln0N

Description: Projective subspace sum operation value for nonempty sets. (Contributed by NM, 27-Jan-2012) (New usage is discouraged.)

Ref Expression
Hypotheses paddfval.l ⊢ ≤ ˙ = ≤ K
paddfval.j ⊢ ∨ ˙ = join ⁡ K
paddfval.a ⊢ A = Atoms ⁡ K
paddfval.p ⊢ + ˙ = + 𝑃 ⁡ K
Assertion paddvaln0N ⊢ K ∈ Lat ∧ X ⊆ A ∧ Y ⊆ A ∧ X ≠ ∅ ∧ Y ≠ ∅ → X + ˙ Y = p ∈ A | ∃ q ∈ X ∃ r ∈ Y p ≤ ˙ q ∨ ˙ r

Proof

Step Hyp Ref Expression
1 paddfval.l ⊢ ≤ ˙ = ≤ K
2 paddfval.j ⊢ ∨ ˙ = join ⁡ K
3 paddfval.a ⊢ A = Atoms ⁡ K
4 paddfval.p ⊢ + ˙ = + 𝑃 ⁡ K
5 1 2 3 4 elpaddn0 ⊢ K ∈ Lat ∧ X ⊆ A ∧ Y ⊆ A ∧ X ≠ ∅ ∧ Y ≠ ∅ → s ∈ X + ˙ Y ↔ s ∈ A ∧ ∃ q ∈ X ∃ r ∈ Y s ≤ ˙ q ∨ ˙ r
6 breq1 ⊢ p = s → p ≤ ˙ q ∨ ˙ r ↔ s ≤ ˙ q ∨ ˙ r
7 6 2rexbidv ⊢ p = s → ∃ q ∈ X ∃ r ∈ Y p ≤ ˙ q ∨ ˙ r ↔ ∃ q ∈ X ∃ r ∈ Y s ≤ ˙ q ∨ ˙ r
8 7 elrab ⊢ s ∈ p ∈ A | ∃ q ∈ X ∃ r ∈ Y p ≤ ˙ q ∨ ˙ r ↔ s ∈ A ∧ ∃ q ∈ X ∃ r ∈ Y s ≤ ˙ q ∨ ˙ r
9 5 8 bitr4di ⊢ K ∈ Lat ∧ X ⊆ A ∧ Y ⊆ A ∧ X ≠ ∅ ∧ Y ≠ ∅ → s ∈ X + ˙ Y ↔ s ∈ p ∈ A | ∃ q ∈ X ∃ r ∈ Y p ≤ ˙ q ∨ ˙ r
10 9 eqrdv ⊢ K ∈ Lat ∧ X ⊆ A ∧ Y ⊆ A ∧ X ≠ ∅ ∧ Y ≠ ∅ → X + ˙ Y = p ∈ A | ∃ q ∈ X ∃ r ∈ Y p ≤ ˙ q ∨ ˙ r