Step | Hyp | Ref
| Expression |
1 | | fveq2 6103 |
. . . 4
⊢ (𝑋 = (0g‘𝑆) → (𝐹‘𝑋) = (𝐹‘(0g‘𝑆))) |
2 | 1 | fveq2d 6107 |
. . 3
⊢ (𝑋 = (0g‘𝑆) → (𝑀‘(𝐹‘𝑋)) = (𝑀‘(𝐹‘(0g‘𝑆)))) |
3 | | fveq2 6103 |
. . . 4
⊢ (𝑋 = (0g‘𝑆) → (𝐿‘𝑋) = (𝐿‘(0g‘𝑆))) |
4 | 3 | oveq2d 6565 |
. . 3
⊢ (𝑋 = (0g‘𝑆) → ((𝑁‘𝐹) · (𝐿‘𝑋)) = ((𝑁‘𝐹) · (𝐿‘(0g‘𝑆)))) |
5 | 2, 4 | breq12d 4596 |
. 2
⊢ (𝑋 = (0g‘𝑆) → ((𝑀‘(𝐹‘𝑋)) ≤ ((𝑁‘𝐹) · (𝐿‘𝑋)) ↔ (𝑀‘(𝐹‘(0g‘𝑆))) ≤ ((𝑁‘𝐹) · (𝐿‘(0g‘𝑆))))) |
6 | | fveq2 6103 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑋 → (𝐹‘𝑥) = (𝐹‘𝑋)) |
7 | 6 | fveq2d 6107 |
. . . . . . . . 9
⊢ (𝑥 = 𝑋 → (𝑀‘(𝐹‘𝑥)) = (𝑀‘(𝐹‘𝑋))) |
8 | | fveq2 6103 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑋 → (𝐿‘𝑥) = (𝐿‘𝑋)) |
9 | 8 | oveq2d 6565 |
. . . . . . . . 9
⊢ (𝑥 = 𝑋 → (𝑟 · (𝐿‘𝑥)) = (𝑟 · (𝐿‘𝑋))) |
10 | 7, 9 | breq12d 4596 |
. . . . . . . 8
⊢ (𝑥 = 𝑋 → ((𝑀‘(𝐹‘𝑥)) ≤ (𝑟 · (𝐿‘𝑥)) ↔ (𝑀‘(𝐹‘𝑋)) ≤ (𝑟 · (𝐿‘𝑋)))) |
11 | 10 | rspcv 3278 |
. . . . . . 7
⊢ (𝑋 ∈ 𝑉 → (∀𝑥 ∈ 𝑉 (𝑀‘(𝐹‘𝑥)) ≤ (𝑟 · (𝐿‘𝑥)) → (𝑀‘(𝐹‘𝑋)) ≤ (𝑟 · (𝐿‘𝑋)))) |
12 | 11 | ad3antlr 763 |
. . . . . 6
⊢ ((((𝐹 ∈ (𝑆 NGHom 𝑇) ∧ 𝑋 ∈ 𝑉) ∧ 𝑋 ≠ (0g‘𝑆)) ∧ 𝑟 ∈ (0[,)+∞)) → (∀𝑥 ∈ 𝑉 (𝑀‘(𝐹‘𝑥)) ≤ (𝑟 · (𝐿‘𝑥)) → (𝑀‘(𝐹‘𝑋)) ≤ (𝑟 · (𝐿‘𝑋)))) |
13 | | nmofval.1 |
. . . . . . . . . . . . . 14
⊢ 𝑁 = (𝑆 normOp 𝑇) |
14 | 13 | isnghm 22337 |
. . . . . . . . . . . . 13
⊢ (𝐹 ∈ (𝑆 NGHom 𝑇) ↔ ((𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp) ∧ (𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ (𝑁‘𝐹) ∈ ℝ))) |
15 | 14 | simplbi 475 |
. . . . . . . . . . . 12
⊢ (𝐹 ∈ (𝑆 NGHom 𝑇) → (𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp)) |
16 | 15 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝐹 ∈ (𝑆 NGHom 𝑇) ∧ 𝑋 ∈ 𝑉) → (𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp)) |
17 | 16 | simprd 478 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ (𝑆 NGHom 𝑇) ∧ 𝑋 ∈ 𝑉) → 𝑇 ∈ NrmGrp) |
18 | 14 | simprbi 479 |
. . . . . . . . . . . . . 14
⊢ (𝐹 ∈ (𝑆 NGHom 𝑇) → (𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ (𝑁‘𝐹) ∈ ℝ)) |
19 | 18 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝐹 ∈ (𝑆 NGHom 𝑇) ∧ 𝑋 ∈ 𝑉) → (𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ (𝑁‘𝐹) ∈ ℝ)) |
20 | 19 | simpld 474 |
. . . . . . . . . . . 12
⊢ ((𝐹 ∈ (𝑆 NGHom 𝑇) ∧ 𝑋 ∈ 𝑉) → 𝐹 ∈ (𝑆 GrpHom 𝑇)) |
21 | | nmoi.2 |
. . . . . . . . . . . . 13
⊢ 𝑉 = (Base‘𝑆) |
22 | | eqid 2610 |
. . . . . . . . . . . . 13
⊢
(Base‘𝑇) =
(Base‘𝑇) |
23 | 21, 22 | ghmf 17487 |
. . . . . . . . . . . 12
⊢ (𝐹 ∈ (𝑆 GrpHom 𝑇) → 𝐹:𝑉⟶(Base‘𝑇)) |
24 | 20, 23 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝐹 ∈ (𝑆 NGHom 𝑇) ∧ 𝑋 ∈ 𝑉) → 𝐹:𝑉⟶(Base‘𝑇)) |
25 | | ffvelrn 6265 |
. . . . . . . . . . 11
⊢ ((𝐹:𝑉⟶(Base‘𝑇) ∧ 𝑋 ∈ 𝑉) → (𝐹‘𝑋) ∈ (Base‘𝑇)) |
26 | 24, 25 | sylancom 698 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ (𝑆 NGHom 𝑇) ∧ 𝑋 ∈ 𝑉) → (𝐹‘𝑋) ∈ (Base‘𝑇)) |
27 | | nmoi.4 |
. . . . . . . . . . 11
⊢ 𝑀 = (norm‘𝑇) |
28 | 22, 27 | nmcl 22230 |
. . . . . . . . . 10
⊢ ((𝑇 ∈ NrmGrp ∧ (𝐹‘𝑋) ∈ (Base‘𝑇)) → (𝑀‘(𝐹‘𝑋)) ∈ ℝ) |
29 | 17, 26, 28 | syl2anc 691 |
. . . . . . . . 9
⊢ ((𝐹 ∈ (𝑆 NGHom 𝑇) ∧ 𝑋 ∈ 𝑉) → (𝑀‘(𝐹‘𝑋)) ∈ ℝ) |
30 | 29 | adantr 480 |
. . . . . . . 8
⊢ (((𝐹 ∈ (𝑆 NGHom 𝑇) ∧ 𝑋 ∈ 𝑉) ∧ 𝑋 ≠ (0g‘𝑆)) → (𝑀‘(𝐹‘𝑋)) ∈ ℝ) |
31 | 30 | adantr 480 |
. . . . . . 7
⊢ ((((𝐹 ∈ (𝑆 NGHom 𝑇) ∧ 𝑋 ∈ 𝑉) ∧ 𝑋 ≠ (0g‘𝑆)) ∧ 𝑟 ∈ (0[,)+∞)) → (𝑀‘(𝐹‘𝑋)) ∈ ℝ) |
32 | | elrege0 12149 |
. . . . . . . . 9
⊢ (𝑟 ∈ (0[,)+∞) ↔
(𝑟 ∈ ℝ ∧ 0
≤ 𝑟)) |
33 | 32 | simplbi 475 |
. . . . . . . 8
⊢ (𝑟 ∈ (0[,)+∞) →
𝑟 ∈
ℝ) |
34 | 33 | adantl 481 |
. . . . . . 7
⊢ ((((𝐹 ∈ (𝑆 NGHom 𝑇) ∧ 𝑋 ∈ 𝑉) ∧ 𝑋 ≠ (0g‘𝑆)) ∧ 𝑟 ∈ (0[,)+∞)) → 𝑟 ∈
ℝ) |
35 | 16 | simpld 474 |
. . . . . . . . . . 11
⊢ ((𝐹 ∈ (𝑆 NGHom 𝑇) ∧ 𝑋 ∈ 𝑉) → 𝑆 ∈ NrmGrp) |
36 | | simpr 476 |
. . . . . . . . . . 11
⊢ ((𝐹 ∈ (𝑆 NGHom 𝑇) ∧ 𝑋 ∈ 𝑉) → 𝑋 ∈ 𝑉) |
37 | 35, 36 | jca 553 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ (𝑆 NGHom 𝑇) ∧ 𝑋 ∈ 𝑉) → (𝑆 ∈ NrmGrp ∧ 𝑋 ∈ 𝑉)) |
38 | | nmoi.3 |
. . . . . . . . . . . 12
⊢ 𝐿 = (norm‘𝑆) |
39 | | eqid 2610 |
. . . . . . . . . . . 12
⊢
(0g‘𝑆) = (0g‘𝑆) |
40 | 21, 38, 39 | nmrpcl 22234 |
. . . . . . . . . . 11
⊢ ((𝑆 ∈ NrmGrp ∧ 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ (0g‘𝑆)) → (𝐿‘𝑋) ∈
ℝ+) |
41 | 40 | 3expa 1257 |
. . . . . . . . . 10
⊢ (((𝑆 ∈ NrmGrp ∧ 𝑋 ∈ 𝑉) ∧ 𝑋 ≠ (0g‘𝑆)) → (𝐿‘𝑋) ∈
ℝ+) |
42 | 37, 41 | sylan 487 |
. . . . . . . . 9
⊢ (((𝐹 ∈ (𝑆 NGHom 𝑇) ∧ 𝑋 ∈ 𝑉) ∧ 𝑋 ≠ (0g‘𝑆)) → (𝐿‘𝑋) ∈
ℝ+) |
43 | 42 | rpregt0d 11754 |
. . . . . . . 8
⊢ (((𝐹 ∈ (𝑆 NGHom 𝑇) ∧ 𝑋 ∈ 𝑉) ∧ 𝑋 ≠ (0g‘𝑆)) → ((𝐿‘𝑋) ∈ ℝ ∧ 0 < (𝐿‘𝑋))) |
44 | 43 | adantr 480 |
. . . . . . 7
⊢ ((((𝐹 ∈ (𝑆 NGHom 𝑇) ∧ 𝑋 ∈ 𝑉) ∧ 𝑋 ≠ (0g‘𝑆)) ∧ 𝑟 ∈ (0[,)+∞)) → ((𝐿‘𝑋) ∈ ℝ ∧ 0 < (𝐿‘𝑋))) |
45 | | ledivmul2 10781 |
. . . . . . 7
⊢ (((𝑀‘(𝐹‘𝑋)) ∈ ℝ ∧ 𝑟 ∈ ℝ ∧ ((𝐿‘𝑋) ∈ ℝ ∧ 0 < (𝐿‘𝑋))) → (((𝑀‘(𝐹‘𝑋)) / (𝐿‘𝑋)) ≤ 𝑟 ↔ (𝑀‘(𝐹‘𝑋)) ≤ (𝑟 · (𝐿‘𝑋)))) |
46 | 31, 34, 44, 45 | syl3anc 1318 |
. . . . . 6
⊢ ((((𝐹 ∈ (𝑆 NGHom 𝑇) ∧ 𝑋 ∈ 𝑉) ∧ 𝑋 ≠ (0g‘𝑆)) ∧ 𝑟 ∈ (0[,)+∞)) → (((𝑀‘(𝐹‘𝑋)) / (𝐿‘𝑋)) ≤ 𝑟 ↔ (𝑀‘(𝐹‘𝑋)) ≤ (𝑟 · (𝐿‘𝑋)))) |
47 | 12, 46 | sylibrd 248 |
. . . . 5
⊢ ((((𝐹 ∈ (𝑆 NGHom 𝑇) ∧ 𝑋 ∈ 𝑉) ∧ 𝑋 ≠ (0g‘𝑆)) ∧ 𝑟 ∈ (0[,)+∞)) → (∀𝑥 ∈ 𝑉 (𝑀‘(𝐹‘𝑥)) ≤ (𝑟 · (𝐿‘𝑥)) → ((𝑀‘(𝐹‘𝑋)) / (𝐿‘𝑋)) ≤ 𝑟)) |
48 | 47 | ralrimiva 2949 |
. . . 4
⊢ (((𝐹 ∈ (𝑆 NGHom 𝑇) ∧ 𝑋 ∈ 𝑉) ∧ 𝑋 ≠ (0g‘𝑆)) → ∀𝑟 ∈ (0[,)+∞)(∀𝑥 ∈ 𝑉 (𝑀‘(𝐹‘𝑥)) ≤ (𝑟 · (𝐿‘𝑥)) → ((𝑀‘(𝐹‘𝑋)) / (𝐿‘𝑋)) ≤ 𝑟)) |
49 | 35 | adantr 480 |
. . . . 5
⊢ (((𝐹 ∈ (𝑆 NGHom 𝑇) ∧ 𝑋 ∈ 𝑉) ∧ 𝑋 ≠ (0g‘𝑆)) → 𝑆 ∈ NrmGrp) |
50 | 17 | adantr 480 |
. . . . 5
⊢ (((𝐹 ∈ (𝑆 NGHom 𝑇) ∧ 𝑋 ∈ 𝑉) ∧ 𝑋 ≠ (0g‘𝑆)) → 𝑇 ∈ NrmGrp) |
51 | 20 | adantr 480 |
. . . . 5
⊢ (((𝐹 ∈ (𝑆 NGHom 𝑇) ∧ 𝑋 ∈ 𝑉) ∧ 𝑋 ≠ (0g‘𝑆)) → 𝐹 ∈ (𝑆 GrpHom 𝑇)) |
52 | 30, 42 | rerpdivcld 11779 |
. . . . . 6
⊢ (((𝐹 ∈ (𝑆 NGHom 𝑇) ∧ 𝑋 ∈ 𝑉) ∧ 𝑋 ≠ (0g‘𝑆)) → ((𝑀‘(𝐹‘𝑋)) / (𝐿‘𝑋)) ∈ ℝ) |
53 | 52 | rexrd 9968 |
. . . . 5
⊢ (((𝐹 ∈ (𝑆 NGHom 𝑇) ∧ 𝑋 ∈ 𝑉) ∧ 𝑋 ≠ (0g‘𝑆)) → ((𝑀‘(𝐹‘𝑋)) / (𝐿‘𝑋)) ∈
ℝ*) |
54 | 13, 21, 38, 27 | nmogelb 22330 |
. . . . 5
⊢ (((𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ (𝑆 GrpHom 𝑇)) ∧ ((𝑀‘(𝐹‘𝑋)) / (𝐿‘𝑋)) ∈ ℝ*) →
(((𝑀‘(𝐹‘𝑋)) / (𝐿‘𝑋)) ≤ (𝑁‘𝐹) ↔ ∀𝑟 ∈ (0[,)+∞)(∀𝑥 ∈ 𝑉 (𝑀‘(𝐹‘𝑥)) ≤ (𝑟 · (𝐿‘𝑥)) → ((𝑀‘(𝐹‘𝑋)) / (𝐿‘𝑋)) ≤ 𝑟))) |
55 | 49, 50, 51, 53, 54 | syl31anc 1321 |
. . . 4
⊢ (((𝐹 ∈ (𝑆 NGHom 𝑇) ∧ 𝑋 ∈ 𝑉) ∧ 𝑋 ≠ (0g‘𝑆)) → (((𝑀‘(𝐹‘𝑋)) / (𝐿‘𝑋)) ≤ (𝑁‘𝐹) ↔ ∀𝑟 ∈ (0[,)+∞)(∀𝑥 ∈ 𝑉 (𝑀‘(𝐹‘𝑥)) ≤ (𝑟 · (𝐿‘𝑥)) → ((𝑀‘(𝐹‘𝑋)) / (𝐿‘𝑋)) ≤ 𝑟))) |
56 | 48, 55 | mpbird 246 |
. . 3
⊢ (((𝐹 ∈ (𝑆 NGHom 𝑇) ∧ 𝑋 ∈ 𝑉) ∧ 𝑋 ≠ (0g‘𝑆)) → ((𝑀‘(𝐹‘𝑋)) / (𝐿‘𝑋)) ≤ (𝑁‘𝐹)) |
57 | 19 | simprd 478 |
. . . . 5
⊢ ((𝐹 ∈ (𝑆 NGHom 𝑇) ∧ 𝑋 ∈ 𝑉) → (𝑁‘𝐹) ∈ ℝ) |
58 | 57 | adantr 480 |
. . . 4
⊢ (((𝐹 ∈ (𝑆 NGHom 𝑇) ∧ 𝑋 ∈ 𝑉) ∧ 𝑋 ≠ (0g‘𝑆)) → (𝑁‘𝐹) ∈ ℝ) |
59 | 30, 58, 42 | ledivmul2d 11802 |
. . 3
⊢ (((𝐹 ∈ (𝑆 NGHom 𝑇) ∧ 𝑋 ∈ 𝑉) ∧ 𝑋 ≠ (0g‘𝑆)) → (((𝑀‘(𝐹‘𝑋)) / (𝐿‘𝑋)) ≤ (𝑁‘𝐹) ↔ (𝑀‘(𝐹‘𝑋)) ≤ ((𝑁‘𝐹) · (𝐿‘𝑋)))) |
60 | 56, 59 | mpbid 221 |
. 2
⊢ (((𝐹 ∈ (𝑆 NGHom 𝑇) ∧ 𝑋 ∈ 𝑉) ∧ 𝑋 ≠ (0g‘𝑆)) → (𝑀‘(𝐹‘𝑋)) ≤ ((𝑁‘𝐹) · (𝐿‘𝑋))) |
61 | | eqid 2610 |
. . . . . . 7
⊢
(0g‘𝑇) = (0g‘𝑇) |
62 | 39, 61 | ghmid 17489 |
. . . . . 6
⊢ (𝐹 ∈ (𝑆 GrpHom 𝑇) → (𝐹‘(0g‘𝑆)) = (0g‘𝑇)) |
63 | 20, 62 | syl 17 |
. . . . 5
⊢ ((𝐹 ∈ (𝑆 NGHom 𝑇) ∧ 𝑋 ∈ 𝑉) → (𝐹‘(0g‘𝑆)) = (0g‘𝑇)) |
64 | 63 | fveq2d 6107 |
. . . 4
⊢ ((𝐹 ∈ (𝑆 NGHom 𝑇) ∧ 𝑋 ∈ 𝑉) → (𝑀‘(𝐹‘(0g‘𝑆))) = (𝑀‘(0g‘𝑇))) |
65 | 27, 61 | nm0 22243 |
. . . . 5
⊢ (𝑇 ∈ NrmGrp → (𝑀‘(0g‘𝑇)) = 0) |
66 | 17, 65 | syl 17 |
. . . 4
⊢ ((𝐹 ∈ (𝑆 NGHom 𝑇) ∧ 𝑋 ∈ 𝑉) → (𝑀‘(0g‘𝑇)) = 0) |
67 | 64, 66 | eqtrd 2644 |
. . 3
⊢ ((𝐹 ∈ (𝑆 NGHom 𝑇) ∧ 𝑋 ∈ 𝑉) → (𝑀‘(𝐹‘(0g‘𝑆))) = 0) |
68 | 38, 39 | nm0 22243 |
. . . . . 6
⊢ (𝑆 ∈ NrmGrp → (𝐿‘(0g‘𝑆)) = 0) |
69 | 35, 68 | syl 17 |
. . . . 5
⊢ ((𝐹 ∈ (𝑆 NGHom 𝑇) ∧ 𝑋 ∈ 𝑉) → (𝐿‘(0g‘𝑆)) = 0) |
70 | | 0re 9919 |
. . . . 5
⊢ 0 ∈
ℝ |
71 | 69, 70 | syl6eqel 2696 |
. . . 4
⊢ ((𝐹 ∈ (𝑆 NGHom 𝑇) ∧ 𝑋 ∈ 𝑉) → (𝐿‘(0g‘𝑆)) ∈
ℝ) |
72 | 13 | nmoge0 22335 |
. . . . 5
⊢ ((𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ (𝑆 GrpHom 𝑇)) → 0 ≤ (𝑁‘𝐹)) |
73 | 35, 17, 20, 72 | syl3anc 1318 |
. . . 4
⊢ ((𝐹 ∈ (𝑆 NGHom 𝑇) ∧ 𝑋 ∈ 𝑉) → 0 ≤ (𝑁‘𝐹)) |
74 | | 0le0 10987 |
. . . . 5
⊢ 0 ≤
0 |
75 | 74, 69 | syl5breqr 4621 |
. . . 4
⊢ ((𝐹 ∈ (𝑆 NGHom 𝑇) ∧ 𝑋 ∈ 𝑉) → 0 ≤ (𝐿‘(0g‘𝑆))) |
76 | 57, 71, 73, 75 | mulge0d 10483 |
. . 3
⊢ ((𝐹 ∈ (𝑆 NGHom 𝑇) ∧ 𝑋 ∈ 𝑉) → 0 ≤ ((𝑁‘𝐹) · (𝐿‘(0g‘𝑆)))) |
77 | 67, 76 | eqbrtrd 4605 |
. 2
⊢ ((𝐹 ∈ (𝑆 NGHom 𝑇) ∧ 𝑋 ∈ 𝑉) → (𝑀‘(𝐹‘(0g‘𝑆))) ≤ ((𝑁‘𝐹) · (𝐿‘(0g‘𝑆)))) |
78 | 5, 60, 77 | pm2.61ne 2867 |
1
⊢ ((𝐹 ∈ (𝑆 NGHom 𝑇) ∧ 𝑋 ∈ 𝑉) → (𝑀‘(𝐹‘𝑋)) ≤ ((𝑁‘𝐹) · (𝐿‘𝑋))) |