Theorem hvsub4

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

	Ref	Expression
Assertion	hvsub4	⊢ ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) ∧ ( 𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ ) ) → ( ( 𝐴 +ℎ 𝐵 ) −ℎ ( 𝐶 +ℎ 𝐷 ) ) = ( ( 𝐴 −ℎ 𝐶 ) +ℎ ( 𝐵 −ℎ 𝐷 ) ) )

Proof

Step	Hyp	Ref	Expression
1		hvaddcl	⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( 𝐴 +ℎ 𝐵 ) ∈ ℋ )
2		hvaddcl	⊢ ( ( 𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ ) → ( 𝐶 +ℎ 𝐷 ) ∈ ℋ )
3		hvsubval	⊢ ( ( ( 𝐴 +ℎ 𝐵 ) ∈ ℋ ∧ ( 𝐶 +ℎ 𝐷 ) ∈ ℋ ) → ( ( 𝐴 +ℎ 𝐵 ) −ℎ ( 𝐶 +ℎ 𝐷 ) ) = ( ( 𝐴 +ℎ 𝐵 ) +ℎ ( - 1 ·ℎ ( 𝐶 +ℎ 𝐷 ) ) ) )
4	1 2 3	syl2an	⊢ ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) ∧ ( 𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ ) ) → ( ( 𝐴 +ℎ 𝐵 ) −ℎ ( 𝐶 +ℎ 𝐷 ) ) = ( ( 𝐴 +ℎ 𝐵 ) +ℎ ( - 1 ·ℎ ( 𝐶 +ℎ 𝐷 ) ) ) )
5		hvsubval	⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐶 ∈ ℋ ) → ( 𝐴 −ℎ 𝐶 ) = ( 𝐴 +ℎ ( - 1 ·ℎ 𝐶 ) ) )
6	5	ad2ant2r	⊢ ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) ∧ ( 𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ ) ) → ( 𝐴 −ℎ 𝐶 ) = ( 𝐴 +ℎ ( - 1 ·ℎ 𝐶 ) ) )
7		hvsubval	⊢ ( ( 𝐵 ∈ ℋ ∧ 𝐷 ∈ ℋ ) → ( 𝐵 −ℎ 𝐷 ) = ( 𝐵 +ℎ ( - 1 ·ℎ 𝐷 ) ) )
8	7	ad2ant2l	⊢ ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) ∧ ( 𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ ) ) → ( 𝐵 −ℎ 𝐷 ) = ( 𝐵 +ℎ ( - 1 ·ℎ 𝐷 ) ) )
9	6 8	oveq12d	⊢ ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) ∧ ( 𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ ) ) → ( ( 𝐴 −ℎ 𝐶 ) +ℎ ( 𝐵 −ℎ 𝐷 ) ) = ( ( 𝐴 +ℎ ( - 1 ·ℎ 𝐶 ) ) +ℎ ( 𝐵 +ℎ ( - 1 ·ℎ 𝐷 ) ) ) )
10		neg1cn	⊢ - 1 ∈ ℂ
11		ax-hvdistr1	⊢ ( ( - 1 ∈ ℂ ∧ 𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ ) → ( - 1 ·ℎ ( 𝐶 +ℎ 𝐷 ) ) = ( ( - 1 ·ℎ 𝐶 ) +ℎ ( - 1 ·ℎ 𝐷 ) ) )
12	10 11	mp3an1	⊢ ( ( 𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ ) → ( - 1 ·ℎ ( 𝐶 +ℎ 𝐷 ) ) = ( ( - 1 ·ℎ 𝐶 ) +ℎ ( - 1 ·ℎ 𝐷 ) ) )
13	12	adantl	⊢ ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) ∧ ( 𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ ) ) → ( - 1 ·ℎ ( 𝐶 +ℎ 𝐷 ) ) = ( ( - 1 ·ℎ 𝐶 ) +ℎ ( - 1 ·ℎ 𝐷 ) ) )
14	13	oveq2d	⊢ ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) ∧ ( 𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ ) ) → ( ( 𝐴 +ℎ 𝐵 ) +ℎ ( - 1 ·ℎ ( 𝐶 +ℎ 𝐷 ) ) ) = ( ( 𝐴 +ℎ 𝐵 ) +ℎ ( ( - 1 ·ℎ 𝐶 ) +ℎ ( - 1 ·ℎ 𝐷 ) ) ) )
15		hvmulcl	⊢ ( ( - 1 ∈ ℂ ∧ 𝐶 ∈ ℋ ) → ( - 1 ·ℎ 𝐶 ) ∈ ℋ )
16	10 15	mpan	⊢ ( 𝐶 ∈ ℋ → ( - 1 ·ℎ 𝐶 ) ∈ ℋ )
17	16	anim2i	⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐶 ∈ ℋ ) → ( 𝐴 ∈ ℋ ∧ ( - 1 ·ℎ 𝐶 ) ∈ ℋ ) )
18		hvmulcl	⊢ ( ( - 1 ∈ ℂ ∧ 𝐷 ∈ ℋ ) → ( - 1 ·ℎ 𝐷 ) ∈ ℋ )
19	10 18	mpan	⊢ ( 𝐷 ∈ ℋ → ( - 1 ·ℎ 𝐷 ) ∈ ℋ )
20	19	anim2i	⊢ ( ( 𝐵 ∈ ℋ ∧ 𝐷 ∈ ℋ ) → ( 𝐵 ∈ ℋ ∧ ( - 1 ·ℎ 𝐷 ) ∈ ℋ ) )
21	17 20	anim12i	⊢ ( ( ( 𝐴 ∈ ℋ ∧ 𝐶 ∈ ℋ ) ∧ ( 𝐵 ∈ ℋ ∧ 𝐷 ∈ ℋ ) ) → ( ( 𝐴 ∈ ℋ ∧ ( - 1 ·ℎ 𝐶 ) ∈ ℋ ) ∧ ( 𝐵 ∈ ℋ ∧ ( - 1 ·ℎ 𝐷 ) ∈ ℋ ) ) )
22	21	an4s	⊢ ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) ∧ ( 𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ ) ) → ( ( 𝐴 ∈ ℋ ∧ ( - 1 ·ℎ 𝐶 ) ∈ ℋ ) ∧ ( 𝐵 ∈ ℋ ∧ ( - 1 ·ℎ 𝐷 ) ∈ ℋ ) ) )
23		hvadd4	⊢ ( ( ( 𝐴 ∈ ℋ ∧ ( - 1 ·ℎ 𝐶 ) ∈ ℋ ) ∧ ( 𝐵 ∈ ℋ ∧ ( - 1 ·ℎ 𝐷 ) ∈ ℋ ) ) → ( ( 𝐴 +ℎ ( - 1 ·ℎ 𝐶 ) ) +ℎ ( 𝐵 +ℎ ( - 1 ·ℎ 𝐷 ) ) ) = ( ( 𝐴 +ℎ 𝐵 ) +ℎ ( ( - 1 ·ℎ 𝐶 ) +ℎ ( - 1 ·ℎ 𝐷 ) ) ) )
24	22 23	syl	⊢ ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) ∧ ( 𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ ) ) → ( ( 𝐴 +ℎ ( - 1 ·ℎ 𝐶 ) ) +ℎ ( 𝐵 +ℎ ( - 1 ·ℎ 𝐷 ) ) ) = ( ( 𝐴 +ℎ 𝐵 ) +ℎ ( ( - 1 ·ℎ 𝐶 ) +ℎ ( - 1 ·ℎ 𝐷 ) ) ) )
25	14 24	eqtr4d	⊢ ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) ∧ ( 𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ ) ) → ( ( 𝐴 +ℎ 𝐵 ) +ℎ ( - 1 ·ℎ ( 𝐶 +ℎ 𝐷 ) ) ) = ( ( 𝐴 +ℎ ( - 1 ·ℎ 𝐶 ) ) +ℎ ( 𝐵 +ℎ ( - 1 ·ℎ 𝐷 ) ) ) )
26	9 25	eqtr4d	⊢ ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) ∧ ( 𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ ) ) → ( ( 𝐴 −ℎ 𝐶 ) +ℎ ( 𝐵 −ℎ 𝐷 ) ) = ( ( 𝐴 +ℎ 𝐵 ) +ℎ ( - 1 ·ℎ ( 𝐶 +ℎ 𝐷 ) ) ) )
27	4 26	eqtr4d	⊢ ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) ∧ ( 𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ ) ) → ( ( 𝐴 +ℎ 𝐵 ) −ℎ ( 𝐶 +ℎ 𝐷 ) ) = ( ( 𝐴 −ℎ 𝐶 ) +ℎ ( 𝐵 −ℎ 𝐷 ) ) )