Metamath Proof Explorer

Theorem addrcom

Description: Vector addition is commutative. (Contributed by Andrew Salmon, 28-Jan-2012)

Ref Expression
Assertion addrcom 
|- ( ( A e. C /\ B e. D ) -> ( A +r B ) = ( B +r A ) )

Proof

Step Hyp Ref Expression
1 addrfn 
 |-  ( ( A e. C /\ B e. D ) -> ( A +r B ) Fn RR )
2 addrfn 
 |-  ( ( B e. D /\ A e. C ) -> ( B +r A ) Fn RR )
3 2 ancoms 
 |-  ( ( A e. C /\ B e. D ) -> ( B +r A ) Fn RR )
4 addcomgi 
 |-  ( ( A ` x ) + ( B ` x ) ) = ( ( B ` x ) + ( A ` x ) )
5 addrfv 
 |-  ( ( A e. C /\ B e. D /\ x e. RR ) -> ( ( A +r B ) ` x ) = ( ( A ` x ) + ( B ` x ) ) )
6 addrfv 
 |-  ( ( B e. D /\ A e. C /\ x e. RR ) -> ( ( B +r A ) ` x ) = ( ( B ` x ) + ( A ` x ) ) )
7 6 3com12 
 |-  ( ( A e. C /\ B e. D /\ x e. RR ) -> ( ( B +r A ) ` x ) = ( ( B ` x ) + ( A ` x ) ) )
8 4 5 7 3eqtr4a 
 |-  ( ( A e. C /\ B e. D /\ x e. RR ) -> ( ( A +r B ) ` x ) = ( ( B +r A ) ` x ) )
9 8 3expia 
 |-  ( ( A e. C /\ B e. D ) -> ( x e. RR -> ( ( A +r B ) ` x ) = ( ( B +r A ) ` x ) ) )
10 9 ralrimiv 
 |-  ( ( A e. C /\ B e. D ) -> A. x e. RR ( ( A +r B ) ` x ) = ( ( B +r A ) ` x ) )
11 eqfnfv 
 |-  ( ( ( A +r B ) Fn RR /\ ( B +r A ) Fn RR ) -> ( ( A +r B ) = ( B +r A ) <-> A. x e. RR ( ( A +r B ) ` x ) = ( ( B +r A ) ` x ) ) )
12 10 11 syl5ibrcom 
 |-  ( ( A e. C /\ B e. D ) -> ( ( ( A +r B ) Fn RR /\ ( B +r A ) Fn RR ) -> ( A +r B ) = ( B +r A ) ) )
13 1 3 12 mp2and 
 |-  ( ( A e. C /\ B e. D ) -> ( A +r B ) = ( B +r A ) )