# 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}\in ℋ$
normlem7t.2 ${⊢}{B}\in ℋ$
Assertion normlem7tALT ${⊢}\left({S}\in ℂ\wedge \left|{S}\right|=1\right)\to \stackrel{‾}{{S}}\left({A}{\cdot }_{\mathrm{ih}}{B}\right)+{S}\left({B}{\cdot }_{\mathrm{ih}}{A}\right)\le 2\sqrt{{B}{\cdot }_{\mathrm{ih}}{B}}\sqrt{{A}{\cdot }_{\mathrm{ih}}{A}}$

### Proof

Step Hyp Ref Expression
1 normlem7t.1 ${⊢}{A}\in ℋ$
2 normlem7t.2 ${⊢}{B}\in ℋ$
3 fveq2 ${⊢}{S}=if\left(\left({S}\in ℂ\wedge \left|{S}\right|=1\right),{S},1\right)\to \stackrel{‾}{{S}}=\stackrel{‾}{if\left(\left({S}\in ℂ\wedge \left|{S}\right|=1\right),{S},1\right)}$
4 3 oveq1d ${⊢}{S}=if\left(\left({S}\in ℂ\wedge \left|{S}\right|=1\right),{S},1\right)\to \stackrel{‾}{{S}}\left({A}{\cdot }_{\mathrm{ih}}{B}\right)=\stackrel{‾}{if\left(\left({S}\in ℂ\wedge \left|{S}\right|=1\right),{S},1\right)}\left({A}{\cdot }_{\mathrm{ih}}{B}\right)$
5 oveq1 ${⊢}{S}=if\left(\left({S}\in ℂ\wedge \left|{S}\right|=1\right),{S},1\right)\to {S}\left({B}{\cdot }_{\mathrm{ih}}{A}\right)=if\left(\left({S}\in ℂ\wedge \left|{S}\right|=1\right),{S},1\right)\left({B}{\cdot }_{\mathrm{ih}}{A}\right)$
6 4 5 oveq12d ${⊢}{S}=if\left(\left({S}\in ℂ\wedge \left|{S}\right|=1\right),{S},1\right)\to \stackrel{‾}{{S}}\left({A}{\cdot }_{\mathrm{ih}}{B}\right)+{S}\left({B}{\cdot }_{\mathrm{ih}}{A}\right)=\stackrel{‾}{if\left(\left({S}\in ℂ\wedge \left|{S}\right|=1\right),{S},1\right)}\left({A}{\cdot }_{\mathrm{ih}}{B}\right)+if\left(\left({S}\in ℂ\wedge \left|{S}\right|=1\right),{S},1\right)\left({B}{\cdot }_{\mathrm{ih}}{A}\right)$
7 6 breq1d ${⊢}{S}=if\left(\left({S}\in ℂ\wedge \left|{S}\right|=1\right),{S},1\right)\to \left(\stackrel{‾}{{S}}\left({A}{\cdot }_{\mathrm{ih}}{B}\right)+{S}\left({B}{\cdot }_{\mathrm{ih}}{A}\right)\le 2\sqrt{{B}{\cdot }_{\mathrm{ih}}{B}}\sqrt{{A}{\cdot }_{\mathrm{ih}}{A}}↔\stackrel{‾}{if\left(\left({S}\in ℂ\wedge \left|{S}\right|=1\right),{S},1\right)}\left({A}{\cdot }_{\mathrm{ih}}{B}\right)+if\left(\left({S}\in ℂ\wedge \left|{S}\right|=1\right),{S},1\right)\left({B}{\cdot }_{\mathrm{ih}}{A}\right)\le 2\sqrt{{B}{\cdot }_{\mathrm{ih}}{B}}\sqrt{{A}{\cdot }_{\mathrm{ih}}{A}}\right)$
8 eleq1 ${⊢}{S}=if\left(\left({S}\in ℂ\wedge \left|{S}\right|=1\right),{S},1\right)\to \left({S}\in ℂ↔if\left(\left({S}\in ℂ\wedge \left|{S}\right|=1\right),{S},1\right)\in ℂ\right)$
9 fveq2 ${⊢}{S}=if\left(\left({S}\in ℂ\wedge \left|{S}\right|=1\right),{S},1\right)\to \left|{S}\right|=\left|if\left(\left({S}\in ℂ\wedge \left|{S}\right|=1\right),{S},1\right)\right|$
10 9 eqeq1d ${⊢}{S}=if\left(\left({S}\in ℂ\wedge \left|{S}\right|=1\right),{S},1\right)\to \left(\left|{S}\right|=1↔\left|if\left(\left({S}\in ℂ\wedge \left|{S}\right|=1\right),{S},1\right)\right|=1\right)$
11 8 10 anbi12d ${⊢}{S}=if\left(\left({S}\in ℂ\wedge \left|{S}\right|=1\right),{S},1\right)\to \left(\left({S}\in ℂ\wedge \left|{S}\right|=1\right)↔\left(if\left(\left({S}\in ℂ\wedge \left|{S}\right|=1\right),{S},1\right)\in ℂ\wedge \left|if\left(\left({S}\in ℂ\wedge \left|{S}\right|=1\right),{S},1\right)\right|=1\right)\right)$
12 eleq1 ${⊢}1=if\left(\left({S}\in ℂ\wedge \left|{S}\right|=1\right),{S},1\right)\to \left(1\in ℂ↔if\left(\left({S}\in ℂ\wedge \left|{S}\right|=1\right),{S},1\right)\in ℂ\right)$
13 fveq2 ${⊢}1=if\left(\left({S}\in ℂ\wedge \left|{S}\right|=1\right),{S},1\right)\to \left|1\right|=\left|if\left(\left({S}\in ℂ\wedge \left|{S}\right|=1\right),{S},1\right)\right|$
14 13 eqeq1d ${⊢}1=if\left(\left({S}\in ℂ\wedge \left|{S}\right|=1\right),{S},1\right)\to \left(\left|1\right|=1↔\left|if\left(\left({S}\in ℂ\wedge \left|{S}\right|=1\right),{S},1\right)\right|=1\right)$
15 12 14 anbi12d ${⊢}1=if\left(\left({S}\in ℂ\wedge \left|{S}\right|=1\right),{S},1\right)\to \left(\left(1\in ℂ\wedge \left|1\right|=1\right)↔\left(if\left(\left({S}\in ℂ\wedge \left|{S}\right|=1\right),{S},1\right)\in ℂ\wedge \left|if\left(\left({S}\in ℂ\wedge \left|{S}\right|=1\right),{S},1\right)\right|=1\right)\right)$
16 ax-1cn ${⊢}1\in ℂ$
17 abs1 ${⊢}\left|1\right|=1$
18 16 17 pm3.2i ${⊢}\left(1\in ℂ\wedge \left|1\right|=1\right)$
19 11 15 18 elimhyp ${⊢}\left(if\left(\left({S}\in ℂ\wedge \left|{S}\right|=1\right),{S},1\right)\in ℂ\wedge \left|if\left(\left({S}\in ℂ\wedge \left|{S}\right|=1\right),{S},1\right)\right|=1\right)$
20 19 simpli ${⊢}if\left(\left({S}\in ℂ\wedge \left|{S}\right|=1\right),{S},1\right)\in ℂ$
21 19 simpri ${⊢}\left|if\left(\left({S}\in ℂ\wedge \left|{S}\right|=1\right),{S},1\right)\right|=1$
22 20 1 2 21 normlem7 ${⊢}\stackrel{‾}{if\left(\left({S}\in ℂ\wedge \left|{S}\right|=1\right),{S},1\right)}\left({A}{\cdot }_{\mathrm{ih}}{B}\right)+if\left(\left({S}\in ℂ\wedge \left|{S}\right|=1\right),{S},1\right)\left({B}{\cdot }_{\mathrm{ih}}{A}\right)\le 2\sqrt{{B}{\cdot }_{\mathrm{ih}}{B}}\sqrt{{A}{\cdot }_{\mathrm{ih}}{A}}$
23 7 22 dedth ${⊢}\left({S}\in ℂ\wedge \left|{S}\right|=1\right)\to \stackrel{‾}{{S}}\left({A}{\cdot }_{\mathrm{ih}}{B}\right)+{S}\left({B}{\cdot }_{\mathrm{ih}}{A}\right)\le 2\sqrt{{B}{\cdot }_{\mathrm{ih}}{B}}\sqrt{{A}{\cdot }_{\mathrm{ih}}{A}}$