This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
dochdmm1.i ⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
dochdmm1.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
dochdmm1.v ⊢ 𝑉 = ( Base ‘ 𝑈 )
dochdmm1.o ⊢ ⊥ = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
dochdmm1.j ⊢ ∨ = ( ( joinH ‘ 𝐾 ) ‘ 𝑊 )
dochdmm1.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
dochdmm1.x ⊢ ( 𝜑 → 𝑋 ∈ ran 𝐼 )
dochdmm1.y ⊢ ( 𝜑 → 𝑌 ∈ ran 𝐼 )
Assertion dochdmm1 ( 𝜑 → ( ⊥ ‘ ( 𝑋 ∩ 𝑌 ) ) = ( ( ⊥ ‘ 𝑋 ) ∨ ( ⊥ ‘ 𝑌 ) ) )

Proof

Step Hyp Ref Expression
1 dochdmm1.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2 dochdmm1.i ⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
3 dochdmm1.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
4 dochdmm1.v ⊢ 𝑉 = ( Base ‘ 𝑈 )
5 dochdmm1.o ⊢ ⊥ = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
6 dochdmm1.j ⊢ ∨ = ( ( joinH ‘ 𝐾 ) ‘ 𝑊 )
7 dochdmm1.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
8 dochdmm1.x ⊢ ( 𝜑 → 𝑋 ∈ ran 𝐼 )
9 dochdmm1.y ⊢ ( 𝜑 → 𝑌 ∈ ran 𝐼 )
10 1 3 2 4 dihrnss ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ ran 𝐼 ) → 𝑋 ⊆ 𝑉 )
11 7 8 10 syl2anc ⊢ ( 𝜑 → 𝑋 ⊆ 𝑉 )
12 1 3 4 5 dochssv ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ⊆ 𝑉 ) → ( ⊥ ‘ 𝑋 ) ⊆ 𝑉 )
13 7 11 12 syl2anc ⊢ ( 𝜑 → ( ⊥ ‘ 𝑋 ) ⊆ 𝑉 )
14 1 3 2 4 dihrnss ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑌 ∈ ran 𝐼 ) → 𝑌 ⊆ 𝑉 )
15 7 9 14 syl2anc ⊢ ( 𝜑 → 𝑌 ⊆ 𝑉 )
16 1 3 4 5 dochssv ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑌 ⊆ 𝑉 ) → ( ⊥ ‘ 𝑌 ) ⊆ 𝑉 )
17 7 15 16 syl2anc ⊢ ( 𝜑 → ( ⊥ ‘ 𝑌 ) ⊆ 𝑉 )
18 1 3 4 5 dochdmj1 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ⊥ ‘ 𝑋 ) ⊆ 𝑉 ∧ ( ⊥ ‘ 𝑌 ) ⊆ 𝑉 ) → ( ⊥ ‘ ( ( ⊥ ‘ 𝑋 ) ∪ ( ⊥ ‘ 𝑌 ) ) ) = ( ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) ∩ ( ⊥ ‘ ( ⊥ ‘ 𝑌 ) ) ) )
19 7 13 17 18 syl3anc ⊢ ( 𝜑 → ( ⊥ ‘ ( ( ⊥ ‘ 𝑋 ) ∪ ( ⊥ ‘ 𝑌 ) ) ) = ( ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) ∩ ( ⊥ ‘ ( ⊥ ‘ 𝑌 ) ) ) )
20 1 2 5 dochoc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ ran 𝐼 ) → ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) = 𝑋 )
21 7 8 20 syl2anc ⊢ ( 𝜑 → ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) = 𝑋 )
22 1 2 5 dochoc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑌 ∈ ran 𝐼 ) → ( ⊥ ‘ ( ⊥ ‘ 𝑌 ) ) = 𝑌 )
23 7 9 22 syl2anc ⊢ ( 𝜑 → ( ⊥ ‘ ( ⊥ ‘ 𝑌 ) ) = 𝑌 )
24 21 23 ineq12d ⊢ ( 𝜑 → ( ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) ∩ ( ⊥ ‘ ( ⊥ ‘ 𝑌 ) ) ) = ( 𝑋 ∩ 𝑌 ) )
25 19 24 eqtr2d ⊢ ( 𝜑 → ( 𝑋 ∩ 𝑌 ) = ( ⊥ ‘ ( ( ⊥ ‘ 𝑋 ) ∪ ( ⊥ ‘ 𝑌 ) ) ) )
26 25 fveq2d ⊢ ( 𝜑 → ( ⊥ ‘ ( 𝑋 ∩ 𝑌 ) ) = ( ⊥ ‘ ( ⊥ ‘ ( ( ⊥ ‘ 𝑋 ) ∪ ( ⊥ ‘ 𝑌 ) ) ) ) )
27 1 3 4 5 6 djhval2 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ⊥ ‘ 𝑋 ) ⊆ 𝑉 ∧ ( ⊥ ‘ 𝑌 ) ⊆ 𝑉 ) → ( ( ⊥ ‘ 𝑋 ) ∨ ( ⊥ ‘ 𝑌 ) ) = ( ⊥ ‘ ( ⊥ ‘ ( ( ⊥ ‘ 𝑋 ) ∪ ( ⊥ ‘ 𝑌 ) ) ) ) )
28 7 13 17 27 syl3anc ⊢ ( 𝜑 → ( ( ⊥ ‘ 𝑋 ) ∨ ( ⊥ ‘ 𝑌 ) ) = ( ⊥ ‘ ( ⊥ ‘ ( ( ⊥ ‘ 𝑋 ) ∪ ( ⊥ ‘ 𝑌 ) ) ) ) )
29 26 28 eqtr4d ⊢ ( 𝜑 → ( ⊥ ‘ ( 𝑋 ∩ 𝑌 ) ) = ( ( ⊥ ‘ 𝑋 ) ∨ ( ⊥ ‘ 𝑌 ) ) )