Metamath Proof Explorer

Theorem dochdmm1

Description: De Morgan-like law for closed subspace orthocomplement. (Contributed by NM, 13-Jan-2015)

Ref Expression
Hypotheses dochdmm1.h ⊢ H = LHyp ⁡ K
dochdmm1.i ⊢ I = DIsoH ⁡ K ⁡ W
dochdmm1.u ⊢ U = DVecH ⁡ K ⁡ W
dochdmm1.v ⊢ V = Base U
dochdmm1.o ⊢ ⊥ ˙ = ocH ⁡ K ⁡ W
dochdmm1.j ⊢ ∨ ˙ = joinH ⁡ K ⁡ W
dochdmm1.k ⊢ φ → K ∈ HL ∧ W ∈ H
dochdmm1.x ⊢ φ → X ∈ ran ⁡ I
dochdmm1.y ⊢ φ → Y ∈ ran ⁡ I
Assertion dochdmm1 ⊢ φ → ⊥ ˙ ⁡ X ∩ Y = ⊥ ˙ ⁡ X ∨ ˙ ⊥ ˙ ⁡ Y

Proof

Step Hyp Ref Expression
1 dochdmm1.h ⊢ H = LHyp ⁡ K
2 dochdmm1.i ⊢ I = DIsoH ⁡ K ⁡ W
3 dochdmm1.u ⊢ U = DVecH ⁡ K ⁡ W
4 dochdmm1.v ⊢ V = Base U
5 dochdmm1.o ⊢ ⊥ ˙ = ocH ⁡ K ⁡ W
6 dochdmm1.j ⊢ ∨ ˙ = joinH ⁡ K ⁡ W
7 dochdmm1.k ⊢ φ → K ∈ HL ∧ W ∈ H
8 dochdmm1.x ⊢ φ → X ∈ ran ⁡ I
9 dochdmm1.y ⊢ φ → Y ∈ ran ⁡ I
10 1 3 2 4 dihrnss ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ ran ⁡ I → X ⊆ V
11 7 8 10 syl2anc ⊢ φ → X ⊆ V
12 1 3 4 5 dochssv ⊢ K ∈ HL ∧ W ∈ H ∧ X ⊆ V → ⊥ ˙ ⁡ X ⊆ V
13 7 11 12 syl2anc ⊢ φ → ⊥ ˙ ⁡ X ⊆ V
14 1 3 2 4 dihrnss ⊢ K ∈ HL ∧ W ∈ H ∧ Y ∈ ran ⁡ I → Y ⊆ V
15 7 9 14 syl2anc ⊢ φ → Y ⊆ V
16 1 3 4 5 dochssv ⊢ K ∈ HL ∧ W ∈ H ∧ Y ⊆ V → ⊥ ˙ ⁡ Y ⊆ V
17 7 15 16 syl2anc ⊢ φ → ⊥ ˙ ⁡ Y ⊆ V
18 1 3 4 5 dochdmj1 ⊢ K ∈ HL ∧ W ∈ H ∧ ⊥ ˙ ⁡ X ⊆ V ∧ ⊥ ˙ ⁡ Y ⊆ V → ⊥ ˙ ⁡ ⊥ ˙ ⁡ X ∪ ⊥ ˙ ⁡ Y = ⊥ ˙ ⁡ ⊥ ˙ ⁡ X ∩ ⊥ ˙ ⁡ ⊥ ˙ ⁡ Y
19 7 13 17 18 syl3anc ⊢ φ → ⊥ ˙ ⁡ ⊥ ˙ ⁡ X ∪ ⊥ ˙ ⁡ Y = ⊥ ˙ ⁡ ⊥ ˙ ⁡ X ∩ ⊥ ˙ ⁡ ⊥ ˙ ⁡ Y
20 1 2 5 dochoc ⊢ K ∈ HL ∧ W ∈ H ∧ X ∈ ran ⁡ I → ⊥ ˙ ⁡ ⊥ ˙ ⁡ X = X
21 7 8 20 syl2anc ⊢ φ → ⊥ ˙ ⁡ ⊥ ˙ ⁡ X = X
22 1 2 5 dochoc ⊢ K ∈ HL ∧ W ∈ H ∧ Y ∈ ran ⁡ I → ⊥ ˙ ⁡ ⊥ ˙ ⁡ Y = Y
23 7 9 22 syl2anc ⊢ φ → ⊥ ˙ ⁡ ⊥ ˙ ⁡ Y = Y
24 21 23 ineq12d ⊢ φ → ⊥ ˙ ⁡ ⊥ ˙ ⁡ X ∩ ⊥ ˙ ⁡ ⊥ ˙ ⁡ Y = X ∩ Y
25 19 24 eqtr2d ⊢ φ → X ∩ Y = ⊥ ˙ ⁡ ⊥ ˙ ⁡ X ∪ ⊥ ˙ ⁡ Y
26 25 fveq2d ⊢ φ → ⊥ ˙ ⁡ X ∩ Y = ⊥ ˙ ⁡ ⊥ ˙ ⁡ ⊥ ˙ ⁡ X ∪ ⊥ ˙ ⁡ Y
27 1 3 4 5 6 djhval2 ⊢ K ∈ HL ∧ W ∈ H ∧ ⊥ ˙ ⁡ X ⊆ V ∧ ⊥ ˙ ⁡ Y ⊆ V → ⊥ ˙ ⁡ X ∨ ˙ ⊥ ˙ ⁡ Y = ⊥ ˙ ⁡ ⊥ ˙ ⁡ ⊥ ˙ ⁡ X ∪ ⊥ ˙ ⁡ Y
28 7 13 17 27 syl3anc ⊢ φ → ⊥ ˙ ⁡ X ∨ ˙ ⊥ ˙ ⁡ Y = ⊥ ˙ ⁡ ⊥ ˙ ⁡ ⊥ ˙ ⁡ X ∪ ⊥ ˙ ⁡ Y
29 26 28 eqtr4d ⊢ φ → ⊥ ˙ ⁡ X ∩ Y = ⊥ ˙ ⁡ X ∨ ˙ ⊥ ˙ ⁡ Y