This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem hvsubsub4i

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

Ref Expression
Hypotheses hvass.1 ⊢ 𝐴 ∈ ℋ
hvass.2 ⊢ 𝐵 ∈ ℋ
hvass.3 ⊢ 𝐶 ∈ ℋ
hvadd4.4 ⊢ 𝐷 ∈ ℋ
Assertion hvsubsub4i ( ( 𝐴 −ℎ 𝐵 ) −ℎ ( 𝐶 −ℎ 𝐷 ) ) = ( ( 𝐴 −ℎ 𝐶 ) −ℎ ( 𝐵 −ℎ 𝐷 ) )

Proof

Step Hyp Ref Expression
1 hvass.1 ⊢ 𝐴 ∈ ℋ
2 hvass.2 ⊢ 𝐵 ∈ ℋ
3 hvass.3 ⊢ 𝐶 ∈ ℋ
4 hvadd4.4 ⊢ 𝐷 ∈ ℋ
5 neg1cn ⊢ - 1 ∈ ℂ
6 5 2 hvmulcli ⊢ ( - 1 ·ℎ 𝐵 ) ∈ ℋ
7 5 3 hvmulcli ⊢ ( - 1 ·ℎ 𝐶 ) ∈ ℋ
8 5 4 hvmulcli ⊢ ( - 1 ·ℎ 𝐷 ) ∈ ℋ
9 5 8 hvmulcli ⊢ ( - 1 ·ℎ ( - 1 ·ℎ 𝐷 ) ) ∈ ℋ
10 1 6 7 9 hvadd4i ⊢ ( ( 𝐴 +ℎ ( - 1 ·ℎ 𝐵 ) ) +ℎ ( ( - 1 ·ℎ 𝐶 ) +ℎ ( - 1 ·ℎ ( - 1 ·ℎ 𝐷 ) ) ) ) = ( ( 𝐴 +ℎ ( - 1 ·ℎ 𝐶 ) ) +ℎ ( ( - 1 ·ℎ 𝐵 ) +ℎ ( - 1 ·ℎ ( - 1 ·ℎ 𝐷 ) ) ) )
11 5 3 8 hvdistr1i ⊢ ( - 1 ·ℎ ( 𝐶 +ℎ ( - 1 ·ℎ 𝐷 ) ) ) = ( ( - 1 ·ℎ 𝐶 ) +ℎ ( - 1 ·ℎ ( - 1 ·ℎ 𝐷 ) ) )
12 11 oveq2i ⊢ ( ( 𝐴 +ℎ ( - 1 ·ℎ 𝐵 ) ) +ℎ ( - 1 ·ℎ ( 𝐶 +ℎ ( - 1 ·ℎ 𝐷 ) ) ) ) = ( ( 𝐴 +ℎ ( - 1 ·ℎ 𝐵 ) ) +ℎ ( ( - 1 ·ℎ 𝐶 ) +ℎ ( - 1 ·ℎ ( - 1 ·ℎ 𝐷 ) ) ) )
13 5 2 8 hvdistr1i ⊢ ( - 1 ·ℎ ( 𝐵 +ℎ ( - 1 ·ℎ 𝐷 ) ) ) = ( ( - 1 ·ℎ 𝐵 ) +ℎ ( - 1 ·ℎ ( - 1 ·ℎ 𝐷 ) ) )
14 13 oveq2i ⊢ ( ( 𝐴 +ℎ ( - 1 ·ℎ 𝐶 ) ) +ℎ ( - 1 ·ℎ ( 𝐵 +ℎ ( - 1 ·ℎ 𝐷 ) ) ) ) = ( ( 𝐴 +ℎ ( - 1 ·ℎ 𝐶 ) ) +ℎ ( ( - 1 ·ℎ 𝐵 ) +ℎ ( - 1 ·ℎ ( - 1 ·ℎ 𝐷 ) ) ) )
15 10 12 14 3eqtr4i ⊢ ( ( 𝐴 +ℎ ( - 1 ·ℎ 𝐵 ) ) +ℎ ( - 1 ·ℎ ( 𝐶 +ℎ ( - 1 ·ℎ 𝐷 ) ) ) ) = ( ( 𝐴 +ℎ ( - 1 ·ℎ 𝐶 ) ) +ℎ ( - 1 ·ℎ ( 𝐵 +ℎ ( - 1 ·ℎ 𝐷 ) ) ) )
16 1 6 hvaddcli ⊢ ( 𝐴 +ℎ ( - 1 ·ℎ 𝐵 ) ) ∈ ℋ
17 3 8 hvaddcli ⊢ ( 𝐶 +ℎ ( - 1 ·ℎ 𝐷 ) ) ∈ ℋ
18 16 17 hvsubvali ⊢ ( ( 𝐴 +ℎ ( - 1 ·ℎ 𝐵 ) ) −ℎ ( 𝐶 +ℎ ( - 1 ·ℎ 𝐷 ) ) ) = ( ( 𝐴 +ℎ ( - 1 ·ℎ 𝐵 ) ) +ℎ ( - 1 ·ℎ ( 𝐶 +ℎ ( - 1 ·ℎ 𝐷 ) ) ) )
19 1 7 hvaddcli ⊢ ( 𝐴 +ℎ ( - 1 ·ℎ 𝐶 ) ) ∈ ℋ
20 2 8 hvaddcli ⊢ ( 𝐵 +ℎ ( - 1 ·ℎ 𝐷 ) ) ∈ ℋ
21 19 20 hvsubvali ⊢ ( ( 𝐴 +ℎ ( - 1 ·ℎ 𝐶 ) ) −ℎ ( 𝐵 +ℎ ( - 1 ·ℎ 𝐷 ) ) ) = ( ( 𝐴 +ℎ ( - 1 ·ℎ 𝐶 ) ) +ℎ ( - 1 ·ℎ ( 𝐵 +ℎ ( - 1 ·ℎ 𝐷 ) ) ) )
22 15 18 21 3eqtr4i ⊢ ( ( 𝐴 +ℎ ( - 1 ·ℎ 𝐵 ) ) −ℎ ( 𝐶 +ℎ ( - 1 ·ℎ 𝐷 ) ) ) = ( ( 𝐴 +ℎ ( - 1 ·ℎ 𝐶 ) ) −ℎ ( 𝐵 +ℎ ( - 1 ·ℎ 𝐷 ) ) )
23 1 2 hvsubvali ⊢ ( 𝐴 −ℎ 𝐵 ) = ( 𝐴 +ℎ ( - 1 ·ℎ 𝐵 ) )
24 3 4 hvsubvali ⊢ ( 𝐶 −ℎ 𝐷 ) = ( 𝐶 +ℎ ( - 1 ·ℎ 𝐷 ) )
25 23 24 oveq12i ⊢ ( ( 𝐴 −ℎ 𝐵 ) −ℎ ( 𝐶 −ℎ 𝐷 ) ) = ( ( 𝐴 +ℎ ( - 1 ·ℎ 𝐵 ) ) −ℎ ( 𝐶 +ℎ ( - 1 ·ℎ 𝐷 ) ) )
26 1 3 hvsubvali ⊢ ( 𝐴 −ℎ 𝐶 ) = ( 𝐴 +ℎ ( - 1 ·ℎ 𝐶 ) )
27 2 4 hvsubvali ⊢ ( 𝐵 −ℎ 𝐷 ) = ( 𝐵 +ℎ ( - 1 ·ℎ 𝐷 ) )
28 26 27 oveq12i ⊢ ( ( 𝐴 −ℎ 𝐶 ) −ℎ ( 𝐵 −ℎ 𝐷 ) ) = ( ( 𝐴 +ℎ ( - 1 ·ℎ 𝐶 ) ) −ℎ ( 𝐵 +ℎ ( - 1 ·ℎ 𝐷 ) ) )
29 22 25 28 3eqtr4i ⊢ ( ( 𝐴 −ℎ 𝐵 ) −ℎ ( 𝐶 −ℎ 𝐷 ) ) = ( ( 𝐴 −ℎ 𝐶 ) −ℎ ( 𝐵 −ℎ 𝐷 ) )