Theorem mulresr 11156

Description: Multiplication of real numbers in terms of intermediate signed reals. (Contributed by NM, 10-May-1996.) (New usage is discouraged.)

Assertion

Ref	Expression
mulresr	⊢ ((𝐴 ∈ R ∧ 𝐵 ∈ R) → (⟨𝐴, 0R⟩ · ⟨𝐵, 0R⟩) = ⟨(𝐴 ·R 𝐵), 0R⟩)

Proof of Theorem mulresr

Step	Hyp	Ref	Expression
1		0r 11097	. . 3 ⊢ 0R ∈ R
2		mulcnsr 11153	. . . 4 ⊢ (((𝐴 ∈ R ∧ 0R ∈ R) ∧ (𝐵 ∈ R ∧ 0R ∈ R)) → (⟨𝐴, 0R⟩ · ⟨𝐵, 0R⟩) = ⟨((𝐴 ·R 𝐵) +R (-1R ·R (0R ·R 0R))), ((0R ·R 𝐵) +R (𝐴 ·R 0R))⟩)
3	2	an4s 659	. . 3 ⊢ (((𝐴 ∈ R ∧ 𝐵 ∈ R) ∧ (0R ∈ R ∧ 0R ∈ R)) → (⟨𝐴, 0R⟩ · ⟨𝐵, 0R⟩) = ⟨((𝐴 ·R 𝐵) +R (-1R ·R (0R ·R 0R))), ((0R ·R 𝐵) +R (𝐴 ·R 0R))⟩)
4	1, 1, 3	mpanr12 704	. 2 ⊢ ((𝐴 ∈ R ∧ 𝐵 ∈ R) → (⟨𝐴, 0R⟩ · ⟨𝐵, 0R⟩) = ⟨((𝐴 ·R 𝐵) +R (-1R ·R (0R ·R 0R))), ((0R ·R 𝐵) +R (𝐴 ·R 0R))⟩)
5		00sr 11116	. . . . . . . 8 ⊢ (0R ∈ R → (0R ·R 0R) = 0R)
6	1, 5	ax-mp 5	. . . . . . 7 ⊢ (0R ·R 0R) = 0R
7	6	oveq2i 7425	. . . . . 6 ⊢ (-1R ·R (0R ·R 0R)) = (-1R ·R 0R)
8		m1r 11099	. . . . . . 7 ⊢ -1R ∈ R
9		00sr 11116	. . . . . . 7 ⊢ (-1R ∈ R → (-1R ·R 0R) = 0R)
10	8, 9	ax-mp 5	. . . . . 6 ⊢ (-1R ·R 0R) = 0R
11	7, 10	eqtri 2756	. . . . 5 ⊢ (-1R ·R (0R ·R 0R)) = 0R
12	11	oveq2i 7425	. . . 4 ⊢ ((𝐴 ·R 𝐵) +R (-1R ·R (0R ·R 0R))) = ((𝐴 ·R 𝐵) +R 0R)
13		mulclsr 11101	. . . . 5 ⊢ ((𝐴 ∈ R ∧ 𝐵 ∈ R) → (𝐴 ·R 𝐵) ∈ R)
14		0idsr 11114	. . . . 5 ⊢ ((𝐴 ·R 𝐵) ∈ R → ((𝐴 ·R 𝐵) +R 0R) = (𝐴 ·R 𝐵))
15	13, 14	syl 17	. . . 4 ⊢ ((𝐴 ∈ R ∧ 𝐵 ∈ R) → ((𝐴 ·R 𝐵) +R 0R) = (𝐴 ·R 𝐵))
16	12, 15	eqtrid 2780	. . 3 ⊢ ((𝐴 ∈ R ∧ 𝐵 ∈ R) → ((𝐴 ·R 𝐵) +R (-1R ·R (0R ·R 0R))) = (𝐴 ·R 𝐵))
17		mulcomsr 11106	. . . . . 6 ⊢ (0R ·R 𝐵) = (𝐵 ·R 0R)
18		00sr 11116	. . . . . 6 ⊢ (𝐵 ∈ R → (𝐵 ·R 0R) = 0R)
19	17, 18	eqtrid 2780	. . . . 5 ⊢ (𝐵 ∈ R → (0R ·R 𝐵) = 0R)
20		00sr 11116	. . . . 5 ⊢ (𝐴 ∈ R → (𝐴 ·R 0R) = 0R)
21	19, 20	oveqan12rd 7434	. . . 4 ⊢ ((𝐴 ∈ R ∧ 𝐵 ∈ R) → ((0R ·R 𝐵) +R (𝐴 ·R 0R)) = (0R +R 0R))
22		0idsr 11114	. . . . 5 ⊢ (0R ∈ R → (0R +R 0R) = 0R)
23	1, 22	ax-mp 5	. . . 4 ⊢ (0R +R 0R) = 0R
24	21, 23	eqtrdi 2784	. . 3 ⊢ ((𝐴 ∈ R ∧ 𝐵 ∈ R) → ((0R ·R 𝐵) +R (𝐴 ·R 0R)) = 0R)
25	16, 24	opeq12d 4877	. 2 ⊢ ((𝐴 ∈ R ∧ 𝐵 ∈ R) → ⟨((𝐴 ·R 𝐵) +R (-1R ·R (0R ·R 0R))), ((0R ·R 𝐵) +R (𝐴 ·R 0R))⟩ = ⟨(𝐴 ·R 𝐵), 0R⟩)
26	4, 25	eqtrd 2768	1 ⊢ ((𝐴 ∈ R ∧ 𝐵 ∈ R) → (⟨𝐴, 0R⟩ · ⟨𝐵, 0R⟩) = ⟨(𝐴 ·R 𝐵), 0R⟩)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1534   ∈ wcel 2099  ⟨cop 4630  (class class class)co 7414  Rcnr 10882  0_Rc0r 10883  -1_Rcm1r 10885   +_R cplr 10886   ·_R cmr 10887   · cmul 11137

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2167  ax-ext 2699  ax-sep 5293  ax-nul 5300  ax-pow 5359  ax-pr 5423  ax-un 7734  ax-inf2 9658

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3or 1086  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2530  df-eu 2559  df-clab 2706  df-cleq 2720  df-clel 2806  df-nfc 2881  df-ne 2937  df-ral 3058  df-rex 3067  df-rmo 3372  df-reu 3373  df-rab 3429  df-v 3472  df-sbc 3776  df-csb 3891  df-dif 3948  df-un 3950  df-in 3952  df-ss 3962  df-pss 3964  df-nul 4319  df-if 4525  df-pw 4600  df-sn 4625  df-pr 4627  df-op 4631  df-uni 4904  df-int 4945  df-iun 4993  df-br 5143  df-opab 5205  df-mpt 5226  df-tr 5260  df-id 5570  df-eprel 5576  df-po 5584  df-so 5585  df-fr 5627  df-we 5629  df-xp 5678  df-rel 5679  df-cnv 5680  df-co 5681  df-dm 5682  df-rn 5683  df-res 5684  df-ima 5685  df-pred 6299  df-ord 6366  df-on 6367  df-lim 6368  df-suc 6369  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-ov 7417  df-oprab 7418  df-mpo 7419  df-om 7865  df-1st 7987  df-2nd 7988  df-frecs 8280  df-wrecs 8311  df-recs 8385  df-rdg 8424  df-1o 8480  df-oadd 8484  df-omul 8485  df-er 8718  df-ec 8720  df-qs 8724  df-ni 10889  df-pli 10890  df-mi 10891  df-lti 10892  df-plpq 10925  df-mpq 10926  df-ltpq 10927  df-enq 10928  df-nq 10929  df-erq 10930  df-plq 10931  df-mq 10932  df-1nq 10933  df-rq 10934  df-ltnq 10935  df-np 10998  df-1p 10999  df-plp 11000  df-mp 11001  df-ltp 11002  df-enr 11072  df-nr 11073  df-plr 11074  df-mr 11075  df-0r 11077  df-m1r 11079  df-c 11138  df-mul 11144

This theorem is referenced by:  axmulrcl  11171  ax1rid  11178  axrrecex  11180  axpre-mulgt0  11185