Metamath Proof Explorer

Theorem normlem7tALT

Description: Lemma used to derive properties of norm. Part of Theorem 3.3(ii) of Beran p. 97. (Contributed by NM, 11-Oct-1999) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Hypotheses normlem7t.1 ⊢ A ∈ ℋ
normlem7t.2 ⊢ B ∈ ℋ
Assertion normlem7tALT ⊢ S ∈ ℂ ∧ S = 1 → S ‾ ⁢ A ⋅ ih B + S ⁢ B ⋅ ih A ≤ 2 ⁢ B ⋅ ih B ⁢ A ⋅ ih A

Proof

Step Hyp Ref Expression
1 normlem7t.1 ⊢ A ∈ ℋ
2 normlem7t.2 ⊢ B ∈ ℋ
3 fveq2 ⊢ S = if S ∈ ℂ ∧ S = 1 S 1 → S ‾ = if S ∈ ℂ ∧ S = 1 S 1 ‾
4 3 oveq1d ⊢ S = if S ∈ ℂ ∧ S = 1 S 1 → S ‾ ⁢ A ⋅ ih B = if S ∈ ℂ ∧ S = 1 S 1 ‾ ⁢ A ⋅ ih B
5 oveq1 ⊢ S = if S ∈ ℂ ∧ S = 1 S 1 → S ⁢ B ⋅ ih A = if S ∈ ℂ ∧ S = 1 S 1 ⁢ B ⋅ ih A
6 4 5 oveq12d ⊢ S = if S ∈ ℂ ∧ S = 1 S 1 → S ‾ ⁢ A ⋅ ih B + S ⁢ B ⋅ ih A = if S ∈ ℂ ∧ S = 1 S 1 ‾ ⁢ A ⋅ ih B + if S ∈ ℂ ∧ S = 1 S 1 ⁢ B ⋅ ih A
7 6 breq1d ⊢ S = if S ∈ ℂ ∧ S = 1 S 1 → S ‾ ⁢ A ⋅ ih B + S ⁢ B ⋅ ih A ≤ 2 ⁢ B ⋅ ih B ⁢ A ⋅ ih A ↔ if S ∈ ℂ ∧ S = 1 S 1 ‾ ⁢ A ⋅ ih B + if S ∈ ℂ ∧ S = 1 S 1 ⁢ B ⋅ ih A ≤ 2 ⁢ B ⋅ ih B ⁢ A ⋅ ih A
8 eleq1 ⊢ S = if S ∈ ℂ ∧ S = 1 S 1 → S ∈ ℂ ↔ if S ∈ ℂ ∧ S = 1 S 1 ∈ ℂ
9 fveq2 ⊢ S = if S ∈ ℂ ∧ S = 1 S 1 → S = if S ∈ ℂ ∧ S = 1 S 1
10 9 eqeq1d ⊢ S = if S ∈ ℂ ∧ S = 1 S 1 → S = 1 ↔ if S ∈ ℂ ∧ S = 1 S 1 = 1
11 8 10 anbi12d ⊢ S = if S ∈ ℂ ∧ S = 1 S 1 → S ∈ ℂ ∧ S = 1 ↔ if S ∈ ℂ ∧ S = 1 S 1 ∈ ℂ ∧ if S ∈ ℂ ∧ S = 1 S 1 = 1
12 eleq1 ⊢ 1 = if S ∈ ℂ ∧ S = 1 S 1 → 1 ∈ ℂ ↔ if S ∈ ℂ ∧ S = 1 S 1 ∈ ℂ
13 fveq2 ⊢ 1 = if S ∈ ℂ ∧ S = 1 S 1 → 1 = if S ∈ ℂ ∧ S = 1 S 1
14 13 eqeq1d ⊢ 1 = if S ∈ ℂ ∧ S = 1 S 1 → 1 = 1 ↔ if S ∈ ℂ ∧ S = 1 S 1 = 1
15 12 14 anbi12d ⊢ 1 = if S ∈ ℂ ∧ S = 1 S 1 → 1 ∈ ℂ ∧ 1 = 1 ↔ if S ∈ ℂ ∧ S = 1 S 1 ∈ ℂ ∧ if S ∈ ℂ ∧ S = 1 S 1 = 1
16 ax-1cn ⊢ 1 ∈ ℂ
17 abs1 ⊢ 1 = 1
18 16 17 pm3.2i ⊢ 1 ∈ ℂ ∧ 1 = 1
19 11 15 18 elimhyp ⊢ if S ∈ ℂ ∧ S = 1 S 1 ∈ ℂ ∧ if S ∈ ℂ ∧ S = 1 S 1 = 1
20 19 simpli ⊢ if S ∈ ℂ ∧ S = 1 S 1 ∈ ℂ
21 19 simpri ⊢ if S ∈ ℂ ∧ S = 1 S 1 = 1
22 20 1 2 21 normlem7 ⊢ if S ∈ ℂ ∧ S = 1 S 1 ‾ ⁢ A ⋅ ih B + if S ∈ ℂ ∧ S = 1 S 1 ⁢ B ⋅ ih A ≤ 2 ⁢ B ⋅ ih B ⁢ A ⋅ ih A
23 7 22 dedth ⊢ S ∈ ℂ ∧ S = 1 → S ‾ ⁢ A ⋅ ih B + S ⁢ B ⋅ ih A ≤ 2 ⁢ B ⋅ ih B ⁢ A ⋅ ih A