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 A = Atoms K
atpsub.s S = PSubSp K
Assertion atpsubN K V A S

Proof

Step Hyp Ref Expression
1 atpsub.a A = Atoms K
2 atpsub.s S = PSubSp K
3 ssid A A
4 ax-1 r A r K p join K q r A
5 4 rgen r A r K p join K q r A
6 5 rgen2w p A q A r A r K p join K q r A
7 3 6 pm3.2i A A p A q A r A r K p join K q r A
8 eqid K = K
9 eqid join K = join K
10 8 9 1 2 ispsubsp K V A S A A p A q A r A r K p join K q r A
11 7 10 mpbiri K V A S