Metamath Proof Explorer


Theorem atpsubN

Description: The set of all atoms is a projective subspace. Remark below Definition 15.1 of MaedaMaeda p. 61. (Contributed by NM, 13-Oct-2011) (New usage is discouraged.)

Ref Expression
Hypotheses atpsub.a 𝐴 = ( Atoms ‘ 𝐾 )
atpsub.s 𝑆 = ( PSubSp ‘ 𝐾 )
Assertion atpsubN ( 𝐾𝑉𝐴𝑆 )

Proof

Step Hyp Ref Expression
1 atpsub.a 𝐴 = ( Atoms ‘ 𝐾 )
2 atpsub.s 𝑆 = ( PSubSp ‘ 𝐾 )
3 ssid 𝐴𝐴
4 ax-1 ( 𝑟𝐴 → ( 𝑟 ( le ‘ 𝐾 ) ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) → 𝑟𝐴 ) )
5 4 rgen 𝑟𝐴 ( 𝑟 ( le ‘ 𝐾 ) ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) → 𝑟𝐴 )
6 5 rgen2w 𝑝𝐴𝑞𝐴𝑟𝐴 ( 𝑟 ( le ‘ 𝐾 ) ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) → 𝑟𝐴 )
7 3 6 pm3.2i ( 𝐴𝐴 ∧ ∀ 𝑝𝐴𝑞𝐴𝑟𝐴 ( 𝑟 ( le ‘ 𝐾 ) ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) → 𝑟𝐴 ) )
8 eqid ( le ‘ 𝐾 ) = ( le ‘ 𝐾 )
9 eqid ( join ‘ 𝐾 ) = ( join ‘ 𝐾 )
10 8 9 1 2 ispsubsp ( 𝐾𝑉 → ( 𝐴𝑆 ↔ ( 𝐴𝐴 ∧ ∀ 𝑝𝐴𝑞𝐴𝑟𝐴 ( 𝑟 ( le ‘ 𝐾 ) ( 𝑝 ( join ‘ 𝐾 ) 𝑞 ) → 𝑟𝐴 ) ) ) )
11 7 10 mpbiri ( 𝐾𝑉𝐴𝑆 )