Metamath Proof Explorer

Theorem isphld

Description: Properties that determine a pre-Hilbert (inner product) space. (Contributed by Mario Carneiro, 18-Nov-2013) (Revised by Mario Carneiro, 7-Oct-2015)

Ref Expression
Hypotheses isphld.v 
|- ( ph -> V = ( Base ` W ) )
isphld.a 
|- ( ph -> .+ = ( +g ` W ) )
isphld.s 
|- ( ph -> .x. = ( .s ` W ) )
isphld.i 
|- ( ph -> I = ( .i ` W ) )
isphld.z 
|- ( ph -> .0. = ( 0g ` W ) )
isphld.f 
|- ( ph -> F = ( Scalar ` W ) )
isphld.k 
|- ( ph -> K = ( Base ` F ) )
isphld.p 
|- ( ph -> .+^ = ( +g ` F ) )
isphld.t 
|- ( ph -> .X. = ( .r ` F ) )
isphld.c 
|- ( ph -> .* = ( *r ` F ) )
isphld.o 
|- ( ph -> O = ( 0g ` F ) )
isphld.l 
|- ( ph -> W e. LVec )
isphld.r 
|- ( ph -> F e. *Ring )
isphld.cl 
|- ( ( ph /\ x e. V /\ y e. V ) -> ( x I y ) e. K )
isphld.d 
|- ( ( ph /\ q e. K /\ ( x e. V /\ y e. V /\ z e. V ) ) -> ( ( ( q .x. x ) .+ y ) I z ) = ( ( q .X. ( x I z ) ) .+^ ( y I z ) ) )
isphld.ns 
|- ( ( ph /\ x e. V /\ ( x I x ) = O ) -> x = .0. )
isphld.cj 
|- ( ( ph /\ x e. V /\ y e. V ) -> ( .* ` ( x I y ) ) = ( y I x ) )
Assertion isphld 
|- ( ph -> W e. PreHil )

Proof

Step Hyp Ref Expression
1 isphld.v 
 |-  ( ph -> V = ( Base ` W ) )
2 isphld.a 
 |-  ( ph -> .+ = ( +g ` W ) )
3 isphld.s 
 |-  ( ph -> .x. = ( .s ` W ) )
4 isphld.i 
 |-  ( ph -> I = ( .i ` W ) )
5 isphld.z 
 |-  ( ph -> .0. = ( 0g ` W ) )
6 isphld.f 
 |-  ( ph -> F = ( Scalar ` W ) )
7 isphld.k 
 |-  ( ph -> K = ( Base ` F ) )
8 isphld.p 
 |-  ( ph -> .+^ = ( +g ` F ) )
9 isphld.t 
 |-  ( ph -> .X. = ( .r ` F ) )
10 isphld.c 
 |-  ( ph -> .* = ( *r ` F ) )
11 isphld.o 
 |-  ( ph -> O = ( 0g ` F ) )
12 isphld.l 
 |-  ( ph -> W e. LVec )
13 isphld.r 
 |-  ( ph -> F e. *Ring )
14 isphld.cl 
 |-  ( ( ph /\ x e. V /\ y e. V ) -> ( x I y ) e. K )
15 isphld.d 
 |-  ( ( ph /\ q e. K /\ ( x e. V /\ y e. V /\ z e. V ) ) -> ( ( ( q .x. x ) .+ y ) I z ) = ( ( q .X. ( x I z ) ) .+^ ( y I z ) ) )
16 isphld.ns 
 |-  ( ( ph /\ x e. V /\ ( x I x ) = O ) -> x = .0. )
17 isphld.cj 
 |-  ( ( ph /\ x e. V /\ y e. V ) -> ( .* ` ( x I y ) ) = ( y I x ) )
18 6 13 eqeltrrd 
 |-  ( ph -> ( Scalar ` W ) e. *Ring )
19 oveq1 
 |-  ( y = w -> ( y ( .i ` W ) x ) = ( w ( .i ` W ) x ) )
20 19 cbvmptv 
 |-  ( y e. ( Base ` W ) |-> ( y ( .i ` W ) x ) ) = ( w e. ( Base ` W ) |-> ( w ( .i ` W ) x ) )
21 14 3expib 
 |-  ( ph -> ( ( x e. V /\ y e. V ) -> ( x I y ) e. K ) )
22 1 eleq2d 
 |-  ( ph -> ( x e. V <-> x e. ( Base ` W ) ) )
23 1 eleq2d 
 |-  ( ph -> ( y e. V <-> y e. ( Base ` W ) ) )
24 22 23 anbi12d 
 |-  ( ph -> ( ( x e. V /\ y e. V ) <-> ( x e. ( Base ` W ) /\ y e. ( Base ` W ) ) ) )
25 4 oveqd 
 |-  ( ph -> ( x I y ) = ( x ( .i ` W ) y ) )
26 6 fveq2d 
 |-  ( ph -> ( Base ` F ) = ( Base ` ( Scalar ` W ) ) )
27 7 26 eqtrd 
 |-  ( ph -> K = ( Base ` ( Scalar ` W ) ) )
28 25 27 eleq12d 
 |-  ( ph -> ( ( x I y ) e. K <-> ( x ( .i ` W ) y ) e. ( Base ` ( Scalar ` W ) ) ) )
