Metamath Proof Explorer

Theorem normpyth

Description: Analogy to Pythagorean theorem for orthogonal vectors. Remark 3.4(C) of Beran p. 98. (Contributed by NM, 17-Oct-1999) (New usage is discouraged.)

Ref Expression
Assertion normpyth ⊢ A ∈ ℋ ∧ B ∈ ℋ → A ⋅ ih B = 0 → norm ℎ ⁡ A + ℎ B 2 = norm ℎ ⁡ A 2 + norm ℎ ⁡ B 2

Proof

Step Hyp Ref Expression
1 oveq1 ⊢ A = if A ∈ ℋ A 0 ℎ → A ⋅ ih B = if A ∈ ℋ A 0 ℎ ⋅ ih B
2 1 eqeq1d ⊢ A = if A ∈ ℋ A 0 ℎ → A ⋅ ih B = 0 ↔ if A ∈ ℋ A 0 ℎ ⋅ ih B = 0
3 fvoveq1 ⊢ A = if A ∈ ℋ A 0 ℎ → norm ℎ ⁡ A + ℎ B = norm ℎ ⁡ if A ∈ ℋ A 0 ℎ + ℎ B
4 3 oveq1d ⊢ A = if A ∈ ℋ A 0 ℎ → norm ℎ ⁡ A + ℎ B 2 = norm ℎ ⁡ if A ∈ ℋ A 0 ℎ + ℎ B 2
5 fveq2 ⊢ A = if A ∈ ℋ A 0 ℎ → norm ℎ ⁡ A = norm ℎ ⁡ if A ∈ ℋ A 0 ℎ
6 5 oveq1d ⊢ A = if A ∈ ℋ A 0 ℎ → norm ℎ ⁡ A 2 = norm ℎ ⁡ if A ∈ ℋ A 0 ℎ 2
7 6 oveq1d ⊢ A = if A ∈ ℋ A 0 ℎ → norm ℎ ⁡ A 2 + norm ℎ ⁡ B 2 = norm ℎ ⁡ if A ∈ ℋ A 0 ℎ 2 + norm ℎ ⁡ B 2
8 4 7 eqeq12d ⊢ A = if A ∈ ℋ A 0 ℎ → norm ℎ ⁡ A + ℎ B 2 = norm ℎ ⁡ A 2 + norm ℎ ⁡ B 2 ↔ norm ℎ ⁡ if A ∈ ℋ A 0 ℎ + ℎ B 2 = norm ℎ ⁡ if A ∈ ℋ A 0 ℎ 2 + norm ℎ ⁡ B 2
9 2 8 imbi12d ⊢ A = if A ∈ ℋ A 0 ℎ → A ⋅ ih B = 0 → norm ℎ ⁡ A + ℎ B 2 = norm ℎ ⁡ A 2 + norm ℎ ⁡ B 2 ↔ if A ∈ ℋ A 0 ℎ ⋅ ih B = 0 → norm ℎ ⁡ if A ∈ ℋ A 0 ℎ + ℎ B 2 = norm ℎ ⁡ if A ∈ ℋ A 0 ℎ 2 + norm ℎ ⁡ B 2
10 oveq2 ⊢ B = if B ∈ ℋ B 0 ℎ → if A ∈ ℋ A 0 ℎ ⋅ ih B = if A ∈ ℋ A 0 ℎ ⋅ ih if B ∈ ℋ B 0 ℎ
11 10 eqeq1d ⊢ B = if B ∈ ℋ B 0 ℎ → if A ∈ ℋ A 0 ℎ ⋅ ih B = 0 ↔ if A ∈ ℋ A 0 ℎ ⋅ ih if B ∈ ℋ B 0 ℎ = 0
12 oveq2 ⊢ B = if B ∈ ℋ B 0 ℎ → if A ∈ ℋ A 0 ℎ + ℎ B = if A ∈ ℋ A 0 ℎ + ℎ if B ∈ ℋ B 0 ℎ
13 12 fveq2d ⊢ B = if B ∈ ℋ B 0 ℎ → norm ℎ ⁡ if A ∈ ℋ A 0 ℎ + ℎ B = norm ℎ ⁡ if A ∈ ℋ A 0 ℎ + ℎ if B ∈ ℋ B 0 ℎ
14 13 oveq1d ⊢ B = if B ∈ ℋ B 0 ℎ → norm ℎ ⁡ if A ∈ ℋ A 0 ℎ + ℎ B 2 = norm ℎ ⁡ if A ∈ ℋ A 0 ℎ + ℎ if B ∈ ℋ B 0 ℎ 2
15 fveq2 ⊢ B = if B ∈ ℋ B 0 ℎ → norm ℎ ⁡ B = norm ℎ ⁡ if B ∈ ℋ B 0 ℎ
16 15 oveq1d ⊢ B = if B ∈ ℋ B 0 ℎ → norm ℎ ⁡ B 2 = norm ℎ ⁡ if B ∈ ℋ B 0 ℎ 2
17 16 oveq2d ⊢ B = if B ∈ ℋ B 0 ℎ → norm ℎ ⁡ if A ∈ ℋ A 0 ℎ 2 + norm ℎ ⁡ B 2 = norm ℎ ⁡ if A ∈ ℋ A 0 ℎ 2 + norm ℎ ⁡ if B ∈ ℋ B 0 ℎ 2
18 14 17 eqeq12d ⊢ B = if B ∈ ℋ B 0 ℎ → norm ℎ ⁡ if A ∈ ℋ A 0 ℎ + ℎ B 2 = norm ℎ ⁡ if A ∈ ℋ A 0 ℎ 2 + norm ℎ ⁡ B 2 ↔ norm ℎ ⁡ if A ∈ ℋ A 0 ℎ + ℎ if B ∈ ℋ B 0 ℎ 2 = norm ℎ ⁡ if A ∈ ℋ A 0 ℎ 2 + norm ℎ ⁡ if B ∈ ℋ B 0 ℎ 2
19 11 18 imbi12d ⊢ B = if B ∈ ℋ B 0 ℎ → if A ∈ ℋ A 0 ℎ ⋅ ih B = 0 → norm ℎ ⁡ if A ∈ ℋ A 0 ℎ + ℎ B 2 = norm ℎ ⁡ if A ∈ ℋ A 0 ℎ 2 + norm ℎ ⁡ B 2 ↔ if A ∈ ℋ A 0 ℎ ⋅ ih if B ∈ ℋ B 0 ℎ = 0 → norm ℎ ⁡ if A ∈ ℋ A 0 ℎ + ℎ if B ∈ ℋ B 0 ℎ 2 = norm ℎ ⁡ if A ∈ ℋ A 0 ℎ 2 + norm ℎ ⁡ if B ∈ ℋ B 0 ℎ 2
20 ifhvhv0 ⊢ if A ∈ ℋ A 0 ℎ ∈ ℋ
21 ifhvhv0 ⊢ if B ∈ ℋ B 0 ℎ ∈ ℋ
22 20 21 normpythi ⊢ if A ∈ ℋ A 0 ℎ ⋅ ih if B ∈ ℋ B 0 ℎ = 0 → norm ℎ ⁡ if A ∈ ℋ A 0 ℎ + ℎ if B ∈ ℋ B 0 ℎ 2 = norm ℎ ⁡ if A ∈ ℋ A 0 ℎ 2 + norm ℎ ⁡ if B ∈ ℋ B 0 ℎ 2
23 9 19 22 dedth2h ⊢ A ∈ ℋ ∧ B ∈ ℋ → A ⋅ ih B = 0 → norm ℎ ⁡ A + ℎ B 2 = norm ℎ ⁡ A 2 + norm ℎ ⁡ B 2