Theorem hvadd12i

Description: Hilbert vector space commutative/associative law. (Contributed by NM, 11-Sep-1999) (New usage is discouraged.)

	Ref	Expression
Hypotheses	hvass.1	$$⊢A\in \mathscr{H}$$
	hvass.2	$$⊢B\in \mathscr{H}$$
	hvass.3	$$⊢C\in \mathscr{H}$$
Assertion	hvadd12i	$$⊢A{+}_{ℎ}\left(B{+}_{ℎ}C\right)=B{+}_{ℎ}\left(A{+}_{ℎ}C\right)$$

Proof

Step	Hyp	Ref	Expression
1		hvass.1	$$⊢A\in \mathscr{H}$$
2		hvass.2	$$⊢B\in \mathscr{H}$$
3		hvass.3	$$⊢C\in \mathscr{H}$$
4	1 2	hvcomi	$$⊢A{+}_{ℎ}B=B{+}_{ℎ}A$$
5	4	oveq1i	$$⊢\left(A{+}_{ℎ}B\right){+}_{ℎ}C=\left(B{+}_{ℎ}A\right){+}_{ℎ}C$$
6	1 2 3	hvassi	$$⊢\left(A{+}_{ℎ}B\right){+}_{ℎ}C=A{+}_{ℎ}\left(B{+}_{ℎ}C\right)$$
7	2 1 3	hvassi	$$⊢\left(B{+}_{ℎ}A\right){+}_{ℎ}C=B{+}_{ℎ}\left(A{+}_{ℎ}C\right)$$
8	5 6 7	3eqtr3i	$$⊢A{+}_{ℎ}\left(B{+}_{ℎ}C\right)=B{+}_{ℎ}\left(A{+}_{ℎ}C\right)$$