Metamath Proof Explorer

Theorem hvsubsub4

Description: Hilbert vector space addition/subtraction law. (Contributed by NM, 2-Apr-2000) (New usage is discouraged.)

Ref Expression
Assertion hvsubsub4 ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ C ∈ ℋ ∧ D ∈ ℋ → A - ℎ B - ℎ C - ℎ D = A - ℎ C - ℎ B - ℎ D

Proof

Step Hyp Ref Expression
1 oveq1 ⊢ A = if A ∈ ℋ A 0 ℎ → A - ℎ B = if A ∈ ℋ A 0 ℎ - ℎ B
2 1 oveq1d ⊢ A = if A ∈ ℋ A 0 ℎ → A - ℎ B - ℎ C - ℎ D = if A ∈ ℋ A 0 ℎ - ℎ B - ℎ C - ℎ D
3 oveq1 ⊢ A = if A ∈ ℋ A 0 ℎ → A - ℎ C = if A ∈ ℋ A 0 ℎ - ℎ C
4 3 oveq1d ⊢ A = if A ∈ ℋ A 0 ℎ → A - ℎ C - ℎ B - ℎ D = if A ∈ ℋ A 0 ℎ - ℎ C - ℎ B - ℎ D
5 2 4 eqeq12d ⊢ A = if A ∈ ℋ A 0 ℎ → A - ℎ B - ℎ C - ℎ D = A - ℎ C - ℎ B - ℎ D ↔ if A ∈ ℋ A 0 ℎ - ℎ B - ℎ C - ℎ D = if A ∈ ℋ A 0 ℎ - ℎ C - ℎ B - ℎ D
6 oveq2 ⊢ B = if B ∈ ℋ B 0 ℎ → if A ∈ ℋ A 0 ℎ - ℎ B = if A ∈ ℋ A 0 ℎ - ℎ if B ∈ ℋ B 0 ℎ
7 6 oveq1d ⊢ B = if B ∈ ℋ B 0 ℎ → if A ∈ ℋ A 0 ℎ - ℎ B - ℎ C - ℎ D = if A ∈ ℋ A 0 ℎ - ℎ if B ∈ ℋ B 0 ℎ - ℎ C - ℎ D
8 oveq1 ⊢ B = if B ∈ ℋ B 0 ℎ → B - ℎ D = if B ∈ ℋ B 0 ℎ - ℎ D
9 8 oveq2d ⊢ B = if B ∈ ℋ B 0 ℎ → if A ∈ ℋ A 0 ℎ - ℎ C - ℎ B - ℎ D = if A ∈ ℋ A 0 ℎ - ℎ C - ℎ if B ∈ ℋ B 0 ℎ - ℎ D
10 7 9 eqeq12d ⊢ B = if B ∈ ℋ B 0 ℎ → if A ∈ ℋ A 0 ℎ - ℎ B - ℎ C - ℎ D = if A ∈ ℋ A 0 ℎ - ℎ C - ℎ B - ℎ D ↔ if A ∈ ℋ A 0 ℎ - ℎ if B ∈ ℋ B 0 ℎ - ℎ C - ℎ D = if A ∈ ℋ A 0 ℎ - ℎ C - ℎ if B ∈ ℋ B 0 ℎ - ℎ D
11 oveq1 ⊢ C = if C ∈ ℋ C 0 ℎ → C - ℎ D = if C ∈ ℋ C 0 ℎ - ℎ D
12 11 oveq2d ⊢ C = if C ∈ ℋ C 0 ℎ → if A ∈ ℋ A 0 ℎ - ℎ if B ∈ ℋ B 0 ℎ - ℎ C - ℎ D = if A ∈ ℋ A 0 ℎ - ℎ if B ∈ ℋ B 0 ℎ - ℎ if C ∈ ℋ C 0 ℎ - ℎ D
13 oveq2 ⊢ C = if C ∈ ℋ C 0 ℎ → if A ∈ ℋ A 0 ℎ - ℎ C = if A ∈ ℋ A 0 ℎ - ℎ if C ∈ ℋ C 0 ℎ
14 13 oveq1d ⊢ C = if C ∈ ℋ C 0 ℎ → if A ∈ ℋ A 0 ℎ - ℎ C - ℎ if B ∈ ℋ B 0 ℎ - ℎ D = if A ∈ ℋ A 0 ℎ - ℎ if C ∈ ℋ C 0 ℎ - ℎ if B ∈ ℋ B 0 ℎ - ℎ D
15 12 14 eqeq12d ⊢ C = if C ∈ ℋ C 0 ℎ → if A ∈ ℋ A 0 ℎ - ℎ if B ∈ ℋ B 0 ℎ - ℎ C - ℎ D = if A ∈ ℋ A 0 ℎ - ℎ C - ℎ if B ∈ ℋ B 0 ℎ - ℎ D ↔ if A ∈ ℋ A 0 ℎ - ℎ if B ∈ ℋ B 0 ℎ - ℎ if C ∈ ℋ C 0 ℎ - ℎ D = if A ∈ ℋ A 0 ℎ - ℎ if C ∈ ℋ C 0 ℎ - ℎ if B ∈ ℋ B 0 ℎ - ℎ D
16 oveq2 ⊢ D = if D ∈ ℋ D 0 ℎ → if C ∈ ℋ C 0 ℎ - ℎ D = if C ∈ ℋ C 0 ℎ - ℎ if D ∈ ℋ D 0 ℎ
17 16 oveq2d ⊢ D = if D ∈ ℋ D 0 ℎ → if A ∈ ℋ A 0 ℎ - ℎ if B ∈ ℋ B 0 ℎ - ℎ if C ∈ ℋ C 0 ℎ - ℎ D = if A ∈ ℋ A 0 ℎ - ℎ if B ∈ ℋ B 0 ℎ - ℎ if C ∈ ℋ C 0 ℎ - ℎ if D ∈ ℋ D 0 ℎ
18 oveq2 ⊢ D = if D ∈ ℋ D 0 ℎ → if B ∈ ℋ B 0 ℎ - ℎ D = if B ∈ ℋ B 0 ℎ - ℎ if D ∈ ℋ D 0 ℎ
19 18 oveq2d ⊢ D = if D ∈ ℋ D 0 ℎ → if A ∈ ℋ A 0 ℎ - ℎ if C ∈ ℋ C 0 ℎ - ℎ if B ∈ ℋ B 0 ℎ - ℎ D = if A ∈ ℋ A 0 ℎ - ℎ if C ∈ ℋ C 0 ℎ - ℎ if B ∈ ℋ B 0 ℎ - ℎ if D ∈ ℋ D 0 ℎ
20 17 19 eqeq12d ⊢ D = if D ∈ ℋ D 0 ℎ → if A ∈ ℋ A 0 ℎ - ℎ if B ∈ ℋ B 0 ℎ - ℎ if C ∈ ℋ C 0 ℎ - ℎ D = if A ∈ ℋ A 0 ℎ - ℎ if C ∈ ℋ C 0 ℎ - ℎ if B ∈ ℋ B 0 ℎ - ℎ D ↔ if A ∈ ℋ A 0 ℎ - ℎ if B ∈ ℋ B 0 ℎ - ℎ if C ∈ ℋ C 0 ℎ - ℎ if D ∈ ℋ D 0 ℎ = if A ∈ ℋ A 0 ℎ - ℎ if C ∈ ℋ C 0 ℎ - ℎ if B ∈ ℋ B 0 ℎ - ℎ if D ∈ ℋ D 0 ℎ
21 ifhvhv0 ⊢ if A ∈ ℋ A 0 ℎ ∈ ℋ
22 ifhvhv0 ⊢ if B ∈ ℋ B 0 ℎ ∈ ℋ
23 ifhvhv0 ⊢ if C ∈ ℋ C 0 ℎ ∈ ℋ
24 ifhvhv0 ⊢ if D ∈ ℋ D 0 ℎ ∈ ℋ
25 21 22 23 24 hvsubsub4i ⊢ if A ∈ ℋ A 0 ℎ - ℎ if B ∈ ℋ B 0 ℎ - ℎ if C ∈ ℋ C 0 ℎ - ℎ if D ∈ ℋ D 0 ℎ = if A ∈ ℋ A 0 ℎ - ℎ if C ∈ ℋ C 0 ℎ - ℎ if B ∈ ℋ B 0 ℎ - ℎ if D ∈ ℋ D 0 ℎ
26 5 10 15 20 25 dedth4h ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ C ∈ ℋ ∧ D ∈ ℋ → A - ℎ B - ℎ C - ℎ D = A - ℎ C - ℎ B - ℎ D