# Metamath Proof Explorer

## Theorem abv1z

Description: The absolute value of one is one in a non-trivial ring. (Contributed by Mario Carneiro, 8-Sep-2014)

Ref Expression
Hypotheses abv0.a 𝐴 = ( AbsVal ‘ 𝑅 )
abv1.p 1 = ( 1r𝑅 )
abv1z.z 0 = ( 0g𝑅 )
Assertion abv1z ( ( 𝐹𝐴10 ) → ( 𝐹1 ) = 1 )

### Proof

Step Hyp Ref Expression
1 abv0.a 𝐴 = ( AbsVal ‘ 𝑅 )
2 abv1.p 1 = ( 1r𝑅 )
3 abv1z.z 0 = ( 0g𝑅 )
4 1 abvrcl ( 𝐹𝐴𝑅 ∈ Ring )
5 eqid ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
6 5 2 ringidcl ( 𝑅 ∈ Ring → 1 ∈ ( Base ‘ 𝑅 ) )
7 4 6 syl ( 𝐹𝐴1 ∈ ( Base ‘ 𝑅 ) )
8 1 5 abvcl ( ( 𝐹𝐴1 ∈ ( Base ‘ 𝑅 ) ) → ( 𝐹1 ) ∈ ℝ )
9 7 8 mpdan ( 𝐹𝐴 → ( 𝐹1 ) ∈ ℝ )
10 9 adantr ( ( 𝐹𝐴10 ) → ( 𝐹1 ) ∈ ℝ )
11 10 recnd ( ( 𝐹𝐴10 ) → ( 𝐹1 ) ∈ ℂ )
12 simpl ( ( 𝐹𝐴10 ) → 𝐹𝐴 )
13 7 adantr ( ( 𝐹𝐴10 ) → 1 ∈ ( Base ‘ 𝑅 ) )
14 simpr ( ( 𝐹𝐴10 ) → 10 )
15 1 5 3 abvne0 ( ( 𝐹𝐴1 ∈ ( Base ‘ 𝑅 ) ∧ 10 ) → ( 𝐹1 ) ≠ 0 )
16 12 13 14 15 syl3anc ( ( 𝐹𝐴10 ) → ( 𝐹1 ) ≠ 0 )
17 11 11 16 divcan3d ( ( 𝐹𝐴10 ) → ( ( ( 𝐹1 ) · ( 𝐹1 ) ) / ( 𝐹1 ) ) = ( 𝐹1 ) )
18 eqid ( .r𝑅 ) = ( .r𝑅 )
19 5 18 2 ringlidm ( ( 𝑅 ∈ Ring ∧ 1 ∈ ( Base ‘ 𝑅 ) ) → ( 1 ( .r𝑅 ) 1 ) = 1 )
20 4 13 19 syl2an2r ( ( 𝐹𝐴10 ) → ( 1 ( .r𝑅 ) 1 ) = 1 )
21 20 fveq2d ( ( 𝐹𝐴10 ) → ( 𝐹 ‘ ( 1 ( .r𝑅 ) 1 ) ) = ( 𝐹1 ) )
22 1 5 18 abvmul ( ( 𝐹𝐴1 ∈ ( Base ‘ 𝑅 ) ∧ 1 ∈ ( Base ‘ 𝑅 ) ) → ( 𝐹 ‘ ( 1 ( .r𝑅 ) 1 ) ) = ( ( 𝐹1 ) · ( 𝐹1 ) ) )
23 12 13 13 22 syl3anc ( ( 𝐹𝐴10 ) → ( 𝐹 ‘ ( 1 ( .r𝑅 ) 1 ) ) = ( ( 𝐹1 ) · ( 𝐹1 ) ) )
24 21 23 eqtr3d ( ( 𝐹𝐴10 ) → ( 𝐹1 ) = ( ( 𝐹1 ) · ( 𝐹1 ) ) )
25 24 oveq1d ( ( 𝐹𝐴10 ) → ( ( 𝐹1 ) / ( 𝐹1 ) ) = ( ( ( 𝐹1 ) · ( 𝐹1 ) ) / ( 𝐹1 ) ) )
26 11 16 dividd ( ( 𝐹𝐴10 ) → ( ( 𝐹1 ) / ( 𝐹1 ) ) = 1 )
27 25 26 eqtr3d ( ( 𝐹𝐴10 ) → ( ( ( 𝐹1 ) · ( 𝐹1 ) ) / ( 𝐹1 ) ) = 1 )
28 17 27 eqtr3d ( ( 𝐹𝐴10 ) → ( 𝐹1 ) = 1 )