Metamath Proof Explorer

Theorem elpaddat

Description: Membership in a projective subspace sum with a point. (Contributed by NM, 29-Jan-2012)

Ref Expression
Hypotheses paddfval.l ⊢ ≤ ˙ = ≤ K
paddfval.j ⊢ ∨ ˙ = join ⁡ K
paddfval.a ⊢ A = Atoms ⁡ K
paddfval.p ⊢ + ˙ = + 𝑃 ⁡ K
Assertion elpaddat ⊢ K ∈ Lat ∧ X ⊆ A ∧ Q ∈ A ∧ X ≠ ∅ → S ∈ X + ˙ Q ↔ S ∈ A ∧ ∃ p ∈ X S ≤ ˙ p ∨ ˙ Q

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 simpl1 ⊢ K ∈ Lat ∧ X ⊆ A ∧ Q ∈ A ∧ X ≠ ∅ → K ∈ Lat
6 simpl2 ⊢ K ∈ Lat ∧ X ⊆ A ∧ Q ∈ A ∧ X ≠ ∅ → X ⊆ A
7 simpl3 ⊢ K ∈ Lat ∧ X ⊆ A ∧ Q ∈ A ∧ X ≠ ∅ → Q ∈ A
8 7 snssd ⊢ K ∈ Lat ∧ X ⊆ A ∧ Q ∈ A ∧ X ≠ ∅ → Q ⊆ A
9 simpr ⊢ K ∈ Lat ∧ X ⊆ A ∧ Q ∈ A ∧ X ≠ ∅ → X ≠ ∅
10 7 snn0d ⊢ K ∈ Lat ∧ X ⊆ A ∧ Q ∈ A ∧ X ≠ ∅ → Q ≠ ∅
11 1 2 3 4 elpaddn0 ⊢ K ∈ Lat ∧ X ⊆ A ∧ Q ⊆ A ∧ X ≠ ∅ ∧ Q ≠ ∅ → S ∈ X + ˙ Q ↔ S ∈ A ∧ ∃ p ∈ X ∃ r ∈ Q S ≤ ˙ p ∨ ˙ r
12 5 6 8 9 10 11 syl32anc ⊢ K ∈ Lat ∧ X ⊆ A ∧ Q ∈ A ∧ X ≠ ∅ → S ∈ X + ˙ Q ↔ S ∈ A ∧ ∃ p ∈ X ∃ r ∈ Q S ≤ ˙ p ∨ ˙ r
13 oveq2 ⊢ r = Q → p ∨ ˙ r = p ∨ ˙ Q
14 13 breq2d ⊢ r = Q → S ≤ ˙ p ∨ ˙ r ↔ S ≤ ˙ p ∨ ˙ Q
15 14 rexsng ⊢ Q ∈ A → ∃ r ∈ Q S ≤ ˙ p ∨ ˙ r ↔ S ≤ ˙ p ∨ ˙ Q
16 7 15 syl ⊢ K ∈ Lat ∧ X ⊆ A ∧ Q ∈ A ∧ X ≠ ∅ → ∃ r ∈ Q S ≤ ˙ p ∨ ˙ r ↔ S ≤ ˙ p ∨ ˙ Q
17 16 rexbidv ⊢ K ∈ Lat ∧ X ⊆ A ∧ Q ∈ A ∧ X ≠ ∅ → ∃ p ∈ X ∃ r ∈ Q S ≤ ˙ p ∨ ˙ r ↔ ∃ p ∈ X S ≤ ˙ p ∨ ˙ Q
18 17 anbi2d ⊢ K ∈ Lat ∧ X ⊆ A ∧ Q ∈ A ∧ X ≠ ∅ → S ∈ A ∧ ∃ p ∈ X ∃ r ∈ Q S ≤ ˙ p ∨ ˙ r ↔ S ∈ A ∧ ∃ p ∈ X S ≤ ˙ p ∨ ˙ Q
19 12 18 bitrd ⊢ K ∈ Lat ∧ X ⊆ A ∧ Q ∈ A ∧ X ≠ ∅ → S ∈ X + ˙ Q ↔ S ∈ A ∧ ∃ p ∈ X S ≤ ˙ p ∨ ˙ Q