MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  isabvd Structured version   Visualization version   GIF version

Theorem isabvd 20428
Description: Properties that determine an absolute value. (Contributed by Mario Carneiro, 8-Sep-2014.) (Revised by Mario Carneiro, 4-Dec-2014.)
Hypotheses
Ref Expression
isabvd.a (πœ‘ β†’ 𝐴 = (AbsValβ€˜π‘…))
isabvd.b (πœ‘ β†’ 𝐡 = (Baseβ€˜π‘…))
isabvd.p (πœ‘ β†’ + = (+gβ€˜π‘…))
isabvd.t (πœ‘ β†’ Β· = (.rβ€˜π‘…))
isabvd.z (πœ‘ β†’ 0 = (0gβ€˜π‘…))
isabvd.1 (πœ‘ β†’ 𝑅 ∈ Ring)
isabvd.2 (πœ‘ β†’ 𝐹:π΅βŸΆβ„)
isabvd.3 (πœ‘ β†’ (πΉβ€˜ 0 ) = 0)
isabvd.4 ((πœ‘ ∧ π‘₯ ∈ 𝐡 ∧ π‘₯ β‰  0 ) β†’ 0 < (πΉβ€˜π‘₯))
isabvd.5 ((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ π‘₯ β‰  0 ) ∧ (𝑦 ∈ 𝐡 ∧ 𝑦 β‰  0 )) β†’ (πΉβ€˜(π‘₯ Β· 𝑦)) = ((πΉβ€˜π‘₯) Β· (πΉβ€˜π‘¦)))
isabvd.6 ((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ π‘₯ β‰  0 ) ∧ (𝑦 ∈ 𝐡 ∧ 𝑦 β‰  0 )) β†’ (πΉβ€˜(π‘₯ + 𝑦)) ≀ ((πΉβ€˜π‘₯) + (πΉβ€˜π‘¦)))
Assertion
Ref Expression
isabvd (πœ‘ β†’ 𝐹 ∈ 𝐴)
Distinct variable groups:   π‘₯,𝑦,𝐹   πœ‘,π‘₯,𝑦   π‘₯,𝑅,𝑦
Allowed substitution hints:   𝐴(π‘₯,𝑦)   𝐡(π‘₯,𝑦)   + (π‘₯,𝑦)   Β· (π‘₯,𝑦)   0 (π‘₯,𝑦)

