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 โŠข ( ( ๐ด โˆ’โ„Ž ๐ต ) โˆ’โ„Ž ( ๐ถ โˆ’โ„Ž ๐ท ) ) = ( ( ๐ด โˆ’โ„Ž ๐ถ ) โˆ’โ„Ž ( ๐ต โˆ’โ„Ž ๐ท ) )