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 / ( 𝐹 ‘ 𝑋 ) ) )