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 ⊢ ≤ = ( le ‘ 𝐾 )
psubspset.j ⊢ ∨ = ( join ‘ 𝐾 )
psubspset.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
psubspset.s ⊢ 𝑆 = ( PSubSp ‘ 𝐾 )
Assertion psubspi2N ( ( ( 𝐾 ∈ 𝐷 ∧ 𝑋 ∈ 𝑆 ∧ 𝑃 ∈ 𝐴 ) ∧ ( 𝑄 ∈ 𝑋 ∧ 𝑅 ∈ 𝑋 ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ) ) → 𝑃 ∈ 𝑋 )

Proof

Step Hyp Ref Expression
1 psubspset.l ⊢ ≤ = ( le ‘ 𝐾 )
2 psubspset.j ⊢ ∨ = ( join ‘ 𝐾 )
3 psubspset.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
4 psubspset.s ⊢ 𝑆 = ( PSubSp ‘ 𝐾 )
5 oveq1 ⊢ ( 𝑞 = 𝑄 → ( 𝑞 ∨ 𝑟 ) = ( 𝑄 ∨ 𝑟 ) )
6 5 breq2d ⊢ ( 𝑞 = 𝑄 → ( 𝑃 ≤ ( 𝑞 ∨ 𝑟 ) ↔ 𝑃 ≤ ( 𝑄 ∨ 𝑟 ) ) )
7 oveq2 ⊢ ( 𝑟 = 𝑅 → ( 𝑄 ∨ 𝑟 ) = ( 𝑄 ∨ 𝑅 ) )
8 7 breq2d ⊢ ( 𝑟 = 𝑅 → ( 𝑃 ≤ ( 𝑄 ∨ 𝑟 ) ↔ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ) )
9 6 8 rspc2ev ⊢ ( ( 𝑄 ∈ 𝑋 ∧ 𝑅 ∈ 𝑋 ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ) → ∃ 𝑞 ∈ 𝑋 ∃ 𝑟 ∈ 𝑋 𝑃 ≤ ( 𝑞 ∨ 𝑟 ) )
10 1 2 3 4 psubspi ⊢ ( ( ( 𝐾 ∈ 𝐷 ∧ 𝑋 ∈ 𝑆 ∧ 𝑃 ∈ 𝐴 ) ∧ ∃ 𝑞 ∈ 𝑋 ∃ 𝑟 ∈ 𝑋 𝑃 ≤ ( 𝑞 ∨ 𝑟 ) ) → 𝑃 ∈ 𝑋 )
11 9 10 sylan2 ⊢ ( ( ( 𝐾 ∈ 𝐷 ∧ 𝑋 ∈ 𝑆 ∧ 𝑃 ∈ 𝐴 ) ∧ ( 𝑄 ∈ 𝑋 ∧ 𝑅 ∈ 𝑋 ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ) ) → 𝑃 ∈ 𝑋 )