Proof of Theorem ipdirilem
Step | Hyp | Ref
| Expression |
1 | | 2cn 11905 |
. . . . . . 7
⊢ 2 ∈
ℂ |
2 | | 2ne0 11934 |
. . . . . . 7
⊢ 2 ≠
0 |
3 | 1, 2 | recidi 11563 |
. . . . . 6
⊢ (2
· (1 / 2)) = 1 |
4 | 3 | oveq1i 7223 |
. . . . 5
⊢ ((2
· (1 / 2))𝑆(𝐴𝐺𝐵)) = (1𝑆(𝐴𝐺𝐵)) |
5 | | ip1i.9 |
. . . . . . 7
⊢ 𝑈 ∈
CPreHilOLD |
6 | 5 | phnvi 28897 |
. . . . . 6
⊢ 𝑈 ∈ NrmCVec |
7 | | halfcn 12045 |
. . . . . . 7
⊢ (1 / 2)
∈ ℂ |
8 | | ipdiri.8 |
. . . . . . . 8
⊢ 𝐴 ∈ 𝑋 |
9 | | ipdiri.9 |
. . . . . . . 8
⊢ 𝐵 ∈ 𝑋 |
10 | | ip1i.1 |
. . . . . . . . 9
⊢ 𝑋 = (BaseSet‘𝑈) |
11 | | ip1i.2 |
. . . . . . . . 9
⊢ 𝐺 = ( +𝑣
‘𝑈) |
12 | 10, 11 | nvgcl 28701 |
. . . . . . . 8
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝐺𝐵) ∈ 𝑋) |
13 | 6, 8, 9, 12 | mp3an 1463 |
. . . . . . 7
⊢ (𝐴𝐺𝐵) ∈ 𝑋 |
14 | 1, 7, 13 | 3pm3.2i 1341 |
. . . . . 6
⊢ (2 ∈
ℂ ∧ (1 / 2) ∈ ℂ ∧ (𝐴𝐺𝐵) ∈ 𝑋) |
15 | | ip1i.4 |
. . . . . . 7
⊢ 𝑆 = (
·𝑠OLD ‘𝑈) |
16 | 10, 15 | nvsass 28709 |
. . . . . 6
⊢ ((𝑈 ∈ NrmCVec ∧ (2 ∈
ℂ ∧ (1 / 2) ∈ ℂ ∧ (𝐴𝐺𝐵) ∈ 𝑋)) → ((2 · (1 / 2))𝑆(𝐴𝐺𝐵)) = (2𝑆((1 / 2)𝑆(𝐴𝐺𝐵)))) |
17 | 6, 14, 16 | mp2an 692 |
. . . . 5
⊢ ((2
· (1 / 2))𝑆(𝐴𝐺𝐵)) = (2𝑆((1 / 2)𝑆(𝐴𝐺𝐵))) |
18 | 10, 15 | nvsid 28708 |
. . . . . 6
⊢ ((𝑈 ∈ NrmCVec ∧ (𝐴𝐺𝐵) ∈ 𝑋) → (1𝑆(𝐴𝐺𝐵)) = (𝐴𝐺𝐵)) |
19 | 6, 13, 18 | mp2an 692 |
. . . . 5
⊢ (1𝑆(𝐴𝐺𝐵)) = (𝐴𝐺𝐵) |
20 | 4, 17, 19 | 3eqtr3i 2773 |
. . . 4
⊢ (2𝑆((1 / 2)𝑆(𝐴𝐺𝐵))) = (𝐴𝐺𝐵) |
21 | 20 | oveq1i 7223 |
. . 3
⊢ ((2𝑆((1 / 2)𝑆(𝐴𝐺𝐵)))𝑃𝐶) = ((𝐴𝐺𝐵)𝑃𝐶) |
22 | | ip1i.7 |
. . . 4
⊢ 𝑃 =
(·𝑖OLD‘𝑈) |
23 | 10, 15 | nvscl 28707 |
. . . . 5
⊢ ((𝑈 ∈ NrmCVec ∧ (1 / 2)
∈ ℂ ∧ (𝐴𝐺𝐵) ∈ 𝑋) → ((1 / 2)𝑆(𝐴𝐺𝐵)) ∈ 𝑋) |
24 | 6, 7, 13, 23 | mp3an 1463 |
. . . 4
⊢ ((1 /
2)𝑆(𝐴𝐺𝐵)) ∈ 𝑋 |
25 | | ipdiri.10 |
. . . 4
⊢ 𝐶 ∈ 𝑋 |
26 | 10, 11, 15, 22, 5, 24, 25 | ip2i 28909 |
. . 3
⊢ ((2𝑆((1 / 2)𝑆(𝐴𝐺𝐵)))𝑃𝐶) = (2 · (((1 / 2)𝑆(𝐴𝐺𝐵))𝑃𝐶)) |
27 | 21, 26 | eqtr3i 2767 |
. 2
⊢ ((𝐴𝐺𝐵)𝑃𝐶) = (2 · (((1 / 2)𝑆(𝐴𝐺𝐵))𝑃𝐶)) |
28 | | neg1cn 11944 |
. . . . . 6
⊢ -1 ∈
ℂ |
29 | 10, 15 | nvscl 28707 |
. . . . . 6
⊢ ((𝑈 ∈ NrmCVec ∧ -1 ∈
ℂ ∧ 𝐵 ∈
𝑋) → (-1𝑆𝐵) ∈ 𝑋) |
30 | 6, 28, 9, 29 | mp3an 1463 |
. . . . 5
⊢ (-1𝑆𝐵) ∈ 𝑋 |
31 | 10, 11 | nvgcl 28701 |
. . . . 5
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ (-1𝑆𝐵) ∈ 𝑋) → (𝐴𝐺(-1𝑆𝐵)) ∈ 𝑋) |
32 | 6, 8, 30, 31 | mp3an 1463 |
. . . 4
⊢ (𝐴𝐺(-1𝑆𝐵)) ∈ 𝑋 |
33 | 10, 15 | nvscl 28707 |
. . . 4
⊢ ((𝑈 ∈ NrmCVec ∧ (1 / 2)
∈ ℂ ∧ (𝐴𝐺(-1𝑆𝐵)) ∈ 𝑋) → ((1 / 2)𝑆(𝐴𝐺(-1𝑆𝐵))) ∈ 𝑋) |
34 | 6, 7, 32, 33 | mp3an 1463 |
. . 3
⊢ ((1 /
2)𝑆(𝐴𝐺(-1𝑆𝐵))) ∈ 𝑋 |
35 | 10, 11, 15, 22, 5, 24, 34, 25 | ip1i 28908 |
. 2
⊢ (((((1 /
2)𝑆(𝐴𝐺𝐵))𝐺((1 / 2)𝑆(𝐴𝐺(-1𝑆𝐵))))𝑃𝐶) + ((((1 / 2)𝑆(𝐴𝐺𝐵))𝐺(-1𝑆((1 / 2)𝑆(𝐴𝐺(-1𝑆𝐵)))))𝑃𝐶)) = (2 · (((1 / 2)𝑆(𝐴𝐺𝐵))𝑃𝐶)) |
36 | | eqid 2737 |
. . . . . . . . . . . 12
⊢
(1st ‘𝑈) = (1st ‘𝑈) |
37 | 36 | nvvc 28696 |
. . . . . . . . . . 11
⊢ (𝑈 ∈ NrmCVec →
(1st ‘𝑈)
∈ CVecOLD) |
38 | 6, 37 | ax-mp 5 |
. . . . . . . . . 10
⊢
(1st ‘𝑈) ∈ CVecOLD |
39 | 11 | vafval 28684 |
. . . . . . . . . . 11
⊢ 𝐺 = (1st
‘(1st ‘𝑈)) |
40 | 39 | vcablo 28650 |
. . . . . . . . . 10
⊢
((1st ‘𝑈) ∈ CVecOLD → 𝐺 ∈ AbelOp) |
41 | 38, 40 | ax-mp 5 |
. . . . . . . . 9
⊢ 𝐺 ∈ AbelOp |
42 | 8, 9 | pm3.2i 474 |
. . . . . . . . 9
⊢ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) |
43 | 8, 30 | pm3.2i 474 |
. . . . . . . . 9
⊢ (𝐴 ∈ 𝑋 ∧ (-1𝑆𝐵) ∈ 𝑋) |
44 | 10, 11 | bafval 28685 |
. . . . . . . . . 10
⊢ 𝑋 = ran 𝐺 |
45 | 44 | ablo4 28631 |
. . . . . . . . 9
⊢ ((𝐺 ∈ AbelOp ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ (-1𝑆𝐵) ∈ 𝑋)) → ((𝐴𝐺𝐵)𝐺(𝐴𝐺(-1𝑆𝐵))) = ((𝐴𝐺𝐴)𝐺(𝐵𝐺(-1𝑆𝐵)))) |
46 | 41, 42, 43, 45 | mp3an 1463 |
. . . . . . . 8
⊢ ((𝐴𝐺𝐵)𝐺(𝐴𝐺(-1𝑆𝐵))) = ((𝐴𝐺𝐴)𝐺(𝐵𝐺(-1𝑆𝐵))) |
47 | 15 | smfval 28686 |
. . . . . . . . . . 11
⊢ 𝑆 = (2nd
‘(1st ‘𝑈)) |
48 | 39, 47, 44 | vc2OLD 28649 |
. . . . . . . . . 10
⊢
(((1st ‘𝑈) ∈ CVecOLD ∧ 𝐴 ∈ 𝑋) → (𝐴𝐺𝐴) = (2𝑆𝐴)) |
49 | 38, 8, 48 | mp2an 692 |
. . . . . . . . 9
⊢ (𝐴𝐺𝐴) = (2𝑆𝐴) |
50 | | eqid 2737 |
. . . . . . . . . . 11
⊢
(0vec‘𝑈) = (0vec‘𝑈) |
51 | 10, 11, 15, 50 | nvrinv 28732 |
. . . . . . . . . 10
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐵 ∈ 𝑋) → (𝐵𝐺(-1𝑆𝐵)) = (0vec‘𝑈)) |
52 | 6, 9, 51 | mp2an 692 |
. . . . . . . . 9
⊢ (𝐵𝐺(-1𝑆𝐵)) = (0vec‘𝑈) |
53 | 49, 52 | oveq12i 7225 |
. . . . . . . 8
⊢ ((𝐴𝐺𝐴)𝐺(𝐵𝐺(-1𝑆𝐵))) = ((2𝑆𝐴)𝐺(0vec‘𝑈)) |
54 | 10, 15 | nvscl 28707 |
. . . . . . . . . 10
⊢ ((𝑈 ∈ NrmCVec ∧ 2 ∈
ℂ ∧ 𝐴 ∈
𝑋) → (2𝑆𝐴) ∈ 𝑋) |
55 | 6, 1, 8, 54 | mp3an 1463 |
. . . . . . . . 9
⊢ (2𝑆𝐴) ∈ 𝑋 |
56 | 10, 11, 50 | nv0rid 28716 |
. . . . . . . . 9
⊢ ((𝑈 ∈ NrmCVec ∧ (2𝑆𝐴) ∈ 𝑋) → ((2𝑆𝐴)𝐺(0vec‘𝑈)) = (2𝑆𝐴)) |
57 | 6, 55, 56 | mp2an 692 |
. . . . . . . 8
⊢ ((2𝑆𝐴)𝐺(0vec‘𝑈)) = (2𝑆𝐴) |
58 | 46, 53, 57 | 3eqtri 2769 |
. . . . . . 7
⊢ ((𝐴𝐺𝐵)𝐺(𝐴𝐺(-1𝑆𝐵))) = (2𝑆𝐴) |
59 | 58 | oveq2i 7224 |
. . . . . 6
⊢ ((1 /
2)𝑆((𝐴𝐺𝐵)𝐺(𝐴𝐺(-1𝑆𝐵)))) = ((1 / 2)𝑆(2𝑆𝐴)) |
60 | 7, 1, 8 | 3pm3.2i 1341 |
. . . . . . 7
⊢ ((1 / 2)
∈ ℂ ∧ 2 ∈ ℂ ∧ 𝐴 ∈ 𝑋) |
61 | 10, 15 | nvsass 28709 |
. . . . . . 7
⊢ ((𝑈 ∈ NrmCVec ∧ ((1 / 2)
∈ ℂ ∧ 2 ∈ ℂ ∧ 𝐴 ∈ 𝑋)) → (((1 / 2) · 2)𝑆𝐴) = ((1 / 2)𝑆(2𝑆𝐴))) |
62 | 6, 60, 61 | mp2an 692 |
. . . . . 6
⊢ (((1 / 2)
· 2)𝑆𝐴) = ((1 / 2)𝑆(2𝑆𝐴)) |
63 | 59, 62 | eqtr4i 2768 |
. . . . 5
⊢ ((1 /
2)𝑆((𝐴𝐺𝐵)𝐺(𝐴𝐺(-1𝑆𝐵)))) = (((1 / 2) · 2)𝑆𝐴) |
64 | 7, 13, 32 | 3pm3.2i 1341 |
. . . . . 6
⊢ ((1 / 2)
∈ ℂ ∧ (𝐴𝐺𝐵) ∈ 𝑋 ∧ (𝐴𝐺(-1𝑆𝐵)) ∈ 𝑋) |
65 | 10, 11, 15 | nvdi 28711 |
. . . . . 6
⊢ ((𝑈 ∈ NrmCVec ∧ ((1 / 2)
∈ ℂ ∧ (𝐴𝐺𝐵) ∈ 𝑋 ∧ (𝐴𝐺(-1𝑆𝐵)) ∈ 𝑋)) → ((1 / 2)𝑆((𝐴𝐺𝐵)𝐺(𝐴𝐺(-1𝑆𝐵)))) = (((1 / 2)𝑆(𝐴𝐺𝐵))𝐺((1 / 2)𝑆(𝐴𝐺(-1𝑆𝐵))))) |
66 | 6, 64, 65 | mp2an 692 |
. . . . 5
⊢ ((1 /
2)𝑆((𝐴𝐺𝐵)𝐺(𝐴𝐺(-1𝑆𝐵)))) = (((1 / 2)𝑆(𝐴𝐺𝐵))𝐺((1 / 2)𝑆(𝐴𝐺(-1𝑆𝐵)))) |
67 | | ax-1cn 10787 |
. . . . . . . 8
⊢ 1 ∈
ℂ |
68 | 67, 1, 2 | divcan1i 11576 |
. . . . . . 7
⊢ ((1 / 2)
· 2) = 1 |
69 | 68 | oveq1i 7223 |
. . . . . 6
⊢ (((1 / 2)
· 2)𝑆𝐴) = (1𝑆𝐴) |
70 | 10, 15 | nvsid 28708 |
. . . . . . 7
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → (1𝑆𝐴) = 𝐴) |
71 | 6, 8, 70 | mp2an 692 |
. . . . . 6
⊢ (1𝑆𝐴) = 𝐴 |
72 | 69, 71 | eqtri 2765 |
. . . . 5
⊢ (((1 / 2)
· 2)𝑆𝐴) = 𝐴 |
73 | 63, 66, 72 | 3eqtr3i 2773 |
. . . 4
⊢ (((1 /
2)𝑆(𝐴𝐺𝐵))𝐺((1 / 2)𝑆(𝐴𝐺(-1𝑆𝐵)))) = 𝐴 |
74 | 73 | oveq1i 7223 |
. . 3
⊢ ((((1 /
2)𝑆(𝐴𝐺𝐵))𝐺((1 / 2)𝑆(𝐴𝐺(-1𝑆𝐵))))𝑃𝐶) = (𝐴𝑃𝐶) |
75 | 28, 7 | mulcomi 10841 |
. . . . . . . . 9
⊢ (-1
· (1 / 2)) = ((1 / 2) · -1) |
76 | 75 | oveq1i 7223 |
. . . . . . . 8
⊢ ((-1
· (1 / 2))𝑆(𝐴𝐺(-1𝑆𝐵))) = (((1 / 2) · -1)𝑆(𝐴𝐺(-1𝑆𝐵))) |
77 | 28, 7, 32 | 3pm3.2i 1341 |
. . . . . . . . 9
⊢ (-1
∈ ℂ ∧ (1 / 2) ∈ ℂ ∧ (𝐴𝐺(-1𝑆𝐵)) ∈ 𝑋) |
78 | 10, 15 | nvsass 28709 |
. . . . . . . . 9
⊢ ((𝑈 ∈ NrmCVec ∧ (-1 ∈
ℂ ∧ (1 / 2) ∈ ℂ ∧ (𝐴𝐺(-1𝑆𝐵)) ∈ 𝑋)) → ((-1 · (1 / 2))𝑆(𝐴𝐺(-1𝑆𝐵))) = (-1𝑆((1 / 2)𝑆(𝐴𝐺(-1𝑆𝐵))))) |
79 | 6, 77, 78 | mp2an 692 |
. . . . . . . 8
⊢ ((-1
· (1 / 2))𝑆(𝐴𝐺(-1𝑆𝐵))) = (-1𝑆((1 / 2)𝑆(𝐴𝐺(-1𝑆𝐵)))) |
80 | 7, 28, 32 | 3pm3.2i 1341 |
. . . . . . . . . 10
⊢ ((1 / 2)
∈ ℂ ∧ -1 ∈ ℂ ∧ (𝐴𝐺(-1𝑆𝐵)) ∈ 𝑋) |
81 | 10, 15 | nvsass 28709 |
. . . . . . . . . 10
⊢ ((𝑈 ∈ NrmCVec ∧ ((1 / 2)
∈ ℂ ∧ -1 ∈ ℂ ∧ (𝐴𝐺(-1𝑆𝐵)) ∈ 𝑋)) → (((1 / 2) · -1)𝑆(𝐴𝐺(-1𝑆𝐵))) = ((1 / 2)𝑆(-1𝑆(𝐴𝐺(-1𝑆𝐵))))) |
82 | 6, 80, 81 | mp2an 692 |
. . . . . . . . 9
⊢ (((1 / 2)
· -1)𝑆(𝐴𝐺(-1𝑆𝐵))) = ((1 / 2)𝑆(-1𝑆(𝐴𝐺(-1𝑆𝐵)))) |
83 | 28, 8, 30 | 3pm3.2i 1341 |
. . . . . . . . . . . 12
⊢ (-1
∈ ℂ ∧ 𝐴
∈ 𝑋 ∧ (-1𝑆𝐵) ∈ 𝑋) |
84 | 10, 11, 15 | nvdi 28711 |
. . . . . . . . . . . 12
⊢ ((𝑈 ∈ NrmCVec ∧ (-1 ∈
ℂ ∧ 𝐴 ∈
𝑋 ∧ (-1𝑆𝐵) ∈ 𝑋)) → (-1𝑆(𝐴𝐺(-1𝑆𝐵))) = ((-1𝑆𝐴)𝐺(-1𝑆(-1𝑆𝐵)))) |
85 | 6, 83, 84 | mp2an 692 |
. . . . . . . . . . 11
⊢ (-1𝑆(𝐴𝐺(-1𝑆𝐵))) = ((-1𝑆𝐴)𝐺(-1𝑆(-1𝑆𝐵))) |
86 | | neg1mulneg1e1 12043 |
. . . . . . . . . . . . . 14
⊢ (-1
· -1) = 1 |
87 | 86 | oveq1i 7223 |
. . . . . . . . . . . . 13
⊢ ((-1
· -1)𝑆𝐵) = (1𝑆𝐵) |
88 | 28, 28, 9 | 3pm3.2i 1341 |
. . . . . . . . . . . . . 14
⊢ (-1
∈ ℂ ∧ -1 ∈ ℂ ∧ 𝐵 ∈ 𝑋) |
89 | 10, 15 | nvsass 28709 |
. . . . . . . . . . . . . 14
⊢ ((𝑈 ∈ NrmCVec ∧ (-1 ∈
ℂ ∧ -1 ∈ ℂ ∧ 𝐵 ∈ 𝑋)) → ((-1 · -1)𝑆𝐵) = (-1𝑆(-1𝑆𝐵))) |
90 | 6, 88, 89 | mp2an 692 |
. . . . . . . . . . . . 13
⊢ ((-1
· -1)𝑆𝐵) = (-1𝑆(-1𝑆𝐵)) |
91 | 10, 15 | nvsid 28708 |
. . . . . . . . . . . . . 14
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐵 ∈ 𝑋) → (1𝑆𝐵) = 𝐵) |
92 | 6, 9, 91 | mp2an 692 |
. . . . . . . . . . . . 13
⊢ (1𝑆𝐵) = 𝐵 |
93 | 87, 90, 92 | 3eqtr3i 2773 |
. . . . . . . . . . . 12
⊢ (-1𝑆(-1𝑆𝐵)) = 𝐵 |
94 | 93 | oveq2i 7224 |
. . . . . . . . . . 11
⊢ ((-1𝑆𝐴)𝐺(-1𝑆(-1𝑆𝐵))) = ((-1𝑆𝐴)𝐺𝐵) |
95 | 85, 94 | eqtri 2765 |
. . . . . . . . . 10
⊢ (-1𝑆(𝐴𝐺(-1𝑆𝐵))) = ((-1𝑆𝐴)𝐺𝐵) |
96 | 95 | oveq2i 7224 |
. . . . . . . . 9
⊢ ((1 /
2)𝑆(-1𝑆(𝐴𝐺(-1𝑆𝐵)))) = ((1 / 2)𝑆((-1𝑆𝐴)𝐺𝐵)) |
97 | 82, 96 | eqtri 2765 |
. . . . . . . 8
⊢ (((1 / 2)
· -1)𝑆(𝐴𝐺(-1𝑆𝐵))) = ((1 / 2)𝑆((-1𝑆𝐴)𝐺𝐵)) |
98 | 76, 79, 97 | 3eqtr3i 2773 |
. . . . . . 7
⊢ (-1𝑆((1 / 2)𝑆(𝐴𝐺(-1𝑆𝐵)))) = ((1 / 2)𝑆((-1𝑆𝐴)𝐺𝐵)) |
99 | 98 | oveq2i 7224 |
. . . . . 6
⊢ (((1 /
2)𝑆(𝐴𝐺𝐵))𝐺(-1𝑆((1 / 2)𝑆(𝐴𝐺(-1𝑆𝐵))))) = (((1 / 2)𝑆(𝐴𝐺𝐵))𝐺((1 / 2)𝑆((-1𝑆𝐴)𝐺𝐵))) |
100 | 10, 15 | nvscl 28707 |
. . . . . . . . . 10
⊢ ((𝑈 ∈ NrmCVec ∧ -1 ∈
ℂ ∧ 𝐴 ∈
𝑋) → (-1𝑆𝐴) ∈ 𝑋) |
101 | 6, 28, 8, 100 | mp3an 1463 |
. . . . . . . . 9
⊢ (-1𝑆𝐴) ∈ 𝑋 |
102 | 10, 11 | nvgcl 28701 |
. . . . . . . . 9
⊢ ((𝑈 ∈ NrmCVec ∧ (-1𝑆𝐴) ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((-1𝑆𝐴)𝐺𝐵) ∈ 𝑋) |
103 | 6, 101, 9, 102 | mp3an 1463 |
. . . . . . . 8
⊢ ((-1𝑆𝐴)𝐺𝐵) ∈ 𝑋 |
104 | 7, 13, 103 | 3pm3.2i 1341 |
. . . . . . 7
⊢ ((1 / 2)
∈ ℂ ∧ (𝐴𝐺𝐵) ∈ 𝑋 ∧ ((-1𝑆𝐴)𝐺𝐵) ∈ 𝑋) |
105 | 10, 11, 15 | nvdi 28711 |
. . . . . . 7
⊢ ((𝑈 ∈ NrmCVec ∧ ((1 / 2)
∈ ℂ ∧ (𝐴𝐺𝐵) ∈ 𝑋 ∧ ((-1𝑆𝐴)𝐺𝐵) ∈ 𝑋)) → ((1 / 2)𝑆((𝐴𝐺𝐵)𝐺((-1𝑆𝐴)𝐺𝐵))) = (((1 / 2)𝑆(𝐴𝐺𝐵))𝐺((1 / 2)𝑆((-1𝑆𝐴)𝐺𝐵)))) |
106 | 6, 104, 105 | mp2an 692 |
. . . . . 6
⊢ ((1 /
2)𝑆((𝐴𝐺𝐵)𝐺((-1𝑆𝐴)𝐺𝐵))) = (((1 / 2)𝑆(𝐴𝐺𝐵))𝐺((1 / 2)𝑆((-1𝑆𝐴)𝐺𝐵))) |
107 | 99, 106 | eqtr4i 2768 |
. . . . 5
⊢ (((1 /
2)𝑆(𝐴𝐺𝐵))𝐺(-1𝑆((1 / 2)𝑆(𝐴𝐺(-1𝑆𝐵))))) = ((1 / 2)𝑆((𝐴𝐺𝐵)𝐺((-1𝑆𝐴)𝐺𝐵))) |
108 | 101, 9 | pm3.2i 474 |
. . . . . . . . 9
⊢ ((-1𝑆𝐴) ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) |
109 | 44 | ablo4 28631 |
. . . . . . . . 9
⊢ ((𝐺 ∈ AbelOp ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ ((-1𝑆𝐴) ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → ((𝐴𝐺𝐵)𝐺((-1𝑆𝐴)𝐺𝐵)) = ((𝐴𝐺(-1𝑆𝐴))𝐺(𝐵𝐺𝐵))) |
110 | 41, 42, 108, 109 | mp3an 1463 |
. . . . . . . 8
⊢ ((𝐴𝐺𝐵)𝐺((-1𝑆𝐴)𝐺𝐵)) = ((𝐴𝐺(-1𝑆𝐴))𝐺(𝐵𝐺𝐵)) |
111 | 10, 11, 15, 50 | nvrinv 28732 |
. . . . . . . . . . 11
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → (𝐴𝐺(-1𝑆𝐴)) = (0vec‘𝑈)) |
112 | 6, 8, 111 | mp2an 692 |
. . . . . . . . . 10
⊢ (𝐴𝐺(-1𝑆𝐴)) = (0vec‘𝑈) |
113 | 112 | oveq1i 7223 |
. . . . . . . . 9
⊢ ((𝐴𝐺(-1𝑆𝐴))𝐺(𝐵𝐺𝐵)) = ((0vec‘𝑈)𝐺(𝐵𝐺𝐵)) |
114 | 10, 11 | nvgcl 28701 |
. . . . . . . . . . 11
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐵 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐵𝐺𝐵) ∈ 𝑋) |
115 | 6, 9, 9, 114 | mp3an 1463 |
. . . . . . . . . 10
⊢ (𝐵𝐺𝐵) ∈ 𝑋 |
116 | 10, 11, 50 | nv0lid 28717 |
. . . . . . . . . 10
⊢ ((𝑈 ∈ NrmCVec ∧ (𝐵𝐺𝐵) ∈ 𝑋) → ((0vec‘𝑈)𝐺(𝐵𝐺𝐵)) = (𝐵𝐺𝐵)) |
117 | 6, 115, 116 | mp2an 692 |
. . . . . . . . 9
⊢
((0vec‘𝑈)𝐺(𝐵𝐺𝐵)) = (𝐵𝐺𝐵) |
118 | 113, 117 | eqtri 2765 |
. . . . . . . 8
⊢ ((𝐴𝐺(-1𝑆𝐴))𝐺(𝐵𝐺𝐵)) = (𝐵𝐺𝐵) |
119 | 39, 47, 44 | vc2OLD 28649 |
. . . . . . . . 9
⊢
(((1st ‘𝑈) ∈ CVecOLD ∧ 𝐵 ∈ 𝑋) → (𝐵𝐺𝐵) = (2𝑆𝐵)) |
120 | 38, 9, 119 | mp2an 692 |
. . . . . . . 8
⊢ (𝐵𝐺𝐵) = (2𝑆𝐵) |
121 | 110, 118,
120 | 3eqtri 2769 |
. . . . . . 7
⊢ ((𝐴𝐺𝐵)𝐺((-1𝑆𝐴)𝐺𝐵)) = (2𝑆𝐵) |
122 | 121 | oveq2i 7224 |
. . . . . 6
⊢ ((1 /
2)𝑆((𝐴𝐺𝐵)𝐺((-1𝑆𝐴)𝐺𝐵))) = ((1 / 2)𝑆(2𝑆𝐵)) |
123 | 7, 1, 9 | 3pm3.2i 1341 |
. . . . . . 7
⊢ ((1 / 2)
∈ ℂ ∧ 2 ∈ ℂ ∧ 𝐵 ∈ 𝑋) |
124 | 10, 15 | nvsass 28709 |
. . . . . . 7
⊢ ((𝑈 ∈ NrmCVec ∧ ((1 / 2)
∈ ℂ ∧ 2 ∈ ℂ ∧ 𝐵 ∈ 𝑋)) → (((1 / 2) · 2)𝑆𝐵) = ((1 / 2)𝑆(2𝑆𝐵))) |
125 | 6, 123, 124 | mp2an 692 |
. . . . . 6
⊢ (((1 / 2)
· 2)𝑆𝐵) = ((1 / 2)𝑆(2𝑆𝐵)) |
126 | 68 | oveq1i 7223 |
. . . . . 6
⊢ (((1 / 2)
· 2)𝑆𝐵) = (1𝑆𝐵) |
127 | 122, 125,
126 | 3eqtr2i 2771 |
. . . . 5
⊢ ((1 /
2)𝑆((𝐴𝐺𝐵)𝐺((-1𝑆𝐴)𝐺𝐵))) = (1𝑆𝐵) |
128 | 107, 127,
92 | 3eqtri 2769 |
. . . 4
⊢ (((1 /
2)𝑆(𝐴𝐺𝐵))𝐺(-1𝑆((1 / 2)𝑆(𝐴𝐺(-1𝑆𝐵))))) = 𝐵 |
129 | 128 | oveq1i 7223 |
. . 3
⊢ ((((1 /
2)𝑆(𝐴𝐺𝐵))𝐺(-1𝑆((1 / 2)𝑆(𝐴𝐺(-1𝑆𝐵)))))𝑃𝐶) = (𝐵𝑃𝐶) |
130 | 74, 129 | oveq12i 7225 |
. 2
⊢ (((((1 /
2)𝑆(𝐴𝐺𝐵))𝐺((1 / 2)𝑆(𝐴𝐺(-1𝑆𝐵))))𝑃𝐶) + ((((1 / 2)𝑆(𝐴𝐺𝐵))𝐺(-1𝑆((1 / 2)𝑆(𝐴𝐺(-1𝑆𝐵)))))𝑃𝐶)) = ((𝐴𝑃𝐶) + (𝐵𝑃𝐶)) |
131 | 27, 35, 130 | 3eqtr2i 2771 |
1
⊢ ((𝐴𝐺𝐵)𝑃𝐶) = ((𝐴𝑃𝐶) + (𝐵𝑃𝐶)) |