Metamath Proof Explorer

Theorem xreceu

Description: Existential uniqueness of reciprocals. Theorem I.8 of Apostol p. 18. (Contributed by Thierry Arnoux, 17-Dec-2016)

Ref Expression
Assertion xreceu ⊢A∈ℝ*∧B∈ℝ∧B≠0→∃!x∈ℝ*B⋅𝑒x=A

Proof

Step Hyp Ref Expression
1 ressxr ⊢ℝ⊆ℝ*
2 xrecex ⊢B∈ℝ∧B≠0→∃y∈ℝB⋅𝑒y=1
3 2 3adant1 ⊢A∈ℝ*∧B∈ℝ∧B≠0→∃y∈ℝB⋅𝑒y=1
4 ssrexv ⊢ℝ⊆ℝ*→∃y∈ℝB⋅𝑒y=1→∃y∈ℝ*B⋅𝑒y=1
5 1 3 4 mpsyl ⊢A∈ℝ*∧B∈ℝ∧B≠0→∃y∈ℝ*B⋅𝑒y=1
6 simprl ⊢A∈ℝ*∧B∈ℝ∧y∈ℝ*∧B⋅𝑒y=1→y∈ℝ*
7 simpll ⊢A∈ℝ*∧B∈ℝ∧y∈ℝ*∧B⋅𝑒y=1→A∈ℝ*
8 6 7 xmulcld ⊢A∈ℝ*∧B∈ℝ∧y∈ℝ*∧B⋅𝑒y=1→y⋅𝑒A∈ℝ*
9 oveq1 ⊢B⋅𝑒y=1→B⋅𝑒y⋅𝑒A=1⋅𝑒A
10 9 ad2antll ⊢A∈ℝ*∧B∈ℝ∧y∈ℝ*∧B⋅𝑒y=1→B⋅𝑒y⋅𝑒A=1⋅𝑒A
11 simplr ⊢A∈ℝ*∧B∈ℝ∧y∈ℝ*∧B⋅𝑒y=1→B∈ℝ
12 11 rexrd ⊢A∈ℝ*∧B∈ℝ∧y∈ℝ*∧B⋅𝑒y=1→B∈ℝ*
13 xmulass ⊢B∈ℝ*∧y∈ℝ*∧A∈ℝ*→B⋅𝑒y⋅𝑒A=B⋅𝑒y⋅𝑒A
14 12 6 7 13 syl3anc ⊢A∈ℝ*∧B∈ℝ∧y∈ℝ*∧B⋅𝑒y=1→B⋅𝑒y⋅𝑒A=B⋅𝑒y⋅𝑒A
15 xmullid ⊢A∈ℝ*→1⋅𝑒A=A
16 7 15 syl ⊢A∈ℝ*∧B∈ℝ∧y∈ℝ*∧B⋅𝑒y=1→1⋅𝑒A=A
17 10 14 16 3eqtr3d ⊢A∈ℝ*∧B∈ℝ∧y∈ℝ*∧B⋅𝑒y=1→B⋅𝑒y⋅𝑒A=A
18 oveq2 ⊢x=y⋅𝑒A→B⋅𝑒x=B⋅𝑒y⋅𝑒A
19 18 eqeq1d ⊢x=y⋅𝑒A→B⋅𝑒x=A↔B⋅𝑒y⋅𝑒A=A
20 19 rspcev ⊢y⋅𝑒A∈ℝ*∧B⋅𝑒y⋅𝑒A=A→∃x∈ℝ*B⋅𝑒x=A
21 8 17 20 syl2anc ⊢A∈ℝ*∧B∈ℝ∧y∈ℝ*∧B⋅𝑒y=1→∃x∈ℝ*B⋅𝑒x=A
22 21 rexlimdvaa ⊢A∈ℝ*∧B∈ℝ→∃y∈ℝ*B⋅𝑒y=1→∃x∈ℝ*B⋅𝑒x=A
23 22 3adant3 ⊢A∈ℝ*∧B∈ℝ∧B≠0→∃y∈ℝ*B⋅𝑒y=1→∃x∈ℝ*B⋅𝑒x=A
24 5 23 mpd ⊢A∈ℝ*∧B∈ℝ∧B≠0→∃x∈ℝ*B⋅𝑒x=A
25 eqtr3 ⊢B⋅𝑒x=A∧B⋅𝑒y=A→B⋅𝑒x=B⋅𝑒y
26 simp1 ⊢x∈ℝ*∧y∈ℝ*∧B∈ℝ∧B≠0→x∈ℝ*
27 simp2 ⊢x∈ℝ*∧y∈ℝ*∧B∈ℝ∧B≠0→y∈ℝ*
28 simp3l ⊢x∈ℝ*∧y∈ℝ*∧B∈ℝ∧B≠0→B∈ℝ
29 simp3r ⊢x∈ℝ*∧y∈ℝ*∧B∈ℝ∧B≠0→B≠0
30 26 27 28 29 xmulcand ⊢x∈ℝ*∧y∈ℝ*∧B∈ℝ∧B≠0→B⋅𝑒x=B⋅𝑒y↔x=y
31 25 30 imbitrid ⊢x∈ℝ*∧y∈ℝ*∧B∈ℝ∧B≠0→B⋅𝑒x=A∧B⋅𝑒y=A→x=y
32 31 3expa ⊢x∈ℝ*∧y∈ℝ*∧B∈ℝ∧B≠0→B⋅𝑒x=A∧B⋅𝑒y=A→x=y
33 32 expcom ⊢B∈ℝ∧B≠0→x∈ℝ*∧y∈ℝ*→B⋅𝑒x=A∧B⋅𝑒y=A→x=y
34 33 3adant1 ⊢A∈ℝ*∧B∈ℝ∧B≠0→x∈ℝ*∧y∈ℝ*→B⋅𝑒x=A∧B⋅𝑒y=A→x=y
35 34 ralrimivv ⊢A∈ℝ*∧B∈ℝ∧B≠0→∀x∈ℝ*∀y∈ℝ*B⋅𝑒x=A∧B⋅𝑒y=A→x=y
36 oveq2 ⊢x=y→B⋅𝑒x=B⋅𝑒y
37 36 eqeq1d ⊢x=y→B⋅𝑒x=A↔B⋅𝑒y=A
38 37 reu4 ⊢∃!x∈ℝ*B⋅𝑒x=A↔∃x∈ℝ*B⋅𝑒x=A∧∀x∈ℝ*∀y∈ℝ*B⋅𝑒x=A∧B⋅𝑒y=A→x=y
39 24 35 38 sylanbrc ⊢A∈ℝ*∧B∈ℝ∧B≠0→∃!x∈ℝ*B⋅𝑒x=A