Metamath Proof Explorer

Theorem phlssphl

Description: A subspace of an inner product space (pre-Hilbert space) is an inner product space. (Contributed by AV, 25-Sep-2022)

Ref Expression
Hypotheses phlssphl.x 
|- X = ( W |`s U )
phlssphl.s 
|- S = ( LSubSp ` W )
Assertion phlssphl 
|- ( ( W e. PreHil /\ U e. S ) -> X e. PreHil )

Proof

Step Hyp Ref Expression
1 phlssphl.x 
 |-  X = ( W |`s U )
2 phlssphl.s 
 |-  S = ( LSubSp ` W )
3 eqidd 
 |-  ( ( W e. PreHil /\ U e. S ) -> ( Base ` X ) = ( Base ` X ) )
4 eqidd 
 |-  ( ( W e. PreHil /\ U e. S ) -> ( +g ` X ) = ( +g ` X ) )
5 eqidd 
 |-  ( ( W e. PreHil /\ U e. S ) -> ( .s ` X ) = ( .s ` X ) )
6 eqidd 
 |-  ( ( W e. PreHil /\ U e. S ) -> ( .i ` X ) = ( .i ` X ) )
7 phllmod 
 |-  ( W e. PreHil -> W e. LMod )
8 eqid 
 |-  ( 0g ` W ) = ( 0g ` W )
9 eqid 
 |-  ( 0g ` X ) = ( 0g ` X )
10 1 8 9 2 lss0v 
 |-  ( ( W e. LMod /\ U e. S ) -> ( 0g ` X ) = ( 0g ` W ) )
11 7 10 sylan 
 |-  ( ( W e. PreHil /\ U e. S ) -> ( 0g ` X ) = ( 0g ` W ) )
12 11 eqcomd 
 |-  ( ( W e. PreHil /\ U e. S ) -> ( 0g ` W ) = ( 0g ` X ) )
13 eqidd 
 |-  ( ( W e. PreHil /\ U e. S ) -> ( Scalar ` X ) = ( Scalar ` X ) )
14 eqidd 
 |-  ( ( W e. PreHil /\ U e. S ) -> ( Base ` ( Scalar ` X ) ) = ( Base ` ( Scalar ` X ) ) )
15 eqidd 
 |-  ( ( W e. PreHil /\ U e. S ) -> ( +g ` ( Scalar ` X ) ) = ( +g ` ( Scalar ` X ) ) )
16 eqidd 
 |-  ( ( W e. PreHil /\ U e. S ) -> ( .r ` ( Scalar ` X ) ) = ( .r ` ( Scalar ` X ) ) )
17 eqidd 
 |-  ( ( W e. PreHil /\ U e. S ) -> ( *r ` ( Scalar ` X ) ) = ( *r ` ( Scalar ` X ) ) )
18 eqidd 
 |-  ( ( W e. PreHil /\ U e. S ) -> ( 0g ` ( Scalar ` X ) ) = ( 0g ` ( Scalar ` X ) ) )
19 phllvec 
 |-  ( W e. PreHil -> W e. LVec )
20 1 2 lsslvec 
 |-  ( ( W e. LVec /\ U e. S ) -> X e. LVec )
21 19 20 sylan 
 |-  ( ( W e. PreHil /\ U e. S ) -> X e. LVec )
22 eqid 
 |-  ( Scalar ` W ) = ( Scalar ` W )
23 1 22 resssca 
 |-  ( U e. S -> ( Scalar ` W ) = ( Scalar ` X ) )
24 23 eqcomd 
 |-  ( U e. S -> ( Scalar ` X ) = ( Scalar ` W ) )
25 24 adantl 
 |-  ( ( W e. PreHil /\ U e. S ) -> ( Scalar ` X ) = ( Scalar ` W ) )
26 22 phlsrng 
 |-  ( W e. PreHil -> ( Scalar ` W ) e. *Ring )
27 26 adantr 
 |-  ( ( W e. PreHil /\ U e. S ) -> ( Scalar ` W ) e. *Ring )
