genpv

Description: Value of general operation (addition or multiplication) on positive reals. (Contributed by NM, 10-Mar-1996) (Revised by Mario Carneiro, 17-Nov-2014) (New usage is discouraged.)

	Ref	Expression
Hypotheses	genp.1	$⊢ F = (w \in 𝑷, v \in 𝑷 ⟼ \{x \| \exists y \in w \exists z \in v x = y G z\})$
	genp.2	$⊢ (y \in 𝑸 \land z \in 𝑸) \to y G z \in 𝑸$
Assertion	genpv	$⊢ (A \in 𝑷 \land B \in 𝑷) \to A F B = \{f \| \exists g \in A \exists h \in B f = g G h\}$

Proof

Step	Hyp	Ref	Expression
1		genp.1	$⊢ F = (w \in 𝑷, v \in 𝑷 ⟼ \{x \| \exists y \in w \exists z \in v x = y G z\})$
2		genp.2	$⊢ (y \in 𝑸 \land z \in 𝑸) \to y G z \in 𝑸$
3		oveq1	$⊢ f = A \to f F g = A F g$
4		rexeq	$⊢ f = A \to (\exists y \in f \exists z \in g x = y G z \leftrightarrow \exists y \in A \exists z \in g x = y G z)$
5	4	abbidv	$⊢ f = A \to \{x \| \exists y \in f \exists z \in g x = y G z\} = \{x \| \exists y \in A \exists z \in g x = y G z\}$
6	3 5	eqeq12d	$⊢ f = A \to (f F g = \{x \| \exists y \in f \exists z \in g x = y G z\} \leftrightarrow A F g = \{x \| \exists y \in A \exists z \in g x = y G z\})$
7		oveq2	$⊢ g = B \to A F g = A F B$
8		rexeq	$⊢ g = B \to (\exists z \in g x = y G z \leftrightarrow \exists z \in B x = y G z)$
9	8	rexbidv	$⊢ g = B \to (\exists y \in A \exists z \in g x = y G z \leftrightarrow \exists y \in A \exists z \in B x = y G z)$
10	9	abbidv	$⊢ g = B \to \{x \| \exists y \in A \exists z \in g x = y G z\} = \{x \| \exists y \in A \exists z \in B x = y G z\}$
11	7 10	eqeq12d	$⊢ g = B \to (A F g = \{x \| \exists y \in A \exists z \in g x = y G z\} \leftrightarrow A F B = \{x \| \exists y \in A \exists z \in B x = y G z\})$
12		elprnq	$⊢ (f \in 𝑷 \land y \in f) \to y \in 𝑸$
13		elprnq	$⊢ (g \in 𝑷 \land z \in g) \to z \in 𝑸$
14		eleq1	$⊢ x = y G z \to (x \in 𝑸 \leftrightarrow y G z \in 𝑸)$
15	2 14	syl5ibrcom	$⊢ (y \in 𝑸 \land z \in 𝑸) \to (x = y G z \to x \in 𝑸)$
16	12 13 15	syl2an	$⊢ ((f \in 𝑷 \land y \in f) \land (g \in 𝑷 \land z \in g)) \to (x = y G z \to x \in 𝑸)$
17	16	an4s	$⊢ ((f \in 𝑷 \land g \in 𝑷) \land (y \in f \land z \in g)) \to (x = y G z \to x \in 𝑸)$
18	17	rexlimdvva	$⊢ (f \in 𝑷 \land g \in 𝑷) \to (\exists y \in f \exists z \in g x = y G z \to x \in 𝑸)$
19	18	abssdv	$⊢ (f \in 𝑷 \land g \in 𝑷) \to \{x \| \exists y \in f \exists z \in g x = y G z\} \subseteq 𝑸$
20		nqex	$⊢ 𝑸 \in V$
21		ssexg	$⊢ (\{x \| \exists y \in f \exists z \in g x = y G z\} \subseteq 𝑸 \land 𝑸 \in V) \to \{x \| \exists y \in f \exists z \in g x = y G z\} \in V$
22	19 20 21	sylancl	$⊢ (f \in 𝑷 \land g \in 𝑷) \to \{x \| \exists y \in f \exists z \in g x = y G z\} \in V$
23		rexeq	$⊢ w = f \to (\exists y \in w \exists z \in v x = y G z \leftrightarrow \exists y \in f \exists z \in v x = y G z)$
24	23	abbidv	$⊢ w = f \to \{x \| \exists y \in w \exists z \in v x = y G z\} = \{x \| \exists y \in f \exists z \in v x = y G z\}$
25		rexeq	$⊢ v = g \to (\exists z \in v x = y G z \leftrightarrow \exists z \in g x = y G z)$
26	25	rexbidv	$⊢ v = g \to (\exists y \in f \exists z \in v x = y G z \leftrightarrow \exists y \in f \exists z \in g x = y G z)$
27	26	abbidv	$⊢ v = g \to \{x \| \exists y \in f \exists z \in v x = y G z\} = \{x \| \exists y \in f \exists z \in g x = y G z\}$
28	24 27 1	ovmpog	$⊢ (f \in 𝑷 \land g \in 𝑷 \land \{x \| \exists y \in f \exists z \in g x = y G z\} \in V) \to f F g = \{x \| \exists y \in f \exists z \in g x = y G z\}$
29	22 28	mpd3an3	$⊢ (f \in 𝑷 \land g \in 𝑷) \to f F g = \{x \| \exists y \in f \exists z \in g x = y G z\}$
30	6 11 29	vtocl2ga	$⊢ (A \in 𝑷 \land B \in 𝑷) \to A F B = \{x \| \exists y \in A \exists z \in B x = y G z\}$
31		eqeq1	$⊢ x = f \to (x = y G z \leftrightarrow f = y G z)$
32	31	2rexbidv	$⊢ x = f \to (\exists y \in A \exists z \in B x = y G z \leftrightarrow \exists y \in A \exists z \in B f = y G z)$
33		oveq1	$⊢ y = g \to y G z = g G z$
34	33	eqeq2d	$⊢ y = g \to (f = y G z \leftrightarrow f = g G z)$
35		oveq2	$⊢ z = h \to g G z = g G h$
36	35	eqeq2d	$⊢ z = h \to (f = g G z \leftrightarrow f = g G h)$
37	34 36	cbvrex2vw	$⊢ \exists y \in A \exists z \in B f = y G z \leftrightarrow \exists g \in A \exists h \in B f = g G h$
38	32 37	bitrdi	$⊢ x = f \to (\exists y \in A \exists z \in B x = y G z \leftrightarrow \exists g \in A \exists h \in B f = g G h)$
39	38	cbvabv	$⊢ \{x \| \exists y \in A \exists z \in B x = y G z\} = \{f \| \exists g \in A \exists h \in B f = g G h\}$
40	30 39	eqtrdi	$⊢ (A \in 𝑷 \land B \in 𝑷) \to A F B = \{f \| \exists g \in A \exists h \in B f = g G h\}$

Metamath Proof Explorer

Theorem genpv

Proof