Proof of Theorem isabvd
StepHypRef Expression
1 isabvd.2 . . . . . 6 (πœ‘ β†’ 𝐹:π΅βŸΆβ„)
2 isabvd.b . . . . . . 7 (πœ‘ β†’ 𝐡 = (Baseβ€˜π‘…))
32feq2d 6704 . . . . . 6 (πœ‘ β†’ (𝐹:π΅βŸΆβ„ ↔ 𝐹:(Baseβ€˜π‘…)βŸΆβ„))
41, 3mpbid 231 . . . . 5 (πœ‘ β†’ 𝐹:(Baseβ€˜π‘…)βŸΆβ„)
54ffnd 6719 . . . 4 (πœ‘ β†’ 𝐹 Fn (Baseβ€˜π‘…))
64ffvelcdmda 7087 . . . . . 6 ((πœ‘ ∧ π‘₯ ∈ (Baseβ€˜π‘…)) β†’ (πΉβ€˜π‘₯) ∈ ℝ)
7 0le0 12313 . . . . . . . . . 10 0 ≀ 0
8 isabvd.z . . . . . . . . . . . 12 (πœ‘ β†’ 0 = (0gβ€˜π‘…))
98fveq2d 6896 . . . . . . . . . . 11 (πœ‘ β†’ (πΉβ€˜ 0 ) = (πΉβ€˜(0gβ€˜π‘…)))
10 isabvd.3 . . . . . . . . . . 11 (πœ‘ β†’ (πΉβ€˜ 0 ) = 0)
119, 10eqtr3d 2775 . . . . . . . . . 10 (πœ‘ β†’ (πΉβ€˜(0gβ€˜π‘…)) = 0)
127, 11breqtrrid 5187 . . . . . . . . 9 (πœ‘ β†’ 0 ≀ (πΉβ€˜(0gβ€˜π‘…)))
1312adantr 482 . . . . . . . 8 ((πœ‘ ∧ π‘₯ ∈ (Baseβ€˜π‘…)) β†’ 0 ≀ (πΉβ€˜(0gβ€˜π‘…)))
14 fveq2 6892 . . . . . . . . 9 (π‘₯ = (0gβ€˜π‘…) β†’ (πΉβ€˜π‘₯) = (πΉβ€˜(0gβ€˜π‘…)))
1514breq2d 5161 . . . . . . . 8 (π‘₯ = (0gβ€˜π‘…) β†’ (0 ≀ (πΉβ€˜π‘₯) ↔ 0 ≀ (πΉβ€˜(0gβ€˜π‘…))))
1613, 15syl5ibrcom 246 . . . . . . 7 ((πœ‘ ∧ π‘₯ ∈ (Baseβ€˜π‘…)) β†’ (π‘₯ = (0gβ€˜π‘…) β†’ 0 ≀ (πΉβ€˜π‘₯)))
17 simp1 1137 . . . . . . . . . 10 ((πœ‘ ∧ π‘₯ ∈ (Baseβ€˜π‘…) ∧ π‘₯ β‰  (0gβ€˜π‘…)) β†’ πœ‘)
18 simp2 1138 . . . . . . . . . . 11 ((πœ‘ ∧ π‘₯ ∈ (Baseβ€˜π‘…) ∧ π‘₯ β‰  (0gβ€˜π‘…)) β†’ π‘₯ ∈ (Baseβ€˜π‘…))
1923ad2ant1 1134 . . . . . . . . . . 11 ((πœ‘ ∧ π‘₯ ∈ (Baseβ€˜π‘…) ∧ π‘₯ β‰  (0gβ€˜π‘…)) β†’ 𝐡 = (Baseβ€˜π‘…))
2018, 19eleqtrrd 2837 . . . . . . . . . 10 ((πœ‘ ∧ π‘₯ ∈ (Baseβ€˜π‘…) ∧ π‘₯ β‰  (0gβ€˜π‘…)) β†’ π‘₯ ∈ 𝐡)
21 simp3 1139 . . . . . . . . . . 11 ((πœ‘ ∧ π‘₯ ∈ (Baseβ€˜π‘…) ∧ π‘₯ β‰  (0gβ€˜π‘…)) β†’ π‘₯ β‰  (0gβ€˜π‘…))
2283ad2ant1 1134 . . . . . . . . . . 11 ((πœ‘ ∧ π‘₯ ∈ (Baseβ€˜π‘…) ∧ π‘₯ β‰  (0gβ€˜π‘…)) β†’ 0 = (0gβ€˜π‘…))
2321, 22neeqtrrd 3016 . . . . . . . . . 10 ((πœ‘ ∧ π‘₯ ∈ (Baseβ€˜π‘…) ∧ π‘₯ β‰  (0gβ€˜π‘…)) β†’ π‘₯ β‰  0 )
24 isabvd.4 . . . . . . . . . 10 ((πœ‘ ∧ π‘₯ ∈ 𝐡 ∧ π‘₯ β‰  0 ) β†’ 0 < (πΉβ€˜π‘₯))
2517, 20, 23, 24syl3anc 1372 . . . . . . . . 9 ((πœ‘ ∧ π‘₯ ∈ (Baseβ€˜π‘…) ∧ π‘₯ β‰  (0gβ€˜π‘…)) β†’ 0 < (πΉβ€˜π‘₯))
26 0re 11216 . . . . . . . . . 10 0 ∈ ℝ
2763adant3 1133 . . . . . . . . . 10 ((πœ‘ ∧ π‘₯ ∈ (Baseβ€˜π‘…) ∧ π‘₯ β‰  (0gβ€˜π‘…)) β†’ (πΉβ€˜π‘₯) ∈ ℝ)
28 ltle 11302 . . . . . . . . . 10 ((0 ∈ ℝ ∧ (πΉβ€˜π‘₯) ∈ ℝ) β†’ (0 < (πΉβ€˜π‘₯) β†’ 0 ≀ (πΉβ€˜π‘₯)))
2926, 27, 28sylancr 588 . . . . . . . . 9 ((πœ‘ ∧ π‘₯ ∈ (Baseβ€˜π‘…) ∧ π‘₯ β‰  (0gβ€˜π‘…)) β†’ (0 < (πΉβ€˜π‘₯) β†’ 0 ≀ (πΉβ€˜π‘₯)))
3025, 29mpd 15 . . . . . . . 8 ((πœ‘ ∧ π‘₯ ∈ (Baseβ€˜π‘…) ∧ π‘₯ β‰  (0gβ€˜π‘…)) β†’ 0 ≀ (πΉβ€˜π‘₯))
31303expia 1122 . . . . . . 7 ((πœ‘ ∧ π‘₯ ∈ (Baseβ€˜π‘…)) β†’ (π‘₯ β‰  (0gβ€˜π‘…) β†’ 0 ≀ (πΉβ€˜π‘₯)))
3216, 31pm2.61dne 3029 . . . . . 6 ((πœ‘ ∧ π‘₯ ∈ (Baseβ€˜π‘…)) β†’ 0 ≀ (πΉβ€˜π‘₯))
33 elrege0 13431 . . . . . 6 ((πΉβ€˜π‘₯) ∈ (0[,)+∞) ↔ ((πΉβ€˜π‘₯) ∈ ℝ ∧ 0 ≀ (πΉβ€˜π‘₯)))
346, 32, 33sylanbrc 584 . . . . 5 ((πœ‘ ∧ π‘₯ ∈ (Baseβ€˜π‘…)) β†’ (πΉβ€˜π‘₯) ∈ (0[,)+∞))
3534ralrimiva 3147 . . . 4 (πœ‘ β†’ βˆ€π‘₯ ∈ (Baseβ€˜π‘…)(πΉβ€˜π‘₯) ∈ (0[,)+∞))
36 ffnfv 7118 . . . 4 (𝐹:(Baseβ€˜π‘…)⟢(0[,)+∞) ↔ (𝐹 Fn (Baseβ€˜π‘…) ∧ βˆ€π‘₯ ∈ (Baseβ€˜π‘…)(πΉβ€˜π‘₯) ∈ (0[,)+∞)))
375, 35, 36sylanbrc 584 . . 3 (πœ‘ β†’ 𝐹:(Baseβ€˜π‘…)⟢(0[,)+∞))
3825gt0ne0d 11778 . . . . . . . 8 ((πœ‘ ∧ π‘₯ ∈ (Baseβ€˜π‘…) ∧ π‘₯ β‰  (0gβ€˜π‘…)) β†’ (πΉβ€˜π‘₯) β‰  0)
39383expia 1122 . . . . . . 7 ((πœ‘ ∧ π‘₯ ∈ (Baseβ€˜π‘…)) β†’ (π‘₯ β‰  (0gβ€˜π‘…) β†’ (πΉβ€˜π‘₯) β‰  0))
4039necon4d 2965 . . . . . 6 ((πœ‘ ∧ π‘₯ ∈ (Baseβ€˜π‘…)) β†’ ((πΉβ€˜π‘₯) = 0 β†’ π‘₯ = (0gβ€˜π‘…)))
4111adantr 482 . . . . . . 7 ((πœ‘ ∧ π‘₯ ∈ (Baseβ€˜π‘…)) β†’ (πΉβ€˜(0gβ€˜π‘…)) = 0)
42 fveqeq2 6901 . . . . . . 7 (π‘₯ = (0gβ€˜π‘…) β†’ ((πΉβ€˜π‘₯) = 0 ↔ (πΉβ€˜(0gβ€˜π‘…)) = 0))
4341, 42syl5ibrcom 246 . . . . . 6 ((πœ‘ ∧ π‘₯ ∈ (Baseβ€˜π‘…)) β†’ (π‘₯ = (0gβ€˜π‘…) β†’ (πΉβ€˜π‘₯) = 0))
4440, 43impbid 211 . . . . 5 ((πœ‘ ∧ π‘₯ ∈ (Baseβ€˜π‘…)) β†’ ((πΉβ€˜π‘₯) = 0 ↔ π‘₯ = (0gβ€˜π‘…)))
45113ad2ant1 1134 . . . . . . . . . . 11 ((πœ‘ ∧ π‘₯ ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ (Baseβ€˜π‘…)) β†’ (πΉβ€˜(0gβ€˜π‘…)) = 0)
4645adantr 482 . . . . . . . . . 10 (((πœ‘ ∧ π‘₯ ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ (Baseβ€˜π‘…)) ∧ π‘₯ = (0gβ€˜π‘…)) β†’ (πΉβ€˜(0gβ€˜π‘…)) = 0)
47 oveq1 7416 . . . . . . . . . . . 12 (π‘₯ = (0gβ€˜π‘…) β†’ (π‘₯(.rβ€˜π‘…)𝑦) = ((0gβ€˜π‘…)(.rβ€˜π‘…)𝑦))
48 isabvd.1 . . . . . . . . . . . . . 14 (πœ‘ β†’ 𝑅 ∈ Ring)
49483ad2ant1 1134 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘₯ ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ (Baseβ€˜π‘…)) β†’ 𝑅 ∈ Ring)
50 simp3 1139 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘₯ ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ (Baseβ€˜π‘…)) β†’ 𝑦 ∈ (Baseβ€˜π‘…))
51 eqid 2733 . . . . . . . . . . . . . 14 (Baseβ€˜π‘…) = (Baseβ€˜π‘…)
52 eqid 2733 . . . . . . . . . . . . . 14 (.rβ€˜π‘…) = (.rβ€˜π‘…)
53 eqid 2733 . . . . . . . . . . . . . 14 (0gβ€˜π‘…) = (0gβ€˜π‘…)
5451, 52, 53ringlz 20107 . . . . . . . . . . . . 13 ((𝑅 ∈ Ring ∧ 𝑦 ∈ (Baseβ€˜π‘…)) β†’ ((0gβ€˜π‘…)(.rβ€˜π‘…)𝑦) = (0gβ€˜π‘…))
5549, 50, 54syl2anc 585 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘₯ ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ (Baseβ€˜π‘…)) β†’ ((0gβ€˜π‘…)(.rβ€˜π‘…)𝑦) = (0gβ€˜π‘…))
5647, 55sylan9eqr 2795 . . . . . . . . . . 11 (((πœ‘ ∧ π‘₯ ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ (Baseβ€˜π‘…)) ∧ π‘₯ = (0gβ€˜π‘…)) β†’ (π‘₯(.rβ€˜π‘…)𝑦) = (0gβ€˜π‘…))
5756fveq2d 6896 . . . . . . . . . 10 (((πœ‘ ∧ π‘₯ ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ (Baseβ€˜π‘…)) ∧ π‘₯ = (0gβ€˜π‘…)) β†’ (πΉβ€˜(π‘₯(.rβ€˜π‘…)𝑦)) = (πΉβ€˜(0gβ€˜π‘…)))
5814, 45sylan9eqr 2795 . . . . . . . . . . . 12 (((πœ‘ ∧ π‘₯ ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ (Baseβ€˜π‘…)) ∧ π‘₯ = (0gβ€˜π‘…)) β†’ (πΉβ€˜π‘₯) = 0)
5958oveq1d 7424 . . . . . . . . . . 11 (((πœ‘ ∧ π‘₯ ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ (Baseβ€˜π‘…)) ∧ π‘₯ = (0gβ€˜π‘…)) β†’ ((πΉβ€˜π‘₯) Β· (πΉβ€˜π‘¦)) = (0 Β· (πΉβ€˜π‘¦)))
6043ad2ant1 1134 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ π‘₯ ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ (Baseβ€˜π‘…)) β†’ 𝐹:(Baseβ€˜π‘…)βŸΆβ„)
6160, 50ffvelcdmd 7088 . . . . . . . . . . . . . 14 ((πœ‘ ∧ π‘₯ ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ (Baseβ€˜π‘…)) β†’ (πΉβ€˜π‘¦) ∈ ℝ)
6261recnd 11242 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘₯ ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ (Baseβ€˜π‘…)) β†’ (πΉβ€˜π‘¦) ∈ β„‚)
6362adantr 482 . . . . . . . . . . . 12 (((πœ‘ ∧ π‘₯ ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ (Baseβ€˜π‘…)) ∧ π‘₯ = (0gβ€˜π‘…)) β†’ (πΉβ€˜π‘¦) ∈ β„‚)
6463mul02d 11412 . . . . . . . . . . 11 (((πœ‘ ∧ π‘₯ ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ (Baseβ€˜π‘…)) ∧ π‘₯ = (0gβ€˜π‘…)) β†’ (0 Β· (πΉβ€˜π‘¦)) = 0)
6559, 64eqtrd 2773 . . . . . . . . . 10 (((πœ‘ ∧ π‘₯ ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ (Baseβ€˜π‘…)) ∧ π‘₯ = (0gβ€˜π‘…)) β†’ ((πΉβ€˜π‘₯) Β· (πΉβ€˜π‘¦)) = 0)
6646, 57, 653eqtr4d 2783 . . . . . . . . 9 (((πœ‘ ∧ π‘₯ ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ (Baseβ€˜π‘…)) ∧ π‘₯ = (0gβ€˜π‘…)) β†’ (πΉβ€˜(π‘₯(.rβ€˜π‘…)𝑦)) = ((πΉβ€˜π‘₯) Β· (πΉβ€˜π‘¦)))
6745adantr 482 . . . . . . . . . 10 (((πœ‘ ∧ π‘₯ ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ (Baseβ€˜π‘…)) ∧ 𝑦 = (0gβ€˜π‘…)) β†’ (πΉβ€˜(0gβ€˜π‘…)) = 0)
68 oveq2 7417 . . . . . . . . . . . 12 (𝑦 = (0gβ€˜π‘…) β†’ (π‘₯(.rβ€˜π‘…)𝑦) = (π‘₯(.rβ€˜π‘…)(0gβ€˜π‘…)))
69 simp2 1138 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘₯ ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ (Baseβ€˜π‘…)) β†’ π‘₯ ∈ (Baseβ€˜π‘…))
7051, 52, 53ringrz 20108 . . . . . . . . . . . . 13 ((𝑅 ∈ Ring ∧ π‘₯ ∈ (Baseβ€˜π‘…)) β†’ (π‘₯(.rβ€˜π‘…)(0gβ€˜π‘…)) = (0gβ€˜π‘…))
7149, 69, 70syl2anc 585 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘₯ ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ (Baseβ€˜π‘…)) β†’ (π‘₯(.rβ€˜π‘…)(0gβ€˜π‘…)) = (0gβ€˜π‘…))
7268, 71sylan9eqr 2795 . . . . . . . . . . 11 (((πœ‘ ∧ π‘₯ ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ (Baseβ€˜π‘…)) ∧ 𝑦 = (0gβ€˜π‘…)) β†’ (π‘₯(.rβ€˜π‘…)𝑦) = (0gβ€˜π‘…))
7372fveq2d 6896 . . . . . . . . . 10 (((πœ‘ ∧ π‘₯ ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ (Baseβ€˜π‘…)) ∧ 𝑦 = (0gβ€˜π‘…)) β†’ (πΉβ€˜(π‘₯(.rβ€˜π‘…)𝑦)) = (πΉβ€˜(0gβ€˜π‘…)))
74 fveq2 6892 . . . . . . . . . . . . 13 (𝑦 = (0gβ€˜π‘…) β†’ (πΉβ€˜π‘¦) = (πΉβ€˜(0gβ€˜π‘…)))
7574, 45sylan9eqr 2795 . . . . . . . . . . . 12 (((πœ‘ ∧ π‘₯ ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ (Baseβ€˜π‘…)) ∧ 𝑦 = (0gβ€˜π‘…)) β†’ (πΉβ€˜π‘¦) = 0)
7675oveq2d 7425 . . . . . . . . . . 11 (((πœ‘ ∧ π‘₯ ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ (Baseβ€˜π‘…)) ∧ 𝑦 = (0gβ€˜π‘…)) β†’ ((πΉβ€˜π‘₯) Β· (πΉβ€˜π‘¦)) = ((πΉβ€˜π‘₯) Β· 0))
7760, 69ffvelcdmd 7088 . . . . . . . . . . . . . 14 ((πœ‘ ∧ π‘₯ ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ (Baseβ€˜π‘…)) β†’ (πΉβ€˜π‘₯) ∈ ℝ)
7877recnd 11242 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘₯ ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ (Baseβ€˜π‘…)) β†’ (πΉβ€˜π‘₯) ∈ β„‚)
7978adantr 482 . . . . . . . . . . . 12 (((πœ‘ ∧ π‘₯ ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ (Baseβ€˜π‘…)) ∧ 𝑦 = (0gβ€˜π‘…)) β†’ (πΉβ€˜π‘₯) ∈ β„‚)
8079mul01d 11413 . . . . . . . . . . 11 (((πœ‘ ∧ π‘₯ ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ (Baseβ€˜π‘…)) ∧ 𝑦 = (0gβ€˜π‘…)) β†’ ((πΉβ€˜π‘₯) Β· 0) = 0)
8176, 80eqtrd 2773 . . . . . . . . . 10 (((πœ‘ ∧ π‘₯ ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ (Baseβ€˜π‘…)) ∧ 𝑦 = (0gβ€˜π‘…)) β†’ ((πΉβ€˜π‘₯) Β· (πΉβ€˜π‘¦)) = 0)
8267, 73, 813eqtr4d 2783 . . . . . . . . 9 (((πœ‘ ∧ π‘₯ ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ (Baseβ€˜π‘…)) ∧ 𝑦 = (0gβ€˜π‘…)) β†’ (πΉβ€˜(π‘₯(.rβ€˜π‘…)𝑦)) = ((πΉβ€˜π‘₯) Β· (πΉβ€˜π‘¦)))
83 simpl1 1192 . . . . . . . . . . . . 13 (((πœ‘ ∧ π‘₯ ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ (Baseβ€˜π‘…)) ∧ (π‘₯ β‰  (0gβ€˜π‘…) ∧ 𝑦 β‰  (0gβ€˜π‘…))) β†’ πœ‘)
84 isabvd.t . . . . . . . . . . . . 13 (πœ‘ β†’ Β· = (.rβ€˜π‘…))
8583, 84syl 17 . . . . . . . . . . . 12 (((πœ‘ ∧ π‘₯ ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ (Baseβ€˜π‘…)) ∧ (π‘₯ β‰  (0gβ€˜π‘…) ∧ 𝑦 β‰  (0gβ€˜π‘…))) β†’ Β· = (.rβ€˜π‘…))
8685oveqd 7426 . . . . . . . . . . 11 (((πœ‘ ∧ π‘₯ ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ (Baseβ€˜π‘…)) ∧ (π‘₯ β‰  (0gβ€˜π‘…) ∧ 𝑦 β‰  (0gβ€˜π‘…))) β†’ (π‘₯ Β· 𝑦) = (π‘₯(.rβ€˜π‘…)𝑦))
8786fveq2d 6896 . . . . . . . . . 10 (((πœ‘ ∧ π‘₯ ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ (Baseβ€˜π‘…)) ∧ (π‘₯ β‰  (0gβ€˜π‘…) ∧ 𝑦 β‰  (0gβ€˜π‘…))) β†’ (πΉβ€˜(π‘₯ Β· 𝑦)) = (πΉβ€˜(π‘₯(.rβ€˜π‘…)𝑦)))
88 simpl2 1193 . . . . . . . . . . . 12 (((πœ‘ ∧ π‘₯ ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ (Baseβ€˜π‘…)) ∧ (π‘₯ β‰  (0gβ€˜π‘…) ∧ 𝑦 β‰  (0gβ€˜π‘…))) β†’ π‘₯ ∈ (Baseβ€˜π‘…))
8983, 2syl 17 . . . . . . . . . . . 12 (((πœ‘ ∧ π‘₯ ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ (Baseβ€˜π‘…)) ∧ (π‘₯ β‰  (0gβ€˜π‘…) ∧ 𝑦 β‰  (0gβ€˜π‘…))) β†’ 𝐡 = (Baseβ€˜π‘…))
9088, 89eleqtrrd 2837 . . . . . . . . . . 11 (((πœ‘ ∧ π‘₯ ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ (Baseβ€˜π‘…)) ∧ (π‘₯ β‰  (0gβ€˜π‘…) ∧ 𝑦 β‰  (0gβ€˜π‘…))) β†’ π‘₯ ∈ 𝐡)
91 simprl 770 . . . . . . . . . . . 12 (((πœ‘ ∧ π‘₯ ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ (Baseβ€˜π‘…)) ∧ (π‘₯ β‰  (0gβ€˜π‘…) ∧ 𝑦 β‰  (0gβ€˜π‘…))) β†’ π‘₯ β‰  (0gβ€˜π‘…))
9283, 8syl 17 . . . . . . . . . . . 12 (((πœ‘ ∧ π‘₯ ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ (Baseβ€˜π‘…)) ∧ (π‘₯ β‰  (0gβ€˜π‘…) ∧ 𝑦 β‰  (0gβ€˜π‘…))) β†’ 0 = (0gβ€˜π‘…))
9391, 92neeqtrrd 3016 . . . . . . . . . . 11 (((πœ‘ ∧ π‘₯ ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ (Baseβ€˜π‘…)) ∧ (π‘₯ β‰  (0gβ€˜π‘…) ∧ 𝑦 β‰  (0gβ€˜π‘…))) β†’ π‘₯ β‰  0 )
94 simpl3 1194 . . . . . . . . . . . 12 (((πœ‘ ∧ π‘₯ ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ (Baseβ€˜π‘…)) ∧ (π‘₯ β‰  (0gβ€˜π‘…) ∧ 𝑦 β‰  (0gβ€˜π‘…))) β†’ 𝑦 ∈ (Baseβ€˜π‘…))
9594, 89eleqtrrd 2837 . . . . . . . . . . 11 (((πœ‘ ∧ π‘₯ ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ (Baseβ€˜π‘…)) ∧ (π‘₯ β‰  (0gβ€˜π‘…) ∧ 𝑦 β‰  (0gβ€˜π‘…))) β†’ 𝑦 ∈ 𝐡)
96 simprr 772 . . . . . . . . . . . 12 (((πœ‘ ∧ π‘₯ ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ (Baseβ€˜π‘…)) ∧ (π‘₯ β‰  (0gβ€˜π‘…) ∧ 𝑦 β‰  (0gβ€˜π‘…))) β†’ 𝑦 β‰  (0gβ€˜π‘…))
9796, 92neeqtrrd 3016 . . . . . . . . . . 11 (((πœ‘ ∧ π‘₯ ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ (Baseβ€˜π‘…)) ∧ (π‘₯ β‰  (0gβ€˜π‘…) ∧ 𝑦 β‰  (0gβ€˜π‘…))) β†’ 𝑦 β‰  0 )
98 isabvd.5 . . . . . . . . . . 11 ((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ π‘₯ β‰  0 ) ∧ (𝑦 ∈ 𝐡 ∧ 𝑦 β‰  0 )) β†’ (πΉβ€˜(π‘₯ Β· 𝑦)) = ((πΉβ€˜π‘₯) Β· (πΉβ€˜π‘¦)))
9983, 90, 93, 95, 97, 98syl122anc 1380 . . . . . . . . . 10 (((πœ‘ ∧ π‘₯ ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ (Baseβ€˜π‘…)) ∧ (π‘₯ β‰  (0gβ€˜π‘…) ∧ 𝑦 β‰  (0gβ€˜π‘…))) β†’ (πΉβ€˜(π‘₯ Β· 𝑦)) = ((πΉβ€˜π‘₯) Β· (πΉβ€˜π‘¦)))
10087, 99eqtr3d 2775 . . . . . . . . 9 (((πœ‘ ∧ π‘₯ ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ (Baseβ€˜π‘…)) ∧ (π‘₯ β‰  (0gβ€˜π‘…) ∧ 𝑦 β‰  (0gβ€˜π‘…))) β†’ (πΉβ€˜(π‘₯(.rβ€˜π‘…)𝑦)) = ((πΉβ€˜π‘₯) Β· (πΉβ€˜π‘¦)))
10166, 82, 100pm2.61da2ne 3031 . . . . . . . 8 ((πœ‘ ∧ π‘₯ ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ (Baseβ€˜π‘…)) β†’ (πΉβ€˜(π‘₯(.rβ€˜π‘…)𝑦)) = ((πΉβ€˜π‘₯) Β· (πΉβ€˜π‘¦)))
102 oveq1 7416 . . . . . . . . . . . 12 (π‘₯ = (0gβ€˜π‘…) β†’ (π‘₯(+gβ€˜π‘…)𝑦) = ((0gβ€˜π‘…)(+gβ€˜π‘…)𝑦))
103 ringgrp 20061 . . . . . . . . . . . . . 14 (𝑅 ∈ Ring β†’ 𝑅 ∈ Grp)
10449, 103syl 17 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘₯ ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ (Baseβ€˜π‘…)) β†’ 𝑅 ∈ Grp)
105 eqid 2733 . . . . . . . . . . . . . 14 (+gβ€˜π‘…) = (+gβ€˜π‘…)
10651, 105, 53grplid 18852 . . . . . . . . . . . . 13 ((𝑅 ∈ Grp ∧ 𝑦 ∈ (Baseβ€˜π‘…)) β†’ ((0gβ€˜π‘…)(+gβ€˜π‘…)𝑦) = 𝑦)
107104, 50, 106syl2anc 585 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘₯ ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ (Baseβ€˜π‘…)) β†’ ((0gβ€˜π‘…)(+gβ€˜π‘…)𝑦) = 𝑦)
108102, 107sylan9eqr 2795 . . . . . . . . . . 11 (((πœ‘ ∧ π‘₯ ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ (Baseβ€˜π‘…)) ∧ π‘₯ = (0gβ€˜π‘…)) β†’ (π‘₯(+gβ€˜π‘…)𝑦) = 𝑦)
109108fveq2d 6896 . . . . . . . . . 10 (((πœ‘ ∧ π‘₯ ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ (Baseβ€˜π‘…)) ∧ π‘₯ = (0gβ€˜π‘…)) β†’ (πΉβ€˜(π‘₯(+gβ€˜π‘…)𝑦)) = (πΉβ€˜π‘¦))
1107, 58breqtrrid 5187 . . . . . . . . . . 11 (((πœ‘ ∧ π‘₯ ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ (Baseβ€˜π‘…)) ∧ π‘₯ = (0gβ€˜π‘…)) β†’ 0 ≀ (πΉβ€˜π‘₯))
11161, 77addge02d 11803 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘₯ ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ (Baseβ€˜π‘…)) β†’ (0 ≀ (πΉβ€˜π‘₯) ↔ (πΉβ€˜π‘¦) ≀ ((πΉβ€˜π‘₯) + (πΉβ€˜π‘¦))))
112111adantr 482 . . . . . . . . . . 11 (((πœ‘ ∧ π‘₯ ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ (Baseβ€˜π‘…)) ∧ π‘₯ = (0gβ€˜π‘…)) β†’ (0 ≀ (πΉβ€˜π‘₯) ↔ (πΉβ€˜π‘¦) ≀ ((πΉβ€˜π‘₯) + (πΉβ€˜π‘¦))))
113110, 112mpbid 231 . . . . . . . . . 10 (((πœ‘ ∧ π‘₯ ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ (Baseβ€˜π‘…)) ∧ π‘₯ = (0gβ€˜π‘…)) β†’ (πΉβ€˜π‘¦) ≀ ((πΉβ€˜π‘₯) + (πΉβ€˜π‘¦)))
114109, 113eqbrtrd 5171 . . . . . . . . 9 (((πœ‘ ∧ π‘₯ ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ (Baseβ€˜π‘…)) ∧ π‘₯ = (0gβ€˜π‘…)) β†’ (πΉβ€˜(π‘₯(+gβ€˜π‘…)𝑦)) ≀ ((πΉβ€˜π‘₯) + (πΉβ€˜π‘¦)))
115 oveq2 7417 . . . . . . . . . . . 12 (𝑦 = (0gβ€˜π‘…) β†’ (π‘₯(+gβ€˜π‘…)𝑦) = (π‘₯(+gβ€˜π‘…)(0gβ€˜π‘…)))
11651, 105, 53grprid 18853 . . . . . . . . . . . . 13 ((𝑅 ∈ Grp ∧ π‘₯ ∈ (Baseβ€˜π‘…)) β†’ (π‘₯(+gβ€˜π‘…)(0gβ€˜π‘…)) = π‘₯)
117104, 69, 116syl2anc 585 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘₯ ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ (Baseβ€˜π‘…)) β†’ (π‘₯(+gβ€˜π‘…)(0gβ€˜π‘…)) = π‘₯)
118115, 117sylan9eqr 2795 . . . . . . . . . . 11 (((πœ‘ ∧ π‘₯ ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ (Baseβ€˜π‘…)) ∧ 𝑦 = (0gβ€˜π‘…)) β†’ (π‘₯(+gβ€˜π‘…)𝑦) = π‘₯)
119118fveq2d 6896 . . . . . . . . . 10 (((πœ‘ ∧ π‘₯ ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ (Baseβ€˜π‘…)) ∧ 𝑦 = (0gβ€˜π‘…)) β†’ (πΉβ€˜(π‘₯(+gβ€˜π‘…)𝑦)) = (πΉβ€˜π‘₯))
1207, 75breqtrrid 5187 . . . . . . . . . . 11 (((πœ‘ ∧ π‘₯ ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ (Baseβ€˜π‘…)) ∧ 𝑦 = (0gβ€˜π‘…)) β†’ 0 ≀ (πΉβ€˜π‘¦))
12177, 61addge01d 11802 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘₯ ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ (Baseβ€˜π‘…)) β†’ (0 ≀ (πΉβ€˜π‘¦) ↔ (πΉβ€˜π‘₯) ≀ ((πΉβ€˜π‘₯) + (πΉβ€˜π‘¦))))
122121adantr 482 . . . . . . . . . . 11 (((πœ‘ ∧ π‘₯ ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ (Baseβ€˜π‘…)) ∧ 𝑦 = (0gβ€˜π‘…)) β†’ (0 ≀ (πΉβ€˜π‘¦) ↔ (πΉβ€˜π‘₯) ≀ ((πΉβ€˜π‘₯) + (πΉβ€˜π‘¦))))
123120, 122mpbid 231 . . . . . . . . . 10 (((πœ‘ ∧ π‘₯ ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ (Baseβ€˜π‘…)) ∧ 𝑦 = (0gβ€˜π‘…)) β†’ (πΉβ€˜π‘₯) ≀ ((πΉβ€˜π‘₯) + (πΉβ€˜π‘¦)))
124119, 123eqbrtrd 5171 . . . . . . . . 9 (((πœ‘ ∧ π‘₯ ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ (Baseβ€˜π‘…)) ∧ 𝑦 = (0gβ€˜π‘…)) β†’ (πΉβ€˜(π‘₯(+gβ€˜π‘…)𝑦)) ≀ ((πΉβ€˜π‘₯) + (πΉβ€˜π‘¦)))
125 isabvd.p . . . . . . . . . . . . 13 (πœ‘ β†’ + = (+gβ€˜π‘…))
12683, 125syl 17 . . . . . . . . . . . 12 (((πœ‘ ∧ π‘₯ ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ (Baseβ€˜π‘…)) ∧ (π‘₯ β‰  (0gβ€˜π‘…) ∧ 𝑦 β‰  (0gβ€˜π‘…))) β†’ + = (+gβ€˜π‘…))
127126oveqd 7426 . . . . . . . . . . 11 (((πœ‘ ∧ π‘₯ ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ (Baseβ€˜π‘…)) ∧ (π‘₯ β‰  (0gβ€˜π‘…) ∧ 𝑦 β‰  (0gβ€˜π‘…))) β†’ (π‘₯ + 𝑦) = (π‘₯(+gβ€˜π‘…)𝑦))
128127fveq2d 6896 . . . . . . . . . 10 (((πœ‘ ∧ π‘₯ ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ (Baseβ€˜π‘…)) ∧ (π‘₯ β‰  (0gβ€˜π‘…) ∧ 𝑦 β‰  (0gβ€˜π‘…))) β†’ (πΉβ€˜(π‘₯ + 𝑦)) = (πΉβ€˜(π‘₯(+gβ€˜π‘…)𝑦)))
129 isabvd.6 . . . . . . . . . . 11 ((πœ‘ ∧ (π‘₯ ∈ 𝐡 ∧ π‘₯ β‰  0 ) ∧ (𝑦 ∈ 𝐡 ∧ 𝑦 β‰  0 )) β†’ (πΉβ€˜(π‘₯ + 𝑦)) ≀ ((πΉβ€˜π‘₯) + (πΉβ€˜π‘¦)))
13083, 90, 93, 95, 97, 129syl122anc 1380 . . . . . . . . . 10 (((πœ‘ ∧ π‘₯ ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ (Baseβ€˜π‘…)) ∧ (π‘₯ β‰  (0gβ€˜π‘…) ∧ 𝑦 β‰  (0gβ€˜π‘…))) β†’ (πΉβ€˜(π‘₯ + 𝑦)) ≀ ((πΉβ€˜π‘₯) + (πΉβ€˜π‘¦)))
131128, 130eqbrtrrd 5173 . . . . . . . . 9 (((πœ‘ ∧ π‘₯ ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ (Baseβ€˜π‘…)) ∧ (π‘₯ β‰  (0gβ€˜π‘…) ∧ 𝑦 β‰  (0gβ€˜π‘…))) β†’ (πΉβ€˜(π‘₯(+gβ€˜π‘…)𝑦)) ≀ ((πΉβ€˜π‘₯) + (πΉβ€˜π‘¦)))
132114, 124, 131pm2.61da2ne 3031 . . . . . . . 8 ((πœ‘ ∧ π‘₯ ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ (Baseβ€˜π‘…)) β†’ (πΉβ€˜(π‘₯(+gβ€˜π‘…)𝑦)) ≀ ((πΉβ€˜π‘₯) + (πΉβ€˜π‘¦)))
133101, 132jca 513 . . . . . . 7 ((πœ‘ ∧ π‘₯ ∈ (Baseβ€˜π‘…) ∧ 𝑦 ∈ (Baseβ€˜π‘…)) β†’ ((πΉβ€˜(π‘₯(.rβ€˜π‘…)𝑦)) = ((πΉβ€˜π‘₯) Β· (πΉβ€˜π‘¦)) ∧ (πΉβ€˜(π‘₯(+gβ€˜π‘…)𝑦)) ≀ ((πΉβ€˜π‘₯) + (πΉβ€˜π‘¦))))
1341333expia 1122 . . . . . 6 ((πœ‘ ∧ π‘₯ ∈ (Baseβ€˜π‘…)) β†’ (𝑦 ∈ (Baseβ€˜π‘…) β†’ ((πΉβ€˜(π‘₯(.rβ€˜π‘…)𝑦)) = ((πΉβ€˜π‘₯) Β· (πΉβ€˜π‘¦)) ∧ (πΉβ€˜(π‘₯(+gβ€˜π‘…)𝑦)) ≀ ((πΉβ€˜π‘₯) + (πΉβ€˜π‘¦)))))
135134ralrimiv 3146 . . . . 5 ((πœ‘ ∧ π‘₯ ∈ (Baseβ€˜π‘…)) β†’ βˆ€π‘¦ ∈ (Baseβ€˜π‘…)((πΉβ€˜(π‘₯(.rβ€˜π‘…)𝑦)) = ((πΉβ€˜π‘₯) Β· (πΉβ€˜π‘¦)) ∧ (πΉβ€˜(π‘₯(+gβ€˜π‘…)𝑦)) ≀ ((πΉβ€˜π‘₯) + (πΉβ€˜π‘¦))))
13644, 135jca 513 . . . 4 ((πœ‘ ∧ π‘₯ ∈ (Baseβ€˜π‘…)) β†’ (((πΉβ€˜π‘₯) = 0 ↔ π‘₯ = (0gβ€˜π‘…)) ∧ βˆ€π‘¦ ∈ (Baseβ€˜π‘…)((πΉβ€˜(π‘₯(.rβ€˜π‘…)𝑦)) = ((πΉβ€˜π‘₯) Β· (πΉβ€˜π‘¦)) ∧ (πΉβ€˜(π‘₯(+gβ€˜π‘…)𝑦)) ≀ ((πΉβ€˜π‘₯) + (πΉβ€˜π‘¦)))))
137136ralrimiva 3147 . . 3 (πœ‘ β†’ βˆ€π‘₯ ∈ (Baseβ€˜π‘…)(((πΉβ€˜π‘₯) = 0 ↔ π‘₯ = (0gβ€˜π‘…)) ∧ βˆ€π‘¦ ∈ (Baseβ€˜π‘…)((πΉβ€˜(π‘₯(.rβ€˜π‘…)𝑦)) = ((πΉβ€˜π‘₯) Β· (πΉβ€˜π‘¦)) ∧ (πΉβ€˜(π‘₯(+gβ€˜π‘…)𝑦)) ≀ ((πΉβ€˜π‘₯) + (πΉβ€˜π‘¦)))))
138 eqid 2733 . . . . 5 (AbsValβ€˜π‘…) = (AbsValβ€˜π‘…)
139138, 51, 105, 52, 53isabv 20427 . . . 4 (𝑅 ∈ Ring β†’ (𝐹 ∈ (AbsValβ€˜π‘…) ↔ (𝐹:(Baseβ€˜π‘…)⟢(0[,)+∞) ∧ βˆ€π‘₯ ∈ (Baseβ€˜π‘…)(((πΉβ€˜π‘₯) = 0 ↔ π‘₯ = (0gβ€˜π‘…)) ∧ βˆ€π‘¦ ∈ (Baseβ€˜π‘…)((πΉβ€˜(π‘₯(.rβ€˜π‘…)𝑦)) = ((πΉβ€˜π‘₯) Β· (πΉβ€˜π‘¦)) ∧ (πΉβ€˜(π‘₯(+gβ€˜π‘…)𝑦)) ≀ ((πΉβ€˜π‘₯) + (πΉβ€˜π‘¦)))))))
14048, 139syl 17 . . 3 (πœ‘ β†’ (𝐹 ∈ (AbsValβ€˜π‘…) ↔ (𝐹:(Baseβ€˜π‘…)⟢(0[,)+∞) ∧ βˆ€π‘₯ ∈ (Baseβ€˜π‘…)(((πΉβ€˜π‘₯) = 0 ↔ π‘₯ = (0gβ€˜π‘…)) ∧ βˆ€π‘¦ ∈ (Baseβ€˜π‘…)((πΉβ€˜(π‘₯(.rβ€˜π‘…)𝑦)) = ((πΉβ€˜π‘₯) Β· (πΉβ€˜π‘¦)) ∧ (πΉβ€˜(π‘₯(+gβ€˜π‘…)𝑦)) ≀ ((πΉβ€˜π‘₯) + (πΉβ€˜π‘¦)))))))
14137, 137, 140mpbir2and 712 . 2 (πœ‘ β†’ 𝐹 ∈ (AbsValβ€˜π‘…))
142 isabvd.a . 2 (πœ‘ β†’ 𝐴 = (AbsValβ€˜π‘…))
143141, 142eleqtrrd 2837 1 (πœ‘ β†’ 𝐹 ∈ 𝐴)
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 397   ∧ w3a 1088   = wceq 1542   ∈ wcel 2107   β‰  wne 2941  βˆ€wral 3062   class class class wbr 5149   Fn wfn 6539  βŸΆwf 6540  β€˜cfv 6544  (class class class)co 7409  β„‚cc 11108  β„cr 11109  0cc0 11110   + caddc 11113   Β· cmul 11115  +∞cpnf 11245   < clt 11248   ≀ cle 11249  [,)cico 13326  Basecbs 17144  +gcplusg 17197  .rcmulr 17198  0gc0g 17385  Grpcgrp 18819  Ringcrg 20056  AbsValcabv 20424
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5300  ax-nul 5307  ax-pow 5364  ax-pr 5428  ax-un 7725  ax-cnex 11166  ax-resscn 11167  ax-1cn 11168  ax-icn 11169  ax-addcl 11170  ax-addrcl 11171  ax-mulcl 11172  ax-mulrcl 11173  ax-mulcom 11174  ax-addass 11175  ax-mulass 11176  ax-distr 11177  ax-i2m1 11178  ax-1ne0 11179  ax-1rid 11180  ax-rnegex 11181  ax-rrecex 11182  ax-cnre 11183  ax-pre-lttri 11184  ax-pre-lttrn 11185  ax-pre-ltadd 11186  ax-pre-mulgt0 11187
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rmo 3377  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-iun 5000  df-br 5150  df-opab 5212  df-mpt 5233  df-tr 5267  df-id 5575  df-eprel 5581  df-po 5589  df-so 5590  df-fr 5632  df-we 5634  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-pred 6301  df-ord 6368  df-on 6369  df-lim 6370  df-suc 6371  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551  df-fv 6552  df-riota 7365  df-ov 7412  df-oprab 7413  df-mpo 7414  df-om 7856  df-2nd 7976  df-frecs 8266  df-wrecs 8297  df-recs 8371  df-rdg 8410  df-er 8703  df-map 8822  df-en 8940  df-dom 8941  df-sdom 8942  df-pnf 11250  df-mnf 11251  df-xr 11252  df-ltxr 11253  df-le 11254  df-sub 11446  df-neg 11447  df-nn 12213  df-2 12275  df-ico 13330  df-sets 17097  df-slot 17115  df-ndx 17127  df-base 17145  df-plusg 17210  df-0g 17387  df-mgm 18561  df-sgrp 18610  df-mnd 18626  df-grp 18822  df-minusg 18823  df-mgp 19988  df-ring 20058  df-abv 20425
This theorem is referenced by:  abvres  20447  abvtrivd  20448  absabv  21002  abvcxp  27118  padicabv  27133
  Copyright terms: Public domain W3C validator