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=BaseU
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=BaseU
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