This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ipcj

Description: Conjugate of an inner product in a pre-Hilbert space. Equation I1 of Ponnusamy p. 362. (Contributed by NM, 1-Feb-2007) (Revised by Mario Carneiro, 7-Oct-2015)

Ref Expression
Hypotheses phlsrng.f 
|- F = ( Scalar ` W )
phllmhm.h 
|- ., = ( .i ` W )
phllmhm.v 
|- V = ( Base ` W )
ipcj.i 
|- .* = ( *r ` F )
Assertion ipcj 
|- ( ( W e. PreHil /\ A e. V /\ B e. V ) -> ( .* ` ( A ., B ) ) = ( B ., A ) )

Proof

Step Hyp Ref Expression
1 phlsrng.f 
 |-  F = ( Scalar ` W )
2 phllmhm.h 
 |-  ., = ( .i ` W )
3 phllmhm.v 
 |-  V = ( Base ` W )
4 ipcj.i 
 |-  .* = ( *r ` F )
5 eqid 
 |-  ( 0g ` W ) = ( 0g ` W )
6 eqid 
 |-  ( 0g ` F ) = ( 0g ` F )
7 3 1 2 5 4 6 isphl 
 |-  ( W e. PreHil <-> ( W e. LVec /\ F e. *Ring /\ A. x e. V ( ( y e. V |-> ( y ., x ) ) e. ( W LMHom ( ringLMod ` F ) ) /\ ( ( x ., x ) = ( 0g ` F ) -> x = ( 0g ` W ) ) /\ A. y e. V ( .* ` ( x ., y ) ) = ( y ., x ) ) ) )
8 7 simp3bi 
 |-  ( W e. PreHil -> A. x e. V ( ( y e. V |-> ( y ., x ) ) e. ( W LMHom ( ringLMod ` F ) ) /\ ( ( x ., x ) = ( 0g ` F ) -> x = ( 0g ` W ) ) /\ A. y e. V ( .* ` ( x ., y ) ) = ( y ., x ) ) )
9 simp3 
 |-  ( ( ( y e. V |-> ( y ., x ) ) e. ( W LMHom ( ringLMod ` F ) ) /\ ( ( x ., x ) = ( 0g ` F ) -> x = ( 0g ` W ) ) /\ A. y e. V ( .* ` ( x ., y ) ) = ( y ., x ) ) -> A. y e. V ( .* ` ( x ., y ) ) = ( y ., x ) )
10 9 ralimi 
 |-  ( A. x e. V ( ( y e. V |-> ( y ., x ) ) e. ( W LMHom ( ringLMod ` F ) ) /\ ( ( x ., x ) = ( 0g ` F ) -> x = ( 0g ` W ) ) /\ A. y e. V ( .* ` ( x ., y ) ) = ( y ., x ) ) -> A. x e. V A. y e. V ( .* ` ( x ., y ) ) = ( y ., x ) )
11 8 10 syl 
 |-  ( W e. PreHil -> A. x e. V A. y e. V ( .* ` ( x ., y ) ) = ( y ., x ) )
12 fvoveq1 
 |-  ( x = A -> ( .* ` ( x ., y ) ) = ( .* ` ( A ., y ) ) )
13 oveq2 
 |-  ( x = A -> ( y ., x ) = ( y ., A ) )
14 12 13 eqeq12d 
 |-  ( x = A -> ( ( .* ` ( x ., y ) ) = ( y ., x ) <-> ( .* ` ( A ., y ) ) = ( y ., A ) ) )
15 oveq2 
 |-  ( y = B -> ( A ., y ) = ( A ., B ) )
16 15 fveq2d 
 |-  ( y = B -> ( .* ` ( A ., y ) ) = ( .* ` ( A ., B ) ) )
17 oveq1 
 |-  ( y = B -> ( y ., A ) = ( B ., A ) )
18 16 17 eqeq12d 
 |-  ( y = B -> ( ( .* ` ( A ., y ) ) = ( y ., A ) <-> ( .* ` ( A ., B ) ) = ( B ., A ) ) )
19 14 18 rspc2v 
 |-  ( ( A e. V /\ B e. V ) -> ( A. x e. V A. y e. V ( .* ` ( x ., y ) ) = ( y ., x ) -> ( .* ` ( A ., B ) ) = ( B ., A ) ) )
20 11 19 syl5com 
 |-  ( W e. PreHil -> ( ( A e. V /\ B e. V ) -> ( .* ` ( A ., B ) ) = ( B ., A ) ) )
21 20 3impib 
 |-  ( ( W e. PreHil /\ A e. V /\ B e. V ) -> ( .* ` ( A ., B ) ) = ( B ., A ) )