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 
|- A = ( AbsVal ` R )
abv1.p 
|- .1. = ( 1r ` R )
abv1z.z 
|- .0. = ( 0g ` R )
Assertion abv1z 
|- ( ( F e. A /\ .1. =/= .0. ) -> ( F ` .1. ) = 1 )

Proof

Step Hyp Ref Expression
1 abv0.a 
 |-  A = ( AbsVal ` R )
2 abv1.p 
 |-  .1. = ( 1r ` R )
3 abv1z.z 
 |-  .0. = ( 0g ` R )
4 1 abvrcl 
 |-  ( F e. A -> R e. Ring )
5 eqid 
 |-  ( Base ` R ) = ( Base ` R )
6 5 2 ringidcl 
 |-  ( R e. Ring -> .1. e. ( Base ` R ) )
7 4 6 syl 
 |-  ( F e. A -> .1. e. ( Base ` R ) )
8 1 5 abvcl 
 |-  ( ( F e. A /\ .1. e. ( Base ` R ) ) -> ( F ` .1. ) e. RR )
9 7 8 mpdan 
 |-  ( F e. A -> ( F ` .1. ) e. RR )
10 9 adantr 
 |-  ( ( F e. A /\ .1. =/= .0. ) -> ( F ` .1. ) e. RR )
11 10 recnd 
 |-  ( ( F e. A /\ .1. =/= .0. ) -> ( F ` .1. ) e. CC )
12 simpl 
 |-  ( ( F e. A /\ .1. =/= .0. ) -> F e. A )
13 7 adantr 
 |-  ( ( F e. A /\ .1. =/= .0. ) -> .1. e. ( Base ` R ) )
14 simpr 
 |-  ( ( F e. A /\ .1. =/= .0. ) -> .1. =/= .0. )
15 1 5 3 abvne0 
 |-  ( ( F e. A /\ .1. e. ( Base ` R ) /\ .1. =/= .0. ) -> ( F ` .1. ) =/= 0 )
16 12 13 14 15 syl3anc 
 |-  ( ( F e. A /\ .1. =/= .0. ) -> ( F ` .1. ) =/= 0 )
17 11 11 16 divcan3d 
 |-  ( ( F e. A /\ .1. =/= .0. ) -> ( ( ( F ` .1. ) x. ( F ` .1. ) ) / ( F ` .1. ) ) = ( F ` .1. ) )
18 eqid 
 |-  ( .r ` R ) = ( .r ` R )
19 5 18 2 ringlidm 
 |-  ( ( R e. Ring /\ .1. e. ( Base ` R ) ) -> ( .1. ( .r ` R ) .1. ) = .1. )
20 4 13 19 syl2an2r 
 |-  ( ( F e. A /\ .1. =/= .0. ) -> ( .1. ( .r ` R ) .1. ) = .1. )
21 20 fveq2d 
 |-  ( ( F e. A /\ .1. =/= .0. ) -> ( F ` ( .1. ( .r ` R ) .1. ) ) = ( F ` .1. ) )
22 1 5 18 abvmul 
 |-  ( ( F e. A /\ .1. e. ( Base ` R ) /\ .1. e. ( Base ` R ) ) -> ( F ` ( .1. ( .r ` R ) .1. ) ) = ( ( F ` .1. ) x. ( F ` .1. ) ) )
23 12 13 13 22 syl3anc 
 |-  ( ( F e. A /\ .1. =/= .0. ) -> ( F ` ( .1. ( .r ` R ) .1. ) ) = ( ( F ` .1. ) x. ( F ` .1. ) ) )
24 21 23 eqtr3d 
 |-  ( ( F e. A /\ .1. =/= .0. ) -> ( F ` .1. ) = ( ( F ` .1. ) x. ( F ` .1. ) ) )
25 24 oveq1d 
 |-  ( ( F e. A /\ .1. =/= .0. ) -> ( ( F ` .1. ) / ( F ` .1. ) ) = ( ( ( F ` .1. ) x. ( F ` .1. ) ) / ( F ` .1. ) ) )
26 11 16 dividd 
 |-  ( ( F e. A /\ .1. =/= .0. ) -> ( ( F ` .1. ) / ( F ` .1. ) ) = 1 )
27 25 26 eqtr3d 
 |-  ( ( F e. A /\ .1. =/= .0. ) -> ( ( ( F ` .1. ) x. ( F ` .1. ) ) / ( F ` .1. ) ) = 1 )
28 17 27 eqtr3d 
 |-  ( ( F e. A /\ .1. =/= .0. ) -> ( F ` .1. ) = 1 )