Theorem psubspi

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

	Ref	Expression
Hypotheses	psubspset.l	⊢ ≤ = ( le ‘ 𝐾 )
	psubspset.j	⊢ ∨ = ( join ‘ 𝐾 )
	psubspset.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
	psubspset.s	⊢ 𝑆 = ( PSubSp ‘ 𝐾 )
Assertion	psubspi	⊢ ( ( ( 𝐾 ∈ 𝐷 ∧ 𝑋 ∈ 𝑆 ∧ 𝑃 ∈ 𝐴 ) ∧ ∃ 𝑞 ∈ 𝑋 ∃ 𝑟 ∈ 𝑋 𝑃 ≤ ( 𝑞 ∨ 𝑟 ) ) → 𝑃 ∈ 𝑋 )

Proof

Step	Hyp	Ref	Expression
1		psubspset.l	⊢ ≤ = ( le ‘ 𝐾 )
2		psubspset.j	⊢ ∨ = ( join ‘ 𝐾 )
3		psubspset.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
4		psubspset.s	⊢ 𝑆 = ( PSubSp ‘ 𝐾 )
5	1 2 3 4	ispsubsp2	⊢ ( 𝐾 ∈ 𝐷 → ( 𝑋 ∈ 𝑆 ↔ ( 𝑋 ⊆ 𝐴 ∧ ∀ 𝑝 ∈ 𝐴 ( ∃ 𝑞 ∈ 𝑋 ∃ 𝑟 ∈ 𝑋 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) → 𝑝 ∈ 𝑋 ) ) ) )
6	5	simplbda	⊢ ( ( 𝐾 ∈ 𝐷 ∧ 𝑋 ∈ 𝑆 ) → ∀ 𝑝 ∈ 𝐴 ( ∃ 𝑞 ∈ 𝑋 ∃ 𝑟 ∈ 𝑋 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) → 𝑝 ∈ 𝑋 ) )
7	6	ex	⊢ ( 𝐾 ∈ 𝐷 → ( 𝑋 ∈ 𝑆 → ∀ 𝑝 ∈ 𝐴 ( ∃ 𝑞 ∈ 𝑋 ∃ 𝑟 ∈ 𝑋 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) → 𝑝 ∈ 𝑋 ) ) )
8		breq1	⊢ ( 𝑝 = 𝑃 → ( 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) ↔ 𝑃 ≤ ( 𝑞 ∨ 𝑟 ) ) )
9	8	2rexbidv	⊢ ( 𝑝 = 𝑃 → ( ∃ 𝑞 ∈ 𝑋 ∃ 𝑟 ∈ 𝑋 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) ↔ ∃ 𝑞 ∈ 𝑋 ∃ 𝑟 ∈ 𝑋 𝑃 ≤ ( 𝑞 ∨ 𝑟 ) ) )
10		eleq1	⊢ ( 𝑝 = 𝑃 → ( 𝑝 ∈ 𝑋 ↔ 𝑃 ∈ 𝑋 ) )
11	9 10	imbi12d	⊢ ( 𝑝 = 𝑃 → ( ( ∃ 𝑞 ∈ 𝑋 ∃ 𝑟 ∈ 𝑋 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) → 𝑝 ∈ 𝑋 ) ↔ ( ∃ 𝑞 ∈ 𝑋 ∃ 𝑟 ∈ 𝑋 𝑃 ≤ ( 𝑞 ∨ 𝑟 ) → 𝑃 ∈ 𝑋 ) ) )
12	11	rspccv	⊢ ( ∀ 𝑝 ∈ 𝐴 ( ∃ 𝑞 ∈ 𝑋 ∃ 𝑟 ∈ 𝑋 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) → 𝑝 ∈ 𝑋 ) → ( 𝑃 ∈ 𝐴 → ( ∃ 𝑞 ∈ 𝑋 ∃ 𝑟 ∈ 𝑋 𝑃 ≤ ( 𝑞 ∨ 𝑟 ) → 𝑃 ∈ 𝑋 ) ) )
13	7 12	syl6	⊢ ( 𝐾 ∈ 𝐷 → ( 𝑋 ∈ 𝑆 → ( 𝑃 ∈ 𝐴 → ( ∃ 𝑞 ∈ 𝑋 ∃ 𝑟 ∈ 𝑋 𝑃 ≤ ( 𝑞 ∨ 𝑟 ) → 𝑃 ∈ 𝑋 ) ) ) )
14	13	3imp1	⊢ ( ( ( 𝐾 ∈ 𝐷 ∧ 𝑋 ∈ 𝑆 ∧ 𝑃 ∈ 𝐴 ) ∧ ∃ 𝑞 ∈ 𝑋 ∃ 𝑟 ∈ 𝑋 𝑃 ≤ ( 𝑞 ∨ 𝑟 ) ) → 𝑃 ∈ 𝑋 )