Step |
Hyp |
Ref |
Expression |
1 |
|
nmofval.1 |
⊢ 𝑁 = ( 𝑆 normOp 𝑇 ) |
2 |
|
oveq12 |
⊢ ( ( 𝑠 = 𝑆 ∧ 𝑡 = 𝑇 ) → ( 𝑠 normOp 𝑡 ) = ( 𝑆 normOp 𝑇 ) ) |
3 |
2 1
|
eqtr4di |
⊢ ( ( 𝑠 = 𝑆 ∧ 𝑡 = 𝑇 ) → ( 𝑠 normOp 𝑡 ) = 𝑁 ) |
4 |
3
|
cnveqd |
⊢ ( ( 𝑠 = 𝑆 ∧ 𝑡 = 𝑇 ) → ◡ ( 𝑠 normOp 𝑡 ) = ◡ 𝑁 ) |
5 |
4
|
imaeq1d |
⊢ ( ( 𝑠 = 𝑆 ∧ 𝑡 = 𝑇 ) → ( ◡ ( 𝑠 normOp 𝑡 ) “ ℝ ) = ( ◡ 𝑁 “ ℝ ) ) |
6 |
|
df-nghm |
⊢ NGHom = ( 𝑠 ∈ NrmGrp , 𝑡 ∈ NrmGrp ↦ ( ◡ ( 𝑠 normOp 𝑡 ) “ ℝ ) ) |
7 |
1
|
ovexi |
⊢ 𝑁 ∈ V |
8 |
7
|
cnvex |
⊢ ◡ 𝑁 ∈ V |
9 |
8
|
imaex |
⊢ ( ◡ 𝑁 “ ℝ ) ∈ V |
10 |
5 6 9
|
ovmpoa |
⊢ ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ) → ( 𝑆 NGHom 𝑇 ) = ( ◡ 𝑁 “ ℝ ) ) |
11 |
6
|
mpondm0 |
⊢ ( ¬ ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ) → ( 𝑆 NGHom 𝑇 ) = ∅ ) |
12 |
|
nmoffn |
⊢ normOp Fn ( NrmGrp × NrmGrp ) |
13 |
12
|
fndmi |
⊢ dom normOp = ( NrmGrp × NrmGrp ) |
14 |
13
|
ndmov |
⊢ ( ¬ ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ) → ( 𝑆 normOp 𝑇 ) = ∅ ) |
15 |
1 14
|
syl5eq |
⊢ ( ¬ ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ) → 𝑁 = ∅ ) |
16 |
15
|
cnveqd |
⊢ ( ¬ ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ) → ◡ 𝑁 = ◡ ∅ ) |
17 |
|
cnv0 |
⊢ ◡ ∅ = ∅ |
18 |
16 17
|
eqtrdi |
⊢ ( ¬ ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ) → ◡ 𝑁 = ∅ ) |
19 |
18
|
imaeq1d |
⊢ ( ¬ ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ) → ( ◡ 𝑁 “ ℝ ) = ( ∅ “ ℝ ) ) |
20 |
|
0ima |
⊢ ( ∅ “ ℝ ) = ∅ |
21 |
19 20
|
eqtrdi |
⊢ ( ¬ ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ) → ( ◡ 𝑁 “ ℝ ) = ∅ ) |
22 |
11 21
|
eqtr4d |
⊢ ( ¬ ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ) → ( 𝑆 NGHom 𝑇 ) = ( ◡ 𝑁 “ ℝ ) ) |
23 |
10 22
|
pm2.61i |
⊢ ( 𝑆 NGHom 𝑇 ) = ( ◡ 𝑁 “ ℝ ) |