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 )