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	syl5eq	⊢ ( 𝐾 ∈ V → 𝑃 = ( 𝑚 ∈ 𝒫 𝐴 ↦ ( 𝐴 ∩ ∩ 𝑝 ∈ 𝑚 ( 𝑀 ‘ ( ⊥ ‘ 𝑝 ) ) ) ) )
25	5 24	syl	⊢ ( 𝐾 ∈ 𝐵 → 𝑃 = ( 𝑚 ∈ 𝒫 𝐴 ↦ ( 𝐴 ∩ ∩ 𝑝 ∈ 𝑚 ( 𝑀 ‘ ( ⊥ ‘ 𝑝 ) ) ) ) )