Metamath Proof Explorer

Description: Commutative/associative law. (Contributed by NM, 19-Oct-1999) (New usage is discouraged.)

Ref Expression
Assertion hvaddsub12 ${⊢}\left({A}\in ℋ\wedge {B}\in ℋ\wedge {C}\in ℋ\right)\to {A}{+}_{ℎ}\left({B}{-}_{ℎ}{C}\right)={B}{+}_{ℎ}\left({A}{-}_{ℎ}{C}\right)$

Proof

Step Hyp Ref Expression
1 neg1cn ${⊢}-1\in ℂ$
2 hvmulcl ${⊢}\left(-1\in ℂ\wedge {C}\in ℋ\right)\to -1{\cdot }_{ℎ}{C}\in ℋ$
3 1 2 mpan ${⊢}{C}\in ℋ\to -1{\cdot }_{ℎ}{C}\in ℋ$
4 hvadd12 ${⊢}\left({A}\in ℋ\wedge {B}\in ℋ\wedge -1{\cdot }_{ℎ}{C}\in ℋ\right)\to {A}{+}_{ℎ}\left({B}{+}_{ℎ}\left(-1{\cdot }_{ℎ}{C}\right)\right)={B}{+}_{ℎ}\left({A}{+}_{ℎ}\left(-1{\cdot }_{ℎ}{C}\right)\right)$
5 3 4 syl3an3 ${⊢}\left({A}\in ℋ\wedge {B}\in ℋ\wedge {C}\in ℋ\right)\to {A}{+}_{ℎ}\left({B}{+}_{ℎ}\left(-1{\cdot }_{ℎ}{C}\right)\right)={B}{+}_{ℎ}\left({A}{+}_{ℎ}\left(-1{\cdot }_{ℎ}{C}\right)\right)$
6 hvsubval ${⊢}\left({B}\in ℋ\wedge {C}\in ℋ\right)\to {B}{-}_{ℎ}{C}={B}{+}_{ℎ}\left(-1{\cdot }_{ℎ}{C}\right)$
7 6 oveq2d ${⊢}\left({B}\in ℋ\wedge {C}\in ℋ\right)\to {A}{+}_{ℎ}\left({B}{-}_{ℎ}{C}\right)={A}{+}_{ℎ}\left({B}{+}_{ℎ}\left(-1{\cdot }_{ℎ}{C}\right)\right)$
8 7 3adant1 ${⊢}\left({A}\in ℋ\wedge {B}\in ℋ\wedge {C}\in ℋ\right)\to {A}{+}_{ℎ}\left({B}{-}_{ℎ}{C}\right)={A}{+}_{ℎ}\left({B}{+}_{ℎ}\left(-1{\cdot }_{ℎ}{C}\right)\right)$
9 hvsubval ${⊢}\left({A}\in ℋ\wedge {C}\in ℋ\right)\to {A}{-}_{ℎ}{C}={A}{+}_{ℎ}\left(-1{\cdot }_{ℎ}{C}\right)$
10 9 oveq2d ${⊢}\left({A}\in ℋ\wedge {C}\in ℋ\right)\to {B}{+}_{ℎ}\left({A}{-}_{ℎ}{C}\right)={B}{+}_{ℎ}\left({A}{+}_{ℎ}\left(-1{\cdot }_{ℎ}{C}\right)\right)$
11 10 3adant2 ${⊢}\left({A}\in ℋ\wedge {B}\in ℋ\wedge {C}\in ℋ\right)\to {B}{+}_{ℎ}\left({A}{-}_{ℎ}{C}\right)={B}{+}_{ℎ}\left({A}{+}_{ℎ}\left(-1{\cdot }_{ℎ}{C}\right)\right)$
12 5 8 11 3eqtr4d ${⊢}\left({A}\in ℋ\wedge {B}\in ℋ\wedge {C}\in ℋ\right)\to {A}{+}_{ℎ}\left({B}{-}_{ℎ}{C}\right)={B}{+}_{ℎ}\left({A}{-}_{ℎ}{C}\right)$