29 21 24 28 3imtr3d 
 |-  ( ph -> ( ( x e. ( Base ` W ) /\ y e. ( Base ` W ) ) -> ( x ( .i ` W ) y ) e. ( Base ` ( Scalar ` W ) ) ) )
30 29 impl 
 |-  ( ( ( ph /\ x e. ( Base ` W ) ) /\ y e. ( Base ` W ) ) -> ( x ( .i ` W ) y ) e. ( Base ` ( Scalar ` W ) ) )
31 30 an32s 
 |-  ( ( ( ph /\ y e. ( Base ` W ) ) /\ x e. ( Base ` W ) ) -> ( x ( .i ` W ) y ) e. ( Base ` ( Scalar ` W ) ) )
32 oveq1 
 |-  ( w = x -> ( w ( .i ` W ) y ) = ( x ( .i ` W ) y ) )
33 32 cbvmptv 
 |-  ( w e. ( Base ` W ) |-> ( w ( .i ` W ) y ) ) = ( x e. ( Base ` W ) |-> ( x ( .i ` W ) y ) )
34 31 33 fmptd 
 |-  ( ( ph /\ y e. ( Base ` W ) ) -> ( w e. ( Base ` W ) |-> ( w ( .i ` W ) y ) ) : ( Base ` W ) --> ( Base ` ( Scalar ` W ) ) )
35 34 ralrimiva 
 |-  ( ph -> A. y e. ( Base ` W ) ( w e. ( Base ` W ) |-> ( w ( .i ` W ) y ) ) : ( Base ` W ) --> ( Base ` ( Scalar ` W ) ) )
36 oveq2 
 |-  ( y = z -> ( w ( .i ` W ) y ) = ( w ( .i ` W ) z ) )
37 36 mpteq2dv 
 |-  ( y = z -> ( w e. ( Base ` W ) |-> ( w ( .i ` W ) y ) ) = ( w e. ( Base ` W ) |-> ( w ( .i ` W ) z ) ) )
38 37 feq1d 
 |-  ( y = z -> ( ( w e. ( Base ` W ) |-> ( w ( .i ` W ) y ) ) : ( Base ` W ) --> ( Base ` ( Scalar ` W ) ) <-> ( w e. ( Base ` W ) |-> ( w ( .i ` W ) z ) ) : ( Base ` W ) --> ( Base ` ( Scalar ` W ) ) ) )
39 38 rspccva 
 |-  ( ( A. y e. ( Base ` W ) ( w e. ( Base ` W ) |-> ( w ( .i ` W ) y ) ) : ( Base ` W ) --> ( Base ` ( Scalar ` W ) ) /\ z e. ( Base ` W ) ) -> ( w e. ( Base ` W ) |-> ( w ( .i ` W ) z ) ) : ( Base ` W ) --> ( Base ` ( Scalar ` W ) ) )
40 35 39 sylan 
 |-  ( ( ph /\ z e. ( Base ` W ) ) -> ( w e. ( Base ` W ) |-> ( w ( .i ` W ) z ) ) : ( Base ` W ) --> ( Base ` ( Scalar ` W ) ) )
41 eqidd 
 |-  ( ( ph /\ z e. ( Base ` W ) ) -> ( Scalar ` W ) = ( Scalar ` W ) )
42 15 3exp 
 |-  ( ph -> ( q e. K -> ( ( x e. V /\ y e. V /\ z e. V ) -> ( ( ( q .x. x ) .+ y ) I z ) = ( ( q .X. ( x I z ) ) .+^ ( y I z ) ) ) ) )
43 27 eleq2d 
 |-  ( ph -> ( q e. K <-> q e. ( Base ` ( Scalar ` W ) ) ) )
44 3anrot 
 |-  ( ( z e. V /\ x e. V /\ y e. V ) <-> ( x e. V /\ y e. V /\ z e. V ) )
45 1 eleq2d 
 |-  ( ph -> ( z e. V <-> z e. ( Base ` W ) ) )
46 45 22 23 3anbi123d 
 |-  ( ph -> ( ( z e. V /\ x e. V /\ y e. V ) <-> ( z e. ( Base ` W ) /\ x e. ( Base ` W ) /\ y e. ( Base ` W ) ) ) )
47 44 46 bitr3id 
 |-  ( ph -> ( ( x e. V /\ y e. V /\ z e. V ) <-> ( z e. ( Base ` W ) /\ x e. ( Base ` W ) /\ y e. ( Base ` W ) ) ) )
48 3 oveqd 
 |-  ( ph -> ( q .x. x ) = ( q ( .s ` W ) x ) )
49 eqidd 
 |-  ( ph -> y = y )
50 2 48 49 oveq123d 
 |-  ( ph -> ( ( q .x. x ) .+ y ) = ( ( q ( .s ` W ) x ) ( +g ` W ) y ) )
51 eqidd 
 |-  ( ph -> z = z )
52 4 50 51 oveq123d 
 |-  ( ph -> ( ( ( q .x. x ) .+ y ) I z ) = ( ( ( q ( .s ` W ) x ) ( +g ` W ) y ) ( .i ` W ) z ) )
53 6 fveq2d 
 |-  ( ph -> ( +g ` F ) = ( +g ` ( Scalar ` W ) ) )
54 8 53 eqtrd 
 |-  ( ph -> .+^ = ( +g ` ( Scalar ` W ) ) )
55 6 fveq2d 
 |-  ( ph -> ( .r ` F ) = ( .r ` ( Scalar ` W ) ) )
56 9 55 eqtrd 
 |-  ( ph -> .X. = ( .r ` ( Scalar ` W ) ) )
57 eqidd 
 |-  ( ph -> q = q )
58 4 oveqd 
 |-  ( ph -> ( x I z ) = ( x ( .i ` W ) z ) )
59 56 57 58 oveq123d 
 |-  ( ph -> ( q .X. ( x I z ) ) = ( q ( .r ` ( Scalar ` W ) ) ( x ( .i ` W ) z ) ) )
60 4 oveqd 
 |-  ( ph -> ( y I z ) = ( y ( .i ` W ) z ) )
61 54 59 60 oveq123d 
 |-  ( ph -> ( ( q .X. ( x I z ) ) .+^ ( y I z ) ) = ( ( q ( .r ` ( Scalar ` W ) ) ( x ( .i ` W ) z ) ) ( +g ` ( Scalar ` W ) ) ( y ( .i ` W ) z ) ) )
62 52 61 eqeq12d 
 |-  ( ph -> ( ( ( ( q .x. x ) .+ y ) I z ) = ( ( q .X. ( x I z ) ) .+^ ( y I z ) ) <-> ( ( ( q ( .s ` W ) x ) ( +g ` W ) y ) ( .i ` W ) z ) = ( ( q ( .r ` ( Scalar ` W ) ) ( x ( .i ` W ) z ) ) ( +g ` ( Scalar ` W ) ) ( y ( .i ` W ) z ) ) ) )
63 47 62 imbi12d 
 |-  ( ph -> ( ( ( x e. V /\ y e. V /\ z e. V ) -> ( ( ( q .x. x ) .+ y ) I z ) = ( ( q .X. ( x I z ) ) .+^ ( y I z ) ) ) <-> ( ( z e. ( Base ` W ) /\ x e. ( Base ` W ) /\ y e. ( Base ` W ) ) -> ( ( ( q ( .s ` W ) x ) ( +g ` W ) y ) ( .i ` W ) z ) = ( ( q ( .r ` ( Scalar ` W ) ) ( x ( .i ` W ) z ) ) ( +g ` ( Scalar ` W ) ) ( y ( .i ` W ) z ) ) ) ) )
64 42 43 63 3imtr3d 
 |-  ( ph -> ( q e. ( Base ` ( Scalar ` W ) ) -> ( ( z e. ( Base ` W ) /\ x e. ( Base ` W ) /\ y e. ( Base ` W ) ) -> ( ( ( q ( .s ` W ) x ) ( +g ` W ) y ) ( .i ` W ) z ) = ( ( q ( .r ` ( Scalar ` W ) ) ( x ( .i ` W ) z ) ) ( +g ` ( Scalar ` W ) ) ( y ( .i ` W ) z ) ) ) ) )
65 64 imp31 
 |-  ( ( ( ph /\ q e. ( Base ` ( Scalar ` W ) ) ) /\ ( z e. ( Base ` W ) /\ x e. ( Base ` W ) /\ y e. ( Base ` W ) ) ) -> ( ( ( q ( .s ` W ) x ) ( +g ` W ) y ) ( .i ` W ) z ) = ( ( q ( .r ` ( Scalar ` W ) ) ( x ( .i ` W ) z ) ) ( +g ` ( Scalar ` W ) ) ( y ( .i ` W ) z ) ) )
66 65 3exp2 
 |-  ( ( ph /\ q e. ( Base ` ( Scalar ` W ) ) ) -> ( z e. ( Base ` W ) -> ( x e. ( Base ` W ) -> ( y e. ( Base ` W ) -> ( ( ( q ( .s ` W ) x ) ( +g ` W ) y ) ( .i ` W ) z ) = ( ( q ( .r ` ( Scalar ` W ) ) ( x ( .i ` W ) z ) ) ( +g ` ( Scalar ` W ) ) ( y ( .i ` W ) z ) ) ) ) ) )
67 66 impancom 
 |-  ( ( ph /\ z e. ( Base ` W ) ) -> ( q e. ( Base ` ( Scalar ` W ) ) -> ( x e. ( Base ` W ) -> ( y e. ( Base ` W ) -> ( ( ( q ( .s ` W ) x ) ( +g ` W ) y ) ( .i ` W ) z ) = ( ( q ( .r ` ( Scalar ` W ) ) ( x ( .i ` W ) z ) ) ( +g ` ( Scalar ` W ) ) ( y ( .i ` W ) z ) ) ) ) ) )
68 67 3imp2 
 |-  ( ( ( ph /\ z e. ( Base ` W ) ) /\ ( q e. ( Base ` ( Scalar ` W ) ) /\ x e. ( Base ` W ) /\ y e. ( Base ` W ) ) ) -> ( ( ( q ( .s ` W ) x ) ( +g ` W ) y ) ( .i ` W ) z ) = ( ( q ( .r ` ( Scalar ` W ) ) ( x ( .i ` W ) z ) ) ( +g ` ( Scalar ` W ) ) ( y ( .i ` W ) z ) ) )
69 lveclmod 
 |-  ( W e. LVec -> W e. LMod )
70 12 69 syl 
 |-  ( ph -> W e. LMod )
71 70 adantr 
 |-  ( ( ph /\ z e. ( Base ` W ) ) -> W e. LMod )
72 71 adantr 
 |-  ( ( ( ph /\ z e. ( Base ` W ) ) /\ ( q e. ( Base ` ( Scalar ` W ) ) /\ x e. ( Base ` W ) /\ y e. ( Base ` W ) ) ) -> W e. LMod )
73 eqid 
 |-  ( Base ` W ) = ( Base ` W )
74 eqid 
 |-  ( LSubSp ` W ) = ( LSubSp ` W )
75 73 74 lss1 
 |-  ( W e. LMod -> ( Base ` W ) e. ( LSubSp ` W ) )
76 72 75 syl 
 |-  ( ( ( ph /\ z e. ( Base ` W ) ) /\ ( q e. ( Base ` ( Scalar ` W ) ) /\ x e. ( Base ` W ) /\ y e. ( Base ` W ) ) ) -> ( Base ` W ) e. ( LSubSp ` W ) )
77 eqid 
 |-  ( Scalar ` W ) = ( Scalar ` W )
78 eqid 
 |-  ( Base ` ( Scalar ` W ) ) = ( Base ` ( Scalar ` W ) )
79 eqid 
 |-  ( +g ` W ) = ( +g ` W )
80 eqid 
 |-  ( .s ` W ) = ( .s ` W )
81 77 78 79 80 74 lsscl 
 |-  ( ( ( Base ` W ) e. ( LSubSp ` W ) /\ ( q e. ( Base ` ( Scalar ` W ) ) /\ x e. ( Base ` W ) /\ y e. ( Base ` W ) ) ) -> ( ( q ( .s ` W ) x ) ( +g ` W ) y ) e. ( Base ` W ) )
82 76 81 sylancom 
 |-  ( ( ( ph /\ z e. ( Base ` W ) ) /\ ( q e. ( Base ` ( Scalar ` W ) ) /\ x e. ( Base ` W ) /\ y e. ( Base ` W ) ) ) -> ( ( q ( .s ` W ) x ) ( +g ` W ) y ) e. ( Base ` W ) )
83 oveq1 
 |-  ( w = ( ( q ( .s ` W ) x ) ( +g ` W ) y ) -> ( w ( .i ` W ) z ) = ( ( ( q ( .s ` W ) x ) ( +g ` W ) y ) ( .i ` W ) z ) )
84 eqid 
 |-  ( w e. ( Base ` W ) |-> ( w ( .i ` W ) z ) ) = ( w e. ( Base ` W ) |-> ( w ( .i ` W ) z ) )
85 ovex 
 |-  ( w ( .i ` W ) z ) e. _V
86 83 84 85 fvmpt3i 
 |-  ( ( ( q ( .s ` W ) x ) ( +g ` W ) y ) e. ( Base ` W ) -> ( ( w e. ( Base ` W ) |-> ( w ( .i ` W ) z ) ) ` ( ( q ( .s ` W ) x ) ( +g ` W ) y ) ) = ( ( ( q ( .s ` W ) x ) ( +g ` W ) y ) ( .i ` W ) z ) )
87 82 86 syl 
 |-  ( ( ( ph /\ z e. ( Base ` W ) ) /\ ( q e. ( Base ` ( Scalar ` W ) ) /\ x e. ( Base ` W ) /\ y e. ( Base ` W ) ) ) -> ( ( w e. ( Base ` W ) |-> ( w ( .i ` W ) z ) ) ` ( ( q ( .s ` W ) x ) ( +g ` W ) y ) ) = ( ( ( q ( .s ` W ) x ) ( +g ` W ) y ) ( .i ` W ) z ) )
88 simpr2 
 |-  ( ( ( ph /\ z e. ( Base ` W ) ) /\ ( q e. ( Base ` ( Scalar ` W ) ) /\ x e. ( Base ` W ) /\ y e. ( Base ` W ) ) ) -> x e. ( Base ` W ) )
89 oveq1 
 |-  ( w = x -> ( w ( .i ` W ) z ) = ( x ( .i ` W ) z ) )
90 89 84 85 fvmpt3i 
 |-  ( x e. ( Base ` W ) -> ( ( w e. ( Base ` W ) |-> ( w ( .i ` W ) z ) ) ` x ) = ( x ( .i ` W ) z ) )
91 88 90 syl 
 |-  ( ( ( ph /\ z e. ( Base ` W ) ) /\ ( q e. ( Base ` ( Scalar ` W ) ) /\ x e. ( Base ` W ) /\ y e. ( Base ` W ) ) ) -> ( ( w e. ( Base ` W ) |-> ( w ( .i ` W ) z ) ) ` x ) = ( x ( .i ` W ) z ) )
92 91 oveq2d 
 |-  ( ( ( ph /\ z e. ( Base ` W ) ) /\ ( q e. ( Base ` ( Scalar ` W ) ) /\ x e. ( Base ` W ) /\ y e. ( Base ` W ) ) ) -> ( q ( .r ` ( Scalar ` W ) ) ( ( w e. ( Base ` W ) |-> ( w ( .i ` W ) z ) ) ` x ) ) = ( q ( .r ` ( Scalar ` W ) ) ( x ( .i ` W ) z ) ) )
93 simpr3 
 |-  ( ( ( ph /\ z e. ( Base ` W ) ) /\ ( q e. ( Base ` ( Scalar ` W ) ) /\ x e. ( Base ` W ) /\ y e. ( Base ` W ) ) ) -> y e. ( Base ` W ) )
94 oveq1 
 |-  ( w = y -> ( w ( .i ` W ) z ) = ( y ( .i ` W ) z ) )
95 94 84 85 fvmpt3i 
 |-  ( y e. ( Base ` W ) -> ( ( w e. ( Base ` W ) |-> ( w ( .i ` W ) z ) ) ` y ) = ( y ( .i ` W ) z ) )
96 93 95 syl 
 |-  ( ( ( ph /\ z e. ( Base ` W ) ) /\ ( q e. ( Base ` ( Scalar ` W ) ) /\ x e. ( Base ` W ) /\ y e. ( Base ` W ) ) ) -> ( ( w e. ( Base ` W ) |-> ( w ( .i ` W ) z ) ) ` y ) = ( y ( .i ` W ) z ) )
97 92 96 oveq12d 
 |-  ( ( ( ph /\ z e. ( Base ` W ) ) /\ ( q e. ( Base ` ( Scalar ` W ) ) /\ x e. ( Base ` W ) /\ y e. ( Base ` W ) ) ) -> ( ( q ( .r ` ( Scalar ` W ) ) ( ( w e. ( Base ` W ) |-> ( w ( .i ` W ) z ) ) ` x ) ) ( +g ` ( Scalar ` W ) ) ( ( w e. ( Base ` W ) |-> ( w ( .i ` W ) z ) ) ` y ) ) = ( ( q ( .r ` ( Scalar ` W ) ) ( x ( .i ` W ) z ) ) ( +g ` ( Scalar ` W ) ) ( y ( .i ` W ) z ) ) )
98 68 87 97 3eqtr4d 
 |-  ( ( ( ph /\ z e. ( Base ` W ) ) /\ ( q e. ( Base ` ( Scalar ` W ) ) /\ x e. ( Base ` W ) /\ y e. ( Base ` W ) ) ) -> ( ( w e. ( Base ` W ) |-> ( w ( .i ` W ) z ) ) ` ( ( q ( .s ` W ) x ) ( +g ` W ) y ) ) = ( ( q ( .r ` ( Scalar ` W ) ) ( ( w e. ( Base ` W ) |-> ( w ( .i ` W ) z ) ) ` x ) ) ( +g ` ( Scalar ` W ) ) ( ( w e. ( Base ` W ) |-> ( w ( .i ` W ) z ) ) ` y ) ) )
99 98 ralrimivvva 
 |-  ( ( ph /\ z e. ( Base ` W ) ) -> A. q e. ( Base ` ( Scalar ` W ) ) A. x e. ( Base ` W ) A. y e. ( Base ` W ) ( ( w e. ( Base ` W ) |-> ( w ( .i ` W ) z ) ) ` ( ( q ( .s ` W ) x ) ( +g ` W ) y ) ) = ( ( q ( .r ` ( Scalar ` W ) ) ( ( w e. ( Base ` W ) |-> ( w ( .i ` W ) z ) ) ` x ) ) ( +g ` ( Scalar ` W ) ) ( ( w e. ( Base ` W ) |-> ( w ( .i ` W ) z ) ) ` y ) ) )
100 77 lmodring 
 |-  ( W e. LMod -> ( Scalar ` W ) e. Ring )
101 rlmlmod 
 |-  ( ( Scalar ` W ) e. Ring -> ( ringLMod ` ( Scalar ` W ) ) e. LMod )
102 70 100 101 3syl 
 |-  ( ph -> ( ringLMod ` ( Scalar ` W ) ) e. LMod )
103 102 adantr 
 |-  ( ( ph /\ z e. ( Base ` W ) ) -> ( ringLMod ` ( Scalar ` W ) ) e. LMod )
104 rlmbas 
 |-  ( Base ` ( Scalar ` W ) ) = ( Base ` ( ringLMod ` ( Scalar ` W ) ) )
105 fvex 
 |-  ( Scalar ` W ) e. _V
106 rlmsca 
 |-  ( ( Scalar ` W ) e. _V -> ( Scalar ` W ) = ( Scalar ` ( ringLMod ` ( Scalar ` W ) ) ) )
107 105 106 ax-mp 
 |-  ( Scalar ` W ) = ( Scalar ` ( ringLMod ` ( Scalar ` W ) ) )
108 rlmplusg 
 |-  ( +g ` ( Scalar ` W ) ) = ( +g ` ( ringLMod ` ( Scalar ` W ) ) )
109 rlmvsca 
 |-  ( .r ` ( Scalar ` W ) ) = ( .s ` ( ringLMod ` ( Scalar ` W ) ) )
110 73 104 77 107 78 79 108 80 109 islmhm2 
 |-  ( ( W e. LMod /\ ( ringLMod ` ( Scalar ` W ) ) e. LMod ) -> ( ( w e. ( Base ` W ) |-> ( w ( .i ` W ) z ) ) e. ( W LMHom ( ringLMod ` ( Scalar ` W ) ) ) <-> ( ( w e. ( Base ` W ) |-> ( w ( .i ` W ) z ) ) : ( Base ` W ) --> ( Base ` ( Scalar ` W ) ) /\ ( Scalar ` W ) = ( Scalar ` W ) /\ A. q e. ( Base ` ( Scalar ` W ) ) A. x e. ( Base ` W ) A. y e. ( Base ` W ) ( ( w e. ( Base ` W ) |-> ( w ( .i ` W ) z ) ) ` ( ( q ( .s ` W ) x ) ( +g ` W ) y ) ) = ( ( q ( .r ` ( Scalar ` W ) ) ( ( w e. ( Base ` W ) |-> ( w ( .i ` W ) z ) ) ` x ) ) ( +g ` ( Scalar ` W ) ) ( ( w e. ( Base ` W ) |-> ( w ( .i ` W ) z ) ) ` y ) ) ) ) )
111 71 103 110 syl2anc 
 |-  ( ( ph /\ z e. ( Base ` W ) ) -> ( ( w e. ( Base ` W ) |-> ( w ( .i ` W ) z ) ) e. ( W LMHom ( ringLMod ` ( Scalar ` W ) ) ) <-> ( ( w e. ( Base ` W ) |-> ( w ( .i ` W ) z ) ) : ( Base ` W ) --> ( Base ` ( Scalar ` W ) ) /\ ( Scalar ` W ) = ( Scalar ` W ) /\ A. q e. ( Base ` ( Scalar ` W ) ) A. x e. ( Base ` W ) A. y e. ( Base ` W ) ( ( w e. ( Base ` W ) |-> ( w ( .i ` W ) z ) ) ` ( ( q ( .s ` W ) x ) ( +g ` W ) y ) ) = ( ( q ( .r ` ( Scalar ` W ) ) ( ( w e. ( Base ` W ) |-> ( w ( .i ` W ) z ) ) ` x ) ) ( +g ` ( Scalar ` W ) ) ( ( w e. ( Base ` W ) |-> ( w ( .i ` W ) z ) ) ` y ) ) ) ) )
112 40 41 99 111 mpbir3and 
 |-  ( ( ph /\ z e. ( Base ` W ) ) -> ( w e. ( Base ` W ) |-> ( w ( .i ` W ) z ) ) e. ( W LMHom ( ringLMod ` ( Scalar ` W ) ) ) )
113 112 ralrimiva 
 |-  ( ph -> A. z e. ( Base ` W ) ( w e. ( Base ` W ) |-> ( w ( .i ` W ) z ) ) e. ( W LMHom ( ringLMod ` ( Scalar ` W ) ) ) )
114 oveq2 
 |-  ( z = x -> ( w ( .i ` W ) z ) = ( w ( .i ` W ) x ) )
115 114 mpteq2dv 
 |-  ( z = x -> ( w e. ( Base ` W ) |-> ( w ( .i ` W ) z ) ) = ( w e. ( Base ` W ) |-> ( w ( .i ` W ) x ) ) )
116 115 eleq1d 
 |-  ( z = x -> ( ( w e. ( Base ` W ) |-> ( w ( .i ` W ) z ) ) e. ( W LMHom ( ringLMod ` ( Scalar ` W ) ) ) <-> ( w e. ( Base ` W ) |-> ( w ( .i ` W ) x ) ) e. ( W LMHom ( ringLMod ` ( Scalar ` W ) ) ) ) )
117 116 rspccva 
 |-  ( ( A. z e. ( Base ` W ) ( w e. ( Base ` W ) |-> ( w ( .i ` W ) z ) ) e. ( W LMHom ( ringLMod ` ( Scalar ` W ) ) ) /\ x e. ( Base ` W ) ) -> ( w e. ( Base ` W ) |-> ( w ( .i ` W ) x ) ) e. ( W LMHom ( ringLMod ` ( Scalar ` W ) ) ) )
118 113 117 sylan 
 |-  ( ( ph /\ x e. ( Base ` W ) ) -> ( w e. ( Base ` W ) |-> ( w ( .i ` W ) x ) ) e. ( W LMHom ( ringLMod ` ( Scalar ` W ) ) ) )
119 20 118 eqeltrid 
 |-  ( ( ph /\ x e. ( Base ` W ) ) -> ( y e. ( Base ` W ) |-> ( y ( .i ` W ) x ) ) e. ( W LMHom ( ringLMod ` ( Scalar ` W ) ) ) )
120 16 3exp 
 |-  ( ph -> ( x e. V -> ( ( x I x ) = O -> x = .0. ) ) )
121 4 oveqd 
 |-  ( ph -> ( x I x ) = ( x ( .i ` W ) x ) )
122 6 fveq2d 
 |-  ( ph -> ( 0g ` F ) = ( 0g ` ( Scalar ` W ) ) )
123 11 122 eqtrd 
 |-  ( ph -> O = ( 0g ` ( Scalar ` W ) ) )
124 121 123 eqeq12d 
 |-  ( ph -> ( ( x I x ) = O <-> ( x ( .i ` W ) x ) = ( 0g ` ( Scalar ` W ) ) ) )
125 5 eqeq2d 
 |-  ( ph -> ( x = .0. <-> x = ( 0g ` W ) ) )
126 124 125 imbi12d 
 |-  ( ph -> ( ( ( x I x ) = O -> x = .0. ) <-> ( ( x ( .i ` W ) x ) = ( 0g ` ( Scalar ` W ) ) -> x = ( 0g ` W ) ) ) )
127 120 22 126 3imtr3d 
 |-  ( ph -> ( x e. ( Base ` W ) -> ( ( x ( .i ` W ) x ) = ( 0g ` ( Scalar ` W ) ) -> x = ( 0g ` W ) ) ) )
128 127 imp 
 |-  ( ( ph /\ x e. ( Base ` W ) ) -> ( ( x ( .i ` W ) x ) = ( 0g ` ( Scalar ` W ) ) -> x = ( 0g ` W ) ) )
129 17 3expib 
 |-  ( ph -> ( ( x e. V /\ y e. V ) -> ( .* ` ( x I y ) ) = ( y I x ) ) )
130 6 fveq2d 
 |-  ( ph -> ( *r ` F ) = ( *r ` ( Scalar ` W ) ) )
131 10 130 eqtrd 
 |-  ( ph -> .* = ( *r ` ( Scalar ` W ) ) )
132 131 25 fveq12d 
 |-  ( ph -> ( .* ` ( x I y ) ) = ( ( *r ` ( Scalar ` W ) ) ` ( x ( .i ` W ) y ) ) )
133 4 oveqd 
 |-  ( ph -> ( y I x ) = ( y ( .i ` W ) x ) )
134 132 133 eqeq12d 
 |-  ( ph -> ( ( .* ` ( x I y ) ) = ( y I x ) <-> ( ( *r ` ( Scalar ` W ) ) ` ( x ( .i ` W ) y ) ) = ( y ( .i ` W ) x ) ) )
135 129 24 134 3imtr3d 
 |-  ( ph -> ( ( x e. ( Base ` W ) /\ y e. ( Base ` W ) ) -> ( ( *r ` ( Scalar ` W ) ) ` ( x ( .i ` W ) y ) ) = ( y ( .i ` W ) x ) ) )
136 135 expdimp 
 |-  ( ( ph /\ x e. ( Base ` W ) ) -> ( y e. ( Base ` W ) -> ( ( *r ` ( Scalar ` W ) ) ` ( x ( .i ` W ) y ) ) = ( y ( .i ` W ) x ) ) )
137 136 ralrimiv 
 |-  ( ( ph /\ x e. ( Base ` W ) ) -> A. y e. ( Base ` W ) ( ( *r ` ( Scalar ` W ) ) ` ( x ( .i ` W ) y ) ) = ( y ( .i ` W ) x ) )
138 119 128 137 3jca 
 |-  ( ( ph /\ x e. ( Base ` W ) ) -> ( ( y e. ( Base ` W ) |-> ( y ( .i ` W ) x ) ) e. ( W LMHom ( ringLMod ` ( Scalar ` W ) ) ) /\ ( ( x ( .i ` W ) x ) = ( 0g ` ( Scalar ` W ) ) -> x = ( 0g ` W ) ) /\ A. y e. ( Base ` W ) ( ( *r ` ( Scalar ` W ) ) ` ( x ( .i ` W ) y ) ) = ( y ( .i ` W ) x ) ) )
139 138 ralrimiva 
 |-  ( ph -> A. x e. ( Base ` W ) ( ( y e. ( Base ` W ) |-> ( y ( .i ` W ) x ) ) e. ( W LMHom ( ringLMod ` ( Scalar ` W ) ) ) /\ ( ( x ( .i ` W ) x ) = ( 0g ` ( Scalar ` W ) ) -> x = ( 0g ` W ) ) /\ A. y e. ( Base ` W ) ( ( *r ` ( Scalar ` W ) ) ` ( x ( .i ` W ) y ) ) = ( y ( .i ` W ) x ) ) )
140 eqid 
 |-  ( .i ` W ) = ( .i ` W )
141 eqid 
 |-  ( 0g ` W ) = ( 0g ` W )
142 eqid 
 |-  ( *r ` ( Scalar ` W ) ) = ( *r ` ( Scalar ` W ) )
143 eqid 
 |-  ( 0g ` ( Scalar ` W ) ) = ( 0g ` ( Scalar ` W ) )
144 73 77 140 141 142 143 isphl 
 |-  ( W e. PreHil <-> ( W e. LVec /\ ( Scalar ` W ) e. *Ring /\ A. x e. ( Base ` W ) ( ( y e. ( Base ` W ) |-> ( y ( .i ` W ) x ) ) e. ( W LMHom ( ringLMod ` ( Scalar ` W ) ) ) /\ ( ( x ( .i ` W ) x ) = ( 0g ` ( Scalar ` W ) ) -> x = ( 0g ` W ) ) /\ A. y e. ( Base ` W ) ( ( *r ` ( Scalar ` W ) ) ` ( x ( .i ` W ) y ) ) = ( y ( .i ` W ) x ) ) ) )
145 12 18 139 144 syl3anbrc 
 |-  ( ph -> W e. PreHil )