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	⊢ ( ( ( 𝐾 ∈ 𝐷 ∧ 𝑋 ∈ 𝑆 ∧ 𝑃 ∈ 𝐴 ) ∧ ( 𝑄 ∈ 𝑋 ∧ 𝑅 ∈ 𝑋 ∧ 𝑃 ≤ ( 𝑄 ∨ 𝑅 ) ) ) → 𝑃 ∈ 𝑋 )