Metamath Proof Explorer

Theorem hvadd4

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

Ref Expression
Assertion hvadd4 ⊢A∈ℋ∧B∈ℋ∧C∈ℋ∧D∈ℋ→A+ℎB+ℎC+ℎD=A+ℎC+ℎB+ℎD

Proof

Step Hyp Ref Expression
1 hvadd32 ⊢A∈ℋ∧B∈ℋ∧C∈ℋ→A+ℎB+ℎC=A+ℎC+ℎB
2 1 oveq1d ⊢A∈ℋ∧B∈ℋ∧C∈ℋ→A+ℎB+ℎC+ℎD=A+ℎC+ℎB+ℎD
3 2 3expa ⊢A∈ℋ∧B∈ℋ∧C∈ℋ→A+ℎB+ℎC+ℎD=A+ℎC+ℎB+ℎD
4 3 adantrr ⊢A∈ℋ∧B∈ℋ∧C∈ℋ∧D∈ℋ→A+ℎB+ℎC+ℎD=A+ℎC+ℎB+ℎD
5 hvaddcl ⊢A∈ℋ∧B∈ℋ→A+ℎB∈ℋ
6 ax-hvass ⊢A+ℎB∈ℋ∧C∈ℋ∧D∈ℋ→A+ℎB+ℎC+ℎD=A+ℎB+ℎC+ℎD
7 6 3expb ⊢A+ℎB∈ℋ∧C∈ℋ∧D∈ℋ→A+ℎB+ℎC+ℎD=A+ℎB+ℎC+ℎD
8 5 7 sylan ⊢A∈ℋ∧B∈ℋ∧C∈ℋ∧D∈ℋ→A+ℎB+ℎC+ℎD=A+ℎB+ℎC+ℎD
9 hvaddcl ⊢A∈ℋ∧C∈ℋ→A+ℎC∈ℋ
10 ax-hvass ⊢A+ℎC∈ℋ∧B∈ℋ∧D∈ℋ→A+ℎC+ℎB+ℎD=A+ℎC+ℎB+ℎD
11 10 3expb ⊢A+ℎC∈ℋ∧B∈ℋ∧D∈ℋ→A+ℎC+ℎB+ℎD=A+ℎC+ℎB+ℎD
12 9 11 sylan ⊢A∈ℋ∧C∈ℋ∧B∈ℋ∧D∈ℋ→A+ℎC+ℎB+ℎD=A+ℎC+ℎB+ℎD
13 12 an4s ⊢A∈ℋ∧B∈ℋ∧C∈ℋ∧D∈ℋ→A+ℎC+ℎB+ℎD=A+ℎC+ℎB+ℎD
14 4 8 13 3eqtr3d ⊢A∈ℋ∧B∈ℋ∧C∈ℋ∧D∈ℋ→A+ℎB+ℎC+ℎD=A+ℎC+ℎB+ℎD