This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( 𝐾 ∈ 𝐷 → ( 𝑋 ∈ 𝑆 ↔ ( 𝑋 ⊆ 𝐴 ∧ ∀ 𝑝 ∈ 𝑋 ∀ 𝑞 ∈ 𝑋 ∀ 𝑟 ∈ 𝐴 ( 𝑟 ≤ ( 𝑝 ∨ 𝑞 ) → 𝑟 ∈ 𝑋 ) ) ) )