ocvpj

Description: The orthocomplement of a projection subspace is a projection subspace. (Contributed by Mario Carneiro, 16-Oct-2015)

	Ref	Expression
Hypotheses	ocvpj.k	$⊢ K = proj (W)$
	ocvpj.o	$⊢ \underset{˙}{⊥} = ocv (W)$
Assertion	ocvpj	$⊢ (W \in PreHil \land T \in dom K) \to \underset{˙}{⊥} (T) \in dom K$

Proof

Step	Hyp	Ref	Expression
1		ocvpj.k	$⊢ K = proj (W)$
2		ocvpj.o	$⊢ \underset{˙}{⊥} = ocv (W)$
3		eqid	$⊢ ClSubSp (W) = ClSubSp (W)$
4	1 3	pjcss	$⊢ W \in PreHil \to dom K \subseteq ClSubSp (W)$
5	4	sselda	$⊢ (W \in PreHil \land T \in dom K) \to T \in ClSubSp (W)$
6		eqid	$⊢ {Base}_{W} = {Base}_{W}$
7	6 3	cssss	$⊢ T \in ClSubSp (W) \to T \subseteq {Base}_{W}$
8	5 7	syl	$⊢ (W \in PreHil \land T \in dom K) \to T \subseteq {Base}_{W}$
9		eqid	$⊢ LSubSp (W) = LSubSp (W)$
10	6 2 9	ocvlss	$⊢ (W \in PreHil \land T \subseteq {Base}_{W}) \to \underset{˙}{⊥} (T) \in LSubSp (W)$
11	8 10	syldan	$⊢ (W \in PreHil \land T \in dom K) \to \underset{˙}{⊥} (T) \in LSubSp (W)$
12		phllmod	$⊢ W \in PreHil \to W \in LMod$
13	12	adantr	$⊢ (W \in PreHil \land T \in dom K) \to W \in LMod$
14		lmodabl	$⊢ W \in LMod \to W \in Abel$
15	13 14	syl	$⊢ (W \in PreHil \land T \in dom K) \to W \in Abel$
16	9	lsssssubg	$⊢ W \in LMod \to LSubSp (W) \subseteq SubGrp (W)$
17	13 16	syl	$⊢ (W \in PreHil \land T \in dom K) \to LSubSp (W) \subseteq SubGrp (W)$
18	17 11	sseldd	$⊢ (W \in PreHil \land T \in dom K) \to \underset{˙}{⊥} (T) \in SubGrp (W)$
19	3 9	csslss	$⊢ (W \in PreHil \land T \in ClSubSp (W)) \to T \in LSubSp (W)$
20	5 19	syldan	$⊢ (W \in PreHil \land T \in dom K) \to T \in LSubSp (W)$
21	17 20	sseldd	$⊢ (W \in PreHil \land T \in dom K) \to T \in SubGrp (W)$
22		eqid	$⊢ LSSum (W) = LSSum (W)$
23	22	lsmcom	$⊢ (W \in Abel \land \underset{˙}{⊥} (T) \in SubGrp (W) \land T \in SubGrp (W)) \to \underset{˙}{⊥} (T) LSSum (W) T = T LSSum (W) \underset{˙}{⊥} (T)$
24	15 18 21 23	syl3anc	$⊢ (W \in PreHil \land T \in dom K) \to \underset{˙}{⊥} (T) LSSum (W) T = T LSSum (W) \underset{˙}{⊥} (T)$
25	2 3	cssi	$⊢ T \in ClSubSp (W) \to T = \underset{˙}{⊥} (\underset{˙}{⊥} (T))$
26	5 25	syl	$⊢ (W \in PreHil \land T \in dom K) \to T = \underset{˙}{⊥} (\underset{˙}{⊥} (T))$
27	26	oveq2d	$⊢ (W \in PreHil \land T \in dom K) \to \underset{˙}{⊥} (T) LSSum (W) T = \underset{˙}{⊥} (T) LSSum (W) \underset{˙}{⊥} (\underset{˙}{⊥} (T))$
28	6 9 2 22 1	pjdm2	$⊢ W \in PreHil \to (T \in dom K \leftrightarrow (T \in LSubSp (W) \land T LSSum (W) \underset{˙}{⊥} (T) = {Base}_{W}))$
29	28	simplbda	$⊢ (W \in PreHil \land T \in dom K) \to T LSSum (W) \underset{˙}{⊥} (T) = {Base}_{W}$
30	24 27 29	3eqtr3d	$⊢ (W \in PreHil \land T \in dom K) \to \underset{˙}{⊥} (T) LSSum (W) \underset{˙}{⊥} (\underset{˙}{⊥} (T)) = {Base}_{W}$
31	6 9 2 22 1	pjdm2	$⊢ W \in PreHil \to (\underset{˙}{⊥} (T) \in dom K \leftrightarrow (\underset{˙}{⊥} (T) \in LSubSp (W) \land \underset{˙}{⊥} (T) LSSum (W) \underset{˙}{⊥} (\underset{˙}{⊥} (T)) = {Base}_{W}))$
32	31	adantr	$⊢ (W \in PreHil \land T \in dom K) \to (\underset{˙}{⊥} (T) \in dom K \leftrightarrow (\underset{˙}{⊥} (T) \in LSubSp (W) \land \underset{˙}{⊥} (T) LSSum (W) \underset{˙}{⊥} (\underset{˙}{⊥} (T)) = {Base}_{W}))$
33	11 30 32	mpbir2and	$⊢ (W \in PreHil \land T \in dom K) \to \underset{˙}{⊥} (T) \in dom K$

Metamath Proof Explorer

Theorem ocvpj

Proof