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

Metamath Proof Explorer

Theorem mulclsr

Description: Closure of multiplication on signed reals. (Contributed by NM, 10-Aug-1995) (New usage is discouraged.)

Ref Expression
Assertion mulclsr ( ( 𝐴 ∈ R ∧ 𝐵 ∈ R ) → ( 𝐴 ·R 𝐵 ) ∈ R )

Proof

Step Hyp Ref Expression
1 df-nr ⊢ R = ( ( P × P ) / ~R )
2 oveq1 ⊢ ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ~R = 𝐴 → ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ~R ·R [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R ) = ( 𝐴 ·R [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R ) )
3 2 eleq1d ⊢ ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ~R = 𝐴 → ( ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ~R ·R [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R ) ∈ ( ( P × P ) / ~R ) ↔ ( 𝐴 ·R [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R ) ∈ ( ( P × P ) / ~R ) ) )
4 oveq2 ⊢ ( [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R = 𝐵 → ( 𝐴 ·R [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R ) = ( 𝐴 ·R 𝐵 ) )
5 4 eleq1d ⊢ ( [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R = 𝐵 → ( ( 𝐴 ·R [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R ) ∈ ( ( P × P ) / ~R ) ↔ ( 𝐴 ·R 𝐵 ) ∈ ( ( P × P ) / ~R ) ) )
6 mulsrpr ⊢ ( ( ( 𝑥 ∈ P ∧ 𝑦 ∈ P ) ∧ ( 𝑧 ∈ P ∧ 𝑤 ∈ P ) ) → ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ~R ·R [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R ) = [ ⟨ ( ( 𝑥 ·P 𝑧 ) +P ( 𝑦 ·P 𝑤 ) ) , ( ( 𝑥 ·P 𝑤 ) +P ( 𝑦 ·P 𝑧 ) ) ⟩ ] ~R )
7 mulclpr ⊢ ( ( 𝑥 ∈ P ∧ 𝑧 ∈ P ) → ( 𝑥 ·P 𝑧 ) ∈ P )
8 mulclpr ⊢ ( ( 𝑦 ∈ P ∧ 𝑤 ∈ P ) → ( 𝑦 ·P 𝑤 ) ∈ P )
9 addclpr ⊢ ( ( ( 𝑥 ·P 𝑧 ) ∈ P ∧ ( 𝑦 ·P 𝑤 ) ∈ P ) → ( ( 𝑥 ·P 𝑧 ) +P ( 𝑦 ·P 𝑤 ) ) ∈ P )
10 7 8 9 syl2an ⊢ ( ( ( 𝑥 ∈ P ∧ 𝑧 ∈ P ) ∧ ( 𝑦 ∈ P ∧ 𝑤 ∈ P ) ) → ( ( 𝑥 ·P 𝑧 ) +P ( 𝑦 ·P 𝑤 ) ) ∈ P )
11 10 an4s ⊢ ( ( ( 𝑥 ∈ P ∧ 𝑦 ∈ P ) ∧ ( 𝑧 ∈ P ∧ 𝑤 ∈ P ) ) → ( ( 𝑥 ·P 𝑧 ) +P ( 𝑦 ·P 𝑤 ) ) ∈ P )
12 mulclpr ⊢ ( ( 𝑥 ∈ P ∧ 𝑤 ∈ P ) → ( 𝑥 ·P 𝑤 ) ∈ P )
13 mulclpr ⊢ ( ( 𝑦 ∈ P ∧ 𝑧 ∈ P ) → ( 𝑦 ·P 𝑧 ) ∈ P )
14 addclpr ⊢ ( ( ( 𝑥 ·P 𝑤 ) ∈ P ∧ ( 𝑦 ·P 𝑧 ) ∈ P ) → ( ( 𝑥 ·P 𝑤 ) +P ( 𝑦 ·P 𝑧 ) ) ∈ P )
15 12 13 14 syl2an ⊢ ( ( ( 𝑥 ∈ P ∧ 𝑤 ∈ P ) ∧ ( 𝑦 ∈ P ∧ 𝑧 ∈ P ) ) → ( ( 𝑥 ·P 𝑤 ) +P ( 𝑦 ·P 𝑧 ) ) ∈ P )
16 15 an42s ⊢ ( ( ( 𝑥 ∈ P ∧ 𝑦 ∈ P ) ∧ ( 𝑧 ∈ P ∧ 𝑤 ∈ P ) ) → ( ( 𝑥 ·P 𝑤 ) +P ( 𝑦 ·P 𝑧 ) ) ∈ P )
17 11 16 jca ⊢ ( ( ( 𝑥 ∈ P ∧ 𝑦 ∈ P ) ∧ ( 𝑧 ∈ P ∧ 𝑤 ∈ P ) ) → ( ( ( 𝑥 ·P 𝑧 ) +P ( 𝑦 ·P 𝑤 ) ) ∈ P ∧ ( ( 𝑥 ·P 𝑤 ) +P ( 𝑦 ·P 𝑧 ) ) ∈ P ) )
18 opelxpi ⊢ ( ( ( ( 𝑥 ·P 𝑧 ) +P ( 𝑦 ·P 𝑤 ) ) ∈ P ∧ ( ( 𝑥 ·P 𝑤 ) +P ( 𝑦 ·P 𝑧 ) ) ∈ P ) → ⟨ ( ( 𝑥 ·P 𝑧 ) +P ( 𝑦 ·P 𝑤 ) ) , ( ( 𝑥 ·P 𝑤 ) +P ( 𝑦 ·P 𝑧 ) ) ⟩ ∈ ( P × P ) )
19 enrex ⊢ ~R ∈ V
20 19 ecelqsi ⊢ ( ⟨ ( ( 𝑥 ·P 𝑧 ) +P ( 𝑦 ·P 𝑤 ) ) , ( ( 𝑥 ·P 𝑤 ) +P ( 𝑦 ·P 𝑧 ) ) ⟩ ∈ ( P × P ) → [ ⟨ ( ( 𝑥 ·P 𝑧 ) +P ( 𝑦 ·P 𝑤 ) ) , ( ( 𝑥 ·P 𝑤 ) +P ( 𝑦 ·P 𝑧 ) ) ⟩ ] ~R ∈ ( ( P × P ) / ~R ) )
21 17 18 20 3syl ⊢ ( ( ( 𝑥 ∈ P ∧ 𝑦 ∈ P ) ∧ ( 𝑧 ∈ P ∧ 𝑤 ∈ P ) ) → [ ⟨ ( ( 𝑥 ·P 𝑧 ) +P ( 𝑦 ·P 𝑤 ) ) , ( ( 𝑥 ·P 𝑤 ) +P ( 𝑦 ·P 𝑧 ) ) ⟩ ] ~R ∈ ( ( P × P ) / ~R ) )
22 6 21 eqeltrd ⊢ ( ( ( 𝑥 ∈ P ∧ 𝑦 ∈ P ) ∧ ( 𝑧 ∈ P ∧ 𝑤 ∈ P ) ) → ( [ ⟨ 𝑥 , 𝑦 ⟩ ] ~R ·R [ ⟨ 𝑧 , 𝑤 ⟩ ] ~R ) ∈ ( ( P × P ) / ~R ) )
23 1 3 5 22 2ecoptocl ⊢ ( ( 𝐴 ∈ R ∧ 𝐵 ∈ R ) → ( 𝐴 ·R 𝐵 ) ∈ ( ( P × P ) / ~R ) )
24 23 1 eleqtrrdi ⊢ ( ( 𝐴 ∈ R ∧ 𝐵 ∈ R ) → ( 𝐴 ·R 𝐵 ) ∈ R )