Step |
Hyp |
Ref |
Expression |
0 |
|
cphl |
⊢ PreHil |
1 |
|
vg |
⊢ 𝑔 |
2 |
|
clvec |
⊢ LVec |
3 |
|
cbs |
⊢ Base |
4 |
1
|
cv |
⊢ 𝑔 |
5 |
4 3
|
cfv |
⊢ ( Base ‘ 𝑔 ) |
6 |
|
vv |
⊢ 𝑣 |
7 |
|
cip |
⊢ ·𝑖 |
8 |
4 7
|
cfv |
⊢ ( ·𝑖 ‘ 𝑔 ) |
9 |
|
vh |
⊢ ℎ |
10 |
|
csca |
⊢ Scalar |
11 |
4 10
|
cfv |
⊢ ( Scalar ‘ 𝑔 ) |
12 |
|
vf |
⊢ 𝑓 |
13 |
12
|
cv |
⊢ 𝑓 |
14 |
|
csr |
⊢ *-Ring |
15 |
13 14
|
wcel |
⊢ 𝑓 ∈ *-Ring |
16 |
|
vx |
⊢ 𝑥 |
17 |
6
|
cv |
⊢ 𝑣 |
18 |
|
vy |
⊢ 𝑦 |
19 |
18
|
cv |
⊢ 𝑦 |
20 |
9
|
cv |
⊢ ℎ |
21 |
16
|
cv |
⊢ 𝑥 |
22 |
19 21 20
|
co |
⊢ ( 𝑦 ℎ 𝑥 ) |
23 |
18 17 22
|
cmpt |
⊢ ( 𝑦 ∈ 𝑣 ↦ ( 𝑦 ℎ 𝑥 ) ) |
24 |
|
clmhm |
⊢ LMHom |
25 |
|
crglmod |
⊢ ringLMod |
26 |
13 25
|
cfv |
⊢ ( ringLMod ‘ 𝑓 ) |
27 |
4 26 24
|
co |
⊢ ( 𝑔 LMHom ( ringLMod ‘ 𝑓 ) ) |
28 |
23 27
|
wcel |
⊢ ( 𝑦 ∈ 𝑣 ↦ ( 𝑦 ℎ 𝑥 ) ) ∈ ( 𝑔 LMHom ( ringLMod ‘ 𝑓 ) ) |
29 |
21 21 20
|
co |
⊢ ( 𝑥 ℎ 𝑥 ) |
30 |
|
c0g |
⊢ 0g |
31 |
13 30
|
cfv |
⊢ ( 0g ‘ 𝑓 ) |
32 |
29 31
|
wceq |
⊢ ( 𝑥 ℎ 𝑥 ) = ( 0g ‘ 𝑓 ) |
33 |
4 30
|
cfv |
⊢ ( 0g ‘ 𝑔 ) |
34 |
21 33
|
wceq |
⊢ 𝑥 = ( 0g ‘ 𝑔 ) |
35 |
32 34
|
wi |
⊢ ( ( 𝑥 ℎ 𝑥 ) = ( 0g ‘ 𝑓 ) → 𝑥 = ( 0g ‘ 𝑔 ) ) |
36 |
|
cstv |
⊢ *𝑟 |
37 |
13 36
|
cfv |
⊢ ( *𝑟 ‘ 𝑓 ) |
38 |
21 19 20
|
co |
⊢ ( 𝑥 ℎ 𝑦 ) |
39 |
38 37
|
cfv |
⊢ ( ( *𝑟 ‘ 𝑓 ) ‘ ( 𝑥 ℎ 𝑦 ) ) |
40 |
39 22
|
wceq |
⊢ ( ( *𝑟 ‘ 𝑓 ) ‘ ( 𝑥 ℎ 𝑦 ) ) = ( 𝑦 ℎ 𝑥 ) |
41 |
40 18 17
|
wral |
⊢ ∀ 𝑦 ∈ 𝑣 ( ( *𝑟 ‘ 𝑓 ) ‘ ( 𝑥 ℎ 𝑦 ) ) = ( 𝑦 ℎ 𝑥 ) |
42 |
28 35 41
|
w3a |
⊢ ( ( 𝑦 ∈ 𝑣 ↦ ( 𝑦 ℎ 𝑥 ) ) ∈ ( 𝑔 LMHom ( ringLMod ‘ 𝑓 ) ) ∧ ( ( 𝑥 ℎ 𝑥 ) = ( 0g ‘ 𝑓 ) → 𝑥 = ( 0g ‘ 𝑔 ) ) ∧ ∀ 𝑦 ∈ 𝑣 ( ( *𝑟 ‘ 𝑓 ) ‘ ( 𝑥 ℎ 𝑦 ) ) = ( 𝑦 ℎ 𝑥 ) ) |
43 |
42 16 17
|
wral |
⊢ ∀ 𝑥 ∈ 𝑣 ( ( 𝑦 ∈ 𝑣 ↦ ( 𝑦 ℎ 𝑥 ) ) ∈ ( 𝑔 LMHom ( ringLMod ‘ 𝑓 ) ) ∧ ( ( 𝑥 ℎ 𝑥 ) = ( 0g ‘ 𝑓 ) → 𝑥 = ( 0g ‘ 𝑔 ) ) ∧ ∀ 𝑦 ∈ 𝑣 ( ( *𝑟 ‘ 𝑓 ) ‘ ( 𝑥 ℎ 𝑦 ) ) = ( 𝑦 ℎ 𝑥 ) ) |
44 |
15 43
|
wa |
⊢ ( 𝑓 ∈ *-Ring ∧ ∀ 𝑥 ∈ 𝑣 ( ( 𝑦 ∈ 𝑣 ↦ ( 𝑦 ℎ 𝑥 ) ) ∈ ( 𝑔 LMHom ( ringLMod ‘ 𝑓 ) ) ∧ ( ( 𝑥 ℎ 𝑥 ) = ( 0g ‘ 𝑓 ) → 𝑥 = ( 0g ‘ 𝑔 ) ) ∧ ∀ 𝑦 ∈ 𝑣 ( ( *𝑟 ‘ 𝑓 ) ‘ ( 𝑥 ℎ 𝑦 ) ) = ( 𝑦 ℎ 𝑥 ) ) ) |
45 |
44 12 11
|
wsbc |
⊢ [ ( Scalar ‘ 𝑔 ) / 𝑓 ] ( 𝑓 ∈ *-Ring ∧ ∀ 𝑥 ∈ 𝑣 ( ( 𝑦 ∈ 𝑣 ↦ ( 𝑦 ℎ 𝑥 ) ) ∈ ( 𝑔 LMHom ( ringLMod ‘ 𝑓 ) ) ∧ ( ( 𝑥 ℎ 𝑥 ) = ( 0g ‘ 𝑓 ) → 𝑥 = ( 0g ‘ 𝑔 ) ) ∧ ∀ 𝑦 ∈ 𝑣 ( ( *𝑟 ‘ 𝑓 ) ‘ ( 𝑥 ℎ 𝑦 ) ) = ( 𝑦 ℎ 𝑥 ) ) ) |
46 |
45 9 8
|
wsbc |
⊢ [ ( ·𝑖 ‘ 𝑔 ) / ℎ ] [ ( Scalar ‘ 𝑔 ) / 𝑓 ] ( 𝑓 ∈ *-Ring ∧ ∀ 𝑥 ∈ 𝑣 ( ( 𝑦 ∈ 𝑣 ↦ ( 𝑦 ℎ 𝑥 ) ) ∈ ( 𝑔 LMHom ( ringLMod ‘ 𝑓 ) ) ∧ ( ( 𝑥 ℎ 𝑥 ) = ( 0g ‘ 𝑓 ) → 𝑥 = ( 0g ‘ 𝑔 ) ) ∧ ∀ 𝑦 ∈ 𝑣 ( ( *𝑟 ‘ 𝑓 ) ‘ ( 𝑥 ℎ 𝑦 ) ) = ( 𝑦 ℎ 𝑥 ) ) ) |
47 |
46 6 5
|
wsbc |
⊢ [ ( Base ‘ 𝑔 ) / 𝑣 ] [ ( ·𝑖 ‘ 𝑔 ) / ℎ ] [ ( Scalar ‘ 𝑔 ) / 𝑓 ] ( 𝑓 ∈ *-Ring ∧ ∀ 𝑥 ∈ 𝑣 ( ( 𝑦 ∈ 𝑣 ↦ ( 𝑦 ℎ 𝑥 ) ) ∈ ( 𝑔 LMHom ( ringLMod ‘ 𝑓 ) ) ∧ ( ( 𝑥 ℎ 𝑥 ) = ( 0g ‘ 𝑓 ) → 𝑥 = ( 0g ‘ 𝑔 ) ) ∧ ∀ 𝑦 ∈ 𝑣 ( ( *𝑟 ‘ 𝑓 ) ‘ ( 𝑥 ℎ 𝑦 ) ) = ( 𝑦 ℎ 𝑥 ) ) ) |
48 |
47 1 2
|
crab |
⊢ { 𝑔 ∈ LVec ∣ [ ( Base ‘ 𝑔 ) / 𝑣 ] [ ( ·𝑖 ‘ 𝑔 ) / ℎ ] [ ( Scalar ‘ 𝑔 ) / 𝑓 ] ( 𝑓 ∈ *-Ring ∧ ∀ 𝑥 ∈ 𝑣 ( ( 𝑦 ∈ 𝑣 ↦ ( 𝑦 ℎ 𝑥 ) ) ∈ ( 𝑔 LMHom ( ringLMod ‘ 𝑓 ) ) ∧ ( ( 𝑥 ℎ 𝑥 ) = ( 0g ‘ 𝑓 ) → 𝑥 = ( 0g ‘ 𝑔 ) ) ∧ ∀ 𝑦 ∈ 𝑣 ( ( *𝑟 ‘ 𝑓 ) ‘ ( 𝑥 ℎ 𝑦 ) ) = ( 𝑦 ℎ 𝑥 ) ) ) } |
49 |
0 48
|
wceq |
⊢ PreHil = { 𝑔 ∈ LVec ∣ [ ( Base ‘ 𝑔 ) / 𝑣 ] [ ( ·𝑖 ‘ 𝑔 ) / ℎ ] [ ( Scalar ‘ 𝑔 ) / 𝑓 ] ( 𝑓 ∈ *-Ring ∧ ∀ 𝑥 ∈ 𝑣 ( ( 𝑦 ∈ 𝑣 ↦ ( 𝑦 ℎ 𝑥 ) ) ∈ ( 𝑔 LMHom ( ringLMod ‘ 𝑓 ) ) ∧ ( ( 𝑥 ℎ 𝑥 ) = ( 0g ‘ 𝑓 ) → 𝑥 = ( 0g ‘ 𝑔 ) ) ∧ ∀ 𝑦 ∈ 𝑣 ( ( *𝑟 ‘ 𝑓 ) ‘ ( 𝑥 ℎ 𝑦 ) ) = ( 𝑦 ℎ 𝑥 ) ) ) } |