Description: Conjugate law for inner product. Postulate (S1) of Beran p. 95. (Contributed by NM, 15-May-2005) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Hypotheses | his1.1 | |- A e. ~H |
|
his1.2 | |- B e. ~H |
||
Assertion | his1i | |- ( A .ih B ) = ( * ` ( B .ih A ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | his1.1 | |- A e. ~H |
|
2 | his1.2 | |- B e. ~H |
|
3 | ax-his1 | |- ( ( A e. ~H /\ B e. ~H ) -> ( A .ih B ) = ( * ` ( B .ih A ) ) ) |
|
4 | 1 2 3 | mp2an | |- ( A .ih B ) = ( * ` ( B .ih A ) ) |