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

Metamath Proof Explorer

Theorem hvaddsub4

Description: Hilbert vector space addition/subtraction law. (Contributed by NM, 18-May-2005) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 hvaddcl ⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( 𝐴 +ℎ 𝐵 ) ∈ ℋ )
2 1 adantr ⊢ ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) ∧ ( 𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ ) ) → ( 𝐴 +ℎ 𝐵 ) ∈ ℋ )
3 hvaddcl ⊢ ( ( 𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ ) → ( 𝐶 +ℎ 𝐷 ) ∈ ℋ )
4 3 adantl ⊢ ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) ∧ ( 𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ ) ) → ( 𝐶 +ℎ 𝐷 ) ∈ ℋ )
5 hvaddcl ⊢ ( ( 𝐶 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( 𝐶 +ℎ 𝐵 ) ∈ ℋ )
6 5 ancoms ⊢ ( ( 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ) → ( 𝐶 +ℎ 𝐵 ) ∈ ℋ )
7 6 ad2ant2lr ⊢ ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) ∧ ( 𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ ) ) → ( 𝐶 +ℎ 𝐵 ) ∈ ℋ )
8 hvsubcan2 ⊢ ( ( ( 𝐴 +ℎ 𝐵 ) ∈ ℋ ∧ ( 𝐶 +ℎ 𝐷 ) ∈ ℋ ∧ ( 𝐶 +ℎ 𝐵 ) ∈ ℋ ) → ( ( ( 𝐴 +ℎ 𝐵 ) −ℎ ( 𝐶 +ℎ 𝐵 ) ) = ( ( 𝐶 +ℎ 𝐷 ) −ℎ ( 𝐶 +ℎ 𝐵 ) ) ↔ ( 𝐴 +ℎ 𝐵 ) = ( 𝐶 +ℎ 𝐷 ) ) )
9 2 4 7 8 syl3anc ⊢ ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) ∧ ( 𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ ) ) → ( ( ( 𝐴 +ℎ 𝐵 ) −ℎ ( 𝐶 +ℎ 𝐵 ) ) = ( ( 𝐶 +ℎ 𝐷 ) −ℎ ( 𝐶 +ℎ 𝐵 ) ) ↔ ( 𝐴 +ℎ 𝐵 ) = ( 𝐶 +ℎ 𝐷 ) ) )
10 simpr ⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → 𝐵 ∈ ℋ )
11 10 anim2i ⊢ ( ( 𝐶 ∈ ℋ ∧ ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) ) → ( 𝐶 ∈ ℋ ∧ 𝐵 ∈ ℋ ) )
12 11 ancoms ⊢ ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) ∧ 𝐶 ∈ ℋ ) → ( 𝐶 ∈ ℋ ∧ 𝐵 ∈ ℋ ) )
13 hvsub4 ⊢ ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) ∧ ( 𝐶 ∈ ℋ ∧ 𝐵 ∈ ℋ ) ) → ( ( 𝐴 +ℎ 𝐵 ) −ℎ ( 𝐶 +ℎ 𝐵 ) ) = ( ( 𝐴 −ℎ 𝐶 ) +ℎ ( 𝐵 −ℎ 𝐵 ) ) )
14 12 13 syldan ⊢ ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) ∧ 𝐶 ∈ ℋ ) → ( ( 𝐴 +ℎ 𝐵 ) −ℎ ( 𝐶 +ℎ 𝐵 ) ) = ( ( 𝐴 −ℎ 𝐶 ) +ℎ ( 𝐵 −ℎ 𝐵 ) ) )
15 hvsubid ⊢ ( 𝐵 ∈ ℋ → ( 𝐵 −ℎ 𝐵 ) = 0ℎ )
16 15 ad2antlr ⊢ ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) ∧ 𝐶 ∈ ℋ ) → ( 𝐵 −ℎ 𝐵 ) = 0ℎ )
17 16 oveq2d ⊢ ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) ∧ 𝐶 ∈ ℋ ) → ( ( 𝐴 −ℎ 𝐶 ) +ℎ ( 𝐵 −ℎ 𝐵 ) ) = ( ( 𝐴 −ℎ 𝐶 ) +ℎ 0ℎ ) )
18 hvsubcl ⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐶 ∈ ℋ ) → ( 𝐴 −ℎ 𝐶 ) ∈ ℋ )
19 ax-hvaddid ⊢ ( ( 𝐴 −ℎ 𝐶 ) ∈ ℋ → ( ( 𝐴 −ℎ 𝐶 ) +ℎ 0ℎ ) = ( 𝐴 −ℎ 𝐶 ) )
20 18 19 syl ⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐶 ∈ ℋ ) → ( ( 𝐴 −ℎ 𝐶 ) +ℎ 0ℎ ) = ( 𝐴 −ℎ 𝐶 ) )
21 20 adantlr ⊢ ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) ∧ 𝐶 ∈ ℋ ) → ( ( 𝐴 −ℎ 𝐶 ) +ℎ 0ℎ ) = ( 𝐴 −ℎ 𝐶 ) )
22 14 17 21 3eqtrd ⊢ ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) ∧ 𝐶 ∈ ℋ ) → ( ( 𝐴 +ℎ 𝐵 ) −ℎ ( 𝐶 +ℎ 𝐵 ) ) = ( 𝐴 −ℎ 𝐶 ) )
23 22 adantrr ⊢ ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) ∧ ( 𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ ) ) → ( ( 𝐴 +ℎ 𝐵 ) −ℎ ( 𝐶 +ℎ 𝐵 ) ) = ( 𝐴 −ℎ 𝐶 ) )
24 simpl ⊢ ( ( 𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ ) → 𝐶 ∈ ℋ )
25 24 anim1i ⊢ ( ( ( 𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ ) ∧ 𝐵 ∈ ℋ ) → ( 𝐶 ∈ ℋ ∧ 𝐵 ∈ ℋ ) )
26 hvsub4 ⊢ ( ( ( 𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ ) ∧ ( 𝐶 ∈ ℋ ∧ 𝐵 ∈ ℋ ) ) → ( ( 𝐶 +ℎ 𝐷 ) −ℎ ( 𝐶 +ℎ 𝐵 ) ) = ( ( 𝐶 −ℎ 𝐶 ) +ℎ ( 𝐷 −ℎ 𝐵 ) ) )
27 25 26 syldan ⊢ ( ( ( 𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ ) ∧ 𝐵 ∈ ℋ ) → ( ( 𝐶 +ℎ 𝐷 ) −ℎ ( 𝐶 +ℎ 𝐵 ) ) = ( ( 𝐶 −ℎ 𝐶 ) +ℎ ( 𝐷 −ℎ 𝐵 ) ) )
28 hvsubid ⊢ ( 𝐶 ∈ ℋ → ( 𝐶 −ℎ 𝐶 ) = 0ℎ )
29 28 ad2antrr ⊢ ( ( ( 𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ ) ∧ 𝐵 ∈ ℋ ) → ( 𝐶 −ℎ 𝐶 ) = 0ℎ )
30 29 oveq1d ⊢ ( ( ( 𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ ) ∧ 𝐵 ∈ ℋ ) → ( ( 𝐶 −ℎ 𝐶 ) +ℎ ( 𝐷 −ℎ 𝐵 ) ) = ( 0ℎ +ℎ ( 𝐷 −ℎ 𝐵 ) ) )
31 hvsubcl ⊢ ( ( 𝐷 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( 𝐷 −ℎ 𝐵 ) ∈ ℋ )
32 hvaddlid ⊢ ( ( 𝐷 −ℎ 𝐵 ) ∈ ℋ → ( 0ℎ +ℎ ( 𝐷 −ℎ 𝐵 ) ) = ( 𝐷 −ℎ 𝐵 ) )
33 31 32 syl ⊢ ( ( 𝐷 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( 0ℎ +ℎ ( 𝐷 −ℎ 𝐵 ) ) = ( 𝐷 −ℎ 𝐵 ) )
34 33 adantll ⊢ ( ( ( 𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ ) ∧ 𝐵 ∈ ℋ ) → ( 0ℎ +ℎ ( 𝐷 −ℎ 𝐵 ) ) = ( 𝐷 −ℎ 𝐵 ) )
35 27 30 34 3eqtrd ⊢ ( ( ( 𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ ) ∧ 𝐵 ∈ ℋ ) → ( ( 𝐶 +ℎ 𝐷 ) −ℎ ( 𝐶 +ℎ 𝐵 ) ) = ( 𝐷 −ℎ 𝐵 ) )
36 35 ancoms ⊢ ( ( 𝐵 ∈ ℋ ∧ ( 𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ ) ) → ( ( 𝐶 +ℎ 𝐷 ) −ℎ ( 𝐶 +ℎ 𝐵 ) ) = ( 𝐷 −ℎ 𝐵 ) )
37 36 adantll ⊢ ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) ∧ ( 𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ ) ) → ( ( 𝐶 +ℎ 𝐷 ) −ℎ ( 𝐶 +ℎ 𝐵 ) ) = ( 𝐷 −ℎ 𝐵 ) )
38 23 37 eqeq12d ⊢ ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) ∧ ( 𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ ) ) → ( ( ( 𝐴 +ℎ 𝐵 ) −ℎ ( 𝐶 +ℎ 𝐵 ) ) = ( ( 𝐶 +ℎ 𝐷 ) −ℎ ( 𝐶 +ℎ 𝐵 ) ) ↔ ( 𝐴 −ℎ 𝐶 ) = ( 𝐷 −ℎ 𝐵 ) ) )
39 9 38 bitr3d ⊢ ( ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) ∧ ( 𝐶 ∈ ℋ ∧ 𝐷 ∈ ℋ ) ) → ( ( 𝐴 +ℎ 𝐵 ) = ( 𝐶 +ℎ 𝐷 ) ↔ ( 𝐴 −ℎ 𝐶 ) = ( 𝐷 −ℎ 𝐵 ) ) )