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

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	⊢ ( 𝐾 ∈ 𝑉 → 𝐴 ∈ 𝑆 )