docaffvalN

Description: Subspace orthocomplement for DVecA partial vector space. (Contributed by NM, 6-Dec-2013) (New usage is discouraged.)

	Ref	Expression
Hypotheses	docaval.j	$⊢ \underset{˙}{\lor} = join (K)$
	docaval.m	$⊢ \underset{˙}{\land} = meet (K)$
	docaval.o	$⊢ \underset{˙}{⊥} = oc (K)$
	docaval.h	$⊢ H = LHyp (K)$
Assertion	docaffvalN	$⊢ K \in V \to ocA (K) = (w \in H ⟼ (x \in 𝒫 LTrn (K) (w) ⟼ DIsoA (K) (w) ((\underset{˙}{⊥} ({DIsoA (K) (w)}^{-1} (⋂ \{z \in ran DIsoA (K) (w) \| x \subseteq z\})) \underset{˙}{\lor} \underset{˙}{⊥} (w)) \underset{˙}{\land} w)))$

Proof

Step	Hyp	Ref	Expression
1		docaval.j	$⊢ \underset{˙}{\lor} = join (K)$
2		docaval.m	$⊢ \underset{˙}{\land} = meet (K)$
3		docaval.o	$⊢ \underset{˙}{⊥} = oc (K)$
4		docaval.h	$⊢ H = LHyp (K)$
5		elex	$⊢ K \in V \to K \in V$
6		fveq2	$⊢ k = K \to LHyp (k) = LHyp (K)$
7	6 4	eqtr4di	$⊢ k = K \to LHyp (k) = H$
8		fveq2	$⊢ k = K \to LTrn (k) = LTrn (K)$
9	8	fveq1d	$⊢ k = K \to LTrn (k) (w) = LTrn (K) (w)$
10	9	pweqd	$⊢ k = K \to 𝒫 LTrn (k) (w) = 𝒫 LTrn (K) (w)$
11		fveq2	$⊢ k = K \to DIsoA (k) = DIsoA (K)$
12	11	fveq1d	$⊢ k = K \to DIsoA (k) (w) = DIsoA (K) (w)$
13		fveq2	$⊢ k = K \to meet (k) = meet (K)$
14	13 2	eqtr4di	$⊢ k = K \to meet (k) = \underset{˙}{\land}$
15		fveq2	$⊢ k = K \to join (k) = join (K)$
16	15 1	eqtr4di	$⊢ k = K \to join (k) = \underset{˙}{\lor}$
17		fveq2	$⊢ k = K \to oc (k) = oc (K)$
18	17 3	eqtr4di	$⊢ k = K \to oc (k) = \underset{˙}{⊥}$
19	12	cnveqd	$⊢ k = K \to {DIsoA (k) (w)}^{-1} = {DIsoA (K) (w)}^{-1}$
20	12	rneqd	$⊢ k = K \to ran DIsoA (k) (w) = ran DIsoA (K) (w)$
21	20	rabeqdv	$⊢ k = K \to \{z \in ran DIsoA (k) (w) \| x \subseteq z\} = \{z \in ran DIsoA (K) (w) \| x \subseteq z\}$
22	21	inteqd	$⊢ k = K \to ⋂ \{z \in ran DIsoA (k) (w) \| x \subseteq z\} = ⋂ \{z \in ran DIsoA (K) (w) \| x \subseteq z\}$
23	19 22	fveq12d	$⊢ k = K \to {DIsoA (k) (w)}^{-1} (⋂ \{z \in ran DIsoA (k) (w) \| x \subseteq z\}) = {DIsoA (K) (w)}^{-1} (⋂ \{z \in ran DIsoA (K) (w) \| x \subseteq z\})$
24	18 23	fveq12d	$⊢ k = K \to oc (k) ({DIsoA (k) (w)}^{-1} (⋂ \{z \in ran DIsoA (k) (w) \| x \subseteq z\})) = \underset{˙}{⊥} ({DIsoA (K) (w)}^{-1} (⋂ \{z \in ran DIsoA (K) (w) \| x \subseteq z\}))$
25	18	fveq1d	$⊢ k = K \to oc (k) (w) = \underset{˙}{⊥} (w)$
26	16 24 25	oveq123d	$⊢ k = K \to oc (k) ({DIsoA (k) (w)}^{-1} (⋂ \{z \in ran DIsoA (k) (w) \| x \subseteq z\})) join (k) oc (k) (w) = \underset{˙}{⊥} ({DIsoA (K) (w)}^{-1} (⋂ \{z \in ran DIsoA (K) (w) \| x \subseteq z\})) \underset{˙}{\lor} \underset{˙}{⊥} (w)$
27		eqidd	$⊢ k = K \to w = w$
28	14 26 27	oveq123d	$⊢ k = K \to (oc (k) ({DIsoA (k) (w)}^{-1} (⋂ \{z \in ran DIsoA (k) (w) \| x \subseteq z\})) join (k) oc (k) (w)) meet (k) w = (\underset{˙}{⊥} ({DIsoA (K) (w)}^{-1} (⋂ \{z \in ran DIsoA (K) (w) \| x \subseteq z\})) \underset{˙}{\lor} \underset{˙}{⊥} (w)) \underset{˙}{\land} w$
29	12 28	fveq12d	$⊢ k = K \to DIsoA (k) (w) ((oc (k) ({DIsoA (k) (w)}^{-1} (⋂ \{z \in ran DIsoA (k) (w) \| x \subseteq z\})) join (k) oc (k) (w)) meet (k) w) = DIsoA (K) (w) ((\underset{˙}{⊥} ({DIsoA (K) (w)}^{-1} (⋂ \{z \in ran DIsoA (K) (w) \| x \subseteq z\})) \underset{˙}{\lor} \underset{˙}{⊥} (w)) \underset{˙}{\land} w)$
30	10 29	mpteq12dv	$⊢ k = K \to (x \in 𝒫 LTrn (k) (w) ⟼ DIsoA (k) (w) ((oc (k) ({DIsoA (k) (w)}^{-1} (⋂ \{z \in ran DIsoA (k) (w) \| x \subseteq z\})) join (k) oc (k) (w)) meet (k) w)) = (x \in 𝒫 LTrn (K) (w) ⟼ DIsoA (K) (w) ((\underset{˙}{⊥} ({DIsoA (K) (w)}^{-1} (⋂ \{z \in ran DIsoA (K) (w) \| x \subseteq z\})) \underset{˙}{\lor} \underset{˙}{⊥} (w)) \underset{˙}{\land} w))$
31	7 30	mpteq12dv	$⊢ k = K \to (w \in LHyp (k) ⟼ (x \in 𝒫 LTrn (k) (w) ⟼ DIsoA (k) (w) ((oc (k) ({DIsoA (k) (w)}^{-1} (⋂ \{z \in ran DIsoA (k) (w) \| x \subseteq z\})) join (k) oc (k) (w)) meet (k) w))) = (w \in H ⟼ (x \in 𝒫 LTrn (K) (w) ⟼ DIsoA (K) (w) ((\underset{˙}{⊥} ({DIsoA (K) (w)}^{-1} (⋂ \{z \in ran DIsoA (K) (w) \| x \subseteq z\})) \underset{˙}{\lor} \underset{˙}{⊥} (w)) \underset{˙}{\land} w)))$
32		df-docaN	$⊢ ocA = (k \in V ⟼ (w \in LHyp (k) ⟼ (x \in 𝒫 LTrn (k) (w) ⟼ DIsoA (k) (w) ((oc (k) ({DIsoA (k) (w)}^{-1} (⋂ \{z \in ran DIsoA (k) (w) \| x \subseteq z\})) join (k) oc (k) (w)) meet (k) w))))$
33	31 32 4	mptfvmpt	$⊢ K \in V \to ocA (K) = (w \in H ⟼ (x \in 𝒫 LTrn (K) (w) ⟼ DIsoA (K) (w) ((\underset{˙}{⊥} ({DIsoA (K) (w)}^{-1} (⋂ \{z \in ran DIsoA (K) (w) \| x \subseteq z\})) \underset{˙}{\lor} \underset{˙}{⊥} (w)) \underset{˙}{\land} w)))$
34	5 33	syl	$⊢ K \in V \to ocA (K) = (w \in H ⟼ (x \in 𝒫 LTrn (K) (w) ⟼ DIsoA (K) (w) ((\underset{˙}{⊥} ({DIsoA (K) (w)}^{-1} (⋂ \{z \in ran DIsoA (K) (w) \| x \subseteq z\})) \underset{˙}{\lor} \underset{˙}{⊥} (w)) \underset{˙}{\land} w)))$

Metamath Proof Explorer

Theorem docaffvalN

Proof