dochssv

Description: A subspace orthocomplement belongs to the DVecH vector space. (Contributed by NM, 22-Jul-2014)

	Ref	Expression
Hypotheses	dochssv.h	$⊢ H = LHyp (K)$
	dochssv.u	$⊢ U = DVecH (K) (W)$
	dochssv.v	$⊢ V = {Base}_{U}$
	dochssv.o	$⊢ \underset{˙}{⊥} = ocH (K) (W)$
Assertion	dochssv	$⊢ ((K \in HL \land W \in H) \land X \subseteq V) \to \underset{˙}{⊥} (X) \subseteq V$

Step	Hyp	Ref	Expression
1		dochssv.h	$⊢ H = LHyp (K)$
2		dochssv.u	$⊢ U = DVecH (K) (W)$
3		dochssv.v	$⊢ V = {Base}_{U}$
4		dochssv.o	$⊢ \underset{˙}{⊥} = ocH (K) (W)$
5		eqid	$⊢ DIsoH (K) (W) = DIsoH (K) (W)$
6	1 5 2 3 4	dochcl	$⊢ ((K \in HL \land W \in H) \land X \subseteq V) \to \underset{˙}{⊥} (X) \in ran DIsoH (K) (W)$
7	1 2 5 3	dihrnss	$⊢ ((K \in HL \land W \in H) \land \underset{˙}{⊥} (X) \in ran DIsoH (K) (W)) \to \underset{˙}{⊥} (X) \subseteq V$
8	6 7	syldan	$⊢ ((K \in HL \land W \in H) \land X \subseteq V) \to \underset{˙}{⊥} (X) \subseteq V$

Metamath Proof Explorer