hdmap1cbv

Description: Frequently used lemma to change bound variables in L hypothesis. (Contributed by NM, 15-May-2015)

		Ref	Expression
	Hypothesis	hdmap1cbv.l	$⊢ L = (x \in V ⟼ if (2^{nd} (x) = \underset{˙}{0}, Q, (ι h \in D \| (M (N (\{2^{nd} (x)\})) = J (\{h\}) \land M (N (\{1^{st} (1^{st} (x)) \underset{˙}{-} 2^{nd} (x)\})) = J (\{2^{nd} (1^{st} (x)) R h\})))))$
	Assertion	hdmap1cbv	$⊢ L = (y \in V ⟼ if (2^{nd} (y) = \underset{˙}{0}, Q, (ι i \in D \| (M (N (\{2^{nd} (y)\})) = J (\{i\}) \land M (N (\{1^{st} (1^{st} (y)) \underset{˙}{-} 2^{nd} (y)\})) = J (\{2^{nd} (1^{st} (y)) R i\})))))$

Proof

Step	Hyp	Ref	Expression
1		hdmap1cbv.l	$⊢ L = (x \in V ⟼ if (2^{nd} (x) = \underset{˙}{0}, Q, (ι h \in D \| (M (N (\{2^{nd} (x)\})) = J (\{h\}) \land M (N (\{1^{st} (1^{st} (x)) \underset{˙}{-} 2^{nd} (x)\})) = J (\{2^{nd} (1^{st} (x)) R h\})))))$
2		fveq2	$⊢ x = y \to 2^{nd} (x) = 2^{nd} (y)$
3	2	eqeq1d	$⊢ x = y \to (2^{nd} (x) = \underset{˙}{0} \leftrightarrow 2^{nd} (y) = \underset{˙}{0})$
4	2	sneqd	$⊢ x = y \to \{2^{nd} (x)\} = \{2^{nd} (y)\}$
5	4	fveq2d	$⊢ x = y \to N (\{2^{nd} (x)\}) = N (\{2^{nd} (y)\})$
6	5	fveq2d	$⊢ x = y \to M (N (\{2^{nd} (x)\})) = M (N (\{2^{nd} (y)\}))$
7	6	eqeq1d	$⊢ x = y \to (M (N (\{2^{nd} (x)\})) = J (\{h\}) \leftrightarrow M (N (\{2^{nd} (y)\})) = J (\{h\}))$
8		2fveq3	$⊢ x = y \to 1^{st} (1^{st} (x)) = 1^{st} (1^{st} (y))$
9	8 2	oveq12d	$⊢ x = y \to 1^{st} (1^{st} (x)) \underset{˙}{-} 2^{nd} (x) = 1^{st} (1^{st} (y)) \underset{˙}{-} 2^{nd} (y)$
10	9	sneqd	$⊢ x = y \to \{1^{st} (1^{st} (x)) \underset{˙}{-} 2^{nd} (x)\} = \{1^{st} (1^{st} (y)) \underset{˙}{-} 2^{nd} (y)\}$
11	10	fveq2d	$⊢ x = y \to N (\{1^{st} (1^{st} (x)) \underset{˙}{-} 2^{nd} (x)\}) = N (\{1^{st} (1^{st} (y)) \underset{˙}{-} 2^{nd} (y)\})$
12	11	fveq2d	$⊢ x = y \to M (N (\{1^{st} (1^{st} (x)) \underset{˙}{-} 2^{nd} (x)\})) = M (N (\{1^{st} (1^{st} (y)) \underset{˙}{-} 2^{nd} (y)\}))$
13		2fveq3	$⊢ x = y \to 2^{nd} (1^{st} (x)) = 2^{nd} (1^{st} (y))$
14	13	oveq1d	$⊢ x = y \to 2^{nd} (1^{st} (x)) R h = 2^{nd} (1^{st} (y)) R h$
15	14	sneqd	$⊢ x = y \to \{2^{nd} (1^{st} (x)) R h\} = \{2^{nd} (1^{st} (y)) R h\}$
16	15	fveq2d	$⊢ x = y \to J (\{2^{nd} (1^{st} (x)) R h\}) = J (\{2^{nd} (1^{st} (y)) R h\})$
17	12 16	eqeq12d	$⊢ x = y \to (M (N (\{1^{st} (1^{st} (x)) \underset{˙}{-} 2^{nd} (x)\})) = J (\{2^{nd} (1^{st} (x)) R h\}) \leftrightarrow M (N (\{1^{st} (1^{st} (y)) \underset{˙}{-} 2^{nd} (y)\})) = J (\{2^{nd} (1^{st} (y)) R h\}))$
18	7 17	anbi12d	$⊢ x = y \to ((M (N (\{2^{nd} (x)\})) = J (\{h\}) \land M (N (\{1^{st} (1^{st} (x)) \underset{˙}{-} 2^{nd} (x)\})) = J (\{2^{nd} (1^{st} (x)) R h\})) \leftrightarrow (M (N (\{2^{nd} (y)\})) = J (\{h\}) \land M (N (\{1^{st} (1^{st} (y)) \underset{˙}{-} 2^{nd} (y)\})) = J (\{2^{nd} (1^{st} (y)) R h\})))$
19	18	riotabidv	$⊢ x = y \to (ι h \in D \| (M (N (\{2^{nd} (x)\})) = J (\{h\}) \land M (N (\{1^{st} (1^{st} (x)) \underset{˙}{-} 2^{nd} (x)\})) = J (\{2^{nd} (1^{st} (x)) R h\}))) = (ι h \in D \| (M (N (\{2^{nd} (y)\})) = J (\{h\}) \land M (N (\{1^{st} (1^{st} (y)) \underset{˙}{-} 2^{nd} (y)\})) = J (\{2^{nd} (1^{st} (y)) R h\})))$
20	3 19	ifbieq2d	$⊢ x = y \to if (2^{nd} (x) = \underset{˙}{0}, Q, (ι h \in D \| (M (N (\{2^{nd} (x)\})) = J (\{h\}) \land M (N (\{1^{st} (1^{st} (x)) \underset{˙}{-} 2^{nd} (x)\})) = J (\{2^{nd} (1^{st} (x)) R h\})))) = if (2^{nd} (y) = \underset{˙}{0}, Q, (ι h \in D \| (M (N (\{2^{nd} (y)\})) = J (\{h\}) \land M (N (\{1^{st} (1^{st} (y)) \underset{˙}{-} 2^{nd} (y)\})) = J (\{2^{nd} (1^{st} (y)) R h\}))))$
21	20	cbvmptv	$⊢ (x \in V ⟼ if (2^{nd} (x) = \underset{˙}{0}, Q, (ι h \in D \| (M (N (\{2^{nd} (x)\})) = J (\{h\}) \land M (N (\{1^{st} (1^{st} (x)) \underset{˙}{-} 2^{nd} (x)\})) = J (\{2^{nd} (1^{st} (x)) R h\}))))) = (y \in V ⟼ if (2^{nd} (y) = \underset{˙}{0}, Q, (ι h \in D \| (M (N (\{2^{nd} (y)\})) = J (\{h\}) \land M (N (\{1^{st} (1^{st} (y)) \underset{˙}{-} 2^{nd} (y)\})) = J (\{2^{nd} (1^{st} (y)) R h\})))))$
22		sneq	$⊢ h = i \to \{h\} = \{i\}$
23	22	fveq2d	$⊢ h = i \to J (\{h\}) = J (\{i\})$
24	23	eqeq2d	$⊢ h = i \to (M (N (\{2^{nd} (y)\})) = J (\{h\}) \leftrightarrow M (N (\{2^{nd} (y)\})) = J (\{i\}))$
25		oveq2	$⊢ h = i \to 2^{nd} (1^{st} (y)) R h = 2^{nd} (1^{st} (y)) R i$
26	25	sneqd	$⊢ h = i \to \{2^{nd} (1^{st} (y)) R h\} = \{2^{nd} (1^{st} (y)) R i\}$
27	26	fveq2d	$⊢ h = i \to J (\{2^{nd} (1^{st} (y)) R h\}) = J (\{2^{nd} (1^{st} (y)) R i\})$
28	27	eqeq2d	$⊢ h = i \to (M (N (\{1^{st} (1^{st} (y)) \underset{˙}{-} 2^{nd} (y)\})) = J (\{2^{nd} (1^{st} (y)) R h\}) \leftrightarrow M (N (\{1^{st} (1^{st} (y)) \underset{˙}{-} 2^{nd} (y)\})) = J (\{2^{nd} (1^{st} (y)) R i\}))$
29	24 28	anbi12d	$⊢ h = i \to ((M (N (\{2^{nd} (y)\})) = J (\{h\}) \land M (N (\{1^{st} (1^{st} (y)) \underset{˙}{-} 2^{nd} (y)\})) = J (\{2^{nd} (1^{st} (y)) R h\})) \leftrightarrow (M (N (\{2^{nd} (y)\})) = J (\{i\}) \land M (N (\{1^{st} (1^{st} (y)) \underset{˙}{-} 2^{nd} (y)\})) = J (\{2^{nd} (1^{st} (y)) R i\})))$
30	29	cbvriotavw	$⊢ (ι h \in D \| (M (N (\{2^{nd} (y)\})) = J (\{h\}) \land M (N (\{1^{st} (1^{st} (y)) \underset{˙}{-} 2^{nd} (y)\})) = J (\{2^{nd} (1^{st} (y)) R h\}))) = (ι i \in D \| (M (N (\{2^{nd} (y)\})) = J (\{i\}) \land M (N (\{1^{st} (1^{st} (y)) \underset{˙}{-} 2^{nd} (y)\})) = J (\{2^{nd} (1^{st} (y)) R i\})))$
31		ifeq2	$⊢ (ι h \in D \| (M (N (\{2^{nd} (y)\})) = J (\{h\}) \land M (N (\{1^{st} (1^{st} (y)) \underset{˙}{-} 2^{nd} (y)\})) = J (\{2^{nd} (1^{st} (y)) R h\}))) = (ι i \in D \| (M (N (\{2^{nd} (y)\})) = J (\{i\}) \land M (N (\{1^{st} (1^{st} (y)) \underset{˙}{-} 2^{nd} (y)\})) = J (\{2^{nd} (1^{st} (y)) R i\}))) \to if (2^{nd} (y) = \underset{˙}{0}, Q, (ι h \in D \| (M (N (\{2^{nd} (y)\})) = J (\{h\}) \land M (N (\{1^{st} (1^{st} (y)) \underset{˙}{-} 2^{nd} (y)\})) = J (\{2^{nd} (1^{st} (y)) R h\})))) = if (2^{nd} (y) = \underset{˙}{0}, Q, (ι i \in D \| (M (N (\{2^{nd} (y)\})) = J (\{i\}) \land M (N (\{1^{st} (1^{st} (y)) \underset{˙}{-} 2^{nd} (y)\})) = J (\{2^{nd} (1^{st} (y)) R i\}))))$
32	30 31	ax-mp	$⊢ if (2^{nd} (y) = \underset{˙}{0}, Q, (ι h \in D \| (M (N (\{2^{nd} (y)\})) = J (\{h\}) \land M (N (\{1^{st} (1^{st} (y)) \underset{˙}{-} 2^{nd} (y)\})) = J (\{2^{nd} (1^{st} (y)) R h\})))) = if (2^{nd} (y) = \underset{˙}{0}, Q, (ι i \in D \| (M (N (\{2^{nd} (y)\})) = J (\{i\}) \land M (N (\{1^{st} (1^{st} (y)) \underset{˙}{-} 2^{nd} (y)\})) = J (\{2^{nd} (1^{st} (y)) R i\}))))$
33	32	mpteq2i	$⊢ (y \in V ⟼ if (2^{nd} (y) = \underset{˙}{0}, Q, (ι h \in D \| (M (N (\{2^{nd} (y)\})) = J (\{h\}) \land M (N (\{1^{st} (1^{st} (y)) \underset{˙}{-} 2^{nd} (y)\})) = J (\{2^{nd} (1^{st} (y)) R h\}))))) = (y \in V ⟼ if (2^{nd} (y) = \underset{˙}{0}, Q, (ι i \in D \| (M (N (\{2^{nd} (y)\})) = J (\{i\}) \land M (N (\{1^{st} (1^{st} (y)) \underset{˙}{-} 2^{nd} (y)\})) = J (\{2^{nd} (1^{st} (y)) R i\})))))$
34	1 21 33	3eqtri	$⊢ L = (y \in V ⟼ if (2^{nd} (y) = \underset{˙}{0}, Q, (ι i \in D \| (M (N (\{2^{nd} (y)\})) = J (\{i\}) \land M (N (\{1^{st} (1^{st} (y)) \underset{˙}{-} 2^{nd} (y)\})) = J (\{2^{nd} (1^{st} (y)) R i\})))))$

Metamath Proof Explorer

Theorem hdmap1cbv

Proof