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=⊥𝑃⁡K
Assertion polval2N ⊢K∈HL∧X⊆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=⊥𝑃⁡K
6 2 3 4 5 polvalN ⊢K∈HL∧X⊆A→P⁡X=A∩⋂p∈XM⁡⊥˙⁡p
7 hlop ⊢K∈HL→K∈OP
8 7 ad2antrr ⊢K∈HL∧X⊆A∧p∈X→K∈OP
9 ssel2 ⊢X⊆A∧p∈X→p∈A
10 9 adantll ⊢K∈HL∧X⊆A∧p∈X→p∈A
11 eqid ⊢BaseK=BaseK
12 11 3 atbase ⊢p∈A→p∈BaseK
13 10 12 syl ⊢K∈HL∧X⊆A∧p∈X→p∈BaseK
14 11 2 opoccl ⊢K∈OP∧p∈BaseK→⊥˙⁡p∈BaseK
15 8 13 14 syl2anc ⊢K∈HL∧X⊆A∧p∈X→⊥˙⁡p∈BaseK
16 15 ralrimiva ⊢K∈HL∧X⊆A→∀p∈X⊥˙⁡p∈BaseK
17 eqid ⊢glb⁡K=glb⁡K
18 11 17 3 4 pmapglb2xN ⊢K∈HL∧∀p∈X⊥˙⁡p∈BaseK→M⁡glb⁡K⁡x|∃p∈Xx=⊥˙⁡p=A∩⋂p∈XM⁡⊥˙⁡p
19 16 18 syldan ⊢K∈HL∧X⊆A→M⁡glb⁡K⁡x|∃p∈Xx=⊥˙⁡p=A∩⋂p∈XM⁡⊥˙⁡p
20 11 1 17 2 glbconxN ⊢K∈HL∧∀p∈X⊥˙⁡p∈BaseK→glb⁡K⁡x|∃p∈Xx=⊥˙⁡p=⊥˙⁡U⁡x|∃p∈Xx=⊥˙⁡⊥˙⁡p
21 16 20 syldan ⊢K∈HL∧X⊆A→glb⁡K⁡x|∃p∈Xx=⊥˙⁡p=⊥˙⁡U⁡x|∃p∈Xx=⊥˙⁡⊥˙⁡p
22 11 2 opococ ⊢K∈OP∧p∈BaseK→⊥˙⁡⊥˙⁡p=p
23 8 13 22 syl2anc ⊢K∈HL∧X⊆A∧p∈X→⊥˙⁡⊥˙⁡p=p
24 23 eqeq2d ⊢K∈HL∧X⊆A∧p∈X→x=⊥˙⁡⊥˙⁡p↔x=p
25 24 rexbidva ⊢K∈HL∧X⊆A→∃p∈Xx=⊥˙⁡⊥˙⁡p↔∃p∈Xx=p
26 25 abbidv ⊢K∈HL∧X⊆A→x|∃p∈Xx=⊥˙⁡⊥˙⁡p=x|∃p∈Xx=p
27 df-rex ⊢∃p∈Xx=p↔∃pp∈X∧x=p
28 equcom ⊢x=p↔p=x
29 28 anbi1ci ⊢p∈X∧x=p↔p=x∧p∈X
30 29 exbii ⊢∃pp∈X∧x=p↔∃pp=x∧p∈X
31 eleq1w ⊢p=x→p∈X↔x∈X
32 31 equsexvw ⊢∃pp=x∧p∈X↔x∈X
33 27 30 32 3bitri ⊢∃p∈Xx=p↔x∈X
34 33 abbii ⊢x|∃p∈Xx=p=x|x∈X
35 abid2 ⊢x|x∈X=X
36 34 35 eqtri ⊢x|∃p∈Xx=p=X
37 26 36 eqtrdi ⊢K∈HL∧X⊆A→x|∃p∈Xx=⊥˙⁡⊥˙⁡p=X
38 37 fveq2d ⊢K∈HL∧X⊆A→U⁡x|∃p∈Xx=⊥˙⁡⊥˙⁡p=U⁡X
39 38 fveq2d ⊢K∈HL∧X⊆A→⊥˙⁡U⁡x|∃p∈Xx=⊥˙⁡⊥˙⁡p=⊥˙⁡U⁡X
40 21 39 eqtrd ⊢K∈HL∧X⊆A→glb⁡K⁡x|∃p∈Xx=⊥˙⁡p=⊥˙⁡U⁡X
41 40 fveq2d ⊢K∈HL∧X⊆A→M⁡glb⁡K⁡x|∃p∈Xx=⊥˙⁡p=M⁡⊥˙⁡U⁡X
42 6 19 41 3eqtr2d ⊢K∈HL∧X⊆A→P⁡X=M⁡⊥˙⁡U⁡X