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