dochn0nv

Description: An orthocomplement is nonzero iff the double orthocomplement is not the whole vector space. (Contributed by NM, 1-Jan-2015)

	Ref	Expression
Hypotheses	dochn0nv.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	dochn0nv.o	⊢ ⊥ = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
	dochn0nv.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
	dochn0nv.v	⊢ 𝑉 = ( Base ‘ 𝑈 )
	dochn0nv.z	⊢ 0 = ( 0_g ‘ 𝑈 )
	dochn0nv.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
	dochn0nv.x	⊢ ( 𝜑 → 𝑋 ⊆ 𝑉 )
Assertion	dochn0nv	⊢ ( 𝜑 → ( ( ⊥ ‘ 𝑋 ) ≠ { 0 } ↔ ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) ≠ 𝑉 ) )

Proof

Step	Hyp	Ref	Expression
1		dochn0nv.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2		dochn0nv.o	⊢ ⊥ = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
3		dochn0nv.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
4		dochn0nv.v	⊢ 𝑉 = ( Base ‘ 𝑈 )
5		dochn0nv.z	⊢ 0 = ( 0_g ‘ 𝑈 )
6		dochn0nv.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
7		dochn0nv.x	⊢ ( 𝜑 → 𝑋 ⊆ 𝑉 )
8		eqid	⊢ ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
9	1 8 3 4 2	dochcl	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ⊆ 𝑉 ) → ( ⊥ ‘ 𝑋 ) ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) )
10	6 7 9	syl2anc	⊢ ( 𝜑 → ( ⊥ ‘ 𝑋 ) ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) )
11	1 8 2	dochoc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ⊥ ‘ 𝑋 ) ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ) → ( ⊥ ‘ ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) ) = ( ⊥ ‘ 𝑋 ) )
12	6 10 11	syl2anc	⊢ ( 𝜑 → ( ⊥ ‘ ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) ) = ( ⊥ ‘ 𝑋 ) )
13	1 3 2 4 5	doch1	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( ⊥ ‘ 𝑉 ) = { 0 } )
14	6 13	syl	⊢ ( 𝜑 → ( ⊥ ‘ 𝑉 ) = { 0 } )
15	12 14	eqeq12d	⊢ ( 𝜑 → ( ( ⊥ ‘ ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) ) = ( ⊥ ‘ 𝑉 ) ↔ ( ⊥ ‘ 𝑋 ) = { 0 } ) )
16	1 3 4 2	dochssv	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ⊆ 𝑉 ) → ( ⊥ ‘ 𝑋 ) ⊆ 𝑉 )
17	6 7 16	syl2anc	⊢ ( 𝜑 → ( ⊥ ‘ 𝑋 ) ⊆ 𝑉 )
18	1 8 3 4 2	dochcl	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ⊥ ‘ 𝑋 ) ⊆ 𝑉 ) → ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) )
19	6 17 18	syl2anc	⊢ ( 𝜑 → ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) )
20	1 8 3 4	dih1rn	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 𝑉 ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) )
21	6 20	syl	⊢ ( 𝜑 → 𝑉 ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) )
22	1 8 2 6 19 21	doch11	⊢ ( 𝜑 → ( ( ⊥ ‘ ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) ) = ( ⊥ ‘ 𝑉 ) ↔ ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) = 𝑉 ) )
23	15 22	bitr3d	⊢ ( 𝜑 → ( ( ⊥ ‘ 𝑋 ) = { 0 } ↔ ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) = 𝑉 ) )
24	23	necon3bid	⊢ ( 𝜑 → ( ( ⊥ ‘ 𝑋 ) ≠ { 0 } ↔ ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) ≠ 𝑉 ) )

Metamath Proof Explorer

Theorem dochn0nv

Proof