Proof of Theorem normpar2i
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | normpar2.1 | . . . . . . 7
⊢ 𝐴 ∈ ℋ | 
| 2 |  | normpar2.2 | . . . . . . 7
⊢ 𝐵 ∈ ℋ | 
| 3 | 1, 2 | hvaddcli 31038 | . . . . . 6
⊢ (𝐴 +ℎ 𝐵) ∈
ℋ | 
| 4 |  | 2cn 12342 | . . . . . . 7
⊢ 2 ∈
ℂ | 
| 5 |  | normpar2.3 | . . . . . . 7
⊢ 𝐶 ∈ ℋ | 
| 6 | 4, 5 | hvmulcli 31034 | . . . . . 6
⊢ (2
·ℎ 𝐶) ∈ ℋ | 
| 7 | 3, 6 | hvsubcli 31041 | . . . . 5
⊢ ((𝐴 +ℎ 𝐵) −ℎ (2
·ℎ 𝐶)) ∈ ℋ | 
| 8 | 7 | normcli 31151 | . . . 4
⊢
(normℎ‘((𝐴 +ℎ 𝐵) −ℎ (2
·ℎ 𝐶))) ∈ ℝ | 
| 9 | 8 | resqcli 14226 | . . 3
⊢
((normℎ‘((𝐴 +ℎ 𝐵) −ℎ (2
·ℎ 𝐶)))↑2) ∈ ℝ | 
| 10 | 9 | recni 11276 | . 2
⊢
((normℎ‘((𝐴 +ℎ 𝐵) −ℎ (2
·ℎ 𝐶)))↑2) ∈ ℂ | 
| 11 | 1, 2 | hvsubcli 31041 | . . . . 5
⊢ (𝐴 −ℎ
𝐵) ∈
ℋ | 
| 12 | 11 | normcli 31151 | . . . 4
⊢
(normℎ‘(𝐴 −ℎ 𝐵)) ∈
ℝ | 
| 13 | 12 | resqcli 14226 | . . 3
⊢
((normℎ‘(𝐴 −ℎ 𝐵))↑2) ∈
ℝ | 
| 14 | 13 | recni 11276 | . 2
⊢
((normℎ‘(𝐴 −ℎ 𝐵))↑2) ∈
ℂ | 
| 15 |  | 4cn 12352 | . . . . 5
⊢ 4 ∈
ℂ | 
| 16 | 1, 5 | hvsubcli 31041 | . . . . . . . 8
⊢ (𝐴 −ℎ
𝐶) ∈
ℋ | 
| 17 | 16 | normcli 31151 | . . . . . . 7
⊢
(normℎ‘(𝐴 −ℎ 𝐶)) ∈
ℝ | 
| 18 | 17 | resqcli 14226 | . . . . . 6
⊢
((normℎ‘(𝐴 −ℎ 𝐶))↑2) ∈
ℝ | 
| 19 | 18 | recni 11276 | . . . . 5
⊢
((normℎ‘(𝐴 −ℎ 𝐶))↑2) ∈
ℂ | 
| 20 | 15, 19 | mulcli 11269 | . . . 4
⊢ (4
· ((normℎ‘(𝐴 −ℎ 𝐶))↑2)) ∈
ℂ | 
| 21 | 2, 5 | hvsubcli 31041 | . . . . . . . 8
⊢ (𝐵 −ℎ
𝐶) ∈
ℋ | 
| 22 | 21 | normcli 31151 | . . . . . . 7
⊢
(normℎ‘(𝐵 −ℎ 𝐶)) ∈
ℝ | 
| 23 | 22 | resqcli 14226 | . . . . . 6
⊢
((normℎ‘(𝐵 −ℎ 𝐶))↑2) ∈
ℝ | 
| 24 | 23 | recni 11276 | . . . . 5
⊢
((normℎ‘(𝐵 −ℎ 𝐶))↑2) ∈
ℂ | 
| 25 | 15, 24 | mulcli 11269 | . . . 4
⊢ (4
· ((normℎ‘(𝐵 −ℎ 𝐶))↑2)) ∈
ℂ | 
| 26 |  | 2ne0 12371 | . . . 4
⊢ 2 ≠
0 | 
| 27 | 20, 25, 4, 26 | divdiri 12025 | . . 3
⊢ (((4
· ((normℎ‘(𝐴 −ℎ 𝐶))↑2)) + (4 ·
((normℎ‘(𝐵 −ℎ 𝐶))↑2))) / 2) = (((4
· ((normℎ‘(𝐴 −ℎ 𝐶))↑2)) / 2) + ((4 ·
((normℎ‘(𝐵 −ℎ 𝐶))↑2)) /
2)) | 
| 28 | 20, 25 | addcomi 11453 | . . . . . . 7
⊢ ((4
· ((normℎ‘(𝐴 −ℎ 𝐶))↑2)) + (4 ·
((normℎ‘(𝐵 −ℎ 𝐶))↑2))) = ((4 ·
((normℎ‘(𝐵 −ℎ 𝐶))↑2)) + (4 ·
((normℎ‘(𝐴 −ℎ 𝐶))↑2))) | 
| 29 |  | neg1cn 12381 | . . . . . . . . . . . . . . . 16
⊢ -1 ∈
ℂ | 
| 30 | 29, 6 | hvmulcli 31034 | . . . . . . . . . . . . . . 15
⊢ (-1
·ℎ (2 ·ℎ 𝐶)) ∈
ℋ | 
| 31 | 29, 11 | hvmulcli 31034 | . . . . . . . . . . . . . . 15
⊢ (-1
·ℎ (𝐴 −ℎ 𝐵)) ∈
ℋ | 
| 32 | 3, 30, 31 | hvadd32i 31074 | . . . . . . . . . . . . . 14
⊢ (((𝐴 +ℎ 𝐵) +ℎ (-1
·ℎ (2 ·ℎ 𝐶))) +ℎ (-1
·ℎ (𝐴 −ℎ 𝐵))) = (((𝐴 +ℎ 𝐵) +ℎ (-1
·ℎ (𝐴 −ℎ 𝐵))) +ℎ (-1
·ℎ (2 ·ℎ 𝐶))) | 
| 33 | 3, 6 | hvsubvali 31040 | . . . . . . . . . . . . . . 15
⊢ ((𝐴 +ℎ 𝐵) −ℎ (2
·ℎ 𝐶)) = ((𝐴 +ℎ 𝐵) +ℎ (-1
·ℎ (2 ·ℎ 𝐶))) | 
| 34 | 33 | oveq1i 7442 | . . . . . . . . . . . . . 14
⊢ (((𝐴 +ℎ 𝐵) −ℎ (2
·ℎ 𝐶)) +ℎ (-1
·ℎ (𝐴 −ℎ 𝐵))) = (((𝐴 +ℎ 𝐵) +ℎ (-1
·ℎ (2 ·ℎ 𝐶))) +ℎ (-1
·ℎ (𝐴 −ℎ 𝐵))) | 
| 35 | 4, 2 | hvmulcli 31034 | . . . . . . . . . . . . . . . 16
⊢ (2
·ℎ 𝐵) ∈ ℋ | 
| 36 | 35, 6 | hvsubvali 31040 | . . . . . . . . . . . . . . 15
⊢ ((2
·ℎ 𝐵) −ℎ (2
·ℎ 𝐶)) = ((2 ·ℎ
𝐵) +ℎ (-1
·ℎ (2 ·ℎ 𝐶))) | 
| 37 | 1, 2 | hvcomi 31039 | . . . . . . . . . . . . . . . . . 18
⊢ (𝐴 +ℎ 𝐵) = (𝐵 +ℎ 𝐴) | 
| 38 | 1, 2 | hvnegdii 31082 | . . . . . . . . . . . . . . . . . 18
⊢ (-1
·ℎ (𝐴 −ℎ 𝐵)) = (𝐵 −ℎ 𝐴) | 
| 39 | 37, 38 | oveq12i 7444 | . . . . . . . . . . . . . . . . 17
⊢ ((𝐴 +ℎ 𝐵) +ℎ (-1
·ℎ (𝐴 −ℎ 𝐵))) = ((𝐵 +ℎ 𝐴) +ℎ (𝐵 −ℎ 𝐴)) | 
| 40 | 2, 1 | hvsubcan2i 31084 | . . . . . . . . . . . . . . . . 17
⊢ ((𝐵 +ℎ 𝐴) +ℎ (𝐵 −ℎ
𝐴)) = (2
·ℎ 𝐵) | 
| 41 | 39, 40 | eqtri 2764 | . . . . . . . . . . . . . . . 16
⊢ ((𝐴 +ℎ 𝐵) +ℎ (-1
·ℎ (𝐴 −ℎ 𝐵))) = (2
·ℎ 𝐵) | 
| 42 | 41 | oveq1i 7442 | . . . . . . . . . . . . . . 15
⊢ (((𝐴 +ℎ 𝐵) +ℎ (-1
·ℎ (𝐴 −ℎ 𝐵))) +ℎ (-1
·ℎ (2 ·ℎ 𝐶))) = ((2
·ℎ 𝐵) +ℎ (-1
·ℎ (2 ·ℎ 𝐶))) | 
| 43 | 36, 42 | eqtr4i 2767 | . . . . . . . . . . . . . 14
⊢ ((2
·ℎ 𝐵) −ℎ (2
·ℎ 𝐶)) = (((𝐴 +ℎ 𝐵) +ℎ (-1
·ℎ (𝐴 −ℎ 𝐵))) +ℎ (-1
·ℎ (2 ·ℎ 𝐶))) | 
| 44 | 32, 34, 43 | 3eqtr4i 2774 | . . . . . . . . . . . . 13
⊢ (((𝐴 +ℎ 𝐵) −ℎ (2
·ℎ 𝐶)) +ℎ (-1
·ℎ (𝐴 −ℎ 𝐵))) = ((2
·ℎ 𝐵) −ℎ (2
·ℎ 𝐶)) | 
| 45 | 7, 11 | hvsubvali 31040 | . . . . . . . . . . . . 13
⊢ (((𝐴 +ℎ 𝐵) −ℎ (2
·ℎ 𝐶)) −ℎ (𝐴 −ℎ
𝐵)) = (((𝐴 +ℎ 𝐵) −ℎ (2
·ℎ 𝐶)) +ℎ (-1
·ℎ (𝐴 −ℎ 𝐵))) | 
| 46 | 4, 2, 5 | hvsubdistr1i 31072 | . . . . . . . . . . . . 13
⊢ (2
·ℎ (𝐵 −ℎ 𝐶)) = ((2
·ℎ 𝐵) −ℎ (2
·ℎ 𝐶)) | 
| 47 | 44, 45, 46 | 3eqtr4i 2774 | . . . . . . . . . . . 12
⊢ (((𝐴 +ℎ 𝐵) −ℎ (2
·ℎ 𝐶)) −ℎ (𝐴 −ℎ
𝐵)) = (2
·ℎ (𝐵 −ℎ 𝐶)) | 
| 48 | 47 | fveq2i 6908 | . . . . . . . . . . 11
⊢
(normℎ‘(((𝐴 +ℎ 𝐵) −ℎ (2
·ℎ 𝐶)) −ℎ (𝐴 −ℎ
𝐵))) =
(normℎ‘(2 ·ℎ (𝐵 −ℎ
𝐶))) | 
| 49 | 4, 21 | norm-iii-i 31159 | . . . . . . . . . . 11
⊢
(normℎ‘(2 ·ℎ
(𝐵
−ℎ 𝐶))) = ((abs‘2) ·
(normℎ‘(𝐵 −ℎ 𝐶))) | 
| 50 |  | 0le2 12369 | . . . . . . . . . . . . 13
⊢ 0 ≤
2 | 
| 51 |  | 2re 12341 | . . . . . . . . . . . . . 14
⊢ 2 ∈
ℝ | 
| 52 | 51 | absidi 15417 | . . . . . . . . . . . . 13
⊢ (0 ≤ 2
→ (abs‘2) = 2) | 
| 53 | 50, 52 | ax-mp 5 | . . . . . . . . . . . 12
⊢
(abs‘2) = 2 | 
| 54 | 53 | oveq1i 7442 | . . . . . . . . . . 11
⊢
((abs‘2) · (normℎ‘(𝐵 −ℎ
𝐶))) = (2 ·
(normℎ‘(𝐵 −ℎ 𝐶))) | 
| 55 | 48, 49, 54 | 3eqtri 2768 | . . . . . . . . . 10
⊢
(normℎ‘(((𝐴 +ℎ 𝐵) −ℎ (2
·ℎ 𝐶)) −ℎ (𝐴 −ℎ
𝐵))) = (2 ·
(normℎ‘(𝐵 −ℎ 𝐶))) | 
| 56 | 55 | oveq1i 7442 | . . . . . . . . 9
⊢
((normℎ‘(((𝐴 +ℎ 𝐵) −ℎ (2
·ℎ 𝐶)) −ℎ (𝐴 −ℎ
𝐵)))↑2) = ((2 ·
(normℎ‘(𝐵 −ℎ 𝐶)))↑2) | 
| 57 | 22 | recni 11276 | . . . . . . . . . 10
⊢
(normℎ‘(𝐵 −ℎ 𝐶)) ∈
ℂ | 
| 58 | 4, 57 | sqmuli 14224 | . . . . . . . . 9
⊢ ((2
· (normℎ‘(𝐵 −ℎ 𝐶)))↑2) = ((2↑2)
· ((normℎ‘(𝐵 −ℎ 𝐶))↑2)) | 
| 59 |  | sq2 14237 | . . . . . . . . . 10
⊢
(2↑2) = 4 | 
| 60 | 59 | oveq1i 7442 | . . . . . . . . 9
⊢
((2↑2) · ((normℎ‘(𝐵 −ℎ 𝐶))↑2)) = (4 ·
((normℎ‘(𝐵 −ℎ 𝐶))↑2)) | 
| 61 | 56, 58, 60 | 3eqtri 2768 | . . . . . . . 8
⊢
((normℎ‘(((𝐴 +ℎ 𝐵) −ℎ (2
·ℎ 𝐶)) −ℎ (𝐴 −ℎ
𝐵)))↑2) = (4 ·
((normℎ‘(𝐵 −ℎ 𝐶))↑2)) | 
| 62 | 1, 2 | hvsubcan2i 31084 | . . . . . . . . . . . . . . 15
⊢ ((𝐴 +ℎ 𝐵) +ℎ (𝐴 −ℎ
𝐵)) = (2
·ℎ 𝐴) | 
| 63 | 62 | oveq1i 7442 | . . . . . . . . . . . . . 14
⊢ (((𝐴 +ℎ 𝐵) +ℎ (𝐴 −ℎ
𝐵)) +ℎ
(-1 ·ℎ (2 ·ℎ
𝐶))) = ((2
·ℎ 𝐴) +ℎ (-1
·ℎ (2 ·ℎ 𝐶))) | 
| 64 | 3, 30, 11 | hvadd32i 31074 | . . . . . . . . . . . . . 14
⊢ (((𝐴 +ℎ 𝐵) +ℎ (-1
·ℎ (2 ·ℎ 𝐶))) +ℎ (𝐴 −ℎ
𝐵)) = (((𝐴 +ℎ 𝐵) +ℎ (𝐴 −ℎ 𝐵)) +ℎ (-1
·ℎ (2 ·ℎ 𝐶))) | 
| 65 | 4, 1 | hvmulcli 31034 | . . . . . . . . . . . . . . 15
⊢ (2
·ℎ 𝐴) ∈ ℋ | 
| 66 | 65, 6 | hvsubvali 31040 | . . . . . . . . . . . . . 14
⊢ ((2
·ℎ 𝐴) −ℎ (2
·ℎ 𝐶)) = ((2 ·ℎ
𝐴) +ℎ (-1
·ℎ (2 ·ℎ 𝐶))) | 
| 67 | 63, 64, 66 | 3eqtr4i 2774 | . . . . . . . . . . . . 13
⊢ (((𝐴 +ℎ 𝐵) +ℎ (-1
·ℎ (2 ·ℎ 𝐶))) +ℎ (𝐴 −ℎ
𝐵)) = ((2
·ℎ 𝐴) −ℎ (2
·ℎ 𝐶)) | 
| 68 | 33 | oveq1i 7442 | . . . . . . . . . . . . 13
⊢ (((𝐴 +ℎ 𝐵) −ℎ (2
·ℎ 𝐶)) +ℎ (𝐴 −ℎ 𝐵)) = (((𝐴 +ℎ 𝐵) +ℎ (-1
·ℎ (2 ·ℎ 𝐶))) +ℎ (𝐴 −ℎ
𝐵)) | 
| 69 | 4, 1, 5 | hvsubdistr1i 31072 | . . . . . . . . . . . . 13
⊢ (2
·ℎ (𝐴 −ℎ 𝐶)) = ((2
·ℎ 𝐴) −ℎ (2
·ℎ 𝐶)) | 
| 70 | 67, 68, 69 | 3eqtr4i 2774 | . . . . . . . . . . . 12
⊢ (((𝐴 +ℎ 𝐵) −ℎ (2
·ℎ 𝐶)) +ℎ (𝐴 −ℎ 𝐵)) = (2
·ℎ (𝐴 −ℎ 𝐶)) | 
| 71 | 70 | fveq2i 6908 | . . . . . . . . . . 11
⊢
(normℎ‘(((𝐴 +ℎ 𝐵) −ℎ (2
·ℎ 𝐶)) +ℎ (𝐴 −ℎ 𝐵))) =
(normℎ‘(2 ·ℎ (𝐴 −ℎ
𝐶))) | 
| 72 | 4, 16 | norm-iii-i 31159 | . . . . . . . . . . 11
⊢
(normℎ‘(2 ·ℎ
(𝐴
−ℎ 𝐶))) = ((abs‘2) ·
(normℎ‘(𝐴 −ℎ 𝐶))) | 
| 73 | 53 | oveq1i 7442 | . . . . . . . . . . 11
⊢
((abs‘2) · (normℎ‘(𝐴 −ℎ
𝐶))) = (2 ·
(normℎ‘(𝐴 −ℎ 𝐶))) | 
| 74 | 71, 72, 73 | 3eqtri 2768 | . . . . . . . . . 10
⊢
(normℎ‘(((𝐴 +ℎ 𝐵) −ℎ (2
·ℎ 𝐶)) +ℎ (𝐴 −ℎ 𝐵))) = (2 ·
(normℎ‘(𝐴 −ℎ 𝐶))) | 
| 75 | 74 | oveq1i 7442 | . . . . . . . . 9
⊢
((normℎ‘(((𝐴 +ℎ 𝐵) −ℎ (2
·ℎ 𝐶)) +ℎ (𝐴 −ℎ 𝐵)))↑2) = ((2 ·
(normℎ‘(𝐴 −ℎ 𝐶)))↑2) | 
| 76 | 17 | recni 11276 | . . . . . . . . . 10
⊢
(normℎ‘(𝐴 −ℎ 𝐶)) ∈
ℂ | 
| 77 | 4, 76 | sqmuli 14224 | . . . . . . . . 9
⊢ ((2
· (normℎ‘(𝐴 −ℎ 𝐶)))↑2) = ((2↑2)
· ((normℎ‘(𝐴 −ℎ 𝐶))↑2)) | 
| 78 | 59 | oveq1i 7442 | . . . . . . . . 9
⊢
((2↑2) · ((normℎ‘(𝐴 −ℎ 𝐶))↑2)) = (4 ·
((normℎ‘(𝐴 −ℎ 𝐶))↑2)) | 
| 79 | 75, 77, 78 | 3eqtri 2768 | . . . . . . . 8
⊢
((normℎ‘(((𝐴 +ℎ 𝐵) −ℎ (2
·ℎ 𝐶)) +ℎ (𝐴 −ℎ 𝐵)))↑2) = (4 ·
((normℎ‘(𝐴 −ℎ 𝐶))↑2)) | 
| 80 | 61, 79 | oveq12i 7444 | . . . . . . 7
⊢
(((normℎ‘(((𝐴 +ℎ 𝐵) −ℎ (2
·ℎ 𝐶)) −ℎ (𝐴 −ℎ
𝐵)))↑2) +
((normℎ‘(((𝐴 +ℎ 𝐵) −ℎ (2
·ℎ 𝐶)) +ℎ (𝐴 −ℎ 𝐵)))↑2)) = ((4 ·
((normℎ‘(𝐵 −ℎ 𝐶))↑2)) + (4 ·
((normℎ‘(𝐴 −ℎ 𝐶))↑2))) | 
| 81 | 28, 80 | eqtr4i 2767 | . . . . . 6
⊢ ((4
· ((normℎ‘(𝐴 −ℎ 𝐶))↑2)) + (4 ·
((normℎ‘(𝐵 −ℎ 𝐶))↑2))) =
(((normℎ‘(((𝐴 +ℎ 𝐵) −ℎ (2
·ℎ 𝐶)) −ℎ (𝐴 −ℎ
𝐵)))↑2) +
((normℎ‘(((𝐴 +ℎ 𝐵) −ℎ (2
·ℎ 𝐶)) +ℎ (𝐴 −ℎ 𝐵)))↑2)) | 
| 82 | 7, 11 | normpari 31174 | . . . . . 6
⊢
(((normℎ‘(((𝐴 +ℎ 𝐵) −ℎ (2
·ℎ 𝐶)) −ℎ (𝐴 −ℎ
𝐵)))↑2) +
((normℎ‘(((𝐴 +ℎ 𝐵) −ℎ (2
·ℎ 𝐶)) +ℎ (𝐴 −ℎ 𝐵)))↑2)) = ((2 ·
((normℎ‘((𝐴 +ℎ 𝐵) −ℎ (2
·ℎ 𝐶)))↑2)) + (2 ·
((normℎ‘(𝐴 −ℎ 𝐵))↑2))) | 
| 83 | 81, 82 | eqtri 2764 | . . . . 5
⊢ ((4
· ((normℎ‘(𝐴 −ℎ 𝐶))↑2)) + (4 ·
((normℎ‘(𝐵 −ℎ 𝐶))↑2))) = ((2 ·
((normℎ‘((𝐴 +ℎ 𝐵) −ℎ (2
·ℎ 𝐶)))↑2)) + (2 ·
((normℎ‘(𝐴 −ℎ 𝐵))↑2))) | 
| 84 | 83 | oveq1i 7442 | . . . 4
⊢ (((4
· ((normℎ‘(𝐴 −ℎ 𝐶))↑2)) + (4 ·
((normℎ‘(𝐵 −ℎ 𝐶))↑2))) / 2) = (((2
· ((normℎ‘((𝐴 +ℎ 𝐵) −ℎ (2
·ℎ 𝐶)))↑2)) + (2 ·
((normℎ‘(𝐴 −ℎ 𝐵))↑2))) /
2) | 
| 85 | 4, 10 | mulcli 11269 | . . . . 5
⊢ (2
· ((normℎ‘((𝐴 +ℎ 𝐵) −ℎ (2
·ℎ 𝐶)))↑2)) ∈ ℂ | 
| 86 | 4, 14 | mulcli 11269 | . . . . 5
⊢ (2
· ((normℎ‘(𝐴 −ℎ 𝐵))↑2)) ∈
ℂ | 
| 87 | 85, 86, 4, 26 | divdiri 12025 | . . . 4
⊢ (((2
· ((normℎ‘((𝐴 +ℎ 𝐵) −ℎ (2
·ℎ 𝐶)))↑2)) + (2 ·
((normℎ‘(𝐴 −ℎ 𝐵))↑2))) / 2) = (((2
· ((normℎ‘((𝐴 +ℎ 𝐵) −ℎ (2
·ℎ 𝐶)))↑2)) / 2) + ((2 ·
((normℎ‘(𝐴 −ℎ 𝐵))↑2)) /
2)) | 
| 88 | 10, 4, 26 | divcan3i 12014 | . . . . 5
⊢ ((2
· ((normℎ‘((𝐴 +ℎ 𝐵) −ℎ (2
·ℎ 𝐶)))↑2)) / 2) =
((normℎ‘((𝐴 +ℎ 𝐵) −ℎ (2
·ℎ 𝐶)))↑2) | 
| 89 | 14, 4, 26 | divcan3i 12014 | . . . . 5
⊢ ((2
· ((normℎ‘(𝐴 −ℎ 𝐵))↑2)) / 2) =
((normℎ‘(𝐴 −ℎ 𝐵))↑2) | 
| 90 | 88, 89 | oveq12i 7444 | . . . 4
⊢ (((2
· ((normℎ‘((𝐴 +ℎ 𝐵) −ℎ (2
·ℎ 𝐶)))↑2)) / 2) + ((2 ·
((normℎ‘(𝐴 −ℎ 𝐵))↑2)) / 2)) =
(((normℎ‘((𝐴 +ℎ 𝐵) −ℎ (2
·ℎ 𝐶)))↑2) +
((normℎ‘(𝐴 −ℎ 𝐵))↑2)) | 
| 91 | 84, 87, 90 | 3eqtri 2768 | . . 3
⊢ (((4
· ((normℎ‘(𝐴 −ℎ 𝐶))↑2)) + (4 ·
((normℎ‘(𝐵 −ℎ 𝐶))↑2))) / 2) =
(((normℎ‘((𝐴 +ℎ 𝐵) −ℎ (2
·ℎ 𝐶)))↑2) +
((normℎ‘(𝐴 −ℎ 𝐵))↑2)) | 
| 92 | 15, 19, 4, 26 | div23i 12026 | . . . . 5
⊢ ((4
· ((normℎ‘(𝐴 −ℎ 𝐶))↑2)) / 2) = ((4 / 2)
· ((normℎ‘(𝐴 −ℎ 𝐶))↑2)) | 
| 93 |  | 4d2e2 12437 | . . . . . 6
⊢ (4 / 2) =
2 | 
| 94 | 93 | oveq1i 7442 | . . . . 5
⊢ ((4 / 2)
· ((normℎ‘(𝐴 −ℎ 𝐶))↑2)) = (2 ·
((normℎ‘(𝐴 −ℎ 𝐶))↑2)) | 
| 95 | 92, 94 | eqtri 2764 | . . . 4
⊢ ((4
· ((normℎ‘(𝐴 −ℎ 𝐶))↑2)) / 2) = (2 ·
((normℎ‘(𝐴 −ℎ 𝐶))↑2)) | 
| 96 | 15, 24, 4, 26 | div23i 12026 | . . . . 5
⊢ ((4
· ((normℎ‘(𝐵 −ℎ 𝐶))↑2)) / 2) = ((4 / 2)
· ((normℎ‘(𝐵 −ℎ 𝐶))↑2)) | 
| 97 | 93 | oveq1i 7442 | . . . . 5
⊢ ((4 / 2)
· ((normℎ‘(𝐵 −ℎ 𝐶))↑2)) = (2 ·
((normℎ‘(𝐵 −ℎ 𝐶))↑2)) | 
| 98 | 96, 97 | eqtri 2764 | . . . 4
⊢ ((4
· ((normℎ‘(𝐵 −ℎ 𝐶))↑2)) / 2) = (2 ·
((normℎ‘(𝐵 −ℎ 𝐶))↑2)) | 
| 99 | 95, 98 | oveq12i 7444 | . . 3
⊢ (((4
· ((normℎ‘(𝐴 −ℎ 𝐶))↑2)) / 2) + ((4 ·
((normℎ‘(𝐵 −ℎ 𝐶))↑2)) / 2)) = ((2 ·
((normℎ‘(𝐴 −ℎ 𝐶))↑2)) + (2 ·
((normℎ‘(𝐵 −ℎ 𝐶))↑2))) | 
| 100 | 27, 91, 99 | 3eqtr3i 2772 | . 2
⊢
(((normℎ‘((𝐴 +ℎ 𝐵) −ℎ (2
·ℎ 𝐶)))↑2) +
((normℎ‘(𝐴 −ℎ 𝐵))↑2)) = ((2 ·
((normℎ‘(𝐴 −ℎ 𝐶))↑2)) + (2 ·
((normℎ‘(𝐵 −ℎ 𝐶))↑2))) | 
| 101 | 10, 14, 100 | mvlladdi 11528 | 1
⊢
((normℎ‘(𝐴 −ℎ 𝐵))↑2) = (((2 ·
((normℎ‘(𝐴 −ℎ 𝐶))↑2)) + (2 ·
((normℎ‘(𝐵 −ℎ 𝐶))↑2))) −
((normℎ‘((𝐴 +ℎ 𝐵) −ℎ (2
·ℎ 𝐶)))↑2)) |