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	⊢ ( ( 𝐾 ∈ 𝐵 ∧ 𝑋 ⊆ 𝐴 ) → ( 𝑃 ‘ 𝑋 ) = ( 𝐴 ∩ ∩ 𝑝 ∈ 𝑋 ( 𝑀 ‘ ( ⊥ ‘ 𝑝 ) ) ) )