erov

Description: The value of an operation defined on equivalence classes. (Contributed by Jeff Madsen, 10-Jun-2010) (Revised by Mario Carneiro, 30-Dec-2014)

	Ref	Expression
Hypotheses	eropr.1	$⊢ J = A / R$
	eropr.2	$⊢ K = B / S$
	eropr.3	$⊢ φ \to T \in Z$
	eropr.4	$⊢ φ \to R Er U$
	eropr.5	$⊢ φ \to S Er V$
	eropr.6	$⊢ φ \to T Er W$
	eropr.7	$⊢ φ \to A \subseteq U$
	eropr.8	$⊢ φ \to B \subseteq V$
	eropr.9	$⊢ φ \to C \subseteq W$
	eropr.10	$⊢ φ \to \underset{˙}{+} : A \times B ⟶ C$
	eropr.11	$⊢ (φ \land ((r \in A \land s \in A) \land (t \in B \land u \in B))) \to ((r R s \land t S u) \to (r \underset{˙}{+} t) T (s \underset{˙}{+} u))$
	eropr.12	$⊢ \underset{˙}{⨣} = \{⟨⟨x, y⟩, z⟩ \| \exists p \in A \exists q \in B ((x = [p] R \land y = [q] S) \land z = [(p \underset{˙}{+} q)] T)\}$
	eropr.13	$⊢ φ \to R \in X$
	eropr.14	$⊢ φ \to S \in Y$
Assertion	erov	$⊢ (φ \land P \in A \land Q \in B) \to [P] R \underset{˙}{⨣} [Q] S = [(P \underset{˙}{+} Q)] T$

Proof

