Theorem hvcomi 10521

Description: Commutation of vector addition.

Hypotheses

Ref	Expression
hvaddcl.1	|- A e. ~H
hvaddcl.2	|- B e. ~H

Assertion

Ref	Expression
hvcomi	|- (A +h B) = (B +h A)

Proof of Theorem hvcomi

Step	Hyp	Ref	Expression
1		hvaddcl.1	. 2 |- A e. ~H
2		hvaddcl.2	. 2 |- B e. ~H
3		ax-hvcom 10503	. 2 |- ((A e. ~H /\ B e. ~H) -> (A +h B) = (B +h A))
4	1, 2, 3	mp2an 761	1 |- (A +h B) = (B +h A)

Syntax hints:   = wceq 1298   e. wcel 1300  (class class class)co 4884  ~Hchil 10420   +h cva 10421

This theorem is referenced by:  hvsub23i 10555  hvadd12i 10556  hvnegdii 10561  norm3difi 10647  normpar2i 10656  nonbooli 11231  lnophmlem2 11579

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-hvcom 10503

This theorem depends on definitions:  df-bi 164  df-an 242

Copyright terms: Public domain