Theorem polval2N

Description: Alternate expression for value of the projective subspace polarity function. Equation for polarity in Holland95 p. 223. (Contributed by NM, 22-Jan-2012) (New usage is discouraged.)

	Ref	Expression
Hypotheses	polval2.u	⊢ 𝑈 = ( lub ‘ 𝐾 )
	polval2.o	⊢ ⊥ = ( oc ‘ 𝐾 )
	polval2.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
	polval2.m	⊢ 𝑀 = ( pmap ‘ 𝐾 )
	polval2.p	⊢ 𝑃 = ( ⊥𝑃 ‘ 𝐾 )
Assertion	polval2N	⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ) → ( 𝑃 ‘ 𝑋 ) = ( 𝑀 ‘ ( ⊥ ‘ ( 𝑈 ‘ 𝑋 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		polval2.u	⊢ 𝑈 = ( lub ‘ 𝐾 )
2		polval2.o	⊢ ⊥ = ( oc ‘ 𝐾 )
3		polval2.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
4		polval2.m	⊢ 𝑀 = ( pmap ‘ 𝐾 )
5		polval2.p	⊢ 𝑃 = ( ⊥𝑃 ‘ 𝐾 )
6	2 3 4 5	polvalN	⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ) → ( 𝑃 ‘ 𝑋 ) = ( 𝐴 ∩ ∩ 𝑝 ∈ 𝑋 ( 𝑀 ‘ ( ⊥ ‘ 𝑝 ) ) ) )
7		hlop	⊢ ( 𝐾 ∈ HL → 𝐾 ∈ OP )
8	7	ad2antrr	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ) ∧ 𝑝 ∈ 𝑋 ) → 𝐾 ∈ OP )
9		ssel2	⊢ ( ( 𝑋 ⊆ 𝐴 ∧ 𝑝 ∈ 𝑋 ) → 𝑝 ∈ 𝐴 )
10	9	adantll	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ) ∧ 𝑝 ∈ 𝑋 ) → 𝑝 ∈ 𝐴 )
11		eqid	⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
12	11 3	atbase	⊢ ( 𝑝 ∈ 𝐴 → 𝑝 ∈ ( Base ‘ 𝐾 ) )
13	10 12	syl	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ) ∧ 𝑝 ∈ 𝑋 ) → 𝑝 ∈ ( Base ‘ 𝐾 ) )
14	11 2	opoccl	⊢ ( ( 𝐾 ∈ OP ∧ 𝑝 ∈ ( Base ‘ 𝐾 ) ) → ( ⊥ ‘ 𝑝 ) ∈ ( Base ‘ 𝐾 ) )
15	8 13 14	syl2anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ) ∧ 𝑝 ∈ 𝑋 ) → ( ⊥ ‘ 𝑝 ) ∈ ( Base ‘ 𝐾 ) )
16	15	ralrimiva	⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ) → ∀ 𝑝 ∈ 𝑋 ( ⊥ ‘ 𝑝 ) ∈ ( Base ‘ 𝐾 ) )
17		eqid	⊢ ( glb ‘ 𝐾 ) = ( glb ‘ 𝐾 )
18	11 17 3 4	pmapglb2xN	⊢ ( ( 𝐾 ∈ HL ∧ ∀ 𝑝 ∈ 𝑋 ( ⊥ ‘ 𝑝 ) ∈ ( Base ‘ 𝐾 ) ) → ( 𝑀 ‘ ( ( glb ‘ 𝐾 ) ‘ { 𝑥 ∣ ∃ 𝑝 ∈ 𝑋 𝑥 = ( ⊥ ‘ 𝑝 ) } ) ) = ( 𝐴 ∩ ∩ 𝑝 ∈ 𝑋 ( 𝑀 ‘ ( ⊥ ‘ 𝑝 ) ) ) )
19	16 18	syldan	⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ) → ( 𝑀 ‘ ( ( glb ‘ 𝐾 ) ‘ { 𝑥 ∣ ∃ 𝑝 ∈ 𝑋 𝑥 = ( ⊥ ‘ 𝑝 ) } ) ) = ( 𝐴 ∩ ∩ 𝑝 ∈ 𝑋 ( 𝑀 ‘ ( ⊥ ‘ 𝑝 ) ) ) )
20	11 1 17 2	glbconxN	⊢ ( ( 𝐾 ∈ HL ∧ ∀ 𝑝 ∈ 𝑋 ( ⊥ ‘ 𝑝 ) ∈ ( Base ‘ 𝐾 ) ) → ( ( glb ‘ 𝐾 ) ‘ { 𝑥 ∣ ∃ 𝑝 ∈ 𝑋 𝑥 = ( ⊥ ‘ 𝑝 ) } ) = ( ⊥ ‘ ( 𝑈 ‘ { 𝑥 ∣ ∃ 𝑝 ∈ 𝑋 𝑥 = ( ⊥ ‘ ( ⊥ ‘ 𝑝 ) ) } ) ) )
21	16 20	syldan	⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ) → ( ( glb ‘ 𝐾 ) ‘ { 𝑥 ∣ ∃ 𝑝 ∈ 𝑋 𝑥 = ( ⊥ ‘ 𝑝 ) } ) = ( ⊥ ‘ ( 𝑈 ‘ { 𝑥 ∣ ∃ 𝑝 ∈ 𝑋 𝑥 = ( ⊥ ‘ ( ⊥ ‘ 𝑝 ) ) } ) ) )
22	11 2	opococ	⊢ ( ( 𝐾 ∈ OP ∧ 𝑝 ∈ ( Base ‘ 𝐾 ) ) → ( ⊥ ‘ ( ⊥ ‘ 𝑝 ) ) = 𝑝 )
23	8 13 22	syl2anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ) ∧ 𝑝 ∈ 𝑋 ) → ( ⊥ ‘ ( ⊥ ‘ 𝑝 ) ) = 𝑝 )
24	23	eqeq2d	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ) ∧ 𝑝 ∈ 𝑋 ) → ( 𝑥 = ( ⊥ ‘ ( ⊥ ‘ 𝑝 ) ) ↔ 𝑥 = 𝑝 ) )
25	24	rexbidva	⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ) → ( ∃ 𝑝 ∈ 𝑋 𝑥 = ( ⊥ ‘ ( ⊥ ‘ 𝑝 ) ) ↔ ∃ 𝑝 ∈ 𝑋 𝑥 = 𝑝 ) )
26	25	abbidv	⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ) → { 𝑥 ∣ ∃ 𝑝 ∈ 𝑋 𝑥 = ( ⊥ ‘ ( ⊥ ‘ 𝑝 ) ) } = { 𝑥 ∣ ∃ 𝑝 ∈ 𝑋 𝑥 = 𝑝 } )
27		df-rex	⊢ ( ∃ 𝑝 ∈ 𝑋 𝑥 = 𝑝 ↔ ∃ 𝑝 ( 𝑝 ∈ 𝑋 ∧ 𝑥 = 𝑝 ) )
28		equcom	⊢ ( 𝑥 = 𝑝 ↔ 𝑝 = 𝑥 )
29	28	anbi1ci	⊢ ( ( 𝑝 ∈ 𝑋 ∧ 𝑥 = 𝑝 ) ↔ ( 𝑝 = 𝑥 ∧ 𝑝 ∈ 𝑋 ) )
30	29	exbii	⊢ ( ∃ 𝑝 ( 𝑝 ∈ 𝑋 ∧ 𝑥 = 𝑝 ) ↔ ∃ 𝑝 ( 𝑝 = 𝑥 ∧ 𝑝 ∈ 𝑋 ) )
31		eleq1w	⊢ ( 𝑝 = 𝑥 → ( 𝑝 ∈ 𝑋 ↔ 𝑥 ∈ 𝑋 ) )
32	31	equsexvw	⊢ ( ∃ 𝑝 ( 𝑝 = 𝑥 ∧ 𝑝 ∈ 𝑋 ) ↔ 𝑥 ∈ 𝑋 )
33	27 30 32	3bitri	⊢ ( ∃ 𝑝 ∈ 𝑋 𝑥 = 𝑝 ↔ 𝑥 ∈ 𝑋 )
34	33	abbii	⊢ { 𝑥 ∣ ∃ 𝑝 ∈ 𝑋 𝑥 = 𝑝 } = { 𝑥 ∣ 𝑥 ∈ 𝑋 }
35		abid2	⊢ { 𝑥 ∣ 𝑥 ∈ 𝑋 } = 𝑋
36	34 35	eqtri	⊢ { 𝑥 ∣ ∃ 𝑝 ∈ 𝑋 𝑥 = 𝑝 } = 𝑋
37	26 36	eqtrdi	⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ) → { 𝑥 ∣ ∃ 𝑝 ∈ 𝑋 𝑥 = ( ⊥ ‘ ( ⊥ ‘ 𝑝 ) ) } = 𝑋 )
38	37	fveq2d	⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ) → ( 𝑈 ‘ { 𝑥 ∣ ∃ 𝑝 ∈ 𝑋 𝑥 = ( ⊥ ‘ ( ⊥ ‘ 𝑝 ) ) } ) = ( 𝑈 ‘ 𝑋 ) )
39	38	fveq2d	⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ) → ( ⊥ ‘ ( 𝑈 ‘ { 𝑥 ∣ ∃ 𝑝 ∈ 𝑋 𝑥 = ( ⊥ ‘ ( ⊥ ‘ 𝑝 ) ) } ) ) = ( ⊥ ‘ ( 𝑈 ‘ 𝑋 ) ) )
40	21 39	eqtrd	⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ) → ( ( glb ‘ 𝐾 ) ‘ { 𝑥 ∣ ∃ 𝑝 ∈ 𝑋 𝑥 = ( ⊥ ‘ 𝑝 ) } ) = ( ⊥ ‘ ( 𝑈 ‘ 𝑋 ) ) )
41	40	fveq2d	⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ) → ( 𝑀 ‘ ( ( glb ‘ 𝐾 ) ‘ { 𝑥 ∣ ∃ 𝑝 ∈ 𝑋 𝑥 = ( ⊥ ‘ 𝑝 ) } ) ) = ( 𝑀 ‘ ( ⊥ ‘ ( 𝑈 ‘ 𝑋 ) ) ) )
42	6 19 41	3eqtr2d	⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ) → ( 𝑃 ‘ 𝑋 ) = ( 𝑀 ‘ ( ⊥ ‘ ( 𝑈 ‘ 𝑋 ) ) ) )