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⋅ihA-ℎB=A⋅ihA+B⋅ihB-A⋅ihB+B⋅ihA

Proof

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