Step |
Hyp |
Ref |
Expression |
1 |
|
phlsrng.f |
⊢ 𝐹 = ( Scalar ‘ 𝑊 ) |
2 |
|
phllmhm.h |
⊢ , = ( ·𝑖 ‘ 𝑊 ) |
3 |
|
phllmhm.v |
⊢ 𝑉 = ( Base ‘ 𝑊 ) |
4 |
|
ip0l.z |
⊢ 𝑍 = ( 0g ‘ 𝐹 ) |
5 |
|
ip0l.o |
⊢ 0 = ( 0g ‘ 𝑊 ) |
6 |
|
phllmod |
⊢ ( 𝑊 ∈ PreHil → 𝑊 ∈ LMod ) |
7 |
|
lmodgrp |
⊢ ( 𝑊 ∈ LMod → 𝑊 ∈ Grp ) |
8 |
3 5
|
grpidcl |
⊢ ( 𝑊 ∈ Grp → 0 ∈ 𝑉 ) |
9 |
6 7 8
|
3syl |
⊢ ( 𝑊 ∈ PreHil → 0 ∈ 𝑉 ) |
10 |
9
|
adantr |
⊢ ( ( 𝑊 ∈ PreHil ∧ 𝐴 ∈ 𝑉 ) → 0 ∈ 𝑉 ) |
11 |
|
oveq1 |
⊢ ( 𝑥 = 0 → ( 𝑥 , 𝐴 ) = ( 0 , 𝐴 ) ) |
12 |
|
eqid |
⊢ ( 𝑥 ∈ 𝑉 ↦ ( 𝑥 , 𝐴 ) ) = ( 𝑥 ∈ 𝑉 ↦ ( 𝑥 , 𝐴 ) ) |
13 |
|
ovex |
⊢ ( 0 , 𝐴 ) ∈ V |
14 |
11 12 13
|
fvmpt |
⊢ ( 0 ∈ 𝑉 → ( ( 𝑥 ∈ 𝑉 ↦ ( 𝑥 , 𝐴 ) ) ‘ 0 ) = ( 0 , 𝐴 ) ) |
15 |
10 14
|
syl |
⊢ ( ( 𝑊 ∈ PreHil ∧ 𝐴 ∈ 𝑉 ) → ( ( 𝑥 ∈ 𝑉 ↦ ( 𝑥 , 𝐴 ) ) ‘ 0 ) = ( 0 , 𝐴 ) ) |
16 |
1 2 3 12
|
phllmhm |
⊢ ( ( 𝑊 ∈ PreHil ∧ 𝐴 ∈ 𝑉 ) → ( 𝑥 ∈ 𝑉 ↦ ( 𝑥 , 𝐴 ) ) ∈ ( 𝑊 LMHom ( ringLMod ‘ 𝐹 ) ) ) |
17 |
|
lmghm |
⊢ ( ( 𝑥 ∈ 𝑉 ↦ ( 𝑥 , 𝐴 ) ) ∈ ( 𝑊 LMHom ( ringLMod ‘ 𝐹 ) ) → ( 𝑥 ∈ 𝑉 ↦ ( 𝑥 , 𝐴 ) ) ∈ ( 𝑊 GrpHom ( ringLMod ‘ 𝐹 ) ) ) |
18 |
|
rlm0 |
⊢ ( 0g ‘ 𝐹 ) = ( 0g ‘ ( ringLMod ‘ 𝐹 ) ) |
19 |
4 18
|
eqtri |
⊢ 𝑍 = ( 0g ‘ ( ringLMod ‘ 𝐹 ) ) |
20 |
5 19
|
ghmid |
⊢ ( ( 𝑥 ∈ 𝑉 ↦ ( 𝑥 , 𝐴 ) ) ∈ ( 𝑊 GrpHom ( ringLMod ‘ 𝐹 ) ) → ( ( 𝑥 ∈ 𝑉 ↦ ( 𝑥 , 𝐴 ) ) ‘ 0 ) = 𝑍 ) |
21 |
16 17 20
|
3syl |
⊢ ( ( 𝑊 ∈ PreHil ∧ 𝐴 ∈ 𝑉 ) → ( ( 𝑥 ∈ 𝑉 ↦ ( 𝑥 , 𝐴 ) ) ‘ 0 ) = 𝑍 ) |
22 |
15 21
|
eqtr3d |
⊢ ( ( 𝑊 ∈ PreHil ∧ 𝐴 ∈ 𝑉 ) → ( 0 , 𝐴 ) = 𝑍 ) |