Metamath Proof Explorer

Theorem norm-iii

Description: Theorem 3.3(iii) of Beran p. 97. (Contributed by NM, 25-Oct-1999) (New usage is discouraged.)

Ref Expression
Assertion norm-iii ⊢A∈ℂ∧B∈ℋ→normℎ⁡A⋅ℎB=A⁢normℎ⁡B

Proof

Step Hyp Ref Expression
1 fvoveq1 ⊢A=ifA∈ℂA0→normℎ⁡A⋅ℎB=normℎ⁡ifA∈ℂA0⋅ℎB
2 fveq2 ⊢A=ifA∈ℂA0→A=ifA∈ℂA0
3 2 oveq1d ⊢A=ifA∈ℂA0→A⁢normℎ⁡B=ifA∈ℂA0⁢normℎ⁡B
4 1 3 eqeq12d ⊢A=ifA∈ℂA0→normℎ⁡A⋅ℎB=A⁢normℎ⁡B↔normℎ⁡ifA∈ℂA0⋅ℎB=ifA∈ℂA0⁢normℎ⁡B
5 oveq2 ⊢B=ifB∈ℋB0ℎ→ifA∈ℂA0⋅ℎB=ifA∈ℂA0⋅ℎifB∈ℋB0ℎ
6 5 fveq2d ⊢B=ifB∈ℋB0ℎ→normℎ⁡ifA∈ℂA0⋅ℎB=normℎ⁡ifA∈ℂA0⋅ℎifB∈ℋB0ℎ
7 fveq2 ⊢B=ifB∈ℋB0ℎ→normℎ⁡B=normℎ⁡ifB∈ℋB0ℎ
8 7 oveq2d ⊢B=ifB∈ℋB0ℎ→ifA∈ℂA0⁢normℎ⁡B=ifA∈ℂA0⁢normℎ⁡ifB∈ℋB0ℎ
9 6 8 eqeq12d ⊢B=ifB∈ℋB0ℎ→normℎ⁡ifA∈ℂA0⋅ℎB=ifA∈ℂA0⁢normℎ⁡B↔normℎ⁡ifA∈ℂA0⋅ℎifB∈ℋB0ℎ=ifA∈ℂA0⁢normℎ⁡ifB∈ℋB0ℎ
10 0cn ⊢0∈ℂ
11 10 elimel ⊢ifA∈ℂA0∈ℂ
12 ifhvhv0 ⊢ifB∈ℋB0ℎ∈ℋ
13 11 12 norm-iii-i ⊢normℎ⁡ifA∈ℂA0⋅ℎifB∈ℋB0ℎ=ifA∈ℂA0⁢normℎ⁡ifB∈ℋB0ℎ
14 4 9 13 dedth2h ⊢A∈ℂ∧B∈ℋ→normℎ⁡A⋅ℎB=A⁢normℎ⁡B