Theorem pol0N

Description: The polarity of the empty projective subspace is the whole space. (Contributed by NM, 29-Oct-2011) (New usage is discouraged.)

	Ref	Expression
Hypotheses	polssat.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
	polssat.p	⊢ ⊥ = ( ⊥𝑃 ‘ 𝐾 )
Assertion	pol0N	⊢ ( 𝐾 ∈ 𝐵 → ( ⊥ ‘ ∅ ) = 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		polssat.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
2		polssat.p	⊢ ⊥ = ( ⊥𝑃 ‘ 𝐾 )
3		0ss	⊢ ∅ ⊆ 𝐴
4		eqid	⊢ ( oc ‘ 𝐾 ) = ( oc ‘ 𝐾 )
5		eqid	⊢ ( pmap ‘ 𝐾 ) = ( pmap ‘ 𝐾 )
6	4 1 5 2	polvalN	⊢ ( ( 𝐾 ∈ 𝐵 ∧ ∅ ⊆ 𝐴 ) → ( ⊥ ‘ ∅ ) = ( 𝐴 ∩ ∩ 𝑝 ∈ ∅ ( ( pmap ‘ 𝐾 ) ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑝 ) ) ) )
7	3 6	mpan2	⊢ ( 𝐾 ∈ 𝐵 → ( ⊥ ‘ ∅ ) = ( 𝐴 ∩ ∩ 𝑝 ∈ ∅ ( ( pmap ‘ 𝐾 ) ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑝 ) ) ) )
8		0iin	⊢ ∩ 𝑝 ∈ ∅ ( ( pmap ‘ 𝐾 ) ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑝 ) ) = V
9	8	ineq2i	⊢ ( 𝐴 ∩ ∩ 𝑝 ∈ ∅ ( ( pmap ‘ 𝐾 ) ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑝 ) ) ) = ( 𝐴 ∩ V )
10		inv1	⊢ ( 𝐴 ∩ V ) = 𝐴
11	9 10	eqtri	⊢ ( 𝐴 ∩ ∩ 𝑝 ∈ ∅ ( ( pmap ‘ 𝐾 ) ‘ ( ( oc ‘ 𝐾 ) ‘ 𝑝 ) ) ) = 𝐴
12	7 11	eqtrdi	⊢ ( 𝐾 ∈ 𝐵 → ( ⊥ ‘ ∅ ) = 𝐴 )