dicffval

Description: The partial isomorphism C for a lattice K . (Contributed by NM, 15-Dec-2013)

	Ref	Expression
Hypotheses	dicval.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	dicval.a	$⊢ A = Atoms (K)$
	dicval.h	$⊢ H = LHyp (K)$
Assertion	dicffval	$⊢ K \in V \to DIsoC (K) = (w \in H ⟼ (q \in \{r \in A \| \neg r \underset{˙}{\leq} w\} ⟼ \{⟨f, s⟩ \| (f = s ((ι g \in LTrn (K) (w) \| g (oc (K) (w)) = q)) \land s \in TEndo (K) (w))\}))$

Proof

Step	Hyp	Ref	Expression
1		dicval.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		dicval.a	$⊢ A = Atoms (K)$
3		dicval.h	$⊢ H = LHyp (K)$
4		elex	$⊢ K \in V \to K \in V$
5		fveq2	$⊢ k = K \to LHyp (k) = LHyp (K)$
6	5 3	eqtr4di	$⊢ k = K \to LHyp (k) = H$
7		fveq2	$⊢ k = K \to Atoms (k) = Atoms (K)$
8	7 2	eqtr4di	$⊢ k = K \to Atoms (k) = A$
9		fveq2	$⊢ k = K \to \leq_{k} = \leq_{K}$
10	9 1	eqtr4di	$⊢ k = K \to \leq_{k} = \underset{˙}{\leq}$
11	10	breqd	$⊢ k = K \to (r \leq_{k} w \leftrightarrow r \underset{˙}{\leq} w)$
12	11	notbid	$⊢ k = K \to (\neg r \leq_{k} w \leftrightarrow \neg r \underset{˙}{\leq} w)$
13	8 12	rabeqbidv	$⊢ k = K \to \{r \in Atoms (k) \| \neg r \leq_{k} w\} = \{r \in A \| \neg r \underset{˙}{\leq} w\}$
14		fveq2	$⊢ k = K \to LTrn (k) = LTrn (K)$
15	14	fveq1d	$⊢ k = K \to LTrn (k) (w) = LTrn (K) (w)$
16		fveq2	$⊢ k = K \to oc (k) = oc (K)$
17	16	fveq1d	$⊢ k = K \to oc (k) (w) = oc (K) (w)$
18	17	fveqeq2d	$⊢ k = K \to (g (oc (k) (w)) = q \leftrightarrow g (oc (K) (w)) = q)$
19	15 18	riotaeqbidv	$⊢ k = K \to (ι g \in LTrn (k) (w) \| g (oc (k) (w)) = q) = (ι g \in LTrn (K) (w) \| g (oc (K) (w)) = q)$
20	19	fveq2d	$⊢ k = K \to s ((ι g \in LTrn (k) (w) \| g (oc (k) (w)) = q)) = s ((ι g \in LTrn (K) (w) \| g (oc (K) (w)) = q))$
21	20	eqeq2d	$⊢ k = K \to (f = s ((ι g \in LTrn (k) (w) \| g (oc (k) (w)) = q)) \leftrightarrow f = s ((ι g \in LTrn (K) (w) \| g (oc (K) (w)) = q)))$
22		fveq2	$⊢ k = K \to TEndo (k) = TEndo (K)$
23	22	fveq1d	$⊢ k = K \to TEndo (k) (w) = TEndo (K) (w)$
24	23	eleq2d	$⊢ k = K \to (s \in TEndo (k) (w) \leftrightarrow s \in TEndo (K) (w))$
25	21 24	anbi12d	$⊢ k = K \to ((f = s ((ι g \in LTrn (k) (w) \| g (oc (k) (w)) = q)) \land s \in TEndo (k) (w)) \leftrightarrow (f = s ((ι g \in LTrn (K) (w) \| g (oc (K) (w)) = q)) \land s \in TEndo (K) (w)))$
26	25	opabbidv	$⊢ k = K \to \{⟨f, s⟩ \| (f = s ((ι g \in LTrn (k) (w) \| g (oc (k) (w)) = q)) \land s \in TEndo (k) (w))\} = \{⟨f, s⟩ \| (f = s ((ι g \in LTrn (K) (w) \| g (oc (K) (w)) = q)) \land s \in TEndo (K) (w))\}$
27	13 26	mpteq12dv	$⊢ k = K \to (q \in \{r \in Atoms (k) \| \neg r \leq_{k} w\} ⟼ \{⟨f, s⟩ \| (f = s ((ι g \in LTrn (k) (w) \| g (oc (k) (w)) = q)) \land s \in TEndo (k) (w))\}) = (q \in \{r \in A \| \neg r \underset{˙}{\leq} w\} ⟼ \{⟨f, s⟩ \| (f = s ((ι g \in LTrn (K) (w) \| g (oc (K) (w)) = q)) \land s \in TEndo (K) (w))\})$
28	6 27	mpteq12dv	$⊢ k = K \to (w \in LHyp (k) ⟼ (q \in \{r \in Atoms (k) \| \neg r \leq_{k} w\} ⟼ \{⟨f, s⟩ \| (f = s ((ι g \in LTrn (k) (w) \| g (oc (k) (w)) = q)) \land s \in TEndo (k) (w))\})) = (w \in H ⟼ (q \in \{r \in A \| \neg r \underset{˙}{\leq} w\} ⟼ \{⟨f, s⟩ \| (f = s ((ι g \in LTrn (K) (w) \| g (oc (K) (w)) = q)) \land s \in TEndo (K) (w))\}))$
29		df-dic	$⊢ DIsoC = (k \in V ⟼ (w \in LHyp (k) ⟼ (q \in \{r \in Atoms (k) \| \neg r \leq_{k} w\} ⟼ \{⟨f, s⟩ \| (f = s ((ι g \in LTrn (k) (w) \| g (oc (k) (w)) = q)) \land s \in TEndo (k) (w))\})))$
30	28 29 3	mptfvmpt	$⊢ K \in V \to DIsoC (K) = (w \in H ⟼ (q \in \{r \in A \| \neg r \underset{˙}{\leq} w\} ⟼ \{⟨f, s⟩ \| (f = s ((ι g \in LTrn (K) (w) \| g (oc (K) (w)) = q)) \land s \in TEndo (K) (w))\}))$
31	4 30	syl	$⊢ K \in V \to DIsoC (K) = (w \in H ⟼ (q \in \{r \in A \| \neg r \underset{˙}{\leq} w\} ⟼ \{⟨f, s⟩ \| (f = s ((ι g \in LTrn (K) (w) \| g (oc (K) (w)) = q)) \land s \in TEndo (K) (w))\}))$

Metamath Proof Explorer

Theorem dicffval

Proof