28 25 27 eqeltrd 
 |-  ( ( W e. PreHil /\ U e. S ) -> ( Scalar ` X ) e. *Ring )
29 simpl 
 |-  ( ( W e. PreHil /\ U e. S ) -> W e. PreHil )
30 eqid 
 |-  ( Base ` W ) = ( Base ` W )
31 1 30 ressbasss 
 |-  ( Base ` X ) C_ ( Base ` W )
32 31 sseli 
 |-  ( x e. ( Base ` X ) -> x e. ( Base ` W ) )
33 31 sseli 
 |-  ( y e. ( Base ` X ) -> y e. ( Base ` W ) )
34 eqid 
 |-  ( .i ` W ) = ( .i ` W )
35 eqid 
 |-  ( Base ` ( Scalar ` W ) ) = ( Base ` ( Scalar ` W ) )
36 22 34 30 35 ipcl 
 |-  ( ( W e. PreHil /\ x e. ( Base ` W ) /\ y e. ( Base ` W ) ) -> ( x ( .i ` W ) y ) e. ( Base ` ( Scalar ` W ) ) )
37 29 32 33 36 syl3an 
 |-  ( ( ( W e. PreHil /\ U e. S ) /\ x e. ( Base ` X ) /\ y e. ( Base ` X ) ) -> ( x ( .i ` W ) y ) e. ( Base ` ( Scalar ` W ) ) )
38 24 fveq2d 
 |-  ( U e. S -> ( Base ` ( Scalar ` X ) ) = ( Base ` ( Scalar ` W ) ) )
39 38 eleq2d 
 |-  ( U e. S -> ( ( x ( .i ` W ) y ) e. ( Base ` ( Scalar ` X ) ) <-> ( x ( .i ` W ) y ) e. ( Base ` ( Scalar ` W ) ) ) )
40 39 adantl 
 |-  ( ( W e. PreHil /\ U e. S ) -> ( ( x ( .i ` W ) y ) e. ( Base ` ( Scalar ` X ) ) <-> ( x ( .i ` W ) y ) e. ( Base ` ( Scalar ` W ) ) ) )
41 40 3ad2ant1 
 |-  ( ( ( W e. PreHil /\ U e. S ) /\ x e. ( Base ` X ) /\ y e. ( Base ` X ) ) -> ( ( x ( .i ` W ) y ) e. ( Base ` ( Scalar ` X ) ) <-> ( x ( .i ` W ) y ) e. ( Base ` ( Scalar ` W ) ) ) )
42 37 41 mpbird 
 |-  ( ( ( W e. PreHil /\ U e. S ) /\ x e. ( Base ` X ) /\ y e. ( Base ` X ) ) -> ( x ( .i ` W ) y ) e. ( Base ` ( Scalar ` X ) ) )
43 eqid 
 |-  ( .i ` X ) = ( .i ` X )
44 1 34 43 ssipeq 
 |-  ( U e. S -> ( .i ` X ) = ( .i ` W ) )
45 44 oveqd 
 |-  ( U e. S -> ( x ( .i ` X ) y ) = ( x ( .i ` W ) y ) )
46 45 eleq1d 
 |-  ( U e. S -> ( ( x ( .i ` X ) y ) e. ( Base ` ( Scalar ` X ) ) <-> ( x ( .i ` W ) y ) e. ( Base ` ( Scalar ` X ) ) ) )
47 46 adantl 
 |-  ( ( W e. PreHil /\ U e. S ) -> ( ( x ( .i ` X ) y ) e. ( Base ` ( Scalar ` X ) ) <-> ( x ( .i ` W ) y ) e. ( Base ` ( Scalar ` X ) ) ) )
48 47 3ad2ant1 
 |-  ( ( ( W e. PreHil /\ U e. S ) /\ x e. ( Base ` X ) /\ y e. ( Base ` X ) ) -> ( ( x ( .i ` X ) y ) e. ( Base ` ( Scalar ` X ) ) <-> ( x ( .i ` W ) y ) e. ( Base ` ( Scalar ` X ) ) ) )
49 42 48 mpbird 
 |-  ( ( ( W e. PreHil /\ U e. S ) /\ x e. ( Base ` X ) /\ y e. ( Base ` X ) ) -> ( x ( .i ` X ) y ) e. ( Base ` ( Scalar ` X ) ) )
50 29 3ad2ant1 
 |-  ( ( ( W e. PreHil /\ U e. S ) /\ q e. ( Base ` ( Scalar ` X ) ) /\ ( x e. ( Base ` X ) /\ y e. ( Base ` X ) /\ z e. ( Base ` X ) ) ) -> W e. PreHil )
51 7 adantr 
 |-  ( ( W e. PreHil /\ U e. S ) -> W e. LMod )
52 51 3ad2ant1 
 |-  ( ( ( W e. PreHil /\ U e. S ) /\ q e. ( Base ` ( Scalar ` X ) ) /\ ( x e. ( Base ` X ) /\ y e. ( Base ` X ) /\ z e. ( Base ` X ) ) ) -> W e. LMod )
53 25 fveq2d 
 |-  ( ( W e. PreHil /\ U e. S ) -> ( Base ` ( Scalar ` X ) ) = ( Base ` ( Scalar ` W ) ) )
54 53 eleq2d 
 |-  ( ( W e. PreHil /\ U e. S ) -> ( q e. ( Base ` ( Scalar ` X ) ) <-> q e. ( Base ` ( Scalar ` W ) ) ) )
55 54 biimpa 
 |-  ( ( ( W e. PreHil /\ U e. S ) /\ q e. ( Base ` ( Scalar ` X ) ) ) -> q e. ( Base ` ( Scalar ` W ) ) )
56 55 3adant3 
 |-  ( ( ( W e. PreHil /\ U e. S ) /\ q e. ( Base ` ( Scalar ` X ) ) /\ ( x e. ( Base ` X ) /\ y e. ( Base ` X ) /\ z e. ( Base ` X ) ) ) -> q e. ( Base ` ( Scalar ` W ) ) )
57 32 3ad2ant1 
 |-  ( ( x e. ( Base ` X ) /\ y e. ( Base ` X ) /\ z e. ( Base ` X ) ) -> x e. ( Base ` W ) )
58 57 3ad2ant3 
 |-  ( ( ( W e. PreHil /\ U e. S ) /\ q e. ( Base ` ( Scalar ` X ) ) /\ ( x e. ( Base ` X ) /\ y e. ( Base ` X ) /\ z e. ( Base ` X ) ) ) -> x e. ( Base ` W ) )
59 eqid 
 |-  ( .s ` W ) = ( .s ` W )
60 30 22 59 35 lmodvscl 
 |-  ( ( W e. LMod /\ q e. ( Base ` ( Scalar ` W ) ) /\ x e. ( Base ` W ) ) -> ( q ( .s ` W ) x ) e. ( Base ` W ) )
61 52 56 58 60 syl3anc 
 |-  ( ( ( W e. PreHil /\ U e. S ) /\ q e. ( Base ` ( Scalar ` X ) ) /\ ( x e. ( Base ` X ) /\ y e. ( Base ` X ) /\ z e. ( Base ` X ) ) ) -> ( q ( .s ` W ) x ) e. ( Base ` W ) )
62 33 3ad2ant2 
 |-  ( ( x e. ( Base ` X ) /\ y e. ( Base ` X ) /\ z e. ( Base ` X ) ) -> y e. ( Base ` W ) )
63 62 3ad2ant3 
 |-  ( ( ( W e. PreHil /\ U e. S ) /\ q e. ( Base ` ( Scalar ` X ) ) /\ ( x e. ( Base ` X ) /\ y e. ( Base ` X ) /\ z e. ( Base ` X ) ) ) -> y e. ( Base ` W ) )
64 31 sseli 
 |-  ( z e. ( Base ` X ) -> z e. ( Base ` W ) )
65 64 3ad2ant3 
 |-  ( ( x e. ( Base ` X ) /\ y e. ( Base ` X ) /\ z e. ( Base ` X ) ) -> z e. ( Base ` W ) )
66 65 3ad2ant3 
 |-  ( ( ( W e. PreHil /\ U e. S ) /\ q e. ( Base ` ( Scalar ` X ) ) /\ ( x e. ( Base ` X ) /\ y e. ( Base ` X ) /\ z e. ( Base ` X ) ) ) -> z e. ( Base ` W ) )
67 eqid 
 |-  ( +g ` W ) = ( +g ` W )
68 eqid 
 |-  ( +g ` ( Scalar ` W ) ) = ( +g ` ( Scalar ` W ) )
69 22 34 30 67 68 ipdir 
 |-  ( ( W e. PreHil /\ ( ( q ( .s ` W ) x ) e. ( Base ` W ) /\ y e. ( Base ` W ) /\ z e. ( Base ` W ) ) ) -> ( ( ( q ( .s ` W ) x ) ( +g ` W ) y ) ( .i ` W ) z ) = ( ( ( q ( .s ` W ) x ) ( .i ` W ) z ) ( +g ` ( Scalar ` W ) ) ( y ( .i ` W ) z ) ) )
70 50 61 63 66 69 syl13anc 
 |-  ( ( ( W e. PreHil /\ U e. S ) /\ q e. ( Base ` ( Scalar ` X ) ) /\ ( x e. ( Base ` X ) /\ y e. ( Base ` X ) /\ z e. ( Base ` X ) ) ) -> ( ( ( q ( .s ` W ) x ) ( +g ` W ) y ) ( .i ` W ) z ) = ( ( ( q ( .s ` W ) x ) ( .i ` W ) z ) ( +g ` ( Scalar ` W ) ) ( y ( .i ` W ) z ) ) )
71 eqid 
 |-  ( .r ` ( Scalar ` W ) ) = ( .r ` ( Scalar ` W ) )
72 22 34 30 35 59 71 ipass 
 |-  ( ( W e. PreHil /\ ( q e. ( Base ` ( Scalar ` W ) ) /\ x e. ( Base ` W ) /\ z e. ( Base ` W ) ) ) -> ( ( q ( .s ` W ) x ) ( .i ` W ) z ) = ( q ( .r ` ( Scalar ` W ) ) ( x ( .i ` W ) z ) ) )
73 50 56 58 66 72 syl13anc 
 |-  ( ( ( W e. PreHil /\ U e. S ) /\ q e. ( Base ` ( Scalar ` X ) ) /\ ( x e. ( Base ` X ) /\ y e. ( Base ` X ) /\ z e. ( Base ` X ) ) ) -> ( ( q ( .s ` W ) x ) ( .i ` W ) z ) = ( q ( .r ` ( Scalar ` W ) ) ( x ( .i ` W ) z ) ) )
74 73 oveq1d 
 |-  ( ( ( W e. PreHil /\ U e. S ) /\ q e. ( Base ` ( Scalar ` X ) ) /\ ( x e. ( Base ` X ) /\ y e. ( Base ` X ) /\ z e. ( Base ` X ) ) ) -> ( ( ( q ( .s ` W ) x ) ( .i ` W ) z ) ( +g ` ( Scalar ` W ) ) ( y ( .i ` W ) z ) ) = ( ( q ( .r ` ( Scalar ` W ) ) ( x ( .i ` W ) z ) ) ( +g ` ( Scalar ` W ) ) ( y ( .i ` W ) z ) ) )
75 70 74 eqtrd 
 |-  ( ( ( W e. PreHil /\ U e. S ) /\ q e. ( Base ` ( Scalar ` X ) ) /\ ( x e. ( Base ` X ) /\ y e. ( Base ` X ) /\ z e. ( Base ` X ) ) ) -> ( ( ( 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 ) ) )
76 1 67 ressplusg 
 |-  ( U e. S -> ( +g ` W ) = ( +g ` X ) )
77 76 eqcomd 
 |-  ( U e. S -> ( +g ` X ) = ( +g ` W ) )
78 1 59 ressvsca 
 |-  ( U e. S -> ( .s ` W ) = ( .s ` X ) )
79 78 eqcomd 
 |-  ( U e. S -> ( .s ` X ) = ( .s ` W ) )
80 79 oveqd 
 |-  ( U e. S -> ( q ( .s ` X ) x ) = ( q ( .s ` W ) x ) )
81 eqidd 
 |-  ( U e. S -> y = y )
82 77 80 81 oveq123d 
 |-  ( U e. S -> ( ( q ( .s ` X ) x ) ( +g ` X ) y ) = ( ( q ( .s ` W ) x ) ( +g ` W ) y ) )
83 eqidd 
 |-  ( U e. S -> z = z )
84 44 82 83 oveq123d 
 |-  ( U e. S -> ( ( ( q ( .s ` X ) x ) ( +g ` X ) y ) ( .i ` X ) z ) = ( ( ( q ( .s ` W ) x ) ( +g ` W ) y ) ( .i ` W ) z ) )
85 24 fveq2d 
 |-  ( U e. S -> ( +g ` ( Scalar ` X ) ) = ( +g ` ( Scalar ` W ) ) )
86 24 fveq2d 
 |-  ( U e. S -> ( .r ` ( Scalar ` X ) ) = ( .r ` ( Scalar ` W ) ) )
87 eqidd 
 |-  ( U e. S -> q = q )
88 44 oveqd 
 |-  ( U e. S -> ( x ( .i ` X ) z ) = ( x ( .i ` W ) z ) )
89 86 87 88 oveq123d 
 |-  ( U e. S -> ( q ( .r ` ( Scalar ` X ) ) ( x ( .i ` X ) z ) ) = ( q ( .r ` ( Scalar ` W ) ) ( x ( .i ` W ) z ) ) )
90 44 oveqd 
 |-  ( U e. S -> ( y ( .i ` X ) z ) = ( y ( .i ` W ) z ) )
91 85 89 90 oveq123d 
 |-  ( U e. S -> ( ( q ( .r ` ( Scalar ` X ) ) ( x ( .i ` X ) z ) ) ( +g ` ( Scalar ` X ) ) ( y ( .i ` X ) z ) ) = ( ( q ( .r ` ( Scalar ` W ) ) ( x ( .i ` W ) z ) ) ( +g ` ( Scalar ` W ) ) ( y ( .i ` W ) z ) ) )
92 84 91 eqeq12d 
 |-  ( U e. S -> ( ( ( ( q ( .s ` X ) x ) ( +g ` X ) y ) ( .i ` X ) z ) = ( ( q ( .r ` ( Scalar ` X ) ) ( x ( .i ` X ) z ) ) ( +g ` ( Scalar ` X ) ) ( y ( .i ` X ) 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 ) ) ) )
93 92 adantl 
 |-  ( ( W e. PreHil /\ U e. S ) -> ( ( ( ( q ( .s ` X ) x ) ( +g ` X ) y ) ( .i ` X ) z ) = ( ( q ( .r ` ( Scalar ` X ) ) ( x ( .i ` X ) z ) ) ( +g ` ( Scalar ` X ) ) ( y ( .i ` X ) 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 ) ) ) )
94 93 3ad2ant1 
 |-  ( ( ( W e. PreHil /\ U e. S ) /\ q e. ( Base ` ( Scalar ` X ) ) /\ ( x e. ( Base ` X ) /\ y e. ( Base ` X ) /\ z e. ( Base ` X ) ) ) -> ( ( ( ( q ( .s ` X ) x ) ( +g ` X ) y ) ( .i ` X ) z ) = ( ( q ( .r ` ( Scalar ` X ) ) ( x ( .i ` X ) z ) ) ( +g ` ( Scalar ` X ) ) ( y ( .i ` X ) 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 ) ) ) )
95 75 94 mpbird 
 |-  ( ( ( W e. PreHil /\ U e. S ) /\ q e. ( Base ` ( Scalar ` X ) ) /\ ( x e. ( Base ` X ) /\ y e. ( Base ` X ) /\ z e. ( Base ` X ) ) ) -> ( ( ( q ( .s ` X ) x ) ( +g ` X ) y ) ( .i ` X ) z ) = ( ( q ( .r ` ( Scalar ` X ) ) ( x ( .i ` X ) z ) ) ( +g ` ( Scalar ` X ) ) ( y ( .i ` X ) z ) ) )
96 44 adantl 
 |-  ( ( W e. PreHil /\ U e. S ) -> ( .i ` X ) = ( .i ` W ) )
97 96 oveqdr 
 |-  ( ( ( W e. PreHil /\ U e. S ) /\ x e. ( Base ` X ) ) -> ( x ( .i ` X ) x ) = ( x ( .i ` W ) x ) )
98 24 fveq2d 
 |-  ( U e. S -> ( 0g ` ( Scalar ` X ) ) = ( 0g ` ( Scalar ` W ) ) )
99 98 adantl 
 |-  ( ( W e. PreHil /\ U e. S ) -> ( 0g ` ( Scalar ` X ) ) = ( 0g ` ( Scalar ` W ) ) )
100 99 adantr 
 |-  ( ( ( W e. PreHil /\ U e. S ) /\ x e. ( Base ` X ) ) -> ( 0g ` ( Scalar ` X ) ) = ( 0g ` ( Scalar ` W ) ) )
101 97 100 eqeq12d 
 |-  ( ( ( W e. PreHil /\ U e. S ) /\ x e. ( Base ` X ) ) -> ( ( x ( .i ` X ) x ) = ( 0g ` ( Scalar ` X ) ) <-> ( x ( .i ` W ) x ) = ( 0g ` ( Scalar ` W ) ) ) )
102 eqid 
 |-  ( 0g ` ( Scalar ` W ) ) = ( 0g ` ( Scalar ` W ) )
103 22 34 30 102 8 ipeq0 
 |-  ( ( W e. PreHil /\ x e. ( Base ` W ) ) -> ( ( x ( .i ` W ) x ) = ( 0g ` ( Scalar ` W ) ) <-> x = ( 0g ` W ) ) )
104 29 32 103 syl2an 
 |-  ( ( ( W e. PreHil /\ U e. S ) /\ x e. ( Base ` X ) ) -> ( ( x ( .i ` W ) x ) = ( 0g ` ( Scalar ` W ) ) <-> x = ( 0g ` W ) ) )
105 104 biimpd 
 |-  ( ( ( W e. PreHil /\ U e. S ) /\ x e. ( Base ` X ) ) -> ( ( x ( .i ` W ) x ) = ( 0g ` ( Scalar ` W ) ) -> x = ( 0g ` W ) ) )
106 101 105 sylbid 
 |-  ( ( ( W e. PreHil /\ U e. S ) /\ x e. ( Base ` X ) ) -> ( ( x ( .i ` X ) x ) = ( 0g ` ( Scalar ` X ) ) -> x = ( 0g ` W ) ) )
107 106 3impia 
 |-  ( ( ( W e. PreHil /\ U e. S ) /\ x e. ( Base ` X ) /\ ( x ( .i ` X ) x ) = ( 0g ` ( Scalar ` X ) ) ) -> x = ( 0g ` W ) )
108 24 fveq2d 
 |-  ( U e. S -> ( *r ` ( Scalar ` X ) ) = ( *r ` ( Scalar ` W ) ) )
109 108 fveq1d 
 |-  ( U e. S -> ( ( *r ` ( Scalar ` X ) ) ` ( x ( .i ` W ) y ) ) = ( ( *r ` ( Scalar ` W ) ) ` ( x ( .i ` W ) y ) ) )
110 109 adantl 
 |-  ( ( W e. PreHil /\ U e. S ) -> ( ( *r ` ( Scalar ` X ) ) ` ( x ( .i ` W ) y ) ) = ( ( *r ` ( Scalar ` W ) ) ` ( x ( .i ` W ) y ) ) )
111 110 3ad2ant1 
 |-  ( ( ( W e. PreHil /\ U e. S ) /\ x e. ( Base ` X ) /\ y e. ( Base ` X ) ) -> ( ( *r ` ( Scalar ` X ) ) ` ( x ( .i ` W ) y ) ) = ( ( *r ` ( Scalar ` W ) ) ` ( x ( .i ` W ) y ) ) )
112 eqid 
 |-  ( *r ` ( Scalar ` W ) ) = ( *r ` ( Scalar ` W ) )
113 22 34 30 112 ipcj 
 |-  ( ( W e. PreHil /\ x e. ( Base ` W ) /\ y e. ( Base ` W ) ) -> ( ( *r ` ( Scalar ` W ) ) ` ( x ( .i ` W ) y ) ) = ( y ( .i ` W ) x ) )
114 29 32 33 113 syl3an 
 |-  ( ( ( W e. PreHil /\ U e. S ) /\ x e. ( Base ` X ) /\ y e. ( Base ` X ) ) -> ( ( *r ` ( Scalar ` W ) ) ` ( x ( .i ` W ) y ) ) = ( y ( .i ` W ) x ) )
115 111 114 eqtrd 
 |-  ( ( ( W e. PreHil /\ U e. S ) /\ x e. ( Base ` X ) /\ y e. ( Base ` X ) ) -> ( ( *r ` ( Scalar ` X ) ) ` ( x ( .i ` W ) y ) ) = ( y ( .i ` W ) x ) )
116 45 fveq2d 
 |-  ( U e. S -> ( ( *r ` ( Scalar ` X ) ) ` ( x ( .i ` X ) y ) ) = ( ( *r ` ( Scalar ` X ) ) ` ( x ( .i ` W ) y ) ) )
117 44 oveqd 
 |-  ( U e. S -> ( y ( .i ` X ) x ) = ( y ( .i ` W ) x ) )
118 116 117 eqeq12d 
 |-  ( U e. S -> ( ( ( *r ` ( Scalar ` X ) ) ` ( x ( .i ` X ) y ) ) = ( y ( .i ` X ) x ) <-> ( ( *r ` ( Scalar ` X ) ) ` ( x ( .i ` W ) y ) ) = ( y ( .i ` W ) x ) ) )
119 118 adantl 
 |-  ( ( W e. PreHil /\ U e. S ) -> ( ( ( *r ` ( Scalar ` X ) ) ` ( x ( .i ` X ) y ) ) = ( y ( .i ` X ) x ) <-> ( ( *r ` ( Scalar ` X ) ) ` ( x ( .i ` W ) y ) ) = ( y ( .i ` W ) x ) ) )
120 119 3ad2ant1 
 |-  ( ( ( W e. PreHil /\ U e. S ) /\ x e. ( Base ` X ) /\ y e. ( Base ` X ) ) -> ( ( ( *r ` ( Scalar ` X ) ) ` ( x ( .i ` X ) y ) ) = ( y ( .i ` X ) x ) <-> ( ( *r ` ( Scalar ` X ) ) ` ( x ( .i ` W ) y ) ) = ( y ( .i ` W ) x ) ) )
121 115 120 mpbird 
 |-  ( ( ( W e. PreHil /\ U e. S ) /\ x e. ( Base ` X ) /\ y e. ( Base ` X ) ) -> ( ( *r ` ( Scalar ` X ) ) ` ( x ( .i ` X ) y ) ) = ( y ( .i ` X ) x ) )
122 3 4 5 6 12 13 14 15 16 17 18 21 28 49 95 107 121 isphld 
 |-  ( ( W e. PreHil /\ U e. S ) -> X e. PreHil )