Theorem normpythi

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
Hypotheses	normsub.1	⊢ 𝐴 ∈ ℋ
	normsub.2	⊢ 𝐵 ∈ ℋ
Assertion	normpythi	⊢ ( ( 𝐴 ·ih 𝐵 ) = 0 → ( ( normℎ ‘ ( 𝐴 +ℎ 𝐵 ) ) ↑ 2 ) = ( ( ( normℎ ‘ 𝐴 ) ↑ 2 ) + ( ( normℎ ‘ 𝐵 ) ↑ 2 ) ) )

Proof

Step	Hyp	Ref	Expression
1		normsub.1	⊢ 𝐴 ∈ ℋ
2		normsub.2	⊢ 𝐵 ∈ ℋ
3	1 2 1 2	normlem8	⊢ ( ( 𝐴 +ℎ 𝐵 ) ·ih ( 𝐴 +ℎ 𝐵 ) ) = ( ( ( 𝐴 ·ih 𝐴 ) + ( 𝐵 ·ih 𝐵 ) ) + ( ( 𝐴 ·ih 𝐵 ) + ( 𝐵 ·ih 𝐴 ) ) )
4		id	⊢ ( ( 𝐴 ·ih 𝐵 ) = 0 → ( 𝐴 ·ih 𝐵 ) = 0 )
5		orthcom	⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( ( 𝐴 ·ih 𝐵 ) = 0 ↔ ( 𝐵 ·ih 𝐴 ) = 0 ) )
6	1 2 5	mp2an	⊢ ( ( 𝐴 ·ih 𝐵 ) = 0 ↔ ( 𝐵 ·ih 𝐴 ) = 0 )
7	6	biimpi	⊢ ( ( 𝐴 ·ih 𝐵 ) = 0 → ( 𝐵 ·ih 𝐴 ) = 0 )
8	4 7	oveq12d	⊢ ( ( 𝐴 ·ih 𝐵 ) = 0 → ( ( 𝐴 ·ih 𝐵 ) + ( 𝐵 ·ih 𝐴 ) ) = ( 0 + 0 ) )
9		00id	⊢ ( 0 + 0 ) = 0
10	8 9	eqtrdi	⊢ ( ( 𝐴 ·ih 𝐵 ) = 0 → ( ( 𝐴 ·ih 𝐵 ) + ( 𝐵 ·ih 𝐴 ) ) = 0 )
11	10	oveq2d	⊢ ( ( 𝐴 ·ih 𝐵 ) = 0 → ( ( ( 𝐴 ·ih 𝐴 ) + ( 𝐵 ·ih 𝐵 ) ) + ( ( 𝐴 ·ih 𝐵 ) + ( 𝐵 ·ih 𝐴 ) ) ) = ( ( ( 𝐴 ·ih 𝐴 ) + ( 𝐵 ·ih 𝐵 ) ) + 0 ) )
12	1 1	hicli	⊢ ( 𝐴 ·ih 𝐴 ) ∈ ℂ
13	2 2	hicli	⊢ ( 𝐵 ·ih 𝐵 ) ∈ ℂ
14	12 13	addcli	⊢ ( ( 𝐴 ·ih 𝐴 ) + ( 𝐵 ·ih 𝐵 ) ) ∈ ℂ
15	14	addid1i	⊢ ( ( ( 𝐴 ·ih 𝐴 ) + ( 𝐵 ·ih 𝐵 ) ) + 0 ) = ( ( 𝐴 ·ih 𝐴 ) + ( 𝐵 ·ih 𝐵 ) )
16	11 15	eqtrdi	⊢ ( ( 𝐴 ·ih 𝐵 ) = 0 → ( ( ( 𝐴 ·ih 𝐴 ) + ( 𝐵 ·ih 𝐵 ) ) + ( ( 𝐴 ·ih 𝐵 ) + ( 𝐵 ·ih 𝐴 ) ) ) = ( ( 𝐴 ·ih 𝐴 ) + ( 𝐵 ·ih 𝐵 ) ) )
17	3 16	syl5eq	⊢ ( ( 𝐴 ·ih 𝐵 ) = 0 → ( ( 𝐴 +ℎ 𝐵 ) ·ih ( 𝐴 +ℎ 𝐵 ) ) = ( ( 𝐴 ·ih 𝐴 ) + ( 𝐵 ·ih 𝐵 ) ) )
18	1 2	hvaddcli	⊢ ( 𝐴 +ℎ 𝐵 ) ∈ ℋ
19	18	normsqi	⊢ ( ( normℎ ‘ ( 𝐴 +ℎ 𝐵 ) ) ↑ 2 ) = ( ( 𝐴 +ℎ 𝐵 ) ·ih ( 𝐴 +ℎ 𝐵 ) )
20	1	normsqi	⊢ ( ( normℎ ‘ 𝐴 ) ↑ 2 ) = ( 𝐴 ·ih 𝐴 )
21	2	normsqi	⊢ ( ( normℎ ‘ 𝐵 ) ↑ 2 ) = ( 𝐵 ·ih 𝐵 )
22	20 21	oveq12i	⊢ ( ( ( normℎ ‘ 𝐴 ) ↑ 2 ) + ( ( normℎ ‘ 𝐵 ) ↑ 2 ) ) = ( ( 𝐴 ·ih 𝐴 ) + ( 𝐵 ·ih 𝐵 ) )
23	17 19 22	3eqtr4g	⊢ ( ( 𝐴 ·ih 𝐵 ) = 0 → ( ( normℎ ‘ ( 𝐴 +ℎ 𝐵 ) ) ↑ 2 ) = ( ( ( normℎ ‘ 𝐴 ) ↑ 2 ) + ( ( normℎ ‘ 𝐵 ) ↑ 2 ) ) )