Metamath Proof Explorer

Theorem ispsubsp2

Description: The predicate "is 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 ispsubsp2 ( 𝐾 ∈ 𝐷 → ( 𝑋 ∈ 𝑆 ↔ ( 𝑋 ⊆ 𝐴 ∧ ∀ 𝑝 ∈ 𝐴 ( ∃ 𝑞 ∈ 𝑋 ∃ 𝑟 ∈ 𝑋 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) → 𝑝 ∈ 𝑋 ) ) ) )

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 ispsubsp ⊢ ( 𝐾 ∈ 𝐷 → ( 𝑋 ∈ 𝑆 ↔ ( 𝑋 ⊆ 𝐴 ∧ ∀ 𝑞 ∈ 𝑋 ∀ 𝑟 ∈ 𝑋 ∀ 𝑝 ∈ 𝐴 ( 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) → 𝑝 ∈ 𝑋 ) ) ) )
6 ralcom ⊢ ( ∀ 𝑟 ∈ 𝑋 ∀ 𝑝 ∈ 𝐴 ( 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) → 𝑝 ∈ 𝑋 ) ↔ ∀ 𝑝 ∈ 𝐴 ∀ 𝑟 ∈ 𝑋 ( 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) → 𝑝 ∈ 𝑋 ) )
7 r19.23v ⊢ ( ∀ 𝑟 ∈ 𝑋 ( 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) → 𝑝 ∈ 𝑋 ) ↔ ( ∃ 𝑟 ∈ 𝑋 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) → 𝑝 ∈ 𝑋 ) )
8 7 ralbii ⊢ ( ∀ 𝑝 ∈ 𝐴 ∀ 𝑟 ∈ 𝑋 ( 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) → 𝑝 ∈ 𝑋 ) ↔ ∀ 𝑝 ∈ 𝐴 ( ∃ 𝑟 ∈ 𝑋 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) → 𝑝 ∈ 𝑋 ) )
9 6 8 bitri ⊢ ( ∀ 𝑟 ∈ 𝑋 ∀ 𝑝 ∈ 𝐴 ( 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) → 𝑝 ∈ 𝑋 ) ↔ ∀ 𝑝 ∈ 𝐴 ( ∃ 𝑟 ∈ 𝑋 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) → 𝑝 ∈ 𝑋 ) )
10 9 ralbii ⊢ ( ∀ 𝑞 ∈ 𝑋 ∀ 𝑟 ∈ 𝑋 ∀ 𝑝 ∈ 𝐴 ( 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) → 𝑝 ∈ 𝑋 ) ↔ ∀ 𝑞 ∈ 𝑋 ∀ 𝑝 ∈ 𝐴 ( ∃ 𝑟 ∈ 𝑋 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) → 𝑝 ∈ 𝑋 ) )
11 ralcom ⊢ ( ∀ 𝑞 ∈ 𝑋 ∀ 𝑝 ∈ 𝐴 ( ∃ 𝑟 ∈ 𝑋 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) → 𝑝 ∈ 𝑋 ) ↔ ∀ 𝑝 ∈ 𝐴 ∀ 𝑞 ∈ 𝑋 ( ∃ 𝑟 ∈ 𝑋 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) → 𝑝 ∈ 𝑋 ) )
12 r19.23v ⊢ ( ∀ 𝑞 ∈ 𝑋 ( ∃ 𝑟 ∈ 𝑋 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) → 𝑝 ∈ 𝑋 ) ↔ ( ∃ 𝑞 ∈ 𝑋 ∃ 𝑟 ∈ 𝑋 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) → 𝑝 ∈ 𝑋 ) )
13 12 ralbii ⊢ ( ∀ 𝑝 ∈ 𝐴 ∀ 𝑞 ∈ 𝑋 ( ∃ 𝑟 ∈ 𝑋 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) → 𝑝 ∈ 𝑋 ) ↔ ∀ 𝑝 ∈ 𝐴 ( ∃ 𝑞 ∈ 𝑋 ∃ 𝑟 ∈ 𝑋 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) → 𝑝 ∈ 𝑋 ) )
14 11 13 bitri ⊢ ( ∀ 𝑞 ∈ 𝑋 ∀ 𝑝 ∈ 𝐴 ( ∃ 𝑟 ∈ 𝑋 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) → 𝑝 ∈ 𝑋 ) ↔ ∀ 𝑝 ∈ 𝐴 ( ∃ 𝑞 ∈ 𝑋 ∃ 𝑟 ∈ 𝑋 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) → 𝑝 ∈ 𝑋 ) )
15 10 14 bitri ⊢ ( ∀ 𝑞 ∈ 𝑋 ∀ 𝑟 ∈ 𝑋 ∀ 𝑝 ∈ 𝐴 ( 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) → 𝑝 ∈ 𝑋 ) ↔ ∀ 𝑝 ∈ 𝐴 ( ∃ 𝑞 ∈ 𝑋 ∃ 𝑟 ∈ 𝑋 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) → 𝑝 ∈ 𝑋 ) )
16 15 a1i ⊢ ( 𝐾 ∈ 𝐷 → ( ∀ 𝑞 ∈ 𝑋 ∀ 𝑟 ∈ 𝑋 ∀ 𝑝 ∈ 𝐴 ( 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) → 𝑝 ∈ 𝑋 ) ↔ ∀ 𝑝 ∈ 𝐴 ( ∃ 𝑞 ∈ 𝑋 ∃ 𝑟 ∈ 𝑋 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) → 𝑝 ∈ 𝑋 ) ) )
17 16 anbi2d ⊢ ( 𝐾 ∈ 𝐷 → ( ( 𝑋 ⊆ 𝐴 ∧ ∀ 𝑞 ∈ 𝑋 ∀ 𝑟 ∈ 𝑋 ∀ 𝑝 ∈ 𝐴 ( 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) → 𝑝 ∈ 𝑋 ) ) ↔ ( 𝑋 ⊆ 𝐴 ∧ ∀ 𝑝 ∈ 𝐴 ( ∃ 𝑞 ∈ 𝑋 ∃ 𝑟 ∈ 𝑋 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) → 𝑝 ∈ 𝑋 ) ) ) )
18 5 17 bitrd ⊢ ( 𝐾 ∈ 𝐷 → ( 𝑋 ∈ 𝑆 ↔ ( 𝑋 ⊆ 𝐴 ∧ ∀ 𝑝 ∈ 𝐴 ( ∃ 𝑞 ∈ 𝑋 ∃ 𝑟 ∈ 𝑋 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) → 𝑝 ∈ 𝑋 ) ) ) )