Step |
Hyp |
Ref |
Expression |
1 |
|
nmofval.1 |
⊢ 𝑁 = ( 𝑆 normOp 𝑇 ) |
2 |
|
elrege0 |
⊢ ( 𝑟 ∈ ( 0 [,) +∞ ) ↔ ( 𝑟 ∈ ℝ ∧ 0 ≤ 𝑟 ) ) |
3 |
2
|
simprbi |
⊢ ( 𝑟 ∈ ( 0 [,) +∞ ) → 0 ≤ 𝑟 ) |
4 |
3
|
adantl |
⊢ ( ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) ∧ 𝑟 ∈ ( 0 [,) +∞ ) ) → 0 ≤ 𝑟 ) |
5 |
4
|
a1d |
⊢ ( ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) ∧ 𝑟 ∈ ( 0 [,) +∞ ) ) → ( ∀ 𝑥 ∈ ( Base ‘ 𝑆 ) ( ( norm ‘ 𝑇 ) ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ ( 𝑟 · ( ( norm ‘ 𝑆 ) ‘ 𝑥 ) ) → 0 ≤ 𝑟 ) ) |
6 |
5
|
ralrimiva |
⊢ ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) → ∀ 𝑟 ∈ ( 0 [,) +∞ ) ( ∀ 𝑥 ∈ ( Base ‘ 𝑆 ) ( ( norm ‘ 𝑇 ) ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ ( 𝑟 · ( ( norm ‘ 𝑆 ) ‘ 𝑥 ) ) → 0 ≤ 𝑟 ) ) |
7 |
|
0xr |
⊢ 0 ∈ ℝ* |
8 |
|
eqid |
⊢ ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 ) |
9 |
|
eqid |
⊢ ( norm ‘ 𝑆 ) = ( norm ‘ 𝑆 ) |
10 |
|
eqid |
⊢ ( norm ‘ 𝑇 ) = ( norm ‘ 𝑇 ) |
11 |
1 8 9 10
|
nmogelb |
⊢ ( ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) ∧ 0 ∈ ℝ* ) → ( 0 ≤ ( 𝑁 ‘ 𝐹 ) ↔ ∀ 𝑟 ∈ ( 0 [,) +∞ ) ( ∀ 𝑥 ∈ ( Base ‘ 𝑆 ) ( ( norm ‘ 𝑇 ) ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ ( 𝑟 · ( ( norm ‘ 𝑆 ) ‘ 𝑥 ) ) → 0 ≤ 𝑟 ) ) ) |
12 |
7 11
|
mpan2 |
⊢ ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) → ( 0 ≤ ( 𝑁 ‘ 𝐹 ) ↔ ∀ 𝑟 ∈ ( 0 [,) +∞ ) ( ∀ 𝑥 ∈ ( Base ‘ 𝑆 ) ( ( norm ‘ 𝑇 ) ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ ( 𝑟 · ( ( norm ‘ 𝑆 ) ‘ 𝑥 ) ) → 0 ≤ 𝑟 ) ) ) |
13 |
6 12
|
mpbird |
⊢ ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) → 0 ≤ ( 𝑁 ‘ 𝐹 ) ) |