Metamath Proof Explorer

Theorem doch2val2

Description: Double orthocomplement for DVecH vector space. (Contributed by NM, 26-Jul-2014)

Ref Expression
Hypotheses doch2val2.h ⊢ H = LHyp ⁡ K
doch2val2.i ⊢ I = DIsoH ⁡ K ⁡ W
doch2val2.u ⊢ U = DVecH ⁡ K ⁡ W
doch2val2.v ⊢ V = Base U
doch2val2.o ⊢ ⊥ ˙ = ocH ⁡ K ⁡ W
doch2val2.k ⊢ φ → K ∈ HL ∧ W ∈ H
doch2val2.x ⊢ φ → X ⊆ V
Assertion doch2val2 ⊢ φ → ⊥ ˙ ⁡ ⊥ ˙ ⁡ X = ⋂ z ∈ ran ⁡ I | X ⊆ z

Proof

Step Hyp Ref Expression
1 doch2val2.h ⊢ H = LHyp ⁡ K
2 doch2val2.i ⊢ I = DIsoH ⁡ K ⁡ W
3 doch2val2.u ⊢ U = DVecH ⁡ K ⁡ W
4 doch2val2.v ⊢ V = Base U
5 doch2val2.o ⊢ ⊥ ˙ = ocH ⁡ K ⁡ W
6 doch2val2.k ⊢ φ → K ∈ HL ∧ W ∈ H
7 doch2val2.x ⊢ φ → X ⊆ V
8 eqid ⊢ oc ⁡ K = oc ⁡ K
9 8 1 2 3 4 5 dochval2 ⊢ K ∈ HL ∧ W ∈ H ∧ X ⊆ V → ⊥ ˙ ⁡ X = I ⁡ oc ⁡ K ⁡ I -1 ⁡ ⋂ z ∈ ran ⁡ I | X ⊆ z
10 6 7 9 syl2anc ⊢ φ → ⊥ ˙ ⁡ X = I ⁡ oc ⁡ K ⁡ I -1 ⁡ ⋂ z ∈ ran ⁡ I | X ⊆ z
11 10 fveq2d ⊢ φ → ⊥ ˙ ⁡ ⊥ ˙ ⁡ X = ⊥ ˙ ⁡ I ⁡ oc ⁡ K ⁡ I -1 ⁡ ⋂ z ∈ ran ⁡ I | X ⊆ z
12 6 simpld ⊢ φ → K ∈ HL
13 hlop ⊢ K ∈ HL → K ∈ OP
14 12 13 syl ⊢ φ → K ∈ OP
15 ssrab2 ⊢ z ∈ ran ⁡ I | X ⊆ z ⊆ ran ⁡ I
16 15 a1i ⊢ φ → z ∈ ran ⁡ I | X ⊆ z ⊆ ran ⁡ I
17 1 2 3 4 dih1rn ⊢ K ∈ HL ∧ W ∈ H → V ∈ ran ⁡ I
18 6 17 syl ⊢ φ → V ∈ ran ⁡ I
19 sseq2 ⊢ z = V → X ⊆ z ↔ X ⊆ V
20 19 elrab ⊢ V ∈ z ∈ ran ⁡ I | X ⊆ z ↔ V ∈ ran ⁡ I ∧ X ⊆ V
21 18 7 20 sylanbrc ⊢ φ → V ∈ z ∈ ran ⁡ I | X ⊆ z
22 21 ne0d ⊢ φ → z ∈ ran ⁡ I | X ⊆ z ≠ ∅
23 1 2 dihintcl ⊢ K ∈ HL ∧ W ∈ H ∧ z ∈ ran ⁡ I | X ⊆ z ⊆ ran ⁡ I ∧ z ∈ ran ⁡ I | X ⊆ z ≠ ∅ → ⋂ z ∈ ran ⁡ I | X ⊆ z ∈ ran ⁡ I
24 6 16 22 23 syl12anc ⊢ φ → ⋂ z ∈ ran ⁡ I | X ⊆ z ∈ ran ⁡ I
25 eqid ⊢ Base K = Base K
26 25 1 2 dihcnvcl ⊢ K ∈ HL ∧ W ∈ H ∧ ⋂ z ∈ ran ⁡ I | X ⊆ z ∈ ran ⁡ I → I -1 ⁡ ⋂ z ∈ ran ⁡ I | X ⊆ z ∈ Base K
27 6 24 26 syl2anc ⊢ φ → I -1 ⁡ ⋂ z ∈ ran ⁡ I | X ⊆ z ∈ Base K
28 25 8 opoccl ⊢ K ∈ OP ∧ I -1 ⁡ ⋂ z ∈ ran ⁡ I | X ⊆ z ∈ Base K → oc ⁡ K ⁡ I -1 ⁡ ⋂ z ∈ ran ⁡ I | X ⊆ z ∈ Base K
29 14 27 28 syl2anc ⊢ φ → oc ⁡ K ⁡ I -1 ⁡ ⋂ z ∈ ran ⁡ I | X ⊆ z ∈ Base K
30 25 8 1 2 5 dochvalr2 ⊢ K ∈ HL ∧ W ∈ H ∧ oc ⁡ K ⁡ I -1 ⁡ ⋂ z ∈ ran ⁡ I | X ⊆ z ∈ Base K → ⊥ ˙ ⁡ I ⁡ oc ⁡ K ⁡ I -1 ⁡ ⋂ z ∈ ran ⁡ I | X ⊆ z = I ⁡ oc ⁡ K ⁡ oc ⁡ K ⁡ I -1 ⁡ ⋂ z ∈ ran ⁡ I | X ⊆ z
31 6 29 30 syl2anc ⊢ φ → ⊥ ˙ ⁡ I ⁡ oc ⁡ K ⁡ I -1 ⁡ ⋂ z ∈ ran ⁡ I | X ⊆ z = I ⁡ oc ⁡ K ⁡ oc ⁡ K ⁡ I -1 ⁡ ⋂ z ∈ ran ⁡ I | X ⊆ z
32 25 8 opococ ⊢ K ∈ OP ∧ I -1 ⁡ ⋂ z ∈ ran ⁡ I | X ⊆ z ∈ Base K → oc ⁡ K ⁡ oc ⁡ K ⁡ I -1 ⁡ ⋂ z ∈ ran ⁡ I | X ⊆ z = I -1 ⁡ ⋂ z ∈ ran ⁡ I | X ⊆ z
33 14 27 32 syl2anc ⊢ φ → oc ⁡ K ⁡ oc ⁡ K ⁡ I -1 ⁡ ⋂ z ∈ ran ⁡ I | X ⊆ z = I -1 ⁡ ⋂ z ∈ ran ⁡ I | X ⊆ z
34 33 fveq2d ⊢ φ → I ⁡ oc ⁡ K ⁡ oc ⁡ K ⁡ I -1 ⁡ ⋂ z ∈ ran ⁡ I | X ⊆ z = I ⁡ I -1 ⁡ ⋂ z ∈ ran ⁡ I | X ⊆ z
35 1 2 dihcnvid2 ⊢ K ∈ HL ∧ W ∈ H ∧ ⋂ z ∈ ran ⁡ I | X ⊆ z ∈ ran ⁡ I → I ⁡ I -1 ⁡ ⋂ z ∈ ran ⁡ I | X ⊆ z = ⋂ z ∈ ran ⁡ I | X ⊆ z
36 6 24 35 syl2anc ⊢ φ → I ⁡ I -1 ⁡ ⋂ z ∈ ran ⁡ I | X ⊆ z = ⋂ z ∈ ran ⁡ I | X ⊆ z
37 34 36 eqtrd ⊢ φ → I ⁡ oc ⁡ K ⁡ oc ⁡ K ⁡ I -1 ⁡ ⋂ z ∈ ran ⁡ I | X ⊆ z = ⋂ z ∈ ran ⁡ I | X ⊆ z
38 11 31 37 3eqtrd ⊢ φ → ⊥ ˙ ⁡ ⊥ ˙ ⁡ X = ⋂ z ∈ ran ⁡ I | X ⊆ z