Proof of Theorem nmoix
Step | Hyp | Ref
| Expression |
1 | | nmofval.1 |
. . . . . . 7
⊢ 𝑁 = (𝑆 normOp 𝑇) |
2 | 1 | isnghm2 23470 |
. . . . . 6
⊢ ((𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ (𝑆 GrpHom 𝑇)) → (𝐹 ∈ (𝑆 NGHom 𝑇) ↔ (𝑁‘𝐹) ∈ ℝ)) |
3 | 2 | biimpar 481 |
. . . . 5
⊢ (((𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ (𝑆 GrpHom 𝑇)) ∧ (𝑁‘𝐹) ∈ ℝ) → 𝐹 ∈ (𝑆 NGHom 𝑇)) |
4 | | nmoi.2 |
. . . . . 6
⊢ 𝑉 = (Base‘𝑆) |
5 | | nmoi.3 |
. . . . . 6
⊢ 𝐿 = (norm‘𝑆) |
6 | | nmoi.4 |
. . . . . 6
⊢ 𝑀 = (norm‘𝑇) |
7 | 1, 4, 5, 6 | nmoi 23474 |
. . . . 5
⊢ ((𝐹 ∈ (𝑆 NGHom 𝑇) ∧ 𝑋 ∈ 𝑉) → (𝑀‘(𝐹‘𝑋)) ≤ ((𝑁‘𝐹) · (𝐿‘𝑋))) |
8 | 3, 7 | sylan 583 |
. . . 4
⊢ ((((𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ (𝑆 GrpHom 𝑇)) ∧ (𝑁‘𝐹) ∈ ℝ) ∧ 𝑋 ∈ 𝑉) → (𝑀‘(𝐹‘𝑋)) ≤ ((𝑁‘𝐹) · (𝐿‘𝑋))) |
9 | 8 | an32s 652 |
. . 3
⊢ ((((𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ (𝑆 GrpHom 𝑇)) ∧ 𝑋 ∈ 𝑉) ∧ (𝑁‘𝐹) ∈ ℝ) → (𝑀‘(𝐹‘𝑋)) ≤ ((𝑁‘𝐹) · (𝐿‘𝑋))) |
10 | | id 22 |
. . . 4
⊢ ((𝑁‘𝐹) ∈ ℝ → (𝑁‘𝐹) ∈ ℝ) |
11 | 4, 5 | nmcl 23362 |
. . . . 5
⊢ ((𝑆 ∈ NrmGrp ∧ 𝑋 ∈ 𝑉) → (𝐿‘𝑋) ∈ ℝ) |
12 | 11 | 3ad2antl1 1186 |
. . . 4
⊢ (((𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ (𝑆 GrpHom 𝑇)) ∧ 𝑋 ∈ 𝑉) → (𝐿‘𝑋) ∈ ℝ) |
13 | | rexmul 12740 |
. . . 4
⊢ (((𝑁‘𝐹) ∈ ℝ ∧ (𝐿‘𝑋) ∈ ℝ) → ((𝑁‘𝐹) ·e (𝐿‘𝑋)) = ((𝑁‘𝐹) · (𝐿‘𝑋))) |
14 | 10, 12, 13 | syl2anr 600 |
. . 3
⊢ ((((𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ (𝑆 GrpHom 𝑇)) ∧ 𝑋 ∈ 𝑉) ∧ (𝑁‘𝐹) ∈ ℝ) → ((𝑁‘𝐹) ·e (𝐿‘𝑋)) = ((𝑁‘𝐹) · (𝐿‘𝑋))) |
15 | 9, 14 | breqtrrd 5055 |
. 2
⊢ ((((𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ (𝑆 GrpHom 𝑇)) ∧ 𝑋 ∈ 𝑉) ∧ (𝑁‘𝐹) ∈ ℝ) → (𝑀‘(𝐹‘𝑋)) ≤ ((𝑁‘𝐹) ·e (𝐿‘𝑋))) |
16 | | fveq2 6668 |
. . . . . . 7
⊢ (𝑋 = (0g‘𝑆) → (𝐹‘𝑋) = (𝐹‘(0g‘𝑆))) |
17 | 16 | fveq2d 6672 |
. . . . . 6
⊢ (𝑋 = (0g‘𝑆) → (𝑀‘(𝐹‘𝑋)) = (𝑀‘(𝐹‘(0g‘𝑆)))) |
18 | | fveq2 6668 |
. . . . . . 7
⊢ (𝑋 = (0g‘𝑆) → (𝐿‘𝑋) = (𝐿‘(0g‘𝑆))) |
19 | 18 | oveq2d 7180 |
. . . . . 6
⊢ (𝑋 = (0g‘𝑆) → (+∞
·e (𝐿‘𝑋)) = (+∞ ·e (𝐿‘(0g‘𝑆)))) |
20 | 17, 19 | breq12d 5040 |
. . . . 5
⊢ (𝑋 = (0g‘𝑆) → ((𝑀‘(𝐹‘𝑋)) ≤ (+∞ ·e
(𝐿‘𝑋)) ↔ (𝑀‘(𝐹‘(0g‘𝑆))) ≤ (+∞
·e (𝐿‘(0g‘𝑆))))) |
21 | | simpl2 1193 |
. . . . . . . . . 10
⊢ (((𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ (𝑆 GrpHom 𝑇)) ∧ 𝑋 ∈ 𝑉) → 𝑇 ∈ NrmGrp) |
22 | | eqid 2738 |
. . . . . . . . . . . . 13
⊢
(Base‘𝑇) =
(Base‘𝑇) |
23 | 4, 22 | ghmf 18473 |
. . . . . . . . . . . 12
⊢ (𝐹 ∈ (𝑆 GrpHom 𝑇) → 𝐹:𝑉⟶(Base‘𝑇)) |
24 | 23 | ffvelrnda 6855 |
. . . . . . . . . . 11
⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝑋 ∈ 𝑉) → (𝐹‘𝑋) ∈ (Base‘𝑇)) |
25 | 24 | 3ad2antl3 1188 |
. . . . . . . . . 10
⊢ (((𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ (𝑆 GrpHom 𝑇)) ∧ 𝑋 ∈ 𝑉) → (𝐹‘𝑋) ∈ (Base‘𝑇)) |
26 | 22, 6 | nmcl 23362 |
. . . . . . . . . 10
⊢ ((𝑇 ∈ NrmGrp ∧ (𝐹‘𝑋) ∈ (Base‘𝑇)) → (𝑀‘(𝐹‘𝑋)) ∈ ℝ) |
27 | 21, 25, 26 | syl2anc 587 |
. . . . . . . . 9
⊢ (((𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ (𝑆 GrpHom 𝑇)) ∧ 𝑋 ∈ 𝑉) → (𝑀‘(𝐹‘𝑋)) ∈ ℝ) |
28 | 27 | adantr 484 |
. . . . . . . 8
⊢ ((((𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ (𝑆 GrpHom 𝑇)) ∧ 𝑋 ∈ 𝑉) ∧ 𝑋 ≠ (0g‘𝑆)) → (𝑀‘(𝐹‘𝑋)) ∈ ℝ) |
29 | 28 | rexrd 10762 |
. . . . . . 7
⊢ ((((𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ (𝑆 GrpHom 𝑇)) ∧ 𝑋 ∈ 𝑉) ∧ 𝑋 ≠ (0g‘𝑆)) → (𝑀‘(𝐹‘𝑋)) ∈
ℝ*) |
30 | | pnfge 12601 |
. . . . . . 7
⊢ ((𝑀‘(𝐹‘𝑋)) ∈ ℝ* → (𝑀‘(𝐹‘𝑋)) ≤ +∞) |
31 | 29, 30 | syl 17 |
. . . . . 6
⊢ ((((𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ (𝑆 GrpHom 𝑇)) ∧ 𝑋 ∈ 𝑉) ∧ 𝑋 ≠ (0g‘𝑆)) → (𝑀‘(𝐹‘𝑋)) ≤ +∞) |
32 | | simp1 1137 |
. . . . . . . 8
⊢ ((𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ (𝑆 GrpHom 𝑇)) → 𝑆 ∈ NrmGrp) |
33 | | eqid 2738 |
. . . . . . . . . 10
⊢
(0g‘𝑆) = (0g‘𝑆) |
34 | 4, 5, 33 | nmrpcl 23366 |
. . . . . . . . 9
⊢ ((𝑆 ∈ NrmGrp ∧ 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ (0g‘𝑆)) → (𝐿‘𝑋) ∈
ℝ+) |
35 | 34 | 3expa 1119 |
. . . . . . . 8
⊢ (((𝑆 ∈ NrmGrp ∧ 𝑋 ∈ 𝑉) ∧ 𝑋 ≠ (0g‘𝑆)) → (𝐿‘𝑋) ∈
ℝ+) |
36 | 32, 35 | sylanl1 680 |
. . . . . . 7
⊢ ((((𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ (𝑆 GrpHom 𝑇)) ∧ 𝑋 ∈ 𝑉) ∧ 𝑋 ≠ (0g‘𝑆)) → (𝐿‘𝑋) ∈
ℝ+) |
37 | | rpxr 12474 |
. . . . . . . 8
⊢ ((𝐿‘𝑋) ∈ ℝ+ → (𝐿‘𝑋) ∈
ℝ*) |
38 | | rpgt0 12477 |
. . . . . . . 8
⊢ ((𝐿‘𝑋) ∈ ℝ+ → 0 <
(𝐿‘𝑋)) |
39 | | xmulpnf2 12744 |
. . . . . . . 8
⊢ (((𝐿‘𝑋) ∈ ℝ* ∧ 0 <
(𝐿‘𝑋)) → (+∞ ·e
(𝐿‘𝑋)) = +∞) |
40 | 37, 38, 39 | syl2anc 587 |
. . . . . . 7
⊢ ((𝐿‘𝑋) ∈ ℝ+ →
(+∞ ·e (𝐿‘𝑋)) = +∞) |
41 | 36, 40 | syl 17 |
. . . . . 6
⊢ ((((𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ (𝑆 GrpHom 𝑇)) ∧ 𝑋 ∈ 𝑉) ∧ 𝑋 ≠ (0g‘𝑆)) → (+∞ ·e
(𝐿‘𝑋)) = +∞) |
42 | 31, 41 | breqtrrd 5055 |
. . . . 5
⊢ ((((𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ (𝑆 GrpHom 𝑇)) ∧ 𝑋 ∈ 𝑉) ∧ 𝑋 ≠ (0g‘𝑆)) → (𝑀‘(𝐹‘𝑋)) ≤ (+∞ ·e
(𝐿‘𝑋))) |
43 | | 0le0 11810 |
. . . . . 6
⊢ 0 ≤
0 |
44 | | simpl3 1194 |
. . . . . . . . . 10
⊢ (((𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ (𝑆 GrpHom 𝑇)) ∧ 𝑋 ∈ 𝑉) → 𝐹 ∈ (𝑆 GrpHom 𝑇)) |
45 | | eqid 2738 |
. . . . . . . . . . 11
⊢
(0g‘𝑇) = (0g‘𝑇) |
46 | 33, 45 | ghmid 18475 |
. . . . . . . . . 10
⊢ (𝐹 ∈ (𝑆 GrpHom 𝑇) → (𝐹‘(0g‘𝑆)) = (0g‘𝑇)) |
47 | 44, 46 | syl 17 |
. . . . . . . . 9
⊢ (((𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ (𝑆 GrpHom 𝑇)) ∧ 𝑋 ∈ 𝑉) → (𝐹‘(0g‘𝑆)) = (0g‘𝑇)) |
48 | 47 | fveq2d 6672 |
. . . . . . . 8
⊢ (((𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ (𝑆 GrpHom 𝑇)) ∧ 𝑋 ∈ 𝑉) → (𝑀‘(𝐹‘(0g‘𝑆))) = (𝑀‘(0g‘𝑇))) |
49 | 6, 45 | nm0 23375 |
. . . . . . . . 9
⊢ (𝑇 ∈ NrmGrp → (𝑀‘(0g‘𝑇)) = 0) |
50 | 21, 49 | syl 17 |
. . . . . . . 8
⊢ (((𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ (𝑆 GrpHom 𝑇)) ∧ 𝑋 ∈ 𝑉) → (𝑀‘(0g‘𝑇)) = 0) |
51 | 48, 50 | eqtrd 2773 |
. . . . . . 7
⊢ (((𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ (𝑆 GrpHom 𝑇)) ∧ 𝑋 ∈ 𝑉) → (𝑀‘(𝐹‘(0g‘𝑆))) = 0) |
52 | | simpl1 1192 |
. . . . . . . . . 10
⊢ (((𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ (𝑆 GrpHom 𝑇)) ∧ 𝑋 ∈ 𝑉) → 𝑆 ∈ NrmGrp) |
53 | 5, 33 | nm0 23375 |
. . . . . . . . . 10
⊢ (𝑆 ∈ NrmGrp → (𝐿‘(0g‘𝑆)) = 0) |
54 | 52, 53 | syl 17 |
. . . . . . . . 9
⊢ (((𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ (𝑆 GrpHom 𝑇)) ∧ 𝑋 ∈ 𝑉) → (𝐿‘(0g‘𝑆)) = 0) |
55 | 54 | oveq2d 7180 |
. . . . . . . 8
⊢ (((𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ (𝑆 GrpHom 𝑇)) ∧ 𝑋 ∈ 𝑉) → (+∞ ·e
(𝐿‘(0g‘𝑆))) = (+∞
·e 0)) |
56 | | pnfxr 10766 |
. . . . . . . . 9
⊢ +∞
∈ ℝ* |
57 | | xmul01 12736 |
. . . . . . . . 9
⊢ (+∞
∈ ℝ* → (+∞ ·e 0) =
0) |
58 | 56, 57 | ax-mp 5 |
. . . . . . . 8
⊢ (+∞
·e 0) = 0 |
59 | 55, 58 | eqtrdi 2789 |
. . . . . . 7
⊢ (((𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ (𝑆 GrpHom 𝑇)) ∧ 𝑋 ∈ 𝑉) → (+∞ ·e
(𝐿‘(0g‘𝑆))) = 0) |
60 | 51, 59 | breq12d 5040 |
. . . . . 6
⊢ (((𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ (𝑆 GrpHom 𝑇)) ∧ 𝑋 ∈ 𝑉) → ((𝑀‘(𝐹‘(0g‘𝑆))) ≤ (+∞
·e (𝐿‘(0g‘𝑆))) ↔ 0 ≤
0)) |
61 | 43, 60 | mpbiri 261 |
. . . . 5
⊢ (((𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ (𝑆 GrpHom 𝑇)) ∧ 𝑋 ∈ 𝑉) → (𝑀‘(𝐹‘(0g‘𝑆))) ≤ (+∞
·e (𝐿‘(0g‘𝑆)))) |
62 | 20, 42, 61 | pm2.61ne 3019 |
. . . 4
⊢ (((𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ (𝑆 GrpHom 𝑇)) ∧ 𝑋 ∈ 𝑉) → (𝑀‘(𝐹‘𝑋)) ≤ (+∞ ·e
(𝐿‘𝑋))) |
63 | 62 | adantr 484 |
. . 3
⊢ ((((𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ (𝑆 GrpHom 𝑇)) ∧ 𝑋 ∈ 𝑉) ∧ (𝑁‘𝐹) = +∞) → (𝑀‘(𝐹‘𝑋)) ≤ (+∞ ·e
(𝐿‘𝑋))) |
64 | | simpr 488 |
. . . 4
⊢ ((((𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ (𝑆 GrpHom 𝑇)) ∧ 𝑋 ∈ 𝑉) ∧ (𝑁‘𝐹) = +∞) → (𝑁‘𝐹) = +∞) |
65 | 64 | oveq1d 7179 |
. . 3
⊢ ((((𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ (𝑆 GrpHom 𝑇)) ∧ 𝑋 ∈ 𝑉) ∧ (𝑁‘𝐹) = +∞) → ((𝑁‘𝐹) ·e (𝐿‘𝑋)) = (+∞ ·e (𝐿‘𝑋))) |
66 | 63, 65 | breqtrrd 5055 |
. 2
⊢ ((((𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ (𝑆 GrpHom 𝑇)) ∧ 𝑋 ∈ 𝑉) ∧ (𝑁‘𝐹) = +∞) → (𝑀‘(𝐹‘𝑋)) ≤ ((𝑁‘𝐹) ·e (𝐿‘𝑋))) |
67 | 1 | nmocl 23466 |
. . . . 5
⊢ ((𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ (𝑆 GrpHom 𝑇)) → (𝑁‘𝐹) ∈
ℝ*) |
68 | 1 | nmoge0 23467 |
. . . . . 6
⊢ ((𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ (𝑆 GrpHom 𝑇)) → 0 ≤ (𝑁‘𝐹)) |
69 | | ge0nemnf 12642 |
. . . . . 6
⊢ (((𝑁‘𝐹) ∈ ℝ* ∧ 0 ≤
(𝑁‘𝐹)) → (𝑁‘𝐹) ≠ -∞) |
70 | 67, 68, 69 | syl2anc 587 |
. . . . 5
⊢ ((𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ (𝑆 GrpHom 𝑇)) → (𝑁‘𝐹) ≠ -∞) |
71 | 67, 70 | jca 515 |
. . . 4
⊢ ((𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ (𝑆 GrpHom 𝑇)) → ((𝑁‘𝐹) ∈ ℝ* ∧ (𝑁‘𝐹) ≠ -∞)) |
72 | | xrnemnf 12588 |
. . . 4
⊢ (((𝑁‘𝐹) ∈ ℝ* ∧ (𝑁‘𝐹) ≠ -∞) ↔ ((𝑁‘𝐹) ∈ ℝ ∨ (𝑁‘𝐹) = +∞)) |
73 | 71, 72 | sylib 221 |
. . 3
⊢ ((𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ (𝑆 GrpHom 𝑇)) → ((𝑁‘𝐹) ∈ ℝ ∨ (𝑁‘𝐹) = +∞)) |
74 | 73 | adantr 484 |
. 2
⊢ (((𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ (𝑆 GrpHom 𝑇)) ∧ 𝑋 ∈ 𝑉) → ((𝑁‘𝐹) ∈ ℝ ∨ (𝑁‘𝐹) = +∞)) |
75 | 15, 66, 74 | mpjaodan 958 |
1
⊢ (((𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ (𝑆 GrpHom 𝑇)) ∧ 𝑋 ∈ 𝑉) → (𝑀‘(𝐹‘𝑋)) ≤ ((𝑁‘𝐹) ·e (𝐿‘𝑋))) |