Step |
Hyp |
Ref |
Expression |
1 |
|
normsub.1 |
|- A e. ~H |
2 |
|
normsub.2 |
|- B e. ~H |
3 |
1 2 1 2
|
normlem8 |
|- ( ( A +h B ) .ih ( A +h B ) ) = ( ( ( A .ih A ) + ( B .ih B ) ) + ( ( A .ih B ) + ( B .ih A ) ) ) |
4 |
|
id |
|- ( ( A .ih B ) = 0 -> ( A .ih B ) = 0 ) |
5 |
|
orthcom |
|- ( ( A e. ~H /\ B e. ~H ) -> ( ( A .ih B ) = 0 <-> ( B .ih A ) = 0 ) ) |
6 |
1 2 5
|
mp2an |
|- ( ( A .ih B ) = 0 <-> ( B .ih A ) = 0 ) |
7 |
6
|
biimpi |
|- ( ( A .ih B ) = 0 -> ( B .ih A ) = 0 ) |
8 |
4 7
|
oveq12d |
|- ( ( A .ih B ) = 0 -> ( ( A .ih B ) + ( B .ih A ) ) = ( 0 + 0 ) ) |
9 |
|
00id |
|- ( 0 + 0 ) = 0 |
10 |
8 9
|
eqtrdi |
|- ( ( A .ih B ) = 0 -> ( ( A .ih B ) + ( B .ih A ) ) = 0 ) |
11 |
10
|
oveq2d |
|- ( ( A .ih B ) = 0 -> ( ( ( A .ih A ) + ( B .ih B ) ) + ( ( A .ih B ) + ( B .ih A ) ) ) = ( ( ( A .ih A ) + ( B .ih B ) ) + 0 ) ) |
12 |
1 1
|
hicli |
|- ( A .ih A ) e. CC |
13 |
2 2
|
hicli |
|- ( B .ih B ) e. CC |
14 |
12 13
|
addcli |
|- ( ( A .ih A ) + ( B .ih B ) ) e. CC |
15 |
14
|
addid1i |
|- ( ( ( A .ih A ) + ( B .ih B ) ) + 0 ) = ( ( A .ih A ) + ( B .ih B ) ) |
16 |
11 15
|
eqtrdi |
|- ( ( A .ih B ) = 0 -> ( ( ( A .ih A ) + ( B .ih B ) ) + ( ( A .ih B ) + ( B .ih A ) ) ) = ( ( A .ih A ) + ( B .ih B ) ) ) |
17 |
3 16
|
syl5eq |
|- ( ( A .ih B ) = 0 -> ( ( A +h B ) .ih ( A +h B ) ) = ( ( A .ih A ) + ( B .ih B ) ) ) |
18 |
1 2
|
hvaddcli |
|- ( A +h B ) e. ~H |
19 |
18
|
normsqi |
|- ( ( normh ` ( A +h B ) ) ^ 2 ) = ( ( A +h B ) .ih ( A +h B ) ) |
20 |
1
|
normsqi |
|- ( ( normh ` A ) ^ 2 ) = ( A .ih A ) |
21 |
2
|
normsqi |
|- ( ( normh ` B ) ^ 2 ) = ( B .ih B ) |
22 |
20 21
|
oveq12i |
|- ( ( ( normh ` A ) ^ 2 ) + ( ( normh ` B ) ^ 2 ) ) = ( ( A .ih A ) + ( B .ih B ) ) |
23 |
17 19 22
|
3eqtr4g |
|- ( ( A .ih B ) = 0 -> ( ( normh ` ( A +h B ) ) ^ 2 ) = ( ( ( normh ` A ) ^ 2 ) + ( ( normh ` B ) ^ 2 ) ) ) |