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⋅ihB=0→normℎ⁡A+ℎB2=normℎ⁡A2+normℎ⁡B2

Proof

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