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