Metamath Proof Explorer

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 
|- U = ( lub ` K )
polval2.o 
|- ._|_ = ( oc ` K )
polval2.a 
|- A = ( Atoms ` K )
polval2.m 
|- M = ( pmap ` K )
polval2.p 
|- P = ( _|_P ` K )
Assertion polval2N 
|- ( ( K e. HL /\ X C_ A ) -> ( P ` X ) = ( M ` ( ._|_ ` ( U ` X ) ) ) )

Proof

Step Hyp Ref Expression
1 polval2.u 
 |-  U = ( lub ` K )
2 polval2.o 
 |-  ._|_ = ( oc ` K )
3 polval2.a 
 |-  A = ( Atoms ` K )
4 polval2.m 
 |-  M = ( pmap ` K )
5 polval2.p 
 |-  P = ( _|_P ` K )
6 2 3 4 5 polvalN 
 |-  ( ( K e. HL /\ X C_ A ) -> ( P ` X ) = ( A i^i |^|_ p e. X ( M ` ( ._|_ ` p ) ) ) )
7 hlop 
 |-  ( K e. HL -> K e. OP )
8 7 ad2antrr 
 |-  ( ( ( K e. HL /\ X C_ A ) /\ p e. X ) -> K e. OP )
9 ssel2 
 |-  ( ( X C_ A /\ p e. X ) -> p e. A )
10 9 adantll 
 |-  ( ( ( K e. HL /\ X C_ A ) /\ p e. X ) -> p e. A )
11 eqid 
 |-  ( Base ` K ) = ( Base ` K )
12 11 3 atbase 
 |-  ( p e. A -> p e. ( Base ` K ) )
13 10 12 syl 
 |-  ( ( ( K e. HL /\ X C_ A ) /\ p e. X ) -> p e. ( Base ` K ) )
14 11 2 opoccl 
 |-  ( ( K e. OP /\ p e. ( Base ` K ) ) -> ( ._|_ ` p ) e. ( Base ` K ) )
15 8 13 14 syl2anc 
 |-  ( ( ( K e. HL /\ X C_ A ) /\ p e. X ) -> ( ._|_ ` p ) e. ( Base ` K ) )
16 15 ralrimiva 
 |-  ( ( K e. HL /\ X C_ A ) -> A. p e. X ( ._|_ ` p ) e. ( Base ` K ) )
17 eqid 
 |-  ( glb ` K ) = ( glb ` K )
18 11 17 3 4 pmapglb2xN 
 |-  ( ( K e. HL /\ A. p e. X ( ._|_ ` p ) e. ( Base ` K ) ) -> ( M ` ( ( glb ` K ) ` { x | E. p e. X x = ( ._|_ ` p ) } ) ) = ( A i^i |^|_ p e. X ( M ` ( ._|_ ` p ) ) ) )
19 16 18 syldan 
 |-  ( ( K e. HL /\ X C_ A ) -> ( M ` ( ( glb ` K ) ` { x | E. p e. X x = ( ._|_ ` p ) } ) ) = ( A i^i |^|_ p e. X ( M ` ( ._|_ ` p ) ) ) )
20 11 1 17 2 glbconxN 
 |-  ( ( K e. HL /\ A. p e. X ( ._|_ ` p ) e. ( Base ` K ) ) -> ( ( glb ` K ) ` { x | E. p e. X x = ( ._|_ ` p ) } ) = ( ._|_ ` ( U ` { x | E. p e. X x = ( ._|_ ` ( ._|_ ` p ) ) } ) ) )
21 16 20 syldan 
 |-  ( ( K e. HL /\ X C_ A ) -> ( ( glb ` K ) ` { x | E. p e. X x = ( ._|_ ` p ) } ) = ( ._|_ ` ( U ` { x | E. p e. X x = ( ._|_ ` ( ._|_ ` p ) ) } ) ) )
22 11 2 opococ 
 |-  ( ( K e. OP /\ p e. ( Base ` K ) ) -> ( ._|_ ` ( ._|_ ` p ) ) = p )
23 8 13 22 syl2anc 
 |-  ( ( ( K e. HL /\ X C_ A ) /\ p e. X ) -> ( ._|_ ` ( ._|_ ` p ) ) = p )
24 23 eqeq2d 
 |-  ( ( ( K e. HL /\ X C_ A ) /\ p e. X ) -> ( x = ( ._|_ ` ( ._|_ ` p ) ) <-> x = p ) )
25 24 rexbidva 
 |-  ( ( K e. HL /\ X C_ A ) -> ( E. p e. X x = ( ._|_ ` ( ._|_ ` p ) ) <-> E. p e. X x = p ) )
26 25 abbidv 
 |-  ( ( K e. HL /\ X C_ A ) -> { x | E. p e. X x = ( ._|_ ` ( ._|_ ` p ) ) } = { x | E. p e. X x = p } )
27 df-rex 
 |-  ( E. p e. X x = p <-> E. p ( p e. X /\ x = p ) )
28 equcom 
 |-  ( x = p <-> p = x )
29 28 anbi1ci 
 |-  ( ( p e. X /\ x = p ) <-> ( p = x /\ p e. X ) )
30 29 exbii 
 |-  ( E. p ( p e. X /\ x = p ) <-> E. p ( p = x /\ p e. X ) )
31 eleq1w 
 |-  ( p = x -> ( p e. X <-> x e. X ) )
32 31 equsexvw 
 |-  ( E. p ( p = x /\ p e. X ) <-> x e. X )
33 27 30 32 3bitri 
 |-  ( E. p e. X x = p <-> x e. X )
34 33 abbii 
 |-  { x | E. p e. X x = p } = { x | x e. X }
35 abid2 
 |-  { x | x e. X } = X
36 34 35 eqtri 
 |-  { x | E. p e. X x = p } = X
37 26 36 eqtrdi 
 |-  ( ( K e. HL /\ X C_ A ) -> { x | E. p e. X x = ( ._|_ ` ( ._|_ ` p ) ) } = X )
38 37 fveq2d 
 |-  ( ( K e. HL /\ X C_ A ) -> ( U ` { x | E. p e. X x = ( ._|_ ` ( ._|_ ` p ) ) } ) = ( U ` X ) )
39 38 fveq2d 
 |-  ( ( K e. HL /\ X C_ A ) -> ( ._|_ ` ( U ` { x | E. p e. X x = ( ._|_ ` ( ._|_ ` p ) ) } ) ) = ( ._|_ ` ( U ` X ) ) )
40 21 39 eqtrd 
 |-  ( ( K e. HL /\ X C_ A ) -> ( ( glb ` K ) ` { x | E. p e. X x = ( ._|_ ` p ) } ) = ( ._|_ ` ( U ` X ) ) )
41 40 fveq2d 
 |-  ( ( K e. HL /\ X C_ A ) -> ( M ` ( ( glb ` K ) ` { x | E. p e. X x = ( ._|_ ` p ) } ) ) = ( M ` ( ._|_ ` ( U ` X ) ) ) )
42 6 19 41 3eqtr2d 
 |-  ( ( K e. HL /\ X C_ A ) -> ( P ` X ) = ( M ` ( ._|_ ` ( U ` X ) ) ) )