Metamath Proof Explorer

Theorem dochpolN

Description: The subspace orthocomplement for the DVecH vector space is a polarity. (Contributed by NM, 27-Dec-2014) (New usage is discouraged.)

Ref Expression
Hypotheses dochpol.h ⊢ H = LHyp ⁡ K
dochpol.o ⊢ ⊥ ˙ = ocH ⁡ K ⁡ W
dochpol.u ⊢ U = DVecH ⁡ K ⁡ W
dochpol.p ⊢ P = LPol ⁡ U
dochpol.k ⊢ φ → K ∈ HL ∧ W ∈ H
Assertion dochpolN ⊢ φ → ⊥ ˙ ∈ P

Proof

Step Hyp Ref Expression
1 dochpol.h ⊢ H = LHyp ⁡ K
2 dochpol.o ⊢ ⊥ ˙ = ocH ⁡ K ⁡ W
3 dochpol.u ⊢ U = DVecH ⁡ K ⁡ W
4 dochpol.p ⊢ P = LPol ⁡ U
5 dochpol.k ⊢ φ → K ∈ HL ∧ W ∈ H
6 eqid ⊢ Base U = Base U
7 eqid ⊢ LSubSp ⁡ U = LSubSp ⁡ U
8 eqid ⊢ 0 U = 0 U
9 eqid ⊢ LSAtoms ⁡ U = LSAtoms ⁡ U
10 eqid ⊢ LSHyp ⁡ U = LSHyp ⁡ U
11 3 fvexi ⊢ U ∈ V
12 11 a1i ⊢ φ → U ∈ V
13 eqid ⊢ DIsoH ⁡ K ⁡ W = DIsoH ⁡ K ⁡ W
14 1 13 3 6 2 5 dochfN ⊢ φ → ⊥ ˙ : 𝒫 Base U ⟶ ran ⁡ DIsoH ⁡ K ⁡ W
15 1 3 13 7 dihsslss ⊢ K ∈ HL ∧ W ∈ H → ran ⁡ DIsoH ⁡ K ⁡ W ⊆ LSubSp ⁡ U
16 5 15 syl ⊢ φ → ran ⁡ DIsoH ⁡ K ⁡ W ⊆ LSubSp ⁡ U
17 14 16 fssd ⊢ φ → ⊥ ˙ : 𝒫 Base U ⟶ LSubSp ⁡ U
18 1 3 2 6 8 doch1 ⊢ K ∈ HL ∧ W ∈ H → ⊥ ˙ ⁡ Base U = 0 U
19 5 18 syl ⊢ φ → ⊥ ˙ ⁡ Base U = 0 U
20 5 adantr ⊢ φ ∧ x ⊆ Base U ∧ y ⊆ Base U ∧ x ⊆ y → K ∈ HL ∧ W ∈ H
21 simpr2 ⊢ φ ∧ x ⊆ Base U ∧ y ⊆ Base U ∧ x ⊆ y → y ⊆ Base U
22 simpr3 ⊢ φ ∧ x ⊆ Base U ∧ y ⊆ Base U ∧ x ⊆ y → x ⊆ y
23 1 3 6 2 dochss ⊢ K ∈ HL ∧ W ∈ H ∧ y ⊆ Base U ∧ x ⊆ y → ⊥ ˙ ⁡ y ⊆ ⊥ ˙ ⁡ x
24 20 21 22 23 syl3anc ⊢ φ ∧ x ⊆ Base U ∧ y ⊆ Base U ∧ x ⊆ y → ⊥ ˙ ⁡ y ⊆ ⊥ ˙ ⁡ x
25 5 adantr ⊢ φ ∧ x ∈ LSAtoms ⁡ U → K ∈ HL ∧ W ∈ H
26 simpr ⊢ φ ∧ x ∈ LSAtoms ⁡ U → x ∈ LSAtoms ⁡ U
27 1 3 2 9 10 25 26 dochsatshp ⊢ φ ∧ x ∈ LSAtoms ⁡ U → ⊥ ˙ ⁡ x ∈ LSHyp ⁡ U
28 1 3 13 9 dih1dimat ⊢ K ∈ HL ∧ W ∈ H ∧ x ∈ LSAtoms ⁡ U → x ∈ ran ⁡ DIsoH ⁡ K ⁡ W
29 25 26 28 syl2anc ⊢ φ ∧ x ∈ LSAtoms ⁡ U → x ∈ ran ⁡ DIsoH ⁡ K ⁡ W
30 1 13 2 dochoc ⊢ K ∈ HL ∧ W ∈ H ∧ x ∈ ran ⁡ DIsoH ⁡ K ⁡ W → ⊥ ˙ ⁡ ⊥ ˙ ⁡ x = x
31 25 29 30 syl2anc ⊢ φ ∧ x ∈ LSAtoms ⁡ U → ⊥ ˙ ⁡ ⊥ ˙ ⁡ x = x
32 6 7 8 9 10 4 12 17 19 24 27 31 islpoldN ⊢ φ → ⊥ ˙ ∈ P