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

Proof

Step Hyp Ref Expression
1 oveq1 ⊢A=ifA∈ℋA0ℎ→A-ℎB=ifA∈ℋA0ℎ-ℎB
2 1 oveq1d ⊢A=ifA∈ℋA0ℎ→A-ℎB-ℎC-ℎD=ifA∈ℋA0ℎ-ℎB-ℎC-ℎD
3 oveq1 ⊢A=ifA∈ℋA0ℎ→A-ℎC=ifA∈ℋA0ℎ-ℎC
4 3 oveq1d ⊢A=ifA∈ℋA0ℎ→A-ℎC-ℎB-ℎD=ifA∈ℋA0ℎ-ℎC-ℎB-ℎD
5 2 4 eqeq12d ⊢A=ifA∈ℋA0ℎ→A-ℎB-ℎC-ℎD=A-ℎC-ℎB-ℎD↔ifA∈ℋA0ℎ-ℎB-ℎC-ℎD=ifA∈ℋA0ℎ-ℎC-ℎB-ℎD
6 oveq2 ⊢B=ifB∈ℋB0ℎ→ifA∈ℋA0ℎ-ℎB=ifA∈ℋA0ℎ-ℎifB∈ℋB0ℎ
7 6 oveq1d ⊢B=ifB∈ℋB0ℎ→ifA∈ℋA0ℎ-ℎB-ℎC-ℎD=ifA∈ℋA0ℎ-ℎifB∈ℋB0ℎ-ℎC-ℎD
8 oveq1 ⊢B=ifB∈ℋB0ℎ→B-ℎD=ifB∈ℋB0ℎ-ℎD
9 8 oveq2d ⊢B=ifB∈ℋB0ℎ→ifA∈ℋA0ℎ-ℎC-ℎB-ℎD=ifA∈ℋA0ℎ-ℎC-ℎifB∈ℋB0ℎ-ℎD
10 7 9 eqeq12d ⊢B=ifB∈ℋB0ℎ→ifA∈ℋA0ℎ-ℎB-ℎC-ℎD=ifA∈ℋA0ℎ-ℎC-ℎB-ℎD↔ifA∈ℋA0ℎ-ℎifB∈ℋB0ℎ-ℎC-ℎD=ifA∈ℋA0ℎ-ℎC-ℎifB∈ℋB0ℎ-ℎD
11 oveq1 ⊢C=ifC∈ℋC0ℎ→C-ℎD=ifC∈ℋC0ℎ-ℎD
12 11 oveq2d ⊢C=ifC∈ℋC0ℎ→ifA∈ℋA0ℎ-ℎifB∈ℋB0ℎ-ℎC-ℎD=ifA∈ℋA0ℎ-ℎifB∈ℋB0ℎ-ℎifC∈ℋC0ℎ-ℎD
13 oveq2 ⊢C=ifC∈ℋC0ℎ→ifA∈ℋA0ℎ-ℎC=ifA∈ℋA0ℎ-ℎifC∈ℋC0ℎ
14 13 oveq1d ⊢C=ifC∈ℋC0ℎ→ifA∈ℋA0ℎ-ℎC-ℎifB∈ℋB0ℎ-ℎD=ifA∈ℋA0ℎ-ℎifC∈ℋC0ℎ-ℎifB∈ℋB0ℎ-ℎD
15 12 14 eqeq12d ⊢C=ifC∈ℋC0ℎ→ifA∈ℋA0ℎ-ℎifB∈ℋB0ℎ-ℎC-ℎD=ifA∈ℋA0ℎ-ℎC-ℎifB∈ℋB0ℎ-ℎD↔ifA∈ℋA0ℎ-ℎifB∈ℋB0ℎ-ℎifC∈ℋC0ℎ-ℎD=ifA∈ℋA0ℎ-ℎifC∈ℋC0ℎ-ℎifB∈ℋB0ℎ-ℎD
16 oveq2 ⊢D=ifD∈ℋD0ℎ→ifC∈ℋC0ℎ-ℎD=ifC∈ℋC0ℎ-ℎifD∈ℋD0ℎ
17 16 oveq2d ⊢D=ifD∈ℋD0ℎ→ifA∈ℋA0ℎ-ℎifB∈ℋB0ℎ-ℎifC∈ℋC0ℎ-ℎD=ifA∈ℋA0ℎ-ℎifB∈ℋB0ℎ-ℎifC∈ℋC0ℎ-ℎifD∈ℋD0ℎ
18 oveq2 ⊢D=ifD∈ℋD0ℎ→ifB∈ℋB0ℎ-ℎD=ifB∈ℋB0ℎ-ℎifD∈ℋD0ℎ
19 18 oveq2d ⊢D=ifD∈ℋD0ℎ→ifA∈ℋA0ℎ-ℎifC∈ℋC0ℎ-ℎifB∈ℋB0ℎ-ℎD=ifA∈ℋA0ℎ-ℎifC∈ℋC0ℎ-ℎifB∈ℋB0ℎ-ℎifD∈ℋD0ℎ
20 17 19 eqeq12d ⊢D=ifD∈ℋD0ℎ→ifA∈ℋA0ℎ-ℎifB∈ℋB0ℎ-ℎifC∈ℋC0ℎ-ℎD=ifA∈ℋA0ℎ-ℎifC∈ℋC0ℎ-ℎifB∈ℋB0ℎ-ℎD↔ifA∈ℋA0ℎ-ℎifB∈ℋB0ℎ-ℎifC∈ℋC0ℎ-ℎifD∈ℋD0ℎ=ifA∈ℋA0ℎ-ℎifC∈ℋC0ℎ-ℎifB∈ℋB0ℎ-ℎifD∈ℋD0ℎ
21 ifhvhv0 ⊢ifA∈ℋA0ℎ∈ℋ
22 ifhvhv0 ⊢ifB∈ℋB0ℎ∈ℋ
23 ifhvhv0 ⊢ifC∈ℋC0ℎ∈ℋ
24 ifhvhv0 ⊢ifD∈ℋD0ℎ∈ℋ
25 21 22 23 24 hvsubsub4i ⊢ifA∈ℋA0ℎ-ℎifB∈ℋB0ℎ-ℎifC∈ℋC0ℎ-ℎifD∈ℋD0ℎ=ifA∈ℋA0ℎ-ℎifC∈ℋC0ℎ-ℎifB∈ℋB0ℎ-ℎifD∈ℋD0ℎ
26 5 10 15 20 25 dedth4h ⊢A∈ℋ∧B∈ℋ∧C∈ℋ∧D∈ℋ→A-ℎB-ℎC-ℎD=A-ℎC-ℎB-ℎD