Theorem 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	⊢ 𝐹 = ( 𝑤 ∈ P , 𝑣 ∈ P ↦ { 𝑥 ∣ ∃ 𝑦 ∈ 𝑤 ∃ 𝑧 ∈ 𝑣 𝑥 = ( 𝑦 𝐺 𝑧 ) } )
	genp.2	⊢ ( ( 𝑦 ∈ Q ∧ 𝑧 ∈ Q ) → ( 𝑦 𝐺 𝑧 ) ∈ Q )
Assertion	genpv	⊢ ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) → ( 𝐴 𝐹 𝐵 ) = { 𝑓 ∣ ∃ 𝑔 ∈ 𝐴 ∃ ℎ ∈ 𝐵 𝑓 = ( 𝑔 𝐺 ℎ ) } )

Proof

Step	Hyp	Ref	Expression
1		genp.1	⊢ 𝐹 = ( 𝑤 ∈ P , 𝑣 ∈ P ↦ { 𝑥 ∣ ∃ 𝑦 ∈ 𝑤 ∃ 𝑧 ∈ 𝑣 𝑥 = ( 𝑦 𝐺 𝑧 ) } )
2		genp.2	⊢ ( ( 𝑦 ∈ Q ∧ 𝑧 ∈ Q ) → ( 𝑦 𝐺 𝑧 ) ∈ Q )
3		oveq1	⊢ ( 𝑓 = 𝐴 → ( 𝑓 𝐹 𝑔 ) = ( 𝐴 𝐹 𝑔 ) )
4		rexeq	⊢ ( 𝑓 = 𝐴 → ( ∃ 𝑦 ∈ 𝑓 ∃ 𝑧 ∈ 𝑔 𝑥 = ( 𝑦 𝐺 𝑧 ) ↔ ∃ 𝑦 ∈ 𝐴 ∃ 𝑧 ∈ 𝑔 𝑥 = ( 𝑦 𝐺 𝑧 ) ) )
5	4	abbidv	⊢ ( 𝑓 = 𝐴 → { 𝑥 ∣ ∃ 𝑦 ∈ 𝑓 ∃ 𝑧 ∈ 𝑔 𝑥 = ( 𝑦 𝐺 𝑧 ) } = { 𝑥 ∣ ∃ 𝑦 ∈ 𝐴 ∃ 𝑧 ∈ 𝑔 𝑥 = ( 𝑦 𝐺 𝑧 ) } )
6	3 5	eqeq12d	⊢ ( 𝑓 = 𝐴 → ( ( 𝑓 𝐹 𝑔 ) = { 𝑥 ∣ ∃ 𝑦 ∈ 𝑓 ∃ 𝑧 ∈ 𝑔 𝑥 = ( 𝑦 𝐺 𝑧 ) } ↔ ( 𝐴 𝐹 𝑔 ) = { 𝑥 ∣ ∃ 𝑦 ∈ 𝐴 ∃ 𝑧 ∈ 𝑔 𝑥 = ( 𝑦 𝐺 𝑧 ) } ) )
7		oveq2	⊢ ( 𝑔 = 𝐵 → ( 𝐴 𝐹 𝑔 ) = ( 𝐴 𝐹 𝐵 ) )
8		rexeq	⊢ ( 𝑔 = 𝐵 → ( ∃ 𝑧 ∈ 𝑔 𝑥 = ( 𝑦 𝐺 𝑧 ) ↔ ∃ 𝑧 ∈ 𝐵 𝑥 = ( 𝑦 𝐺 𝑧 ) ) )
9	8	rexbidv	⊢ ( 𝑔 = 𝐵 → ( ∃ 𝑦 ∈ 𝐴 ∃ 𝑧 ∈ 𝑔 𝑥 = ( 𝑦 𝐺 𝑧 ) ↔ ∃ 𝑦 ∈ 𝐴 ∃ 𝑧 ∈ 𝐵 𝑥 = ( 𝑦 𝐺 𝑧 ) ) )
10	9	abbidv	⊢ ( 𝑔 = 𝐵 → { 𝑥 ∣ ∃ 𝑦 ∈ 𝐴 ∃ 𝑧 ∈ 𝑔 𝑥 = ( 𝑦 𝐺 𝑧 ) } = { 𝑥 ∣ ∃ 𝑦 ∈ 𝐴 ∃ 𝑧 ∈ 𝐵 𝑥 = ( 𝑦 𝐺 𝑧 ) } )
11	7 10	eqeq12d	⊢ ( 𝑔 = 𝐵 → ( ( 𝐴 𝐹 𝑔 ) = { 𝑥 ∣ ∃ 𝑦 ∈ 𝐴 ∃ 𝑧 ∈ 𝑔 𝑥 = ( 𝑦 𝐺 𝑧 ) } ↔ ( 𝐴 𝐹 𝐵 ) = { 𝑥 ∣ ∃ 𝑦 ∈ 𝐴 ∃ 𝑧 ∈ 𝐵 𝑥 = ( 𝑦 𝐺 𝑧 ) } ) )
12		elprnq	⊢ ( ( 𝑓 ∈ P ∧ 𝑦 ∈ 𝑓 ) → 𝑦 ∈ Q )
13		elprnq	⊢ ( ( 𝑔 ∈ P ∧ 𝑧 ∈ 𝑔 ) → 𝑧 ∈ Q )
14		eleq1	⊢ ( 𝑥 = ( 𝑦 𝐺 𝑧 ) → ( 𝑥 ∈ Q ↔ ( 𝑦 𝐺 𝑧 ) ∈ Q ) )
15	2 14	syl5ibrcom	⊢ ( ( 𝑦 ∈ Q ∧ 𝑧 ∈ Q ) → ( 𝑥 = ( 𝑦 𝐺 𝑧 ) → 𝑥 ∈ Q ) )
16	12 13 15	syl2an	⊢ ( ( ( 𝑓 ∈ P ∧ 𝑦 ∈ 𝑓 ) ∧ ( 𝑔 ∈ P ∧ 𝑧 ∈ 𝑔 ) ) → ( 𝑥 = ( 𝑦 𝐺 𝑧 ) → 𝑥 ∈ Q ) )
17	16	an4s	⊢ ( ( ( 𝑓 ∈ P ∧ 𝑔 ∈ P ) ∧ ( 𝑦 ∈ 𝑓 ∧ 𝑧 ∈ 𝑔 ) ) → ( 𝑥 = ( 𝑦 𝐺 𝑧 ) → 𝑥 ∈ Q ) )
18	17	rexlimdvva	⊢ ( ( 𝑓 ∈ P ∧ 𝑔 ∈ P ) → ( ∃ 𝑦 ∈ 𝑓 ∃ 𝑧 ∈ 𝑔 𝑥 = ( 𝑦 𝐺 𝑧 ) → 𝑥 ∈ Q ) )
19	18	abssdv	⊢ ( ( 𝑓 ∈ P ∧ 𝑔 ∈ P ) → { 𝑥 ∣ ∃ 𝑦 ∈ 𝑓 ∃ 𝑧 ∈ 𝑔 𝑥 = ( 𝑦 𝐺 𝑧 ) } ⊆ Q )
20		nqex	⊢ Q ∈ V
21		ssexg	⊢ ( ( { 𝑥 ∣ ∃ 𝑦 ∈ 𝑓 ∃ 𝑧 ∈ 𝑔 𝑥 = ( 𝑦 𝐺 𝑧 ) } ⊆ Q ∧ Q ∈ V ) → { 𝑥 ∣ ∃ 𝑦 ∈ 𝑓 ∃ 𝑧 ∈ 𝑔 𝑥 = ( 𝑦 𝐺 𝑧 ) } ∈ V )
22	19 20 21	sylancl	⊢ ( ( 𝑓 ∈ P ∧ 𝑔 ∈ P ) → { 𝑥 ∣ ∃ 𝑦 ∈ 𝑓 ∃ 𝑧 ∈ 𝑔 𝑥 = ( 𝑦 𝐺 𝑧 ) } ∈ V )
23		rexeq	⊢ ( 𝑤 = 𝑓 → ( ∃ 𝑦 ∈ 𝑤 ∃ 𝑧 ∈ 𝑣 𝑥 = ( 𝑦 𝐺 𝑧 ) ↔ ∃ 𝑦 ∈ 𝑓 ∃ 𝑧 ∈ 𝑣 𝑥 = ( 𝑦 𝐺 𝑧 ) ) )
24	23	abbidv	⊢ ( 𝑤 = 𝑓 → { 𝑥 ∣ ∃ 𝑦 ∈ 𝑤 ∃ 𝑧 ∈ 𝑣 𝑥 = ( 𝑦 𝐺 𝑧 ) } = { 𝑥 ∣ ∃ 𝑦 ∈ 𝑓 ∃ 𝑧 ∈ 𝑣 𝑥 = ( 𝑦 𝐺 𝑧 ) } )
25		rexeq	⊢ ( 𝑣 = 𝑔 → ( ∃ 𝑧 ∈ 𝑣 𝑥 = ( 𝑦 𝐺 𝑧 ) ↔ ∃ 𝑧 ∈ 𝑔 𝑥 = ( 𝑦 𝐺 𝑧 ) ) )
26	25	rexbidv	⊢ ( 𝑣 = 𝑔 → ( ∃ 𝑦 ∈ 𝑓 ∃ 𝑧 ∈ 𝑣 𝑥 = ( 𝑦 𝐺 𝑧 ) ↔ ∃ 𝑦 ∈ 𝑓 ∃ 𝑧 ∈ 𝑔 𝑥 = ( 𝑦 𝐺 𝑧 ) ) )
27	26	abbidv	⊢ ( 𝑣 = 𝑔 → { 𝑥 ∣ ∃ 𝑦 ∈ 𝑓 ∃ 𝑧 ∈ 𝑣 𝑥 = ( 𝑦 𝐺 𝑧 ) } = { 𝑥 ∣ ∃ 𝑦 ∈ 𝑓 ∃ 𝑧 ∈ 𝑔 𝑥 = ( 𝑦 𝐺 𝑧 ) } )
28	24 27 1	ovmpog	⊢ ( ( 𝑓 ∈ P ∧ 𝑔 ∈ P ∧ { 𝑥 ∣ ∃ 𝑦 ∈ 𝑓 ∃ 𝑧 ∈ 𝑔 𝑥 = ( 𝑦 𝐺 𝑧 ) } ∈ V ) → ( 𝑓 𝐹 𝑔 ) = { 𝑥 ∣ ∃ 𝑦 ∈ 𝑓 ∃ 𝑧 ∈ 𝑔 𝑥 = ( 𝑦 𝐺 𝑧 ) } )
29	22 28	mpd3an3	⊢ ( ( 𝑓 ∈ P ∧ 𝑔 ∈ P ) → ( 𝑓 𝐹 𝑔 ) = { 𝑥 ∣ ∃ 𝑦 ∈ 𝑓 ∃ 𝑧 ∈ 𝑔 𝑥 = ( 𝑦 𝐺 𝑧 ) } )
30	6 11 29	vtocl2ga	⊢ ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) → ( 𝐴 𝐹 𝐵 ) = { 𝑥 ∣ ∃ 𝑦 ∈ 𝐴 ∃ 𝑧 ∈ 𝐵 𝑥 = ( 𝑦 𝐺 𝑧 ) } )
31		eqeq1	⊢ ( 𝑥 = 𝑓 → ( 𝑥 = ( 𝑦 𝐺 𝑧 ) ↔ 𝑓 = ( 𝑦 𝐺 𝑧 ) ) )
32	31	2rexbidv	⊢ ( 𝑥 = 𝑓 → ( ∃ 𝑦 ∈ 𝐴 ∃ 𝑧 ∈ 𝐵 𝑥 = ( 𝑦 𝐺 𝑧 ) ↔ ∃ 𝑦 ∈ 𝐴 ∃ 𝑧 ∈ 𝐵 𝑓 = ( 𝑦 𝐺 𝑧 ) ) )
33		oveq1	⊢ ( 𝑦 = 𝑔 → ( 𝑦 𝐺 𝑧 ) = ( 𝑔 𝐺 𝑧 ) )
34	33	eqeq2d	⊢ ( 𝑦 = 𝑔 → ( 𝑓 = ( 𝑦 𝐺 𝑧 ) ↔ 𝑓 = ( 𝑔 𝐺 𝑧 ) ) )
35		oveq2	⊢ ( 𝑧 = ℎ → ( 𝑔 𝐺 𝑧 ) = ( 𝑔 𝐺 ℎ ) )
36	35	eqeq2d	⊢ ( 𝑧 = ℎ → ( 𝑓 = ( 𝑔 𝐺 𝑧 ) ↔ 𝑓 = ( 𝑔 𝐺 ℎ ) ) )
37	34 36	cbvrex2vw	⊢ ( ∃ 𝑦 ∈ 𝐴 ∃ 𝑧 ∈ 𝐵 𝑓 = ( 𝑦 𝐺 𝑧 ) ↔ ∃ 𝑔 ∈ 𝐴 ∃ ℎ ∈ 𝐵 𝑓 = ( 𝑔 𝐺 ℎ ) )
38	32 37	bitrdi	⊢ ( 𝑥 = 𝑓 → ( ∃ 𝑦 ∈ 𝐴 ∃ 𝑧 ∈ 𝐵 𝑥 = ( 𝑦 𝐺 𝑧 ) ↔ ∃ 𝑔 ∈ 𝐴 ∃ ℎ ∈ 𝐵 𝑓 = ( 𝑔 𝐺 ℎ ) ) )
39	38	cbvabv	⊢ { 𝑥 ∣ ∃ 𝑦 ∈ 𝐴 ∃ 𝑧 ∈ 𝐵 𝑥 = ( 𝑦 𝐺 𝑧 ) } = { 𝑓 ∣ ∃ 𝑔 ∈ 𝐴 ∃ ℎ ∈ 𝐵 𝑓 = ( 𝑔 𝐺 ℎ ) }
40	30 39	eqtrdi	⊢ ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) → ( 𝐴 𝐹 𝐵 ) = { 𝑓 ∣ ∃ 𝑔 ∈ 𝐴 ∃ ℎ ∈ 𝐵 𝑓 = ( 𝑔 𝐺 ℎ ) } )