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 ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) ∧ ( 𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ ) ) → ( ( 𝐴 −ℎ 𝐵 ) −ℎ ( 𝐶 −ℎ 𝐷 ) ) = ( ( 𝐴 −ℎ 𝐶 ) −ℎ ( 𝐵 −ℎ 𝐷 ) ) )

Proof

Step Hyp Ref Expression
1 oveq1 ⊢ ( 𝐴 = if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) → ( 𝐴 −ℎ 𝐵 ) = ( if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) −ℎ 𝐵 ) )
2 1 oveq1d ⊢ ( 𝐴 = if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) → ( ( 𝐴 −ℎ 𝐵 ) −ℎ ( 𝐶 −ℎ 𝐷 ) ) = ( ( if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) −ℎ 𝐵 ) −ℎ ( 𝐶 −ℎ 𝐷 ) ) )
3 oveq1 ⊢ ( 𝐴 = if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) → ( 𝐴 −ℎ 𝐶 ) = ( if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) −ℎ 𝐶 ) )
4 3 oveq1d ⊢ ( 𝐴 = if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) → ( ( 𝐴 −ℎ 𝐶 ) −ℎ ( 𝐵 −ℎ 𝐷 ) ) = ( ( if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) −ℎ 𝐶 ) −ℎ ( 𝐵 −ℎ 𝐷 ) ) )
5 2 4 eqeq12d ⊢ ( 𝐴 = if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) → ( ( ( 𝐴 −ℎ 𝐵 ) −ℎ ( 𝐶 −ℎ 𝐷 ) ) = ( ( 𝐴 −ℎ 𝐶 ) −ℎ ( 𝐵 −ℎ 𝐷 ) ) ↔ ( ( if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) −ℎ 𝐵 ) −ℎ ( 𝐶 −ℎ 𝐷 ) ) = ( ( if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) −ℎ 𝐶 ) −ℎ ( 𝐵 −ℎ 𝐷 ) ) ) )
6 oveq2 ⊢ ( 𝐵 = if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) → ( if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) −ℎ 𝐵 ) = ( if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) −ℎ if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) ) )
7 6 oveq1d ⊢ ( 𝐵 = if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) → ( ( if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) −ℎ 𝐵 ) −ℎ ( 𝐶 −ℎ 𝐷 ) ) = ( ( if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) −ℎ if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) ) −ℎ ( 𝐶 −ℎ 𝐷 ) ) )
8 oveq1 ⊢ ( 𝐵 = if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) → ( 𝐵 −ℎ 𝐷 ) = ( if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) −ℎ 𝐷 ) )
9 8 oveq2d ⊢ ( 𝐵 = if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) → ( ( if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) −ℎ 𝐶 ) −ℎ ( 𝐵 −ℎ 𝐷 ) ) = ( ( if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) −ℎ 𝐶 ) −ℎ ( if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) −ℎ 𝐷 ) ) )
10 7 9 eqeq12d ⊢ ( 𝐵 = if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) → ( ( ( if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) −ℎ 𝐵 ) −ℎ ( 𝐶 −ℎ 𝐷 ) ) = ( ( if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) −ℎ 𝐶 ) −ℎ ( 𝐵 −ℎ 𝐷 ) ) ↔ ( ( if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) −ℎ if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) ) −ℎ ( 𝐶 −ℎ 𝐷 ) ) = ( ( if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) −ℎ 𝐶 ) −ℎ ( if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) −ℎ 𝐷 ) ) ) )
11 oveq1 ⊢ ( 𝐶 = if ( 𝐶 ∈ ℋ , 𝐶 , 0ℎ ) → ( 𝐶 −ℎ 𝐷 ) = ( if ( 𝐶 ∈ ℋ , 𝐶 , 0ℎ ) −ℎ 𝐷 ) )
12 11 oveq2d ⊢ ( 𝐶 = if ( 𝐶 ∈ ℋ , 𝐶 , 0ℎ ) → ( ( if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) −ℎ if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) ) −ℎ ( 𝐶 −ℎ 𝐷 ) ) = ( ( if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) −ℎ if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) ) −ℎ ( if ( 𝐶 ∈ ℋ , 𝐶 , 0ℎ ) −ℎ 𝐷 ) ) )
13 oveq2 ⊢ ( 𝐶 = if ( 𝐶 ∈ ℋ , 𝐶 , 0ℎ ) → ( if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) −ℎ 𝐶 ) = ( if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) −ℎ if ( 𝐶 ∈ ℋ , 𝐶 , 0ℎ ) ) )
14 13 oveq1d ⊢ ( 𝐶 = if ( 𝐶 ∈ ℋ , 𝐶 , 0ℎ ) → ( ( if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) −ℎ 𝐶 ) −ℎ ( if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) −ℎ 𝐷 ) ) = ( ( if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) −ℎ if ( 𝐶 ∈ ℋ , 𝐶 , 0ℎ ) ) −ℎ ( if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) −ℎ 𝐷 ) ) )
15 12 14 eqeq12d ⊢ ( 𝐶 = if ( 𝐶 ∈ ℋ , 𝐶 , 0ℎ ) → ( ( ( if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) −ℎ if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) ) −ℎ ( 𝐶 −ℎ 𝐷 ) ) = ( ( if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) −ℎ 𝐶 ) −ℎ ( if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) −ℎ 𝐷 ) ) ↔ ( ( if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) −ℎ if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) ) −ℎ ( if ( 𝐶 ∈ ℋ , 𝐶 , 0ℎ ) −ℎ 𝐷 ) ) = ( ( if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) −ℎ if ( 𝐶 ∈ ℋ , 𝐶 , 0ℎ ) ) −ℎ ( if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) −ℎ 𝐷 ) ) ) )
16 oveq2 ⊢ ( 𝐷 = if ( 𝐷 ∈ ℋ , 𝐷 , 0ℎ ) → ( if ( 𝐶 ∈ ℋ , 𝐶 , 0ℎ ) −ℎ 𝐷 ) = ( if ( 𝐶 ∈ ℋ , 𝐶 , 0ℎ ) −ℎ if ( 𝐷 ∈ ℋ , 𝐷 , 0ℎ ) ) )
17 16 oveq2d ⊢ ( 𝐷 = if ( 𝐷 ∈ ℋ , 𝐷 , 0ℎ ) → ( ( if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) −ℎ if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) ) −ℎ ( if ( 𝐶 ∈ ℋ , 𝐶 , 0ℎ ) −ℎ 𝐷 ) ) = ( ( if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) −ℎ if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) ) −ℎ ( if ( 𝐶 ∈ ℋ , 𝐶 , 0ℎ ) −ℎ if ( 𝐷 ∈ ℋ , 𝐷 , 0ℎ ) ) ) )
18 oveq2 ⊢ ( 𝐷 = if ( 𝐷 ∈ ℋ , 𝐷 , 0ℎ ) → ( if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) −ℎ 𝐷 ) = ( if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) −ℎ if ( 𝐷 ∈ ℋ , 𝐷 , 0ℎ ) ) )
19 18 oveq2d ⊢ ( 𝐷 = if ( 𝐷 ∈ ℋ , 𝐷 , 0ℎ ) → ( ( if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) −ℎ if ( 𝐶 ∈ ℋ , 𝐶 , 0ℎ ) ) −ℎ ( if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) −ℎ 𝐷 ) ) = ( ( if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) −ℎ if ( 𝐶 ∈ ℋ , 𝐶 , 0ℎ ) ) −ℎ ( if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) −ℎ if ( 𝐷 ∈ ℋ , 𝐷 , 0ℎ ) ) ) )
20 17 19 eqeq12d ⊢ ( 𝐷 = if ( 𝐷 ∈ ℋ , 𝐷 , 0ℎ ) → ( ( ( if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) −ℎ if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) ) −ℎ ( if ( 𝐶 ∈ ℋ , 𝐶 , 0ℎ ) −ℎ 𝐷 ) ) = ( ( if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) −ℎ if ( 𝐶 ∈ ℋ , 𝐶 , 0ℎ ) ) −ℎ ( if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) −ℎ 𝐷 ) ) ↔ ( ( if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) −ℎ if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) ) −ℎ ( if ( 𝐶 ∈ ℋ , 𝐶 , 0ℎ ) −ℎ if ( 𝐷 ∈ ℋ , 𝐷 , 0ℎ ) ) ) = ( ( if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) −ℎ if ( 𝐶 ∈ ℋ , 𝐶 , 0ℎ ) ) −ℎ ( if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) −ℎ if ( 𝐷 ∈ ℋ , 𝐷 , 0ℎ ) ) ) ) )
21 ifhvhv0 ⊢ if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) ∈ ℋ
22 ifhvhv0 ⊢ if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) ∈ ℋ
23 ifhvhv0 ⊢ if ( 𝐶 ∈ ℋ , 𝐶 , 0ℎ ) ∈ ℋ
24 ifhvhv0 ⊢ if ( 𝐷 ∈ ℋ , 𝐷 , 0ℎ ) ∈ ℋ
25 21 22 23 24 hvsubsub4i ⊢ ( ( if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) −ℎ if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) ) −ℎ ( if ( 𝐶 ∈ ℋ , 𝐶 , 0ℎ ) −ℎ if ( 𝐷 ∈ ℋ , 𝐷 , 0ℎ ) ) ) = ( ( if ( 𝐴 ∈ ℋ , 𝐴 , 0ℎ ) −ℎ if ( 𝐶 ∈ ℋ , 𝐶 , 0ℎ ) ) −ℎ ( if ( 𝐵 ∈ ℋ , 𝐵 , 0ℎ ) −ℎ if ( 𝐷 ∈ ℋ , 𝐷 , 0ℎ ) ) )
26 5 10 15 20 25 dedth4h ⊢ ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) ∧ ( 𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ ) ) → ( ( 𝐴 −ℎ 𝐵 ) −ℎ ( 𝐶 −ℎ 𝐷 ) ) = ( ( 𝐴 −ℎ 𝐶 ) −ℎ ( 𝐵 −ℎ 𝐷 ) ) )