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

Metamath Proof Explorer

Theorem polvalN

Description: Value of the projective subspace polarity function. (Contributed by NM, 23-Oct-2011) (New usage is discouraged.)

Ref Expression
Hypotheses polfval.o ⊢ ⊥ = ( oc ‘ 𝐾 )
polfval.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
polfval.m ⊢ 𝑀 = ( pmap ‘ 𝐾 )
polfval.p ⊢ 𝑃 = ( ⊥𝑃 ‘ 𝐾 )
Assertion polvalN ( ( 𝐾 ∈ 𝐵 ∧ 𝑋 ⊆ 𝐴 ) → ( 𝑃 ‘ 𝑋 ) = ( 𝐴 ∩ ∩ 𝑝 ∈ 𝑋 ( 𝑀 ‘ ( ⊥ ‘ 𝑝 ) ) ) )

Proof

Step Hyp Ref Expression
1 polfval.o ⊢ ⊥ = ( oc ‘ 𝐾 )
2 polfval.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
3 polfval.m ⊢ 𝑀 = ( pmap ‘ 𝐾 )
4 polfval.p ⊢ 𝑃 = ( ⊥𝑃 ‘ 𝐾 )
5 2 fvexi ⊢ 𝐴 ∈ V
6 5 elpw2 ⊢ ( 𝑋 ∈ 𝒫 𝐴 ↔ 𝑋 ⊆ 𝐴 )
7 1 2 3 4 polfvalN ⊢ ( 𝐾 ∈ 𝐵 → 𝑃 = ( 𝑚 ∈ 𝒫 𝐴 ↦ ( 𝐴 ∩ ∩ 𝑝 ∈ 𝑚 ( 𝑀 ‘ ( ⊥ ‘ 𝑝 ) ) ) ) )
8 7 fveq1d ⊢ ( 𝐾 ∈ 𝐵 → ( 𝑃 ‘ 𝑋 ) = ( ( 𝑚 ∈ 𝒫 𝐴 ↦ ( 𝐴 ∩ ∩ 𝑝 ∈ 𝑚 ( 𝑀 ‘ ( ⊥ ‘ 𝑝 ) ) ) ) ‘ 𝑋 ) )
9 iineq1 ⊢ ( 𝑚 = 𝑋 → ∩ 𝑝 ∈ 𝑚 ( 𝑀 ‘ ( ⊥ ‘ 𝑝 ) ) = ∩ 𝑝 ∈ 𝑋 ( 𝑀 ‘ ( ⊥ ‘ 𝑝 ) ) )
10 9 ineq2d ⊢ ( 𝑚 = 𝑋 → ( 𝐴 ∩ ∩ 𝑝 ∈ 𝑚 ( 𝑀 ‘ ( ⊥ ‘ 𝑝 ) ) ) = ( 𝐴 ∩ ∩ 𝑝 ∈ 𝑋 ( 𝑀 ‘ ( ⊥ ‘ 𝑝 ) ) ) )
11 eqid ⊢ ( 𝑚 ∈ 𝒫 𝐴 ↦ ( 𝐴 ∩ ∩ 𝑝 ∈ 𝑚 ( 𝑀 ‘ ( ⊥ ‘ 𝑝 ) ) ) ) = ( 𝑚 ∈ 𝒫 𝐴 ↦ ( 𝐴 ∩ ∩ 𝑝 ∈ 𝑚 ( 𝑀 ‘ ( ⊥ ‘ 𝑝 ) ) ) )
12 5 inex1 ⊢ ( 𝐴 ∩ ∩ 𝑝 ∈ 𝑋 ( 𝑀 ‘ ( ⊥ ‘ 𝑝 ) ) ) ∈ V
13 10 11 12 fvmpt ⊢ ( 𝑋 ∈ 𝒫 𝐴 → ( ( 𝑚 ∈ 𝒫 𝐴 ↦ ( 𝐴 ∩ ∩ 𝑝 ∈ 𝑚 ( 𝑀 ‘ ( ⊥ ‘ 𝑝 ) ) ) ) ‘ 𝑋 ) = ( 𝐴 ∩ ∩ 𝑝 ∈ 𝑋 ( 𝑀 ‘ ( ⊥ ‘ 𝑝 ) ) ) )
14 8 13 sylan9eq ⊢ ( ( 𝐾 ∈ 𝐵 ∧ 𝑋 ∈ 𝒫 𝐴 ) → ( 𝑃 ‘ 𝑋 ) = ( 𝐴 ∩ ∩ 𝑝 ∈ 𝑋 ( 𝑀 ‘ ( ⊥ ‘ 𝑝 ) ) ) )
15 6 14 sylan2br ⊢ ( ( 𝐾 ∈ 𝐵 ∧ 𝑋 ⊆ 𝐴 ) → ( 𝑃 ‘ 𝑋 ) = ( 𝐴 ∩ ∩ 𝑝 ∈ 𝑋 ( 𝑀 ‘ ( ⊥ ‘ 𝑝 ) ) ) )