Metamath Proof Explorer


Theorem normlem3

Description: Lemma used to derive properties of norm. Part of Theorem 3.3(ii) of Beran p. 97. (Contributed by NM, 21-Aug-1999) (New usage is discouraged.)

Ref Expression
Hypotheses normlem1.1 S
normlem1.2 F
normlem1.3 G
normlem2.4 B = S F ih G + S G ih F
normlem3.5 A = G ih G
normlem3.6 C = F ih F
normlem3.7 R
Assertion normlem3 A R 2 + B R + C = F ih F + S R F ih G + S R G ih F + R 2 G ih G

Proof

Step Hyp Ref Expression
1 normlem1.1 S
2 normlem1.2 F
3 normlem1.3 G
4 normlem2.4 B = S F ih G + S G ih F
5 normlem3.5 A = G ih G
6 normlem3.6 C = F ih F
7 normlem3.7 R
8 3 3 hicli G ih G
9 5 8 eqeltri A
10 7 recni R
11 10 sqcli R 2
12 9 11 mulcli A R 2
13 1 2 3 4 normlem2 B
14 13 recni B
15 14 10 mulcli B R
16 12 15 addcomi A R 2 + B R = B R + A R 2
17 1 cjcli S
18 2 3 hicli F ih G
19 17 18 mulcli S F ih G
20 3 2 hicli G ih F
21 1 20 mulcli S G ih F
22 19 21 addcli S F ih G + S G ih F
23 22 10 mulneg1i S F ih G + S G ih F R = S F ih G + S G ih F R
24 4 oveq1i B R = S F ih G + S G ih F R
25 22 10 mulneg2i S F ih G + S G ih F R = S F ih G + S G ih F R
26 23 24 25 3eqtr4i B R = S F ih G + S G ih F R
27 10 negcli R
28 19 21 27 adddiri S F ih G + S G ih F R = S F ih G R + S G ih F R
29 17 18 27 mul32i S F ih G R = S R F ih G
30 1 20 27 mul32i S G ih F R = S R G ih F
31 29 30 oveq12i S F ih G R + S G ih F R = S R F ih G + S R G ih F
32 26 28 31 3eqtri B R = S R F ih G + S R G ih F
33 5 oveq2i R 2 A = R 2 G ih G
34 11 9 33 mulcomli A R 2 = R 2 G ih G
35 32 34 oveq12i B R + A R 2 = S R F ih G + S R G ih F + R 2 G ih G
36 17 27 mulcli S R
37 36 18 mulcli S R F ih G
38 1 27 mulcli S R
39 38 20 mulcli S R G ih F
40 11 8 mulcli R 2 G ih G
41 37 39 40 addassi S R F ih G + S R G ih F + R 2 G ih G = S R F ih G + S R G ih F + R 2 G ih G
42 16 35 41 3eqtri A R 2 + B R = S R F ih G + S R G ih F + R 2 G ih G
43 6 42 oveq12i C + A R 2 + B R = F ih F + S R F ih G + S R G ih F + R 2 G ih G
44 12 15 addcli A R 2 + B R
45 2 2 hicli F ih F
46 6 45 eqeltri C
47 44 46 addcomi A R 2 + B R + C = C + A R 2 + B R
48 39 40 addcli S R G ih F + R 2 G ih G
49 45 37 48 addassi F ih F + S R F ih G + S R G ih F + R 2 G ih G = F ih F + S R F ih G + S R G ih F + R 2 G ih G
50 43 47 49 3eqtr4i A R 2 + B R + C = F ih F + S R F ih G + S R G ih F + R 2 G ih G