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 ( ( 𝐹 ∈ 𝐴 ∧ 1 ≠ 0 ) → ( 𝐹 ‘ 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 ⊢ ( ( 𝐹 ∈ 𝐴 ∧ 1 ≠ 0 ) → ( 𝐹 ‘ 1 ) ∈ ℝ )
11 10 recnd ⊢ ( ( 𝐹 ∈ 𝐴 ∧ 1 ≠ 0 ) → ( 𝐹 ‘ 1 ) ∈ ℂ )
12 simpl ⊢ ( ( 𝐹 ∈ 𝐴 ∧ 1 ≠ 0 ) → 𝐹 ∈ 𝐴 )
13 7 adantr ⊢ ( ( 𝐹 ∈ 𝐴 ∧ 1 ≠ 0 ) → 1 ∈ ( Base ‘ 𝑅 ) )
14 simpr ⊢ ( ( 𝐹 ∈ 𝐴 ∧ 1 ≠ 0 ) → 1 ≠ 0 )
15 1 5 3 abvne0 ⊢ ( ( 𝐹 ∈ 𝐴 ∧ 1 ∈ ( Base ‘ 𝑅 ) ∧ 1 ≠ 0 ) → ( 𝐹 ‘ 1 ) ≠ 0 )
16 12 13 14 15 syl3anc ⊢ ( ( 𝐹 ∈ 𝐴 ∧ 1 ≠ 0 ) → ( 𝐹 ‘ 1 ) ≠ 0 )
17 11 11 16 divcan3d ⊢ ( ( 𝐹 ∈ 𝐴 ∧ 1 ≠ 0 ) → ( ( ( 𝐹 ‘ 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 ⊢ ( ( 𝐹 ∈ 𝐴 ∧ 1 ≠ 0 ) → ( 1 ( .r ‘ 𝑅 ) 1 ) = 1 )
21 20 fveq2d ⊢ ( ( 𝐹 ∈ 𝐴 ∧ 1 ≠ 0 ) → ( 𝐹 ‘ ( 1 ( .r ‘ 𝑅 ) 1 ) ) = ( 𝐹 ‘ 1 ) )
22 1 5 18 abvmul ⊢ ( ( 𝐹 ∈ 𝐴 ∧ 1 ∈ ( Base ‘ 𝑅 ) ∧ 1 ∈ ( Base ‘ 𝑅 ) ) → ( 𝐹 ‘ ( 1 ( .r ‘ 𝑅 ) 1 ) ) = ( ( 𝐹 ‘ 1 ) · ( 𝐹 ‘ 1 ) ) )
23 12 13 13 22 syl3anc ⊢ ( ( 𝐹 ∈ 𝐴 ∧ 1 ≠ 0 ) → ( 𝐹 ‘ ( 1 ( .r ‘ 𝑅 ) 1 ) ) = ( ( 𝐹 ‘ 1 ) · ( 𝐹 ‘ 1 ) ) )
24 21 23 eqtr3d ⊢ ( ( 𝐹 ∈ 𝐴 ∧ 1 ≠ 0 ) → ( 𝐹 ‘ 1 ) = ( ( 𝐹 ‘ 1 ) · ( 𝐹 ‘ 1 ) ) )
25 24 oveq1d ⊢ ( ( 𝐹 ∈ 𝐴 ∧ 1 ≠ 0 ) → ( ( 𝐹 ‘ 1 ) / ( 𝐹 ‘ 1 ) ) = ( ( ( 𝐹 ‘ 1 ) · ( 𝐹 ‘ 1 ) ) / ( 𝐹 ‘ 1 ) ) )
26 11 16 dividd ⊢ ( ( 𝐹 ∈ 𝐴 ∧ 1 ≠ 0 ) → ( ( 𝐹 ‘ 1 ) / ( 𝐹 ‘ 1 ) ) = 1 )
27 25 26 eqtr3d ⊢ ( ( 𝐹 ∈ 𝐴 ∧ 1 ≠ 0 ) → ( ( ( 𝐹 ‘ 1 ) · ( 𝐹 ‘ 1 ) ) / ( 𝐹 ‘ 1 ) ) = 1 )
28 17 27 eqtr3d ⊢ ( ( 𝐹 ∈ 𝐴 ∧ 1 ≠ 0 ) → ( 𝐹 ‘ 1 ) = 1 )