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

Metamath Proof Explorer

Theorem genpprecl

Description: Pre-closure law for general operation on positive reals. (Contributed by NM, 10-Mar-1996) (Revised by Mario Carneiro, 12-Jun-2013) (New usage is discouraged.)

Ref Expression
Hypotheses genp.1 ⊢ 𝐹 = ( 𝑤 ∈ P , 𝑣 ∈ P ↦ { 𝑥 ∣ ∃ 𝑦 ∈ 𝑤 ∃ 𝑧 ∈ 𝑣 𝑥 = ( 𝑦 𝐺 𝑧 ) } )
genp.2 ⊢ ( ( 𝑦 ∈ Q ∧ 𝑧 ∈ Q ) → ( 𝑦 𝐺 𝑧 ) ∈ Q )
Assertion genpprecl ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) → ( ( 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐵 ) → ( 𝐶 𝐺 𝐷 ) ∈ ( 𝐴 𝐹 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 genp.1 ⊢ 𝐹 = ( 𝑤 ∈ P , 𝑣 ∈ P ↦ { 𝑥 ∣ ∃ 𝑦 ∈ 𝑤 ∃ 𝑧 ∈ 𝑣 𝑥 = ( 𝑦 𝐺 𝑧 ) } )
2 genp.2 ⊢ ( ( 𝑦 ∈ Q ∧ 𝑧 ∈ Q ) → ( 𝑦 𝐺 𝑧 ) ∈ Q )
3 eqid ⊢ ( 𝐶 𝐺 𝐷 ) = ( 𝐶 𝐺 𝐷 )
4 rspceov ⊢ ( ( 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐵 ∧ ( 𝐶 𝐺 𝐷 ) = ( 𝐶 𝐺 𝐷 ) ) → ∃ 𝑔 ∈ 𝐴 ∃ ℎ ∈ 𝐵 ( 𝐶 𝐺 𝐷 ) = ( 𝑔 𝐺 ℎ ) )
5 3 4 mp3an3 ⊢ ( ( 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐵 ) → ∃ 𝑔 ∈ 𝐴 ∃ ℎ ∈ 𝐵 ( 𝐶 𝐺 𝐷 ) = ( 𝑔 𝐺 ℎ ) )
6 1 2 genpelv ⊢ ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) → ( ( 𝐶 𝐺 𝐷 ) ∈ ( 𝐴 𝐹 𝐵 ) ↔ ∃ 𝑔 ∈ 𝐴 ∃ ℎ ∈ 𝐵 ( 𝐶 𝐺 𝐷 ) = ( 𝑔 𝐺 ℎ ) ) )
7 5 6 imbitrrid ⊢ ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) → ( ( 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐵 ) → ( 𝐶 𝐺 𝐷 ) ∈ ( 𝐴 𝐹 𝐵 ) ) )