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

Metamath Proof Explorer

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