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

Metamath Proof Explorer

Theorem psubspi2N

Description: Property of a projective subspace. (Contributed by NM, 13-Jan-2012) (New usage is discouraged.)

Ref Expression
Hypotheses psubspset.l ⊢ ≤ ˙ = ≤ K
psubspset.j ⊢ ∨ ˙ = join ⁡ K
psubspset.a ⊢ A = Atoms ⁡ K
psubspset.s ⊢ S = PSubSp ⁡ K
Assertion psubspi2N ⊢ K ∈ D ∧ X ∈ S ∧ P ∈ A ∧ Q ∈ X ∧ R ∈ X ∧ P ≤ ˙ Q ∨ ˙ R → P ∈ X

Proof

Step Hyp Ref Expression
1 psubspset.l ⊢ ≤ ˙ = ≤ K
2 psubspset.j ⊢ ∨ ˙ = join ⁡ K
3 psubspset.a ⊢ A = Atoms ⁡ K
4 psubspset.s ⊢ S = PSubSp ⁡ K
5 oveq1 ⊢ q = Q → q ∨ ˙ r = Q ∨ ˙ r
6 5 breq2d ⊢ q = Q → P ≤ ˙ q ∨ ˙ r ↔ P ≤ ˙ Q ∨ ˙ r
7 oveq2 ⊢ r = R → Q ∨ ˙ r = Q ∨ ˙ R
8 7 breq2d ⊢ r = R → P ≤ ˙ Q ∨ ˙ r ↔ P ≤ ˙ Q ∨ ˙ R
9 6 8 rspc2ev ⊢ Q ∈ X ∧ R ∈ X ∧ P ≤ ˙ Q ∨ ˙ R → ∃ q ∈ X ∃ r ∈ X P ≤ ˙ q ∨ ˙ r
10 1 2 3 4 psubspi ⊢ K ∈ D ∧ X ∈ S ∧ P ∈ A ∧ ∃ q ∈ X ∃ r ∈ X P ≤ ˙ q ∨ ˙ r → P ∈ X
11 9 10 sylan2 ⊢ K ∈ D ∧ X ∈ S ∧ P ∈ A ∧ Q ∈ X ∧ R ∈ X ∧ P ≤ ˙ Q ∨ ˙ R → P ∈ X