Step |
Hyp |
Ref |
Expression |
1 |
|
0nmhm.1 |
⊢ 𝑉 = ( Base ‘ 𝑆 ) |
2 |
|
0nmhm.2 |
⊢ 0 = ( 0g ‘ 𝑇 ) |
3 |
|
0nmhm.f |
⊢ 𝐹 = ( Scalar ‘ 𝑆 ) |
4 |
|
0nmhm.g |
⊢ 𝐺 = ( Scalar ‘ 𝑇 ) |
5 |
|
nlmlmod |
⊢ ( 𝑆 ∈ NrmMod → 𝑆 ∈ LMod ) |
6 |
|
nlmlmod |
⊢ ( 𝑇 ∈ NrmMod → 𝑇 ∈ LMod ) |
7 |
|
id |
⊢ ( 𝐹 = 𝐺 → 𝐹 = 𝐺 ) |
8 |
2 1 3 4
|
0lmhm |
⊢ ( ( 𝑆 ∈ LMod ∧ 𝑇 ∈ LMod ∧ 𝐹 = 𝐺 ) → ( 𝑉 × { 0 } ) ∈ ( 𝑆 LMHom 𝑇 ) ) |
9 |
5 6 7 8
|
syl3an |
⊢ ( ( 𝑆 ∈ NrmMod ∧ 𝑇 ∈ NrmMod ∧ 𝐹 = 𝐺 ) → ( 𝑉 × { 0 } ) ∈ ( 𝑆 LMHom 𝑇 ) ) |
10 |
|
nlmngp |
⊢ ( 𝑆 ∈ NrmMod → 𝑆 ∈ NrmGrp ) |
11 |
|
nlmngp |
⊢ ( 𝑇 ∈ NrmMod → 𝑇 ∈ NrmGrp ) |
12 |
1 2
|
0nghm |
⊢ ( ( 𝑆 ∈ NrmGrp ∧ 𝑇 ∈ NrmGrp ) → ( 𝑉 × { 0 } ) ∈ ( 𝑆 NGHom 𝑇 ) ) |
13 |
10 11 12
|
syl2an |
⊢ ( ( 𝑆 ∈ NrmMod ∧ 𝑇 ∈ NrmMod ) → ( 𝑉 × { 0 } ) ∈ ( 𝑆 NGHom 𝑇 ) ) |
14 |
13
|
3adant3 |
⊢ ( ( 𝑆 ∈ NrmMod ∧ 𝑇 ∈ NrmMod ∧ 𝐹 = 𝐺 ) → ( 𝑉 × { 0 } ) ∈ ( 𝑆 NGHom 𝑇 ) ) |
15 |
|
isnmhm |
⊢ ( ( 𝑉 × { 0 } ) ∈ ( 𝑆 NMHom 𝑇 ) ↔ ( ( 𝑆 ∈ NrmMod ∧ 𝑇 ∈ NrmMod ) ∧ ( ( 𝑉 × { 0 } ) ∈ ( 𝑆 LMHom 𝑇 ) ∧ ( 𝑉 × { 0 } ) ∈ ( 𝑆 NGHom 𝑇 ) ) ) ) |
16 |
15
|
baib |
⊢ ( ( 𝑆 ∈ NrmMod ∧ 𝑇 ∈ NrmMod ) → ( ( 𝑉 × { 0 } ) ∈ ( 𝑆 NMHom 𝑇 ) ↔ ( ( 𝑉 × { 0 } ) ∈ ( 𝑆 LMHom 𝑇 ) ∧ ( 𝑉 × { 0 } ) ∈ ( 𝑆 NGHom 𝑇 ) ) ) ) |
17 |
16
|
3adant3 |
⊢ ( ( 𝑆 ∈ NrmMod ∧ 𝑇 ∈ NrmMod ∧ 𝐹 = 𝐺 ) → ( ( 𝑉 × { 0 } ) ∈ ( 𝑆 NMHom 𝑇 ) ↔ ( ( 𝑉 × { 0 } ) ∈ ( 𝑆 LMHom 𝑇 ) ∧ ( 𝑉 × { 0 } ) ∈ ( 𝑆 NGHom 𝑇 ) ) ) ) |
18 |
9 14 17
|
mpbir2and |
⊢ ( ( 𝑆 ∈ NrmMod ∧ 𝑇 ∈ NrmMod ∧ 𝐹 = 𝐺 ) → ( 𝑉 × { 0 } ) ∈ ( 𝑆 NMHom 𝑇 ) ) |