# Metamath Proof Explorer

Description: Hilbert vector space addition law. (Contributed by NM, 16-Oct-1999) (New usage is discouraged.)

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

### Proof

Step Hyp Ref Expression
1 hvadd32 ${⊢}\left({A}\in ℋ\wedge {B}\in ℋ\wedge {C}\in ℋ\right)\to \left({A}{+}_{ℎ}{B}\right){+}_{ℎ}{C}=\left({A}{+}_{ℎ}{C}\right){+}_{ℎ}{B}$
2 1 oveq1d ${⊢}\left({A}\in ℋ\wedge {B}\in ℋ\wedge {C}\in ℋ\right)\to \left(\left({A}{+}_{ℎ}{B}\right){+}_{ℎ}{C}\right){+}_{ℎ}{D}=\left(\left({A}{+}_{ℎ}{C}\right){+}_{ℎ}{B}\right){+}_{ℎ}{D}$
3 2 3expa ${⊢}\left(\left({A}\in ℋ\wedge {B}\in ℋ\right)\wedge {C}\in ℋ\right)\to \left(\left({A}{+}_{ℎ}{B}\right){+}_{ℎ}{C}\right){+}_{ℎ}{D}=\left(\left({A}{+}_{ℎ}{C}\right){+}_{ℎ}{B}\right){+}_{ℎ}{D}$
4 3 adantrr ${⊢}\left(\left({A}\in ℋ\wedge {B}\in ℋ\right)\wedge \left({C}\in ℋ\wedge {D}\in ℋ\right)\right)\to \left(\left({A}{+}_{ℎ}{B}\right){+}_{ℎ}{C}\right){+}_{ℎ}{D}=\left(\left({A}{+}_{ℎ}{C}\right){+}_{ℎ}{B}\right){+}_{ℎ}{D}$
5 hvaddcl ${⊢}\left({A}\in ℋ\wedge {B}\in ℋ\right)\to {A}{+}_{ℎ}{B}\in ℋ$
6 ax-hvass ${⊢}\left({A}{+}_{ℎ}{B}\in ℋ\wedge {C}\in ℋ\wedge {D}\in ℋ\right)\to \left(\left({A}{+}_{ℎ}{B}\right){+}_{ℎ}{C}\right){+}_{ℎ}{D}=\left({A}{+}_{ℎ}{B}\right){+}_{ℎ}\left({C}{+}_{ℎ}{D}\right)$
7 6 3expb ${⊢}\left({A}{+}_{ℎ}{B}\in ℋ\wedge \left({C}\in ℋ\wedge {D}\in ℋ\right)\right)\to \left(\left({A}{+}_{ℎ}{B}\right){+}_{ℎ}{C}\right){+}_{ℎ}{D}=\left({A}{+}_{ℎ}{B}\right){+}_{ℎ}\left({C}{+}_{ℎ}{D}\right)$
8 5 7 sylan ${⊢}\left(\left({A}\in ℋ\wedge {B}\in ℋ\right)\wedge \left({C}\in ℋ\wedge {D}\in ℋ\right)\right)\to \left(\left({A}{+}_{ℎ}{B}\right){+}_{ℎ}{C}\right){+}_{ℎ}{D}=\left({A}{+}_{ℎ}{B}\right){+}_{ℎ}\left({C}{+}_{ℎ}{D}\right)$
9 hvaddcl ${⊢}\left({A}\in ℋ\wedge {C}\in ℋ\right)\to {A}{+}_{ℎ}{C}\in ℋ$
10 ax-hvass ${⊢}\left({A}{+}_{ℎ}{C}\in ℋ\wedge {B}\in ℋ\wedge {D}\in ℋ\right)\to \left(\left({A}{+}_{ℎ}{C}\right){+}_{ℎ}{B}\right){+}_{ℎ}{D}=\left({A}{+}_{ℎ}{C}\right){+}_{ℎ}\left({B}{+}_{ℎ}{D}\right)$
11 10 3expb ${⊢}\left({A}{+}_{ℎ}{C}\in ℋ\wedge \left({B}\in ℋ\wedge {D}\in ℋ\right)\right)\to \left(\left({A}{+}_{ℎ}{C}\right){+}_{ℎ}{B}\right){+}_{ℎ}{D}=\left({A}{+}_{ℎ}{C}\right){+}_{ℎ}\left({B}{+}_{ℎ}{D}\right)$
12 9 11 sylan ${⊢}\left(\left({A}\in ℋ\wedge {C}\in ℋ\right)\wedge \left({B}\in ℋ\wedge {D}\in ℋ\right)\right)\to \left(\left({A}{+}_{ℎ}{C}\right){+}_{ℎ}{B}\right){+}_{ℎ}{D}=\left({A}{+}_{ℎ}{C}\right){+}_{ℎ}\left({B}{+}_{ℎ}{D}\right)$
13 12 an4s ${⊢}\left(\left({A}\in ℋ\wedge {B}\in ℋ\right)\wedge \left({C}\in ℋ\wedge {D}\in ℋ\right)\right)\to \left(\left({A}{+}_{ℎ}{C}\right){+}_{ℎ}{B}\right){+}_{ℎ}{D}=\left({A}{+}_{ℎ}{C}\right){+}_{ℎ}\left({B}{+}_{ℎ}{D}\right)$
14 4 8 13 3eqtr3d ${⊢}\left(\left({A}\in ℋ\wedge {B}\in ℋ\right)\wedge \left({C}\in ℋ\wedge {D}\in ℋ\right)\right)\to \left({A}{+}_{ℎ}{B}\right){+}_{ℎ}\left({C}{+}_{ℎ}{D}\right)=\left({A}{+}_{ℎ}{C}\right){+}_{ℎ}\left({B}{+}_{ℎ}{D}\right)$