Step	Hyp	Ref	Expression
1		eropr.1	$⊢ J = A / R$
2		eropr.2	$⊢ K = B / S$
3		eropr.3	$⊢ φ \to T \in Z$
4		eropr.4	$⊢ φ \to R Er U$
5		eropr.5	$⊢ φ \to S Er V$
6		eropr.6	$⊢ φ \to T Er W$
7		eropr.7	$⊢ φ \to A \subseteq U$
8		eropr.8	$⊢ φ \to B \subseteq V$
9		eropr.9	$⊢ φ \to C \subseteq W$
10		eropr.10	$⊢ φ \to \underset{˙}{+} : A \times B ⟶ C$
11		eropr.11	$⊢ (φ \land ((r \in A \land s \in A) \land (t \in B \land u \in B))) \to ((r R s \land t S u) \to (r \underset{˙}{+} t) T (s \underset{˙}{+} u))$
12		eropr.12	$⊢ \underset{˙}{⨣} = \{⟨⟨x, y⟩, z⟩ \| \exists p \in A \exists q \in B ((x = [p] R \land y = [q] S) \land z = [(p \underset{˙}{+} q)] T)\}$
13		eropr.13	$⊢ φ \to R \in X$
14		eropr.14	$⊢ φ \to S \in Y$
15	1 2 3 4 5 6 7 8 9 10 11 12	erovlem	$⊢ φ \to \underset{˙}{⨣} = (x \in J, y \in K ⟼ (ι z \| \exists p \in A \exists q \in B ((x = [p] R \land y = [q] S) \land z = [(p \underset{˙}{+} q)] T)))$
16	15	3ad2ant1	$⊢ (φ \land P \in A \land Q \in B) \to \underset{˙}{⨣} = (x \in J, y \in K ⟼ (ι z \| \exists p \in A \exists q \in B ((x = [p] R \land y = [q] S) \land z = [(p \underset{˙}{+} q)] T)))$
17		simprl	$⊢ ((φ \land P \in A \land Q \in B) \land (x = [P] R \land y = [Q] S)) \to x = [P] R$
18	17	eqeq1d	$⊢ ((φ \land P \in A \land Q \in B) \land (x = [P] R \land y = [Q] S)) \to (x = [p] R \leftrightarrow [P] R = [p] R)$
19		simprr	$⊢ ((φ \land P \in A \land Q \in B) \land (x = [P] R \land y = [Q] S)) \to y = [Q] S$
20	19	eqeq1d	$⊢ ((φ \land P \in A \land Q \in B) \land (x = [P] R \land y = [Q] S)) \to (y = [q] S \leftrightarrow [Q] S = [q] S)$
21	18 20	anbi12d	$⊢ ((φ \land P \in A \land Q \in B) \land (x = [P] R \land y = [Q] S)) \to ((x = [p] R \land y = [q] S) \leftrightarrow ([P] R = [p] R \land [Q] S = [q] S))$
22	21	anbi1d	$⊢ ((φ \land P \in A \land Q \in B) \land (x = [P] R \land y = [Q] S)) \to (((x = [p] R \land y = [q] S) \land z = [(p \underset{˙}{+} q)] T) \leftrightarrow (([P] R = [p] R \land [Q] S = [q] S) \land z = [(p \underset{˙}{+} q)] T))$
23	22	2rexbidv	$⊢ ((φ \land P \in A \land Q \in B) \land (x = [P] R \land y = [Q] S)) \to (\exists p \in A \exists q \in B ((x = [p] R \land y = [q] S) \land z = [(p \underset{˙}{+} q)] T) \leftrightarrow \exists p \in A \exists q \in B (([P] R = [p] R \land [Q] S = [q] S) \land z = [(p \underset{˙}{+} q)] T))$
24	23	iotabidv	$⊢ ((φ \land P \in A \land Q \in B) \land (x = [P] R \land y = [Q] S)) \to (ι z \| \exists p \in A \exists q \in B ((x = [p] R \land y = [q] S) \land z = [(p \underset{˙}{+} q)] T)) = (ι z \| \exists p \in A \exists q \in B (([P] R = [p] R \land [Q] S = [q] S) \land z = [(p \underset{˙}{+} q)] T))$
25		ecelqsg	$⊢ (R \in X \land P \in A) \to [P] R \in (A / R)$
26	25 1	eleqtrrdi	$⊢ (R \in X \land P \in A) \to [P] R \in J$
27	13 26	sylan	$⊢ (φ \land P \in A) \to [P] R \in J$
28	27	3adant3	$⊢ (φ \land P \in A \land Q \in B) \to [P] R \in J$
29		ecelqsg	$⊢ (S \in Y \land Q \in B) \to [Q] S \in (B / S)$
30	29 2	eleqtrrdi	$⊢ (S \in Y \land Q \in B) \to [Q] S \in K$
31	14 30	sylan	$⊢ (φ \land Q \in B) \to [Q] S \in K$
32	31	3adant2	$⊢ (φ \land P \in A \land Q \in B) \to [Q] S \in K$
33		iotaex	$⊢ (ι z \| \exists p \in A \exists q \in B (([P] R = [p] R \land [Q] S = [q] S) \land z = [(p \underset{˙}{+} q)] T)) \in V$
34	33	a1i	$⊢ (φ \land P \in A \land Q \in B) \to (ι z \| \exists p \in A \exists q \in B (([P] R = [p] R \land [Q] S = [q] S) \land z = [(p \underset{˙}{+} q)] T)) \in V$
35	16 24 28 32 34	ovmpod	$⊢ (φ \land P \in A \land Q \in B) \to [P] R \underset{˙}{⨣} [Q] S = (ι z \| \exists p \in A \exists q \in B (([P] R = [p] R \land [Q] S = [q] S) \land z = [(p \underset{˙}{+} q)] T))$
36		eqid	$⊢ [P] R = [P] R$
37		eqid	$⊢ [Q] S = [Q] S$
38	36 37	pm3.2i	$⊢ ([P] R = [P] R \land [Q] S = [Q] S)$
39		eqid	$⊢ [(P \underset{˙}{+} Q)] T = [(P \underset{˙}{+} Q)] T$
40	38 39	pm3.2i	$⊢ (([P] R = [P] R \land [Q] S = [Q] S) \land [(P \underset{˙}{+} Q)] T = [(P \underset{˙}{+} Q)] T)$
41		eceq1	$⊢ p = P \to [p] R = [P] R$
42	41	eqeq2d	$⊢ p = P \to ([P] R = [p] R \leftrightarrow [P] R = [P] R)$
43	42	anbi1d	$⊢ p = P \to (([P] R = [p] R \land [Q] S = [q] S) \leftrightarrow ([P] R = [P] R \land [Q] S = [q] S))$
44		oveq1	$⊢ p = P \to p \underset{˙}{+} q = P \underset{˙}{+} q$
45	44	eceq1d	$⊢ p = P \to [(p \underset{˙}{+} q)] T = [(P \underset{˙}{+} q)] T$
46	45	eqeq2d	$⊢ p = P \to ([(P \underset{˙}{+} Q)] T = [(p \underset{˙}{+} q)] T \leftrightarrow [(P \underset{˙}{+} Q)] T = [(P \underset{˙}{+} q)] T)$
47	43 46	anbi12d	$⊢ p = P \to ((([P] R = [p] R \land [Q] S = [q] S) \land [(P \underset{˙}{+} Q)] T = [(p \underset{˙}{+} q)] T) \leftrightarrow (([P] R = [P] R \land [Q] S = [q] S) \land [(P \underset{˙}{+} Q)] T = [(P \underset{˙}{+} q)] T))$
48		eceq1	$⊢ q = Q \to [q] S = [Q] S$
49	48	eqeq2d	$⊢ q = Q \to ([Q] S = [q] S \leftrightarrow [Q] S = [Q] S)$
50	49	anbi2d	$⊢ q = Q \to (([P] R = [P] R \land [Q] S = [q] S) \leftrightarrow ([P] R = [P] R \land [Q] S = [Q] S))$
51		oveq2	$⊢ q = Q \to P \underset{˙}{+} q = P \underset{˙}{+} Q$
52	51	eceq1d	$⊢ q = Q \to [(P \underset{˙}{+} q)] T = [(P \underset{˙}{+} Q)] T$
53	52	eqeq2d	$⊢ q = Q \to ([(P \underset{˙}{+} Q)] T = [(P \underset{˙}{+} q)] T \leftrightarrow [(P \underset{˙}{+} Q)] T = [(P \underset{˙}{+} Q)] T)$
54	50 53	anbi12d	$⊢ q = Q \to ((([P] R = [P] R \land [Q] S = [q] S) \land [(P \underset{˙}{+} Q)] T = [(P \underset{˙}{+} q)] T) \leftrightarrow (([P] R = [P] R \land [Q] S = [Q] S) \land [(P \underset{˙}{+} Q)] T = [(P \underset{˙}{+} Q)] T))$
55	47 54	rspc2ev	$⊢ (P \in A \land Q \in B \land (([P] R = [P] R \land [Q] S = [Q] S) \land [(P \underset{˙}{+} Q)] T = [(P \underset{˙}{+} Q)] T)) \to \exists p \in A \exists q \in B (([P] R = [p] R \land [Q] S = [q] S) \land [(P \underset{˙}{+} Q)] T = [(p \underset{˙}{+} q)] T)$
56	40 55	mp3an3	$⊢ (P \in A \land Q \in B) \to \exists p \in A \exists q \in B (([P] R = [p] R \land [Q] S = [q] S) \land [(P \underset{˙}{+} Q)] T = [(p \underset{˙}{+} q)] T)$
57	56	3adant1	$⊢ (φ \land P \in A \land Q \in B) \to \exists p \in A \exists q \in B (([P] R = [p] R \land [Q] S = [q] S) \land [(P \underset{˙}{+} Q)] T = [(p \underset{˙}{+} q)] T)$
58		ecexg	$⊢ T \in Z \to [(P \underset{˙}{+} Q)] T \in V$
59	3 58	syl	$⊢ φ \to [(P \underset{˙}{+} Q)] T \in V$
60	59	3ad2ant1	$⊢ (φ \land P \in A \land Q \in B) \to [(P \underset{˙}{+} Q)] T \in V$
61		simp1	$⊢ (φ \land P \in A \land Q \in B) \to φ$
62	1 2 3 4 5 6 7 8 9 10 11	eroveu	$⊢ (φ \land ([P] R \in J \land [Q] S \in K)) \to \exists! z \exists p \in A \exists q \in B (([P] R = [p] R \land [Q] S = [q] S) \land z = [(p \underset{˙}{+} q)] T)$
63	61 28 32 62	syl12anc	$⊢ (φ \land P \in A \land Q \in B) \to \exists! z \exists p \in A \exists q \in B (([P] R = [p] R \land [Q] S = [q] S) \land z = [(p \underset{˙}{+} q)] T)$
64		simpr	$⊢ ((φ \land P \in A \land Q \in B) \land z = [(P \underset{˙}{+} Q)] T) \to z = [(P \underset{˙}{+} Q)] T$
65	64	eqeq1d	$⊢ ((φ \land P \in A \land Q \in B) \land z = [(P \underset{˙}{+} Q)] T) \to (z = [(p \underset{˙}{+} q)] T \leftrightarrow [(P \underset{˙}{+} Q)] T = [(p \underset{˙}{+} q)] T)$
66	65	anbi2d	$⊢ ((φ \land P \in A \land Q \in B) \land z = [(P \underset{˙}{+} Q)] T) \to ((([P] R = [p] R \land [Q] S = [q] S) \land z = [(p \underset{˙}{+} q)] T) \leftrightarrow (([P] R = [p] R \land [Q] S = [q] S) \land [(P \underset{˙}{+} Q)] T = [(p \underset{˙}{+} q)] T))$
67	66	2rexbidv	$⊢ ((φ \land P \in A \land Q \in B) \land z = [(P \underset{˙}{+} Q)] T) \to (\exists p \in A \exists q \in B (([P] R = [p] R \land [Q] S = [q] S) \land z = [(p \underset{˙}{+} q)] T) \leftrightarrow \exists p \in A \exists q \in B (([P] R = [p] R \land [Q] S = [q] S) \land [(P \underset{˙}{+} Q)] T = [(p \underset{˙}{+} q)] T))$
68	60 63 67	iota2d	$⊢ (φ \land P \in A \land Q \in B) \to (\exists p \in A \exists q \in B (([P] R = [p] R \land [Q] S = [q] S) \land [(P \underset{˙}{+} Q)] T = [(p \underset{˙}{+} q)] T) \leftrightarrow (ι z \| \exists p \in A \exists q \in B (([P] R = [p] R \land [Q] S = [q] S) \land z = [(p \underset{˙}{+} q)] T)) = [(P \underset{˙}{+} Q)] T)$
69	57 68	mpbid	$⊢ (φ \land P \in A \land Q \in B) \to (ι z \| \exists p \in A \exists q \in B (([P] R = [p] R \land [Q] S = [q] S) \land z = [(p \underset{˙}{+} q)] T)) = [(P \underset{˙}{+} Q)] T$
70	35 69	eqtrd	$⊢ (φ \land P \in A \land Q \in B) \to [P] R \underset{˙}{⨣} [Q] S = [(P \underset{˙}{+} Q)] T$

Metamath Proof Explorer

Theorem erov

Proof