Step |
Hyp |
Ref |
Expression |
1 |
|
nmofval.1 |
⊢ 𝑁 = ( 𝑆 normOp 𝑇 ) |
2 |
|
nmoi.2 |
⊢ 𝑉 = ( Base ‘ 𝑆 ) |
3 |
|
nmoi.3 |
⊢ 𝐿 = ( norm ‘ 𝑆 ) |
4 |
|
nmoi.4 |
⊢ 𝑀 = ( norm ‘ 𝑇 ) |
5 |
|
nmoi2.z |
⊢ 0 = ( 0g ‘ 𝑆 ) |
6 |
|
simpl2 |
⊢ ( ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ) ) → 𝑇 ∈ NrmGrp ) |
7 |
|
simpl3 |
⊢ ( ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ) ) → 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) |
8 |
|
eqid |
⊢ ( Base ‘ 𝑇 ) = ( Base ‘ 𝑇 ) |
9 |
2 8
|
ghmf |
⊢ ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) → 𝐹 : 𝑉 ⟶ ( Base ‘ 𝑇 ) ) |
10 |
7 9
|
syl |
⊢ ( ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ) ) → 𝐹 : 𝑉 ⟶ ( Base ‘ 𝑇 ) ) |
11 |
|
simprl |
⊢ ( ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ) ) → 𝑋 ∈ 𝑉 ) |
12 |
10 11
|
ffvelrnd |
⊢ ( ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ) ) → ( 𝐹 ‘ 𝑋 ) ∈ ( Base ‘ 𝑇 ) ) |
13 |
8 4
|
nmcl |
⊢ ( ( 𝑇 ∈ NrmGrp ∧ ( 𝐹 ‘ 𝑋 ) ∈ ( Base ‘ 𝑇 ) ) → ( 𝑀 ‘ ( 𝐹 ‘ 𝑋 ) ) ∈ ℝ ) |
14 |
6 12 13
|
syl2anc |
⊢ ( ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ) ) → ( 𝑀 ‘ ( 𝐹 ‘ 𝑋 ) ) ∈ ℝ ) |
15 |
14
|
rexrd |
⊢ ( ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ) ) → ( 𝑀 ‘ ( 𝐹 ‘ 𝑋 ) ) ∈ ℝ* ) |
16 |
1
|
nmocl |
⊢ ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) → ( 𝑁 ‘ 𝐹 ) ∈ ℝ* ) |
17 |
16
|
adantr |
⊢ ( ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ) ) → ( 𝑁 ‘ 𝐹 ) ∈ ℝ* ) |
18 |
2 3 5
|
nmrpcl |
⊢ ( ( 𝑆 ∈ NrmGrp ∧ 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ) → ( 𝐿 ‘ 𝑋 ) ∈ ℝ+ ) |
19 |
18
|
3expb |
⊢ ( ( 𝑆 ∈ NrmGrp ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ) ) → ( 𝐿 ‘ 𝑋 ) ∈ ℝ+ ) |
20 |
19
|
3ad2antl1 |
⊢ ( ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ) ) → ( 𝐿 ‘ 𝑋 ) ∈ ℝ+ ) |
21 |
20
|
rpxrd |
⊢ ( ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ) ) → ( 𝐿 ‘ 𝑋 ) ∈ ℝ* ) |
22 |
17 21
|
xmulcld |
⊢ ( ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ) ) → ( ( 𝑁 ‘ 𝐹 ) ·e ( 𝐿 ‘ 𝑋 ) ) ∈ ℝ* ) |
23 |
20
|
rpreccld |
⊢ ( ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ) ) → ( 1 / ( 𝐿 ‘ 𝑋 ) ) ∈ ℝ+ ) |
24 |
23
|
rpxrd |
⊢ ( ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ) ) → ( 1 / ( 𝐿 ‘ 𝑋 ) ) ∈ ℝ* ) |
25 |
23
|
rpge0d |
⊢ ( ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ) ) → 0 ≤ ( 1 / ( 𝐿 ‘ 𝑋 ) ) ) |
26 |
24 25
|
jca |
⊢ ( ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ) ) → ( ( 1 / ( 𝐿 ‘ 𝑋 ) ) ∈ ℝ* ∧ 0 ≤ ( 1 / ( 𝐿 ‘ 𝑋 ) ) ) ) |
27 |
1 2 3 4
|
nmoix |
⊢ ( ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) ∧ 𝑋 ∈ 𝑉 ) → ( 𝑀 ‘ ( 𝐹 ‘ 𝑋 ) ) ≤ ( ( 𝑁 ‘ 𝐹 ) ·e ( 𝐿 ‘ 𝑋 ) ) ) |
28 |
27
|
adantrr |
⊢ ( ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ) ) → ( 𝑀 ‘ ( 𝐹 ‘ 𝑋 ) ) ≤ ( ( 𝑁 ‘ 𝐹 ) ·e ( 𝐿 ‘ 𝑋 ) ) ) |
29 |
|
xlemul1a |
⊢ ( ( ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑋 ) ) ∈ ℝ* ∧ ( ( 𝑁 ‘ 𝐹 ) ·e ( 𝐿 ‘ 𝑋 ) ) ∈ ℝ* ∧ ( ( 1 / ( 𝐿 ‘ 𝑋 ) ) ∈ ℝ* ∧ 0 ≤ ( 1 / ( 𝐿 ‘ 𝑋 ) ) ) ) ∧ ( 𝑀 ‘ ( 𝐹 ‘ 𝑋 ) ) ≤ ( ( 𝑁 ‘ 𝐹 ) ·e ( 𝐿 ‘ 𝑋 ) ) ) → ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑋 ) ) ·e ( 1 / ( 𝐿 ‘ 𝑋 ) ) ) ≤ ( ( ( 𝑁 ‘ 𝐹 ) ·e ( 𝐿 ‘ 𝑋 ) ) ·e ( 1 / ( 𝐿 ‘ 𝑋 ) ) ) ) |
30 |
15 22 26 28 29
|
syl31anc |
⊢ ( ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ) ) → ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑋 ) ) ·e ( 1 / ( 𝐿 ‘ 𝑋 ) ) ) ≤ ( ( ( 𝑁 ‘ 𝐹 ) ·e ( 𝐿 ‘ 𝑋 ) ) ·e ( 1 / ( 𝐿 ‘ 𝑋 ) ) ) ) |
31 |
23
|
rpred |
⊢ ( ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ) ) → ( 1 / ( 𝐿 ‘ 𝑋 ) ) ∈ ℝ ) |
32 |
|
rexmul |
⊢ ( ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑋 ) ) ∈ ℝ ∧ ( 1 / ( 𝐿 ‘ 𝑋 ) ) ∈ ℝ ) → ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑋 ) ) ·e ( 1 / ( 𝐿 ‘ 𝑋 ) ) ) = ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑋 ) ) · ( 1 / ( 𝐿 ‘ 𝑋 ) ) ) ) |
33 |
14 31 32
|
syl2anc |
⊢ ( ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ) ) → ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑋 ) ) ·e ( 1 / ( 𝐿 ‘ 𝑋 ) ) ) = ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑋 ) ) · ( 1 / ( 𝐿 ‘ 𝑋 ) ) ) ) |
34 |
14
|
recnd |
⊢ ( ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ) ) → ( 𝑀 ‘ ( 𝐹 ‘ 𝑋 ) ) ∈ ℂ ) |
35 |
20
|
rpcnd |
⊢ ( ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ) ) → ( 𝐿 ‘ 𝑋 ) ∈ ℂ ) |
36 |
20
|
rpne0d |
⊢ ( ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ) ) → ( 𝐿 ‘ 𝑋 ) ≠ 0 ) |
37 |
34 35 36
|
divrecd |
⊢ ( ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ) ) → ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑋 ) ) / ( 𝐿 ‘ 𝑋 ) ) = ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑋 ) ) · ( 1 / ( 𝐿 ‘ 𝑋 ) ) ) ) |
38 |
33 37
|
eqtr4d |
⊢ ( ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ) ) → ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑋 ) ) ·e ( 1 / ( 𝐿 ‘ 𝑋 ) ) ) = ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑋 ) ) / ( 𝐿 ‘ 𝑋 ) ) ) |
39 |
|
xmulass |
⊢ ( ( ( 𝑁 ‘ 𝐹 ) ∈ ℝ* ∧ ( 𝐿 ‘ 𝑋 ) ∈ ℝ* ∧ ( 1 / ( 𝐿 ‘ 𝑋 ) ) ∈ ℝ* ) → ( ( ( 𝑁 ‘ 𝐹 ) ·e ( 𝐿 ‘ 𝑋 ) ) ·e ( 1 / ( 𝐿 ‘ 𝑋 ) ) ) = ( ( 𝑁 ‘ 𝐹 ) ·e ( ( 𝐿 ‘ 𝑋 ) ·e ( 1 / ( 𝐿 ‘ 𝑋 ) ) ) ) ) |
40 |
17 21 24 39
|
syl3anc |
⊢ ( ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ) ) → ( ( ( 𝑁 ‘ 𝐹 ) ·e ( 𝐿 ‘ 𝑋 ) ) ·e ( 1 / ( 𝐿 ‘ 𝑋 ) ) ) = ( ( 𝑁 ‘ 𝐹 ) ·e ( ( 𝐿 ‘ 𝑋 ) ·e ( 1 / ( 𝐿 ‘ 𝑋 ) ) ) ) ) |
41 |
20
|
rpred |
⊢ ( ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ) ) → ( 𝐿 ‘ 𝑋 ) ∈ ℝ ) |
42 |
|
rexmul |
⊢ ( ( ( 𝐿 ‘ 𝑋 ) ∈ ℝ ∧ ( 1 / ( 𝐿 ‘ 𝑋 ) ) ∈ ℝ ) → ( ( 𝐿 ‘ 𝑋 ) ·e ( 1 / ( 𝐿 ‘ 𝑋 ) ) ) = ( ( 𝐿 ‘ 𝑋 ) · ( 1 / ( 𝐿 ‘ 𝑋 ) ) ) ) |
43 |
41 31 42
|
syl2anc |
⊢ ( ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ) ) → ( ( 𝐿 ‘ 𝑋 ) ·e ( 1 / ( 𝐿 ‘ 𝑋 ) ) ) = ( ( 𝐿 ‘ 𝑋 ) · ( 1 / ( 𝐿 ‘ 𝑋 ) ) ) ) |
44 |
35 36
|
recidd |
⊢ ( ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ) ) → ( ( 𝐿 ‘ 𝑋 ) · ( 1 / ( 𝐿 ‘ 𝑋 ) ) ) = 1 ) |
45 |
43 44
|
eqtrd |
⊢ ( ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ) ) → ( ( 𝐿 ‘ 𝑋 ) ·e ( 1 / ( 𝐿 ‘ 𝑋 ) ) ) = 1 ) |
46 |
45
|
oveq2d |
⊢ ( ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ) ) → ( ( 𝑁 ‘ 𝐹 ) ·e ( ( 𝐿 ‘ 𝑋 ) ·e ( 1 / ( 𝐿 ‘ 𝑋 ) ) ) ) = ( ( 𝑁 ‘ 𝐹 ) ·e 1 ) ) |
47 |
|
xmulid1 |
⊢ ( ( 𝑁 ‘ 𝐹 ) ∈ ℝ* → ( ( 𝑁 ‘ 𝐹 ) ·e 1 ) = ( 𝑁 ‘ 𝐹 ) ) |
48 |
17 47
|
syl |
⊢ ( ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ) ) → ( ( 𝑁 ‘ 𝐹 ) ·e 1 ) = ( 𝑁 ‘ 𝐹 ) ) |
49 |
40 46 48
|
3eqtrd |
⊢ ( ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ) ) → ( ( ( 𝑁 ‘ 𝐹 ) ·e ( 𝐿 ‘ 𝑋 ) ) ·e ( 1 / ( 𝐿 ‘ 𝑋 ) ) ) = ( 𝑁 ‘ 𝐹 ) ) |
50 |
30 38 49
|
3brtr3d |
⊢ ( ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ∧ 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ) ) → ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑋 ) ) / ( 𝐿 ‘ 𝑋 ) ) ≤ ( 𝑁 ‘ 𝐹 ) ) |