dochvalr

Description: Orthocomplement of a closed subspace. (Contributed by NM, 14-Mar-2014)

	Ref	Expression
Hypotheses	dochvalr.o	$⊢ \underset{˙}{⊥} = oc (K)$
	dochvalr.h	$⊢ H = LHyp (K)$
	dochvalr.i	$⊢ I = DIsoH (K) (W)$
	dochvalr.n	$⊢ N = ocH (K) (W)$
Assertion	dochvalr	$⊢ ((K \in HL \land W \in H) \land X \in ran I) \to N (X) = I (\underset{˙}{⊥} (I^{-1} (X)))$

Proof

Step	Hyp	Ref	Expression
1		dochvalr.o	$⊢ \underset{˙}{⊥} = oc (K)$
2		dochvalr.h	$⊢ H = LHyp (K)$
3		dochvalr.i	$⊢ I = DIsoH (K) (W)$
4		dochvalr.n	$⊢ N = ocH (K) (W)$
5		eqid	$⊢ DVecH (K) (W) = DVecH (K) (W)$
6		eqid	$⊢ {Base}_{DVecH (K) (W)} = {Base}_{DVecH (K) (W)}$
7	2 5 3 6	dihrnss	$⊢ ((K \in HL \land W \in H) \land X \in ran I) \to X \subseteq {Base}_{DVecH (K) (W)}$
8		eqid	$⊢ {Base}_{K} = {Base}_{K}$
9		eqid	$⊢ glb (K) = glb (K)$
10	8 9 1 2 3 5 6 4	dochval	$⊢ ((K \in HL \land W \in H) \land X \subseteq {Base}_{DVecH (K) (W)}) \to N (X) = I (\underset{˙}{⊥} (glb (K) (\{y \in {Base}_{K} \| X \subseteq I (y)\})))$
11	7 10	syldan	$⊢ ((K \in HL \land W \in H) \land X \in ran I) \to N (X) = I (\underset{˙}{⊥} (glb (K) (\{y \in {Base}_{K} \| X \subseteq I (y)\})))$
12		eqid	$⊢ \leq_{K} = \leq_{K}$
13		hllat	$⊢ K \in HL \to K \in Lat$
14	13	ad2antrr	$⊢ ((K \in HL \land W \in H) \land X \in ran I) \to K \in Lat$
15		hlclat	$⊢ K \in HL \to K \in CLat$
16	15	ad2antrr	$⊢ ((K \in HL \land W \in H) \land X \in ran I) \to K \in CLat$
17		ssrab2	$⊢ \{y \in {Base}_{K} \| X \subseteq I (y)\} \subseteq {Base}_{K}$
18	8 9	clatglbcl	$⊢ (K \in CLat \land \{y \in {Base}_{K} \| X \subseteq I (y)\} \subseteq {Base}_{K}) \to glb (K) (\{y \in {Base}_{K} \| X \subseteq I (y)\}) \in {Base}_{K}$
19	16 17 18	sylancl	$⊢ ((K \in HL \land W \in H) \land X \in ran I) \to glb (K) (\{y \in {Base}_{K} \| X \subseteq I (y)\}) \in {Base}_{K}$
20	8 2 3	dihcnvcl	$⊢ ((K \in HL \land W \in H) \land X \in ran I) \to I^{-1} (X) \in {Base}_{K}$
21	17	a1i	$⊢ ((K \in HL \land W \in H) \land X \in ran I) \to \{y \in {Base}_{K} \| X \subseteq I (y)\} \subseteq {Base}_{K}$
22		ssid	$⊢ X \subseteq X$
23	2 3	dihcnvid2	$⊢ ((K \in HL \land W \in H) \land X \in ran I) \to I (I^{-1} (X)) = X$
24	22 23	sseqtrrid	$⊢ ((K \in HL \land W \in H) \land X \in ran I) \to X \subseteq I (I^{-1} (X))$
25		fveq2	$⊢ y = I^{-1} (X) \to I (y) = I (I^{-1} (X))$
26	25	sseq2d	$⊢ y = I^{-1} (X) \to (X \subseteq I (y) \leftrightarrow X \subseteq I (I^{-1} (X)))$
27	26	elrab	$⊢ I^{-1} (X) \in \{y \in {Base}_{K} \| X \subseteq I (y)\} \leftrightarrow (I^{-1} (X) \in {Base}_{K} \land X \subseteq I (I^{-1} (X)))$
28	20 24 27	sylanbrc	$⊢ ((K \in HL \land W \in H) \land X \in ran I) \to I^{-1} (X) \in \{y \in {Base}_{K} \| X \subseteq I (y)\}$
29	8 12 9	clatglble	$⊢ (K \in CLat \land \{y \in {Base}_{K} \| X \subseteq I (y)\} \subseteq {Base}_{K} \land I^{-1} (X) \in \{y \in {Base}_{K} \| X \subseteq I (y)\}) \to glb (K) (\{y \in {Base}_{K} \| X \subseteq I (y)\}) \leq_{K} I^{-1} (X)$
30	16 21 28 29	syl3anc	$⊢ ((K \in HL \land W \in H) \land X \in ran I) \to glb (K) (\{y \in {Base}_{K} \| X \subseteq I (y)\}) \leq_{K} I^{-1} (X)$
31		fveq2	$⊢ y = z \to I (y) = I (z)$
32	31	sseq2d	$⊢ y = z \to (X \subseteq I (y) \leftrightarrow X \subseteq I (z))$
33	32	elrab	$⊢ z \in \{y \in {Base}_{K} \| X \subseteq I (y)\} \leftrightarrow (z \in {Base}_{K} \land X \subseteq I (z))$
34	23	adantr	$⊢ (((K \in HL \land W \in H) \land X \in ran I) \land z \in {Base}_{K}) \to I (I^{-1} (X)) = X$
35	34	sseq1d	$⊢ (((K \in HL \land W \in H) \land X \in ran I) \land z \in {Base}_{K}) \to (I (I^{-1} (X)) \subseteq I (z) \leftrightarrow X \subseteq I (z))$
36		simpll	$⊢ (((K \in HL \land W \in H) \land X \in ran I) \land z \in {Base}_{K}) \to (K \in HL \land W \in H)$
37	20	adantr	$⊢ (((K \in HL \land W \in H) \land X \in ran I) \land z \in {Base}_{K}) \to I^{-1} (X) \in {Base}_{K}$
38		simpr	$⊢ (((K \in HL \land W \in H) \land X \in ran I) \land z \in {Base}_{K}) \to z \in {Base}_{K}$
39	8 12 2 3	dihord	$⊢ ((K \in HL \land W \in H) \land I^{-1} (X) \in {Base}_{K} \land z \in {Base}_{K}) \to (I (I^{-1} (X)) \subseteq I (z) \leftrightarrow I^{-1} (X) \leq_{K} z)$
40	36 37 38 39	syl3anc	$⊢ (((K \in HL \land W \in H) \land X \in ran I) \land z \in {Base}_{K}) \to (I (I^{-1} (X)) \subseteq I (z) \leftrightarrow I^{-1} (X) \leq_{K} z)$
41	35 40	bitr3d	$⊢ (((K \in HL \land W \in H) \land X \in ran I) \land z \in {Base}_{K}) \to (X \subseteq I (z) \leftrightarrow I^{-1} (X) \leq_{K} z)$
42	41	biimpd	$⊢ (((K \in HL \land W \in H) \land X \in ran I) \land z \in {Base}_{K}) \to (X \subseteq I (z) \to I^{-1} (X) \leq_{K} z)$
43	42	expimpd	$⊢ ((K \in HL \land W \in H) \land X \in ran I) \to ((z \in {Base}_{K} \land X \subseteq I (z)) \to I^{-1} (X) \leq_{K} z)$
44	33 43	biimtrid	$⊢ ((K \in HL \land W \in H) \land X \in ran I) \to (z \in \{y \in {Base}_{K} \| X \subseteq I (y)\} \to I^{-1} (X) \leq_{K} z)$
45	44	ralrimiv	$⊢ ((K \in HL \land W \in H) \land X \in ran I) \to \forall z \in \{y \in {Base}_{K} \| X \subseteq I (y)\} I^{-1} (X) \leq_{K} z$
46	8 12 9	clatleglb	$⊢ (K \in CLat \land I^{-1} (X) \in {Base}_{K} \land \{y \in {Base}_{K} \| X \subseteq I (y)\} \subseteq {Base}_{K}) \to (I^{-1} (X) \leq_{K} glb (K) (\{y \in {Base}_{K} \| X \subseteq I (y)\}) \leftrightarrow \forall z \in \{y \in {Base}_{K} \| X \subseteq I (y)\} I^{-1} (X) \leq_{K} z)$
47	16 20 21 46	syl3anc	$⊢ ((K \in HL \land W \in H) \land X \in ran I) \to (I^{-1} (X) \leq_{K} glb (K) (\{y \in {Base}_{K} \| X \subseteq I (y)\}) \leftrightarrow \forall z \in \{y \in {Base}_{K} \| X \subseteq I (y)\} I^{-1} (X) \leq_{K} z)$
48	45 47	mpbird	$⊢ ((K \in HL \land W \in H) \land X \in ran I) \to I^{-1} (X) \leq_{K} glb (K) (\{y \in {Base}_{K} \| X \subseteq I (y)\})$
49	8 12 14 19 20 30 48	latasymd	$⊢ ((K \in HL \land W \in H) \land X \in ran I) \to glb (K) (\{y \in {Base}_{K} \| X \subseteq I (y)\}) = I^{-1} (X)$
50	49	fveq2d	$⊢ ((K \in HL \land W \in H) \land X \in ran I) \to \underset{˙}{⊥} (glb (K) (\{y \in {Base}_{K} \| X \subseteq I (y)\})) = \underset{˙}{⊥} (I^{-1} (X))$
51	50	fveq2d	$⊢ ((K \in HL \land W \in H) \land X \in ran I) \to I (\underset{˙}{⊥} (glb (K) (\{y \in {Base}_{K} \| X \subseteq I (y)\}))) = I (\underset{˙}{⊥} (I^{-1} (X)))$
52	11 51	eqtrd	$⊢ ((K \in HL \land W \in H) \land X \in ran I) \to N (X) = I (\underset{˙}{⊥} (I^{-1} (X)))$

Metamath Proof Explorer

Theorem dochvalr

Proof