doch1

Description: Orthocomplement of the unit subspace (all vectors). (Contributed by NM, 19-Jun-2014)

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

Step	Hyp	Ref	Expression
1		doch1.h	$⊢ H = LHyp (K)$
2		doch1.u	$⊢ U = DVecH (K) (W)$
3		doch1.o	$⊢ \underset{˙}{⊥} = ocH (K) (W)$
4		doch1.v	$⊢ V = {Base}_{U}$
5		doch1.z	$⊢ \underset{˙}{0} = 0_{U}$
6		eqid	$⊢ DIsoH (K) (W) = DIsoH (K) (W)$
7	1 6 2 4	dih1rn	$⊢ (K \in HL \land W \in H) \to V \in ran DIsoH (K) (W)$
8		eqid	$⊢ oc (K) = oc (K)$
9	8 1 6 3	dochvalr	$⊢ ((K \in HL \land W \in H) \land V \in ran DIsoH (K) (W)) \to \underset{˙}{⊥} (V) = DIsoH (K) (W) (oc (K) ({DIsoH (K) (W)}^{-1} (V)))$
10	7 9	mpdan	$⊢ (K \in HL \land W \in H) \to \underset{˙}{⊥} (V) = DIsoH (K) (W) (oc (K) ({DIsoH (K) (W)}^{-1} (V)))$
11		eqid	$⊢ 1. (K) = 1. (K)$
12	1 11 6 2 4	dih1cnv	$⊢ (K \in HL \land W \in H) \to {DIsoH (K) (W)}^{-1} (V) = 1. (K)$
13	12	fveq2d	$⊢ (K \in HL \land W \in H) \to oc (K) ({DIsoH (K) (W)}^{-1} (V)) = oc (K) (1. (K))$
14		hlop	$⊢ K \in HL \to K \in OP$
15	14	adantr	$⊢ (K \in HL \land W \in H) \to K \in OP$
16		eqid	$⊢ 0. (K) = 0. (K)$
17	16 11 8	opoc1	$⊢ K \in OP \to oc (K) (1. (K)) = 0. (K)$
18	15 17	syl	$⊢ (K \in HL \land W \in H) \to oc (K) (1. (K)) = 0. (K)$
19	13 18	eqtrd	$⊢ (K \in HL \land W \in H) \to oc (K) ({DIsoH (K) (W)}^{-1} (V)) = 0. (K)$
20	19	fveq2d	$⊢ (K \in HL \land W \in H) \to DIsoH (K) (W) (oc (K) ({DIsoH (K) (W)}^{-1} (V))) = DIsoH (K) (W) (0. (K))$
21	16 1 6 2 5	dih0	$⊢ (K \in HL \land W \in H) \to DIsoH (K) (W) (0. (K)) = \{\underset{˙}{0}\}$
22	10 20 21	3eqtrd	$⊢ (K \in HL \land W \in H) \to \underset{˙}{⊥} (V) = \{\underset{˙}{0}\}$

Metamath Proof Explorer