Theorem ispsubsp

Description: The predicate "is a projective subspace". (Contributed by NM, 2-Oct-2011)

	Ref	Expression
Hypotheses	psubspset.l	⊢ ≤ = ( le ‘ 𝐾 )
	psubspset.j	⊢ ∨ = ( join ‘ 𝐾 )
	psubspset.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
	psubspset.s	⊢ 𝑆 = ( PSubSp ‘ 𝐾 )
Assertion	ispsubsp	⊢ ( 𝐾 ∈ 𝐷 → ( 𝑋 ∈ 𝑆 ↔ ( 𝑋 ⊆ 𝐴 ∧ ∀ 𝑝 ∈ 𝑋 ∀ 𝑞 ∈ 𝑋 ∀ 𝑟 ∈ 𝐴 ( 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) → 𝑟 ∈ 𝑋 ) ) ) )

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	psubspset	⊢ ( 𝐾 ∈ 𝐷 → 𝑆 = { 𝑥 ∣ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑝 ∈ 𝑥 ∀ 𝑞 ∈ 𝑥 ∀ 𝑟 ∈ 𝐴 ( 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) → 𝑟 ∈ 𝑥 ) ) } )
6	5	eleq2d	⊢ ( 𝐾 ∈ 𝐷 → ( 𝑋 ∈ 𝑆 ↔ 𝑋 ∈ { 𝑥 ∣ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑝 ∈ 𝑥 ∀ 𝑞 ∈ 𝑥 ∀ 𝑟 ∈ 𝐴 ( 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) → 𝑟 ∈ 𝑥 ) ) } ) )
7	3	fvexi	⊢ 𝐴 ∈ V
8	7	ssex	⊢ ( 𝑋 ⊆ 𝐴 → 𝑋 ∈ V )
9	8	adantr	⊢ ( ( 𝑋 ⊆ 𝐴 ∧ ∀ 𝑝 ∈ 𝑋 ∀ 𝑞 ∈ 𝑋 ∀ 𝑟 ∈ 𝐴 ( 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) → 𝑟 ∈ 𝑋 ) ) → 𝑋 ∈ V )
10		sseq1	⊢ ( 𝑥 = 𝑋 → ( 𝑥 ⊆ 𝐴 ↔ 𝑋 ⊆ 𝐴 ) )
11		eleq2	⊢ ( 𝑥 = 𝑋 → ( 𝑟 ∈ 𝑥 ↔ 𝑟 ∈ 𝑋 ) )
12	11	imbi2d	⊢ ( 𝑥 = 𝑋 → ( ( 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) → 𝑟 ∈ 𝑥 ) ↔ ( 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) → 𝑟 ∈ 𝑋 ) ) )
13	12	ralbidv	⊢ ( 𝑥 = 𝑋 → ( ∀ 𝑟 ∈ 𝐴 ( 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) → 𝑟 ∈ 𝑥 ) ↔ ∀ 𝑟 ∈ 𝐴 ( 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) → 𝑟 ∈ 𝑋 ) ) )
14	13	raleqbi1dv	⊢ ( 𝑥 = 𝑋 → ( ∀ 𝑞 ∈ 𝑥 ∀ 𝑟 ∈ 𝐴 ( 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) → 𝑟 ∈ 𝑥 ) ↔ ∀ 𝑞 ∈ 𝑋 ∀ 𝑟 ∈ 𝐴 ( 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) → 𝑟 ∈ 𝑋 ) ) )
15	14	raleqbi1dv	⊢ ( 𝑥 = 𝑋 → ( ∀ 𝑝 ∈ 𝑥 ∀ 𝑞 ∈ 𝑥 ∀ 𝑟 ∈ 𝐴 ( 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) → 𝑟 ∈ 𝑥 ) ↔ ∀ 𝑝 ∈ 𝑋 ∀ 𝑞 ∈ 𝑋 ∀ 𝑟 ∈ 𝐴 ( 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) → 𝑟 ∈ 𝑋 ) ) )
16	10 15	anbi12d	⊢ ( 𝑥 = 𝑋 → ( ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑝 ∈ 𝑥 ∀ 𝑞 ∈ 𝑥 ∀ 𝑟 ∈ 𝐴 ( 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) → 𝑟 ∈ 𝑥 ) ) ↔ ( 𝑋 ⊆ 𝐴 ∧ ∀ 𝑝 ∈ 𝑋 ∀ 𝑞 ∈ 𝑋 ∀ 𝑟 ∈ 𝐴 ( 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) → 𝑟 ∈ 𝑋 ) ) ) )
17	9 16	elab3	⊢ ( 𝑋 ∈ { 𝑥 ∣ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑝 ∈ 𝑥 ∀ 𝑞 ∈ 𝑥 ∀ 𝑟 ∈ 𝐴 ( 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) → 𝑟 ∈ 𝑥 ) ) } ↔ ( 𝑋 ⊆ 𝐴 ∧ ∀ 𝑝 ∈ 𝑋 ∀ 𝑞 ∈ 𝑋 ∀ 𝑟 ∈ 𝐴 ( 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) → 𝑟 ∈ 𝑋 ) ) )
18	6 17	bitrdi	⊢ ( 𝐾 ∈ 𝐷 → ( 𝑋 ∈ 𝑆 ↔ ( 𝑋 ⊆ 𝐴 ∧ ∀ 𝑝 ∈ 𝑋 ∀ 𝑞 ∈ 𝑋 ∀ 𝑟 ∈ 𝐴 ( 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) → 𝑟 ∈ 𝑋 ) ) ) )