Step |
Hyp |
Ref |
Expression |
1 |
|
nmofval.1 |
⊢ 𝑁 = ( 𝑆 normOp 𝑇 ) |
2 |
1
|
nghmfval |
⊢ ( 𝑆 NGHom 𝑇 ) = ( ◡ 𝑁 “ ℝ ) |
3 |
2
|
eleq2i |
⊢ ( 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) ↔ 𝐹 ∈ ( ◡ 𝑁 “ ℝ ) ) |
4 |
|
n0i |
⊢ ( 𝐹 ∈ ( ◡ 𝑁 “ ℝ ) → ¬ ( ◡ 𝑁 “ ℝ ) = ∅ ) |
5 |
|
nmoffn |
⊢ normOp Fn ( NrmGrp × NrmGrp ) |
6 |
5
|
fndmi |
⊢ dom normOp = ( NrmGrp × NrmGrp ) |
7 |
6
|
ndmov |
⊢ ( ¬ ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ) → ( 𝑆 normOp 𝑇 ) = ∅ ) |
8 |
1 7
|
syl5eq |
⊢ ( ¬ ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ) → 𝑁 = ∅ ) |
9 |
8
|
cnveqd |
⊢ ( ¬ ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ) → ◡ 𝑁 = ◡ ∅ ) |
10 |
|
cnv0 |
⊢ ◡ ∅ = ∅ |
11 |
9 10
|
eqtrdi |
⊢ ( ¬ ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ) → ◡ 𝑁 = ∅ ) |
12 |
11
|
imaeq1d |
⊢ ( ¬ ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ) → ( ◡ 𝑁 “ ℝ ) = ( ∅ “ ℝ ) ) |
13 |
|
0ima |
⊢ ( ∅ “ ℝ ) = ∅ |
14 |
12 13
|
eqtrdi |
⊢ ( ¬ ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ) → ( ◡ 𝑁 “ ℝ ) = ∅ ) |
15 |
4 14
|
nsyl2 |
⊢ ( 𝐹 ∈ ( ◡ 𝑁 “ ℝ ) → ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ) ) |
16 |
1
|
nmof |
⊢ ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ) → 𝑁 : ( 𝑆 GrpHom 𝑇 ) ⟶ ℝ* ) |
17 |
|
ffn |
⊢ ( 𝑁 : ( 𝑆 GrpHom 𝑇 ) ⟶ ℝ* → 𝑁 Fn ( 𝑆 GrpHom 𝑇 ) ) |
18 |
|
elpreima |
⊢ ( 𝑁 Fn ( 𝑆 GrpHom 𝑇 ) → ( 𝐹 ∈ ( ◡ 𝑁 “ ℝ ) ↔ ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ ( 𝑁 ‘ 𝐹 ) ∈ ℝ ) ) ) |
19 |
16 17 18
|
3syl |
⊢ ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ) → ( 𝐹 ∈ ( ◡ 𝑁 “ ℝ ) ↔ ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ ( 𝑁 ‘ 𝐹 ) ∈ ℝ ) ) ) |
20 |
15 19
|
biadanii |
⊢ ( 𝐹 ∈ ( ◡ 𝑁 “ ℝ ) ↔ ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ) ∧ ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ ( 𝑁 ‘ 𝐹 ) ∈ ℝ ) ) ) |
21 |
3 20
|
bitri |
⊢ ( 𝐹 ∈ ( 𝑆 NGHom 𝑇 ) ↔ ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ) ∧ ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ ( 𝑁 ‘ 𝐹 ) ∈ ℝ ) ) ) |