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	⊢ ( 𝜑 → ( ⊥ ‘ ( 𝑋 ∩ 𝑌 ) ) = ( ( ⊥ ‘ 𝑋 ) ∨ ( ⊥ ‘ 𝑌 ) ) )

Metamath Proof Explorer

Theorem dochdmm1

Proof