This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) → ( 𝐴 𝐹 𝐵 ) = { 𝑓 ∣ ∃ 𝑔 ∈ 𝐴 ∃ ℎ ∈ 𝐵 𝑓 = ( 𝑔 𝐺 ℎ ) } )