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