# Metamath Proof Explorer

## Theorem abvrec

Description: The absolute value distributes under reciprocal. (Contributed by Mario Carneiro, 10-Sep-2014)

Ref Expression
Hypotheses abv0.a 𝐴 = ( AbsVal ‘ 𝑅 )
abvneg.b 𝐵 = ( Base ‘ 𝑅 )
abvrec.z 0 = ( 0g𝑅 )
abvrec.p 𝐼 = ( invr𝑅 )
Assertion abvrec ( ( ( 𝑅 ∈ DivRing ∧ 𝐹𝐴 ) ∧ ( 𝑋𝐵𝑋0 ) ) → ( 𝐹 ‘ ( 𝐼𝑋 ) ) = ( 1 / ( 𝐹𝑋 ) ) )

### Proof

Step Hyp Ref Expression
1 abv0.a 𝐴 = ( AbsVal ‘ 𝑅 )
2 abvneg.b 𝐵 = ( Base ‘ 𝑅 )
3 abvrec.z 0 = ( 0g𝑅 )
4 abvrec.p 𝐼 = ( invr𝑅 )
5 simplr ( ( ( 𝑅 ∈ DivRing ∧ 𝐹𝐴 ) ∧ ( 𝑋𝐵𝑋0 ) ) → 𝐹𝐴 )
6 simprl ( ( ( 𝑅 ∈ DivRing ∧ 𝐹𝐴 ) ∧ ( 𝑋𝐵𝑋0 ) ) → 𝑋𝐵 )
7 1 2 abvcl ( ( 𝐹𝐴𝑋𝐵 ) → ( 𝐹𝑋 ) ∈ ℝ )
8 5 6 7 syl2anc ( ( ( 𝑅 ∈ DivRing ∧ 𝐹𝐴 ) ∧ ( 𝑋𝐵𝑋0 ) ) → ( 𝐹𝑋 ) ∈ ℝ )
9 8 recnd ( ( ( 𝑅 ∈ DivRing ∧ 𝐹𝐴 ) ∧ ( 𝑋𝐵𝑋0 ) ) → ( 𝐹𝑋 ) ∈ ℂ )
10 simpll ( ( ( 𝑅 ∈ DivRing ∧ 𝐹𝐴 ) ∧ ( 𝑋𝐵𝑋0 ) ) → 𝑅 ∈ DivRing )
11 simprr ( ( ( 𝑅 ∈ DivRing ∧ 𝐹𝐴 ) ∧ ( 𝑋𝐵𝑋0 ) ) → 𝑋0 )
12 2 3 4 drnginvrcl ( ( 𝑅 ∈ DivRing ∧ 𝑋𝐵𝑋0 ) → ( 𝐼𝑋 ) ∈ 𝐵 )
13 10 6 11 12 syl3anc ( ( ( 𝑅 ∈ DivRing ∧ 𝐹𝐴 ) ∧ ( 𝑋𝐵𝑋0 ) ) → ( 𝐼𝑋 ) ∈ 𝐵 )
14 1 2 abvcl ( ( 𝐹𝐴 ∧ ( 𝐼𝑋 ) ∈ 𝐵 ) → ( 𝐹 ‘ ( 𝐼𝑋 ) ) ∈ ℝ )
15 5 13 14 syl2anc ( ( ( 𝑅 ∈ DivRing ∧ 𝐹𝐴 ) ∧ ( 𝑋𝐵𝑋0 ) ) → ( 𝐹 ‘ ( 𝐼𝑋 ) ) ∈ ℝ )
16 15 recnd ( ( ( 𝑅 ∈ DivRing ∧ 𝐹𝐴 ) ∧ ( 𝑋𝐵𝑋0 ) ) → ( 𝐹 ‘ ( 𝐼𝑋 ) ) ∈ ℂ )
17 1 2 3 abvne0 ( ( 𝐹𝐴𝑋𝐵𝑋0 ) → ( 𝐹𝑋 ) ≠ 0 )
18 5 6 11 17 syl3anc ( ( ( 𝑅 ∈ DivRing ∧ 𝐹𝐴 ) ∧ ( 𝑋𝐵𝑋0 ) ) → ( 𝐹𝑋 ) ≠ 0 )
19 eqid ( .r𝑅 ) = ( .r𝑅 )
20 eqid ( 1r𝑅 ) = ( 1r𝑅 )
21 2 3 19 20 4 drnginvrr ( ( 𝑅 ∈ DivRing ∧ 𝑋𝐵𝑋0 ) → ( 𝑋 ( .r𝑅 ) ( 𝐼𝑋 ) ) = ( 1r𝑅 ) )
22 10 6 11 21 syl3anc ( ( ( 𝑅 ∈ DivRing ∧ 𝐹𝐴 ) ∧ ( 𝑋𝐵𝑋0 ) ) → ( 𝑋 ( .r𝑅 ) ( 𝐼𝑋 ) ) = ( 1r𝑅 ) )
23 22 fveq2d ( ( ( 𝑅 ∈ DivRing ∧ 𝐹𝐴 ) ∧ ( 𝑋𝐵𝑋0 ) ) → ( 𝐹 ‘ ( 𝑋 ( .r𝑅 ) ( 𝐼𝑋 ) ) ) = ( 𝐹 ‘ ( 1r𝑅 ) ) )
24 1 2 19 abvmul ( ( 𝐹𝐴𝑋𝐵 ∧ ( 𝐼𝑋 ) ∈ 𝐵 ) → ( 𝐹 ‘ ( 𝑋 ( .r𝑅 ) ( 𝐼𝑋 ) ) ) = ( ( 𝐹𝑋 ) · ( 𝐹 ‘ ( 𝐼𝑋 ) ) ) )
25 5 6 13 24 syl3anc ( ( ( 𝑅 ∈ DivRing ∧ 𝐹𝐴 ) ∧ ( 𝑋𝐵𝑋0 ) ) → ( 𝐹 ‘ ( 𝑋 ( .r𝑅 ) ( 𝐼𝑋 ) ) ) = ( ( 𝐹𝑋 ) · ( 𝐹 ‘ ( 𝐼𝑋 ) ) ) )
26 1 20 abv1 ( ( 𝑅 ∈ DivRing ∧ 𝐹𝐴 ) → ( 𝐹 ‘ ( 1r𝑅 ) ) = 1 )
27 26 adantr ( ( ( 𝑅 ∈ DivRing ∧ 𝐹𝐴 ) ∧ ( 𝑋𝐵𝑋0 ) ) → ( 𝐹 ‘ ( 1r𝑅 ) ) = 1 )
28 23 25 27 3eqtr3d ( ( ( 𝑅 ∈ DivRing ∧ 𝐹𝐴 ) ∧ ( 𝑋𝐵𝑋0 ) ) → ( ( 𝐹𝑋 ) · ( 𝐹 ‘ ( 𝐼𝑋 ) ) ) = 1 )
29 9 16 18 28 mvllmuld ( ( ( 𝑅 ∈ DivRing ∧ 𝐹𝐴 ) ∧ ( 𝑋𝐵𝑋0 ) ) → ( 𝐹 ‘ ( 𝐼𝑋 ) ) = ( 1 / ( 𝐹𝑋 ) ) )