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

Metamath Proof Explorer

Theorem polfvalN

Description: 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 polfvalN ( 𝐾 ∈ 𝐵 → 𝑃 = ( 𝑚 ∈ 𝒫 𝐴 ↦ ( 𝐴 ∩ ∩ 𝑝 ∈ 𝑚 ( 𝑀 ‘ ( ⊥ ‘ 𝑝 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 polfval.o ⊢ ⊥ = ( oc ‘ 𝐾 )
2 polfval.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
3 polfval.m ⊢ 𝑀 = ( pmap ‘ 𝐾 )
4 polfval.p ⊢ 𝑃 = ( ⊥𝑃 ‘ 𝐾 )
5 elex ⊢ ( 𝐾 ∈ 𝐵 → 𝐾 ∈ V )
6 fveq2 ⊢ ( ℎ = 𝐾 → ( Atoms ‘ ℎ ) = ( Atoms ‘ 𝐾 ) )
7 6 2 eqtr4di ⊢ ( ℎ = 𝐾 → ( Atoms ‘ ℎ ) = 𝐴 )
8 7 pweqd ⊢ ( ℎ = 𝐾 → 𝒫 ( Atoms ‘ ℎ ) = 𝒫 𝐴 )
9 fveq2 ⊢ ( ℎ = 𝐾 → ( pmap ‘ ℎ ) = ( pmap ‘ 𝐾 ) )
10 9 3 eqtr4di ⊢ ( ℎ = 𝐾 → ( pmap ‘ ℎ ) = 𝑀 )
11 fveq2 ⊢ ( ℎ = 𝐾 → ( oc ‘ ℎ ) = ( oc ‘ 𝐾 ) )
12 11 1 eqtr4di ⊢ ( ℎ = 𝐾 → ( oc ‘ ℎ ) = ⊥ )
13 12 fveq1d ⊢ ( ℎ = 𝐾 → ( ( oc ‘ ℎ ) ‘ 𝑝 ) = ( ⊥ ‘ 𝑝 ) )
14 10 13 fveq12d ⊢ ( ℎ = 𝐾 → ( ( pmap ‘ ℎ ) ‘ ( ( oc ‘ ℎ ) ‘ 𝑝 ) ) = ( 𝑀 ‘ ( ⊥ ‘ 𝑝 ) ) )
15 14 adantr ⊢ ( ( ℎ = 𝐾 ∧ 𝑝 ∈ 𝑚 ) → ( ( pmap ‘ ℎ ) ‘ ( ( oc ‘ ℎ ) ‘ 𝑝 ) ) = ( 𝑀 ‘ ( ⊥ ‘ 𝑝 ) ) )
16 15 iineq2dv ⊢ ( ℎ = 𝐾 → ∩ 𝑝 ∈ 𝑚 ( ( pmap ‘ ℎ ) ‘ ( ( oc ‘ ℎ ) ‘ 𝑝 ) ) = ∩ 𝑝 ∈ 𝑚 ( 𝑀 ‘ ( ⊥ ‘ 𝑝 ) ) )
17 7 16 ineq12d ⊢ ( ℎ = 𝐾 → ( ( Atoms ‘ ℎ ) ∩ ∩ 𝑝 ∈ 𝑚 ( ( pmap ‘ ℎ ) ‘ ( ( oc ‘ ℎ ) ‘ 𝑝 ) ) ) = ( 𝐴 ∩ ∩ 𝑝 ∈ 𝑚 ( 𝑀 ‘ ( ⊥ ‘ 𝑝 ) ) ) )
18 8 17 mpteq12dv ⊢ ( ℎ = 𝐾 → ( 𝑚 ∈ 𝒫 ( Atoms ‘ ℎ ) ↦ ( ( Atoms ‘ ℎ ) ∩ ∩ 𝑝 ∈ 𝑚 ( ( pmap ‘ ℎ ) ‘ ( ( oc ‘ ℎ ) ‘ 𝑝 ) ) ) ) = ( 𝑚 ∈ 𝒫 𝐴 ↦ ( 𝐴 ∩ ∩ 𝑝 ∈ 𝑚 ( 𝑀 ‘ ( ⊥ ‘ 𝑝 ) ) ) ) )
19 df-polarityN ⊢ ⊥𝑃 = ( ℎ ∈ V ↦ ( 𝑚 ∈ 𝒫 ( Atoms ‘ ℎ ) ↦ ( ( Atoms ‘ ℎ ) ∩ ∩ 𝑝 ∈ 𝑚 ( ( pmap ‘ ℎ ) ‘ ( ( oc ‘ ℎ ) ‘ 𝑝 ) ) ) ) )
20 2 fvexi ⊢ 𝐴 ∈ V
21 20 pwex ⊢ 𝒫 𝐴 ∈ V
22 21 mptex ⊢ ( 𝑚 ∈ 𝒫 𝐴 ↦ ( 𝐴 ∩ ∩ 𝑝 ∈ 𝑚 ( 𝑀 ‘ ( ⊥ ‘ 𝑝 ) ) ) ) ∈ V
23 18 19 22 fvmpt ⊢ ( 𝐾 ∈ V → ( ⊥𝑃 ‘ 𝐾 ) = ( 𝑚 ∈ 𝒫 𝐴 ↦ ( 𝐴 ∩ ∩ 𝑝 ∈ 𝑚 ( 𝑀 ‘ ( ⊥ ‘ 𝑝 ) ) ) ) )
24 4 23 eqtrid ⊢ ( 𝐾 ∈ V → 𝑃 = ( 𝑚 ∈ 𝒫 𝐴 ↦ ( 𝐴 ∩ ∩ 𝑝 ∈ 𝑚 ( 𝑀 ‘ ( ⊥ ‘ 𝑝 ) ) ) ) )
25 5 24 syl ⊢ ( 𝐾 ∈ 𝐵 → 𝑃 = ( 𝑚 ∈ 𝒫 𝐴 ↦ ( 𝐴 ∩ ∩ 𝑝 ∈ 𝑚 ( 𝑀 ‘ ( ⊥ ‘ 𝑝 ) ) ) ) )