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 ⊢A∈ℋ∧B∈ℋ∧C∈ℋ∧D∈ℋ→A+ℎB=C+ℎD↔A-ℎC=D-ℎB

Proof

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