Step |
Hyp |
Ref |
Expression |
1 |
|
isphl.v |
⊢ 𝑉 = ( Base ‘ 𝑊 ) |
2 |
|
isphl.f |
⊢ 𝐹 = ( Scalar ‘ 𝑊 ) |
3 |
|
isphl.h |
⊢ , = ( ·𝑖 ‘ 𝑊 ) |
4 |
|
isphl.o |
⊢ 0 = ( 0g ‘ 𝑊 ) |
5 |
|
isphl.i |
⊢ ∗ = ( *𝑟 ‘ 𝐹 ) |
6 |
|
isphl.z |
⊢ 𝑍 = ( 0g ‘ 𝐹 ) |
7 |
|
fvexd |
⊢ ( 𝑔 = 𝑊 → ( Base ‘ 𝑔 ) ∈ V ) |
8 |
|
fvexd |
⊢ ( ( 𝑔 = 𝑊 ∧ 𝑣 = ( Base ‘ 𝑔 ) ) → ( ·𝑖 ‘ 𝑔 ) ∈ V ) |
9 |
|
fvexd |
⊢ ( ( ( 𝑔 = 𝑊 ∧ 𝑣 = ( Base ‘ 𝑔 ) ) ∧ ℎ = ( ·𝑖 ‘ 𝑔 ) ) → ( Scalar ‘ 𝑔 ) ∈ V ) |
10 |
|
id |
⊢ ( 𝑓 = ( Scalar ‘ 𝑔 ) → 𝑓 = ( Scalar ‘ 𝑔 ) ) |
11 |
|
simpll |
⊢ ( ( ( 𝑔 = 𝑊 ∧ 𝑣 = ( Base ‘ 𝑔 ) ) ∧ ℎ = ( ·𝑖 ‘ 𝑔 ) ) → 𝑔 = 𝑊 ) |
12 |
11
|
fveq2d |
⊢ ( ( ( 𝑔 = 𝑊 ∧ 𝑣 = ( Base ‘ 𝑔 ) ) ∧ ℎ = ( ·𝑖 ‘ 𝑔 ) ) → ( Scalar ‘ 𝑔 ) = ( Scalar ‘ 𝑊 ) ) |
13 |
12 2
|
eqtr4di |
⊢ ( ( ( 𝑔 = 𝑊 ∧ 𝑣 = ( Base ‘ 𝑔 ) ) ∧ ℎ = ( ·𝑖 ‘ 𝑔 ) ) → ( Scalar ‘ 𝑔 ) = 𝐹 ) |
14 |
10 13
|
sylan9eqr |
⊢ ( ( ( ( 𝑔 = 𝑊 ∧ 𝑣 = ( Base ‘ 𝑔 ) ) ∧ ℎ = ( ·𝑖 ‘ 𝑔 ) ) ∧ 𝑓 = ( Scalar ‘ 𝑔 ) ) → 𝑓 = 𝐹 ) |
15 |
14
|
eleq1d |
⊢ ( ( ( ( 𝑔 = 𝑊 ∧ 𝑣 = ( Base ‘ 𝑔 ) ) ∧ ℎ = ( ·𝑖 ‘ 𝑔 ) ) ∧ 𝑓 = ( Scalar ‘ 𝑔 ) ) → ( 𝑓 ∈ *-Ring ↔ 𝐹 ∈ *-Ring ) ) |
16 |
|
simpllr |
⊢ ( ( ( ( 𝑔 = 𝑊 ∧ 𝑣 = ( Base ‘ 𝑔 ) ) ∧ ℎ = ( ·𝑖 ‘ 𝑔 ) ) ∧ 𝑓 = ( Scalar ‘ 𝑔 ) ) → 𝑣 = ( Base ‘ 𝑔 ) ) |
17 |
|
simplll |
⊢ ( ( ( ( 𝑔 = 𝑊 ∧ 𝑣 = ( Base ‘ 𝑔 ) ) ∧ ℎ = ( ·𝑖 ‘ 𝑔 ) ) ∧ 𝑓 = ( Scalar ‘ 𝑔 ) ) → 𝑔 = 𝑊 ) |
18 |
17
|
fveq2d |
⊢ ( ( ( ( 𝑔 = 𝑊 ∧ 𝑣 = ( Base ‘ 𝑔 ) ) ∧ ℎ = ( ·𝑖 ‘ 𝑔 ) ) ∧ 𝑓 = ( Scalar ‘ 𝑔 ) ) → ( Base ‘ 𝑔 ) = ( Base ‘ 𝑊 ) ) |
19 |
18 1
|
eqtr4di |
⊢ ( ( ( ( 𝑔 = 𝑊 ∧ 𝑣 = ( Base ‘ 𝑔 ) ) ∧ ℎ = ( ·𝑖 ‘ 𝑔 ) ) ∧ 𝑓 = ( Scalar ‘ 𝑔 ) ) → ( Base ‘ 𝑔 ) = 𝑉 ) |
20 |
16 19
|
eqtrd |
⊢ ( ( ( ( 𝑔 = 𝑊 ∧ 𝑣 = ( Base ‘ 𝑔 ) ) ∧ ℎ = ( ·𝑖 ‘ 𝑔 ) ) ∧ 𝑓 = ( Scalar ‘ 𝑔 ) ) → 𝑣 = 𝑉 ) |
21 |
|
simplr |
⊢ ( ( ( ( 𝑔 = 𝑊 ∧ 𝑣 = ( Base ‘ 𝑔 ) ) ∧ ℎ = ( ·𝑖 ‘ 𝑔 ) ) ∧ 𝑓 = ( Scalar ‘ 𝑔 ) ) → ℎ = ( ·𝑖 ‘ 𝑔 ) ) |
22 |
17
|
fveq2d |
⊢ ( ( ( ( 𝑔 = 𝑊 ∧ 𝑣 = ( Base ‘ 𝑔 ) ) ∧ ℎ = ( ·𝑖 ‘ 𝑔 ) ) ∧ 𝑓 = ( Scalar ‘ 𝑔 ) ) → ( ·𝑖 ‘ 𝑔 ) = ( ·𝑖 ‘ 𝑊 ) ) |
23 |
22 3
|
eqtr4di |
⊢ ( ( ( ( 𝑔 = 𝑊 ∧ 𝑣 = ( Base ‘ 𝑔 ) ) ∧ ℎ = ( ·𝑖 ‘ 𝑔 ) ) ∧ 𝑓 = ( Scalar ‘ 𝑔 ) ) → ( ·𝑖 ‘ 𝑔 ) = , ) |
24 |
21 23
|
eqtrd |
⊢ ( ( ( ( 𝑔 = 𝑊 ∧ 𝑣 = ( Base ‘ 𝑔 ) ) ∧ ℎ = ( ·𝑖 ‘ 𝑔 ) ) ∧ 𝑓 = ( Scalar ‘ 𝑔 ) ) → ℎ = , ) |
25 |
24
|
oveqd |
⊢ ( ( ( ( 𝑔 = 𝑊 ∧ 𝑣 = ( Base ‘ 𝑔 ) ) ∧ ℎ = ( ·𝑖 ‘ 𝑔 ) ) ∧ 𝑓 = ( Scalar ‘ 𝑔 ) ) → ( 𝑦 ℎ 𝑥 ) = ( 𝑦 , 𝑥 ) ) |
26 |
20 25
|
mpteq12dv |
⊢ ( ( ( ( 𝑔 = 𝑊 ∧ 𝑣 = ( Base ‘ 𝑔 ) ) ∧ ℎ = ( ·𝑖 ‘ 𝑔 ) ) ∧ 𝑓 = ( Scalar ‘ 𝑔 ) ) → ( 𝑦 ∈ 𝑣 ↦ ( 𝑦 ℎ 𝑥 ) ) = ( 𝑦 ∈ 𝑉 ↦ ( 𝑦 , 𝑥 ) ) ) |
27 |
14
|
fveq2d |
⊢ ( ( ( ( 𝑔 = 𝑊 ∧ 𝑣 = ( Base ‘ 𝑔 ) ) ∧ ℎ = ( ·𝑖 ‘ 𝑔 ) ) ∧ 𝑓 = ( Scalar ‘ 𝑔 ) ) → ( ringLMod ‘ 𝑓 ) = ( ringLMod ‘ 𝐹 ) ) |
28 |
17 27
|
oveq12d |
⊢ ( ( ( ( 𝑔 = 𝑊 ∧ 𝑣 = ( Base ‘ 𝑔 ) ) ∧ ℎ = ( ·𝑖 ‘ 𝑔 ) ) ∧ 𝑓 = ( Scalar ‘ 𝑔 ) ) → ( 𝑔 LMHom ( ringLMod ‘ 𝑓 ) ) = ( 𝑊 LMHom ( ringLMod ‘ 𝐹 ) ) ) |
29 |
26 28
|
eleq12d |
⊢ ( ( ( ( 𝑔 = 𝑊 ∧ 𝑣 = ( Base ‘ 𝑔 ) ) ∧ ℎ = ( ·𝑖 ‘ 𝑔 ) ) ∧ 𝑓 = ( Scalar ‘ 𝑔 ) ) → ( ( 𝑦 ∈ 𝑣 ↦ ( 𝑦 ℎ 𝑥 ) ) ∈ ( 𝑔 LMHom ( ringLMod ‘ 𝑓 ) ) ↔ ( 𝑦 ∈ 𝑉 ↦ ( 𝑦 , 𝑥 ) ) ∈ ( 𝑊 LMHom ( ringLMod ‘ 𝐹 ) ) ) ) |
30 |
24
|
oveqd |
⊢ ( ( ( ( 𝑔 = 𝑊 ∧ 𝑣 = ( Base ‘ 𝑔 ) ) ∧ ℎ = ( ·𝑖 ‘ 𝑔 ) ) ∧ 𝑓 = ( Scalar ‘ 𝑔 ) ) → ( 𝑥 ℎ 𝑥 ) = ( 𝑥 , 𝑥 ) ) |
31 |
14
|
fveq2d |
⊢ ( ( ( ( 𝑔 = 𝑊 ∧ 𝑣 = ( Base ‘ 𝑔 ) ) ∧ ℎ = ( ·𝑖 ‘ 𝑔 ) ) ∧ 𝑓 = ( Scalar ‘ 𝑔 ) ) → ( 0g ‘ 𝑓 ) = ( 0g ‘ 𝐹 ) ) |
32 |
31 6
|
eqtr4di |
⊢ ( ( ( ( 𝑔 = 𝑊 ∧ 𝑣 = ( Base ‘ 𝑔 ) ) ∧ ℎ = ( ·𝑖 ‘ 𝑔 ) ) ∧ 𝑓 = ( Scalar ‘ 𝑔 ) ) → ( 0g ‘ 𝑓 ) = 𝑍 ) |
33 |
30 32
|
eqeq12d |
⊢ ( ( ( ( 𝑔 = 𝑊 ∧ 𝑣 = ( Base ‘ 𝑔 ) ) ∧ ℎ = ( ·𝑖 ‘ 𝑔 ) ) ∧ 𝑓 = ( Scalar ‘ 𝑔 ) ) → ( ( 𝑥 ℎ 𝑥 ) = ( 0g ‘ 𝑓 ) ↔ ( 𝑥 , 𝑥 ) = 𝑍 ) ) |
34 |
17
|
fveq2d |
⊢ ( ( ( ( 𝑔 = 𝑊 ∧ 𝑣 = ( Base ‘ 𝑔 ) ) ∧ ℎ = ( ·𝑖 ‘ 𝑔 ) ) ∧ 𝑓 = ( Scalar ‘ 𝑔 ) ) → ( 0g ‘ 𝑔 ) = ( 0g ‘ 𝑊 ) ) |
35 |
34 4
|
eqtr4di |
⊢ ( ( ( ( 𝑔 = 𝑊 ∧ 𝑣 = ( Base ‘ 𝑔 ) ) ∧ ℎ = ( ·𝑖 ‘ 𝑔 ) ) ∧ 𝑓 = ( Scalar ‘ 𝑔 ) ) → ( 0g ‘ 𝑔 ) = 0 ) |
36 |
35
|
eqeq2d |
⊢ ( ( ( ( 𝑔 = 𝑊 ∧ 𝑣 = ( Base ‘ 𝑔 ) ) ∧ ℎ = ( ·𝑖 ‘ 𝑔 ) ) ∧ 𝑓 = ( Scalar ‘ 𝑔 ) ) → ( 𝑥 = ( 0g ‘ 𝑔 ) ↔ 𝑥 = 0 ) ) |
37 |
33 36
|
imbi12d |
⊢ ( ( ( ( 𝑔 = 𝑊 ∧ 𝑣 = ( Base ‘ 𝑔 ) ) ∧ ℎ = ( ·𝑖 ‘ 𝑔 ) ) ∧ 𝑓 = ( Scalar ‘ 𝑔 ) ) → ( ( ( 𝑥 ℎ 𝑥 ) = ( 0g ‘ 𝑓 ) → 𝑥 = ( 0g ‘ 𝑔 ) ) ↔ ( ( 𝑥 , 𝑥 ) = 𝑍 → 𝑥 = 0 ) ) ) |
38 |
14
|
fveq2d |
⊢ ( ( ( ( 𝑔 = 𝑊 ∧ 𝑣 = ( Base ‘ 𝑔 ) ) ∧ ℎ = ( ·𝑖 ‘ 𝑔 ) ) ∧ 𝑓 = ( Scalar ‘ 𝑔 ) ) → ( *𝑟 ‘ 𝑓 ) = ( *𝑟 ‘ 𝐹 ) ) |
39 |
38 5
|
eqtr4di |
⊢ ( ( ( ( 𝑔 = 𝑊 ∧ 𝑣 = ( Base ‘ 𝑔 ) ) ∧ ℎ = ( ·𝑖 ‘ 𝑔 ) ) ∧ 𝑓 = ( Scalar ‘ 𝑔 ) ) → ( *𝑟 ‘ 𝑓 ) = ∗ ) |
40 |
24
|
oveqd |
⊢ ( ( ( ( 𝑔 = 𝑊 ∧ 𝑣 = ( Base ‘ 𝑔 ) ) ∧ ℎ = ( ·𝑖 ‘ 𝑔 ) ) ∧ 𝑓 = ( Scalar ‘ 𝑔 ) ) → ( 𝑥 ℎ 𝑦 ) = ( 𝑥 , 𝑦 ) ) |
41 |
39 40
|
fveq12d |
⊢ ( ( ( ( 𝑔 = 𝑊 ∧ 𝑣 = ( Base ‘ 𝑔 ) ) ∧ ℎ = ( ·𝑖 ‘ 𝑔 ) ) ∧ 𝑓 = ( Scalar ‘ 𝑔 ) ) → ( ( *𝑟 ‘ 𝑓 ) ‘ ( 𝑥 ℎ 𝑦 ) ) = ( ∗ ‘ ( 𝑥 , 𝑦 ) ) ) |
42 |
41 25
|
eqeq12d |
⊢ ( ( ( ( 𝑔 = 𝑊 ∧ 𝑣 = ( Base ‘ 𝑔 ) ) ∧ ℎ = ( ·𝑖 ‘ 𝑔 ) ) ∧ 𝑓 = ( Scalar ‘ 𝑔 ) ) → ( ( ( *𝑟 ‘ 𝑓 ) ‘ ( 𝑥 ℎ 𝑦 ) ) = ( 𝑦 ℎ 𝑥 ) ↔ ( ∗ ‘ ( 𝑥 , 𝑦 ) ) = ( 𝑦 , 𝑥 ) ) ) |
43 |
20 42
|
raleqbidv |
⊢ ( ( ( ( 𝑔 = 𝑊 ∧ 𝑣 = ( Base ‘ 𝑔 ) ) ∧ ℎ = ( ·𝑖 ‘ 𝑔 ) ) ∧ 𝑓 = ( Scalar ‘ 𝑔 ) ) → ( ∀ 𝑦 ∈ 𝑣 ( ( *𝑟 ‘ 𝑓 ) ‘ ( 𝑥 ℎ 𝑦 ) ) = ( 𝑦 ℎ 𝑥 ) ↔ ∀ 𝑦 ∈ 𝑉 ( ∗ ‘ ( 𝑥 , 𝑦 ) ) = ( 𝑦 , 𝑥 ) ) ) |
44 |
29 37 43
|
3anbi123d |
⊢ ( ( ( ( 𝑔 = 𝑊 ∧ 𝑣 = ( Base ‘ 𝑔 ) ) ∧ ℎ = ( ·𝑖 ‘ 𝑔 ) ) ∧ 𝑓 = ( Scalar ‘ 𝑔 ) ) → ( ( ( 𝑦 ∈ 𝑣 ↦ ( 𝑦 ℎ 𝑥 ) ) ∈ ( 𝑔 LMHom ( ringLMod ‘ 𝑓 ) ) ∧ ( ( 𝑥 ℎ 𝑥 ) = ( 0g ‘ 𝑓 ) → 𝑥 = ( 0g ‘ 𝑔 ) ) ∧ ∀ 𝑦 ∈ 𝑣 ( ( *𝑟 ‘ 𝑓 ) ‘ ( 𝑥 ℎ 𝑦 ) ) = ( 𝑦 ℎ 𝑥 ) ) ↔ ( ( 𝑦 ∈ 𝑉 ↦ ( 𝑦 , 𝑥 ) ) ∈ ( 𝑊 LMHom ( ringLMod ‘ 𝐹 ) ) ∧ ( ( 𝑥 , 𝑥 ) = 𝑍 → 𝑥 = 0 ) ∧ ∀ 𝑦 ∈ 𝑉 ( ∗ ‘ ( 𝑥 , 𝑦 ) ) = ( 𝑦 , 𝑥 ) ) ) ) |
45 |
20 44
|
raleqbidv |
⊢ ( ( ( ( 𝑔 = 𝑊 ∧ 𝑣 = ( Base ‘ 𝑔 ) ) ∧ ℎ = ( ·𝑖 ‘ 𝑔 ) ) ∧ 𝑓 = ( Scalar ‘ 𝑔 ) ) → ( ∀ 𝑥 ∈ 𝑣 ( ( 𝑦 ∈ 𝑣 ↦ ( 𝑦 ℎ 𝑥 ) ) ∈ ( 𝑔 LMHom ( ringLMod ‘ 𝑓 ) ) ∧ ( ( 𝑥 ℎ 𝑥 ) = ( 0g ‘ 𝑓 ) → 𝑥 = ( 0g ‘ 𝑔 ) ) ∧ ∀ 𝑦 ∈ 𝑣 ( ( *𝑟 ‘ 𝑓 ) ‘ ( 𝑥 ℎ 𝑦 ) ) = ( 𝑦 ℎ 𝑥 ) ) ↔ ∀ 𝑥 ∈ 𝑉 ( ( 𝑦 ∈ 𝑉 ↦ ( 𝑦 , 𝑥 ) ) ∈ ( 𝑊 LMHom ( ringLMod ‘ 𝐹 ) ) ∧ ( ( 𝑥 , 𝑥 ) = 𝑍 → 𝑥 = 0 ) ∧ ∀ 𝑦 ∈ 𝑉 ( ∗ ‘ ( 𝑥 , 𝑦 ) ) = ( 𝑦 , 𝑥 ) ) ) ) |
46 |
15 45
|
anbi12d |
⊢ ( ( ( ( 𝑔 = 𝑊 ∧ 𝑣 = ( Base ‘ 𝑔 ) ) ∧ ℎ = ( ·𝑖 ‘ 𝑔 ) ) ∧ 𝑓 = ( Scalar ‘ 𝑔 ) ) → ( ( 𝑓 ∈ *-Ring ∧ ∀ 𝑥 ∈ 𝑣 ( ( 𝑦 ∈ 𝑣 ↦ ( 𝑦 ℎ 𝑥 ) ) ∈ ( 𝑔 LMHom ( ringLMod ‘ 𝑓 ) ) ∧ ( ( 𝑥 ℎ 𝑥 ) = ( 0g ‘ 𝑓 ) → 𝑥 = ( 0g ‘ 𝑔 ) ) ∧ ∀ 𝑦 ∈ 𝑣 ( ( *𝑟 ‘ 𝑓 ) ‘ ( 𝑥 ℎ 𝑦 ) ) = ( 𝑦 ℎ 𝑥 ) ) ) ↔ ( 𝐹 ∈ *-Ring ∧ ∀ 𝑥 ∈ 𝑉 ( ( 𝑦 ∈ 𝑉 ↦ ( 𝑦 , 𝑥 ) ) ∈ ( 𝑊 LMHom ( ringLMod ‘ 𝐹 ) ) ∧ ( ( 𝑥 , 𝑥 ) = 𝑍 → 𝑥 = 0 ) ∧ ∀ 𝑦 ∈ 𝑉 ( ∗ ‘ ( 𝑥 , 𝑦 ) ) = ( 𝑦 , 𝑥 ) ) ) ) ) |
47 |
9 46
|
sbcied |
⊢ ( ( ( 𝑔 = 𝑊 ∧ 𝑣 = ( Base ‘ 𝑔 ) ) ∧ ℎ = ( ·𝑖 ‘ 𝑔 ) ) → ( [ ( Scalar ‘ 𝑔 ) / 𝑓 ] ( 𝑓 ∈ *-Ring ∧ ∀ 𝑥 ∈ 𝑣 ( ( 𝑦 ∈ 𝑣 ↦ ( 𝑦 ℎ 𝑥 ) ) ∈ ( 𝑔 LMHom ( ringLMod ‘ 𝑓 ) ) ∧ ( ( 𝑥 ℎ 𝑥 ) = ( 0g ‘ 𝑓 ) → 𝑥 = ( 0g ‘ 𝑔 ) ) ∧ ∀ 𝑦 ∈ 𝑣 ( ( *𝑟 ‘ 𝑓 ) ‘ ( 𝑥 ℎ 𝑦 ) ) = ( 𝑦 ℎ 𝑥 ) ) ) ↔ ( 𝐹 ∈ *-Ring ∧ ∀ 𝑥 ∈ 𝑉 ( ( 𝑦 ∈ 𝑉 ↦ ( 𝑦 , 𝑥 ) ) ∈ ( 𝑊 LMHom ( ringLMod ‘ 𝐹 ) ) ∧ ( ( 𝑥 , 𝑥 ) = 𝑍 → 𝑥 = 0 ) ∧ ∀ 𝑦 ∈ 𝑉 ( ∗ ‘ ( 𝑥 , 𝑦 ) ) = ( 𝑦 , 𝑥 ) ) ) ) ) |
48 |
8 47
|
sbcied |
⊢ ( ( 𝑔 = 𝑊 ∧ 𝑣 = ( Base ‘ 𝑔 ) ) → ( [ ( ·𝑖 ‘ 𝑔 ) / ℎ ] [ ( Scalar ‘ 𝑔 ) / 𝑓 ] ( 𝑓 ∈ *-Ring ∧ ∀ 𝑥 ∈ 𝑣 ( ( 𝑦 ∈ 𝑣 ↦ ( 𝑦 ℎ 𝑥 ) ) ∈ ( 𝑔 LMHom ( ringLMod ‘ 𝑓 ) ) ∧ ( ( 𝑥 ℎ 𝑥 ) = ( 0g ‘ 𝑓 ) → 𝑥 = ( 0g ‘ 𝑔 ) ) ∧ ∀ 𝑦 ∈ 𝑣 ( ( *𝑟 ‘ 𝑓 ) ‘ ( 𝑥 ℎ 𝑦 ) ) = ( 𝑦 ℎ 𝑥 ) ) ) ↔ ( 𝐹 ∈ *-Ring ∧ ∀ 𝑥 ∈ 𝑉 ( ( 𝑦 ∈ 𝑉 ↦ ( 𝑦 , 𝑥 ) ) ∈ ( 𝑊 LMHom ( ringLMod ‘ 𝐹 ) ) ∧ ( ( 𝑥 , 𝑥 ) = 𝑍 → 𝑥 = 0 ) ∧ ∀ 𝑦 ∈ 𝑉 ( ∗ ‘ ( 𝑥 , 𝑦 ) ) = ( 𝑦 , 𝑥 ) ) ) ) ) |
49 |
7 48
|
sbcied |
⊢ ( 𝑔 = 𝑊 → ( [ ( Base ‘ 𝑔 ) / 𝑣 ] [ ( ·𝑖 ‘ 𝑔 ) / ℎ ] [ ( Scalar ‘ 𝑔 ) / 𝑓 ] ( 𝑓 ∈ *-Ring ∧ ∀ 𝑥 ∈ 𝑣 ( ( 𝑦 ∈ 𝑣 ↦ ( 𝑦 ℎ 𝑥 ) ) ∈ ( 𝑔 LMHom ( ringLMod ‘ 𝑓 ) ) ∧ ( ( 𝑥 ℎ 𝑥 ) = ( 0g ‘ 𝑓 ) → 𝑥 = ( 0g ‘ 𝑔 ) ) ∧ ∀ 𝑦 ∈ 𝑣 ( ( *𝑟 ‘ 𝑓 ) ‘ ( 𝑥 ℎ 𝑦 ) ) = ( 𝑦 ℎ 𝑥 ) ) ) ↔ ( 𝐹 ∈ *-Ring ∧ ∀ 𝑥 ∈ 𝑉 ( ( 𝑦 ∈ 𝑉 ↦ ( 𝑦 , 𝑥 ) ) ∈ ( 𝑊 LMHom ( ringLMod ‘ 𝐹 ) ) ∧ ( ( 𝑥 , 𝑥 ) = 𝑍 → 𝑥 = 0 ) ∧ ∀ 𝑦 ∈ 𝑉 ( ∗ ‘ ( 𝑥 , 𝑦 ) ) = ( 𝑦 , 𝑥 ) ) ) ) ) |
50 |
|
df-phl |
⊢ PreHil = { 𝑔 ∈ LVec ∣ [ ( Base ‘ 𝑔 ) / 𝑣 ] [ ( ·𝑖 ‘ 𝑔 ) / ℎ ] [ ( Scalar ‘ 𝑔 ) / 𝑓 ] ( 𝑓 ∈ *-Ring ∧ ∀ 𝑥 ∈ 𝑣 ( ( 𝑦 ∈ 𝑣 ↦ ( 𝑦 ℎ 𝑥 ) ) ∈ ( 𝑔 LMHom ( ringLMod ‘ 𝑓 ) ) ∧ ( ( 𝑥 ℎ 𝑥 ) = ( 0g ‘ 𝑓 ) → 𝑥 = ( 0g ‘ 𝑔 ) ) ∧ ∀ 𝑦 ∈ 𝑣 ( ( *𝑟 ‘ 𝑓 ) ‘ ( 𝑥 ℎ 𝑦 ) ) = ( 𝑦 ℎ 𝑥 ) ) ) } |
51 |
49 50
|
elrab2 |
⊢ ( 𝑊 ∈ PreHil ↔ ( 𝑊 ∈ LVec ∧ ( 𝐹 ∈ *-Ring ∧ ∀ 𝑥 ∈ 𝑉 ( ( 𝑦 ∈ 𝑉 ↦ ( 𝑦 , 𝑥 ) ) ∈ ( 𝑊 LMHom ( ringLMod ‘ 𝐹 ) ) ∧ ( ( 𝑥 , 𝑥 ) = 𝑍 → 𝑥 = 0 ) ∧ ∀ 𝑦 ∈ 𝑉 ( ∗ ‘ ( 𝑥 , 𝑦 ) ) = ( 𝑦 , 𝑥 ) ) ) ) ) |
52 |
|
3anass |
⊢ ( ( 𝑊 ∈ LVec ∧ 𝐹 ∈ *-Ring ∧ ∀ 𝑥 ∈ 𝑉 ( ( 𝑦 ∈ 𝑉 ↦ ( 𝑦 , 𝑥 ) ) ∈ ( 𝑊 LMHom ( ringLMod ‘ 𝐹 ) ) ∧ ( ( 𝑥 , 𝑥 ) = 𝑍 → 𝑥 = 0 ) ∧ ∀ 𝑦 ∈ 𝑉 ( ∗ ‘ ( 𝑥 , 𝑦 ) ) = ( 𝑦 , 𝑥 ) ) ) ↔ ( 𝑊 ∈ LVec ∧ ( 𝐹 ∈ *-Ring ∧ ∀ 𝑥 ∈ 𝑉 ( ( 𝑦 ∈ 𝑉 ↦ ( 𝑦 , 𝑥 ) ) ∈ ( 𝑊 LMHom ( ringLMod ‘ 𝐹 ) ) ∧ ( ( 𝑥 , 𝑥 ) = 𝑍 → 𝑥 = 0 ) ∧ ∀ 𝑦 ∈ 𝑉 ( ∗ ‘ ( 𝑥 , 𝑦 ) ) = ( 𝑦 , 𝑥 ) ) ) ) ) |
53 |
51 52
|
bitr4i |
⊢ ( 𝑊 ∈ PreHil ↔ ( 𝑊 ∈ LVec ∧ 𝐹 ∈ *-Ring ∧ ∀ 𝑥 ∈ 𝑉 ( ( 𝑦 ∈ 𝑉 ↦ ( 𝑦 , 𝑥 ) ) ∈ ( 𝑊 LMHom ( ringLMod ‘ 𝐹 ) ) ∧ ( ( 𝑥 , 𝑥 ) = 𝑍 → 𝑥 = 0 ) ∧ ∀ 𝑦 ∈ 𝑉 ( ∗ ‘ ( 𝑥 , 𝑦 ) ) = ( 𝑦 , 𝑥 ) ) ) ) |