doch2val2

Description: Double orthocomplement for DVecH vector space. (Contributed by NM, 26-Jul-2014)

	Ref	Expression
Hypotheses	doch2val2.h	$⊢ H = LHyp (K)$
	doch2val2.i	$⊢ I = DIsoH (K) (W)$
	doch2val2.u	$⊢ U = DVecH (K) (W)$
	doch2val2.v	$⊢ V = {Base}_{U}$
	doch2val2.o	$⊢ \underset{˙}{⊥} = ocH (K) (W)$
	doch2val2.k	$⊢ φ \to (K \in HL \land W \in H)$
	doch2val2.x	$⊢ φ \to X \subseteq V$
Assertion	doch2val2	$⊢ φ \to \underset{˙}{⊥} (\underset{˙}{⊥} (X)) = ⋂ \{z \in ran I \| X \subseteq z\}$

Proof

Step	Hyp	Ref	Expression
1		doch2val2.h	$⊢ H = LHyp (K)$
2		doch2val2.i	$⊢ I = DIsoH (K) (W)$
3		doch2val2.u	$⊢ U = DVecH (K) (W)$
4		doch2val2.v	$⊢ V = {Base}_{U}$
5		doch2val2.o	$⊢ \underset{˙}{⊥} = ocH (K) (W)$
6		doch2val2.k	$⊢ φ \to (K \in HL \land W \in H)$
7		doch2val2.x	$⊢ φ \to X \subseteq V$
8		eqid	$⊢ oc (K) = oc (K)$
9	8 1 2 3 4 5	dochval2	$⊢ ((K \in HL \land W \in H) \land X \subseteq V) \to \underset{˙}{⊥} (X) = I (oc (K) (I^{-1} (⋂ \{z \in ran I \| X \subseteq z\})))$
10	6 7 9	syl2anc	$⊢ φ \to \underset{˙}{⊥} (X) = I (oc (K) (I^{-1} (⋂ \{z \in ran I \| X \subseteq z\})))$
11	10	fveq2d	$⊢ φ \to \underset{˙}{⊥} (\underset{˙}{⊥} (X)) = \underset{˙}{⊥} (I (oc (K) (I^{-1} (⋂ \{z \in ran I \| X \subseteq z\}))))$
12	6	simpld	$⊢ φ \to K \in HL$
13		hlop	$⊢ K \in HL \to K \in OP$
14	12 13	syl	$⊢ φ \to K \in OP$
15		ssrab2	$⊢ \{z \in ran I \| X \subseteq z\} \subseteq ran I$
16	15	a1i	$⊢ φ \to \{z \in ran I \| X \subseteq z\} \subseteq ran I$
17	1 2 3 4	dih1rn	$⊢ (K \in HL \land W \in H) \to V \in ran I$
18	6 17	syl	$⊢ φ \to V \in ran I$
19		sseq2	$⊢ z = V \to (X \subseteq z \leftrightarrow X \subseteq V)$
20	19	elrab	$⊢ V \in \{z \in ran I \| X \subseteq z\} \leftrightarrow (V \in ran I \land X \subseteq V)$
21	18 7 20	sylanbrc	$⊢ φ \to V \in \{z \in ran I \| X \subseteq z\}$
22	21	ne0d	$⊢ φ \to \{z \in ran I \| X \subseteq z\} \neq \emptyset$
23	1 2	dihintcl	$⊢ ((K \in HL \land W \in H) \land (\{z \in ran I \| X \subseteq z\} \subseteq ran I \land \{z \in ran I \| X \subseteq z\} \neq \emptyset)) \to ⋂ \{z \in ran I \| X \subseteq z\} \in ran I$
24	6 16 22 23	syl12anc	$⊢ φ \to ⋂ \{z \in ran I \| X \subseteq z\} \in ran I$
25		eqid	$⊢ {Base}_{K} = {Base}_{K}$
26	25 1 2	dihcnvcl	$⊢ ((K \in HL \land W \in H) \land ⋂ \{z \in ran I \| X \subseteq z\} \in ran I) \to I^{-1} (⋂ \{z \in ran I \| X \subseteq z\}) \in {Base}_{K}$
27	6 24 26	syl2anc	$⊢ φ \to I^{-1} (⋂ \{z \in ran I \| X \subseteq z\}) \in {Base}_{K}$
28	25 8	opoccl	$⊢ (K \in OP \land I^{-1} (⋂ \{z \in ran I \| X \subseteq z\}) \in {Base}_{K}) \to oc (K) (I^{-1} (⋂ \{z \in ran I \| X \subseteq z\})) \in {Base}_{K}$
29	14 27 28	syl2anc	$⊢ φ \to oc (K) (I^{-1} (⋂ \{z \in ran I \| X \subseteq z\})) \in {Base}_{K}$
30	25 8 1 2 5	dochvalr2	$⊢ ((K \in HL \land W \in H) \land oc (K) (I^{-1} (⋂ \{z \in ran I \| X \subseteq z\})) \in {Base}_{K}) \to \underset{˙}{⊥} (I (oc (K) (I^{-1} (⋂ \{z \in ran I \| X \subseteq z\})))) = I (oc (K) (oc (K) (I^{-1} (⋂ \{z \in ran I \| X \subseteq z\}))))$
31	6 29 30	syl2anc	$⊢ φ \to \underset{˙}{⊥} (I (oc (K) (I^{-1} (⋂ \{z \in ran I \| X \subseteq z\})))) = I (oc (K) (oc (K) (I^{-1} (⋂ \{z \in ran I \| X \subseteq z\}))))$
32	25 8	opococ	$⊢ (K \in OP \land I^{-1} (⋂ \{z \in ran I \| X \subseteq z\}) \in {Base}_{K}) \to oc (K) (oc (K) (I^{-1} (⋂ \{z \in ran I \| X \subseteq z\}))) = I^{-1} (⋂ \{z \in ran I \| X \subseteq z\})$
33	14 27 32	syl2anc	$⊢ φ \to oc (K) (oc (K) (I^{-1} (⋂ \{z \in ran I \| X \subseteq z\}))) = I^{-1} (⋂ \{z \in ran I \| X \subseteq z\})$
34	33	fveq2d	$⊢ φ \to I (oc (K) (oc (K) (I^{-1} (⋂ \{z \in ran I \| X \subseteq z\})))) = I (I^{-1} (⋂ \{z \in ran I \| X \subseteq z\}))$
35	1 2	dihcnvid2	$⊢ ((K \in HL \land W \in H) \land ⋂ \{z \in ran I \| X \subseteq z\} \in ran I) \to I (I^{-1} (⋂ \{z \in ran I \| X \subseteq z\})) = ⋂ \{z \in ran I \| X \subseteq z\}$
36	6 24 35	syl2anc	$⊢ φ \to I (I^{-1} (⋂ \{z \in ran I \| X \subseteq z\})) = ⋂ \{z \in ran I \| X \subseteq z\}$
37	34 36	eqtrd	$⊢ φ \to I (oc (K) (oc (K) (I^{-1} (⋂ \{z \in ran I \| X \subseteq z\})))) = ⋂ \{z \in ran I \| X \subseteq z\}$
38	11 31 37	3eqtrd	$⊢ φ \to \underset{˙}{⊥} (\underset{˙}{⊥} (X)) = ⋂ \{z \in ran I \| X \subseteq z\}$

Metamath Proof Explorer

Theorem doch2val2

Proof