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

Metamath Proof Explorer

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 ⊢ ( 𝐾 ∈ 𝐵 → ( ⊥ ‘ ∅ ) = 𝐴 )