Metamath Proof Explorer

Theorem normlem9at

Description: Lemma used to derive properties of norm. Part of Remark 3.4(B) of Beran p. 98. (Contributed by NM, 10-May-2005) (New usage is discouraged.)

Ref Expression
Assertion normlem9at ⊢ A ∈ ℋ ∧ B ∈ ℋ → A - ℎ B ⋅ ih A - ℎ B = A ⋅ ih A + B ⋅ ih B - A ⋅ ih B + B ⋅ ih A

Proof

Step Hyp Ref Expression
1 oveq1 ⊢ A = if A ∈ ℋ A 0 ℎ → A - ℎ B = if A ∈ ℋ A 0 ℎ - ℎ B
2 1 1 oveq12d ⊢ A = if A ∈ ℋ A 0 ℎ → A - ℎ B ⋅ ih A - ℎ B = if A ∈ ℋ A 0 ℎ - ℎ B ⋅ ih if A ∈ ℋ A 0 ℎ - ℎ B
3 id ⊢ A = if A ∈ ℋ A 0 ℎ → A = if A ∈ ℋ A 0 ℎ
4 3 3 oveq12d ⊢ A = if A ∈ ℋ A 0 ℎ → A ⋅ ih A = if A ∈ ℋ A 0 ℎ ⋅ ih if A ∈ ℋ A 0 ℎ
5 4 oveq1d ⊢ A = if A ∈ ℋ A 0 ℎ → A ⋅ ih A + B ⋅ ih B = if A ∈ ℋ A 0 ℎ ⋅ ih if A ∈ ℋ A 0 ℎ + B ⋅ ih B
6 oveq1 ⊢ A = if A ∈ ℋ A 0 ℎ → A ⋅ ih B = if A ∈ ℋ A 0 ℎ ⋅ ih B
7 oveq2 ⊢ A = if A ∈ ℋ A 0 ℎ → B ⋅ ih A = B ⋅ ih if A ∈ ℋ A 0 ℎ
8 6 7 oveq12d ⊢ A = if A ∈ ℋ A 0 ℎ → A ⋅ ih B + B ⋅ ih A = if A ∈ ℋ A 0 ℎ ⋅ ih B + B ⋅ ih if A ∈ ℋ A 0 ℎ
9 5 8 oveq12d ⊢ A = if A ∈ ℋ A 0 ℎ → A ⋅ ih A + B ⋅ ih B - A ⋅ ih B + B ⋅ ih A = if A ∈ ℋ A 0 ℎ ⋅ ih if A ∈ ℋ A 0 ℎ + B ⋅ ih B - if A ∈ ℋ A 0 ℎ ⋅ ih B + B ⋅ ih if A ∈ ℋ A 0 ℎ
10 2 9 eqeq12d ⊢ A = if A ∈ ℋ A 0 ℎ → A - ℎ B ⋅ ih A - ℎ B = A ⋅ ih A + B ⋅ ih B - A ⋅ ih B + B ⋅ ih A ↔ if A ∈ ℋ A 0 ℎ - ℎ B ⋅ ih if A ∈ ℋ A 0 ℎ - ℎ B = if A ∈ ℋ A 0 ℎ ⋅ ih if A ∈ ℋ A 0 ℎ + B ⋅ ih B - if A ∈ ℋ A 0 ℎ ⋅ ih B + B ⋅ ih if A ∈ ℋ A 0 ℎ
11 oveq2 ⊢ B = if B ∈ ℋ B 0 ℎ → if A ∈ ℋ A 0 ℎ - ℎ B = if A ∈ ℋ A 0 ℎ - ℎ if B ∈ ℋ B 0 ℎ
12 11 11 oveq12d ⊢ B = if B ∈ ℋ B 0 ℎ → if A ∈ ℋ A 0 ℎ - ℎ B ⋅ ih if A ∈ ℋ A 0 ℎ - ℎ B = if A ∈ ℋ A 0 ℎ - ℎ if B ∈ ℋ B 0 ℎ ⋅ ih if A ∈ ℋ A 0 ℎ - ℎ if B ∈ ℋ B 0 ℎ
13 id ⊢ B = if B ∈ ℋ B 0 ℎ → B = if B ∈ ℋ B 0 ℎ
14 13 13 oveq12d ⊢ B = if B ∈ ℋ B 0 ℎ → B ⋅ ih B = if B ∈ ℋ B 0 ℎ ⋅ ih if B ∈ ℋ B 0 ℎ
15 14 oveq2d ⊢ B = if B ∈ ℋ B 0 ℎ → if A ∈ ℋ A 0 ℎ ⋅ ih if A ∈ ℋ A 0 ℎ + B ⋅ ih B = if A ∈ ℋ A 0 ℎ ⋅ ih if A ∈ ℋ A 0 ℎ + if B ∈ ℋ B 0 ℎ ⋅ ih if B ∈ ℋ B 0 ℎ
16 oveq2 ⊢ B = if B ∈ ℋ B 0 ℎ → if A ∈ ℋ A 0 ℎ ⋅ ih B = if A ∈ ℋ A 0 ℎ ⋅ ih if B ∈ ℋ B 0 ℎ
17 oveq1 ⊢ B = if B ∈ ℋ B 0 ℎ → B ⋅ ih if A ∈ ℋ A 0 ℎ = if B ∈ ℋ B 0 ℎ ⋅ ih if A ∈ ℋ A 0 ℎ
18 16 17 oveq12d ⊢ B = if B ∈ ℋ B 0 ℎ → if A ∈ ℋ A 0 ℎ ⋅ ih B + B ⋅ ih if A ∈ ℋ A 0 ℎ = if A ∈ ℋ A 0 ℎ ⋅ ih if B ∈ ℋ B 0 ℎ + if B ∈ ℋ B 0 ℎ ⋅ ih if A ∈ ℋ A 0 ℎ
19 15 18 oveq12d ⊢ B = if B ∈ ℋ B 0 ℎ → if A ∈ ℋ A 0 ℎ ⋅ ih if A ∈ ℋ A 0 ℎ + B ⋅ ih B - if A ∈ ℋ A 0 ℎ ⋅ ih B + B ⋅ ih if A ∈ ℋ A 0 ℎ = if A ∈ ℋ A 0 ℎ ⋅ ih if A ∈ ℋ A 0 ℎ + if B ∈ ℋ B 0 ℎ ⋅ ih if B ∈ ℋ B 0 ℎ - if A ∈ ℋ A 0 ℎ ⋅ ih if B ∈ ℋ B 0 ℎ + if B ∈ ℋ B 0 ℎ ⋅ ih if A ∈ ℋ A 0 ℎ
20 12 19 eqeq12d ⊢ B = if B ∈ ℋ B 0 ℎ → if A ∈ ℋ A 0 ℎ - ℎ B ⋅ ih if A ∈ ℋ A 0 ℎ - ℎ B = if A ∈ ℋ A 0 ℎ ⋅ ih if A ∈ ℋ A 0 ℎ + B ⋅ ih B - if A ∈ ℋ A 0 ℎ ⋅ ih B + B ⋅ ih if A ∈ ℋ A 0 ℎ ↔ if A ∈ ℋ A 0 ℎ - ℎ if B ∈ ℋ B 0 ℎ ⋅ ih if A ∈ ℋ A 0 ℎ - ℎ if B ∈ ℋ B 0 ℎ = if A ∈ ℋ A 0 ℎ ⋅ ih if A ∈ ℋ A 0 ℎ + if B ∈ ℋ B 0 ℎ ⋅ ih if B ∈ ℋ B 0 ℎ - if A ∈ ℋ A 0 ℎ ⋅ ih if B ∈ ℋ B 0 ℎ + if B ∈ ℋ B 0 ℎ ⋅ ih if A ∈ ℋ A 0 ℎ
21 ifhvhv0 ⊢ if A ∈ ℋ A 0 ℎ ∈ ℋ
22 ifhvhv0 ⊢ if B ∈ ℋ B 0 ℎ ∈ ℋ
23 21 22 21 22 normlem9 ⊢ if A ∈ ℋ A 0 ℎ - ℎ if B ∈ ℋ B 0 ℎ ⋅ ih if A ∈ ℋ A 0 ℎ - ℎ if B ∈ ℋ B 0 ℎ = if A ∈ ℋ A 0 ℎ ⋅ ih if A ∈ ℋ A 0 ℎ + if B ∈ ℋ B 0 ℎ ⋅ ih if B ∈ ℋ B 0 ℎ - if A ∈ ℋ A 0 ℎ ⋅ ih if B ∈ ℋ B 0 ℎ + if B ∈ ℋ B 0 ℎ ⋅ ih if A ∈ ℋ A 0 ℎ
24 10 20 23 dedth2h ⊢ A ∈ ℋ ∧ B ∈ ℋ → A - ℎ B ⋅ ih A - ℎ B = A ⋅ ih A + B ⋅ ih B - A ⋅ ih B + B ⋅ ih A