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 ( 𝐾𝐷 → ( 𝑋𝑆 ↔ ( 𝑋𝐴 ∧ ∀ 𝑝𝐴 ( ∃ 𝑞𝑋𝑟𝑋 𝑝 ( 𝑞 𝑟 ) → 𝑝𝑋 ) ) ) )