Step |
Hyp |
Ref |
Expression |
1 |
|
phlsrng.f |
⊢ 𝐹 = ( Scalar ‘ 𝑊 ) |
2 |
|
phllmhm.h |
⊢ , = ( ·𝑖 ‘ 𝑊 ) |
3 |
|
phllmhm.v |
⊢ 𝑉 = ( Base ‘ 𝑊 ) |
4 |
|
ipsubdir.m |
⊢ − = ( -g ‘ 𝑊 ) |
5 |
|
ipsubdir.s |
⊢ 𝑆 = ( -g ‘ 𝐹 ) |
6 |
|
simpl |
⊢ ( ( 𝑊 ∈ PreHil ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → 𝑊 ∈ PreHil ) |
7 |
|
simpr1 |
⊢ ( ( 𝑊 ∈ PreHil ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → 𝐴 ∈ 𝑉 ) |
8 |
|
phllmod |
⊢ ( 𝑊 ∈ PreHil → 𝑊 ∈ LMod ) |
9 |
8
|
adantr |
⊢ ( ( 𝑊 ∈ PreHil ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → 𝑊 ∈ LMod ) |
10 |
|
lmodgrp |
⊢ ( 𝑊 ∈ LMod → 𝑊 ∈ Grp ) |
11 |
9 10
|
syl |
⊢ ( ( 𝑊 ∈ PreHil ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → 𝑊 ∈ Grp ) |
12 |
|
simpr2 |
⊢ ( ( 𝑊 ∈ PreHil ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → 𝐵 ∈ 𝑉 ) |
13 |
|
simpr3 |
⊢ ( ( 𝑊 ∈ PreHil ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → 𝐶 ∈ 𝑉 ) |
14 |
3 4
|
grpsubcl |
⊢ ( ( 𝑊 ∈ Grp ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) → ( 𝐵 − 𝐶 ) ∈ 𝑉 ) |
15 |
11 12 13 14
|
syl3anc |
⊢ ( ( 𝑊 ∈ PreHil ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → ( 𝐵 − 𝐶 ) ∈ 𝑉 ) |
16 |
|
eqid |
⊢ ( +g ‘ 𝑊 ) = ( +g ‘ 𝑊 ) |
17 |
|
eqid |
⊢ ( +g ‘ 𝐹 ) = ( +g ‘ 𝐹 ) |
18 |
1 2 3 16 17
|
ipdi |
⊢ ( ( 𝑊 ∈ PreHil ∧ ( 𝐴 ∈ 𝑉 ∧ ( 𝐵 − 𝐶 ) ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → ( 𝐴 , ( ( 𝐵 − 𝐶 ) ( +g ‘ 𝑊 ) 𝐶 ) ) = ( ( 𝐴 , ( 𝐵 − 𝐶 ) ) ( +g ‘ 𝐹 ) ( 𝐴 , 𝐶 ) ) ) |
19 |
6 7 15 13 18
|
syl13anc |
⊢ ( ( 𝑊 ∈ PreHil ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → ( 𝐴 , ( ( 𝐵 − 𝐶 ) ( +g ‘ 𝑊 ) 𝐶 ) ) = ( ( 𝐴 , ( 𝐵 − 𝐶 ) ) ( +g ‘ 𝐹 ) ( 𝐴 , 𝐶 ) ) ) |
20 |
3 16 4
|
grpnpcan |
⊢ ( ( 𝑊 ∈ Grp ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) → ( ( 𝐵 − 𝐶 ) ( +g ‘ 𝑊 ) 𝐶 ) = 𝐵 ) |
21 |
11 12 13 20
|
syl3anc |
⊢ ( ( 𝑊 ∈ PreHil ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → ( ( 𝐵 − 𝐶 ) ( +g ‘ 𝑊 ) 𝐶 ) = 𝐵 ) |
22 |
21
|
oveq2d |
⊢ ( ( 𝑊 ∈ PreHil ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → ( 𝐴 , ( ( 𝐵 − 𝐶 ) ( +g ‘ 𝑊 ) 𝐶 ) ) = ( 𝐴 , 𝐵 ) ) |
23 |
19 22
|
eqtr3d |
⊢ ( ( 𝑊 ∈ PreHil ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → ( ( 𝐴 , ( 𝐵 − 𝐶 ) ) ( +g ‘ 𝐹 ) ( 𝐴 , 𝐶 ) ) = ( 𝐴 , 𝐵 ) ) |
24 |
1
|
lmodfgrp |
⊢ ( 𝑊 ∈ LMod → 𝐹 ∈ Grp ) |
25 |
9 24
|
syl |
⊢ ( ( 𝑊 ∈ PreHil ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → 𝐹 ∈ Grp ) |
26 |
|
eqid |
⊢ ( Base ‘ 𝐹 ) = ( Base ‘ 𝐹 ) |
27 |
1 2 3 26
|
ipcl |
⊢ ( ( 𝑊 ∈ PreHil ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) → ( 𝐴 , 𝐵 ) ∈ ( Base ‘ 𝐹 ) ) |
28 |
6 7 12 27
|
syl3anc |
⊢ ( ( 𝑊 ∈ PreHil ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → ( 𝐴 , 𝐵 ) ∈ ( Base ‘ 𝐹 ) ) |
29 |
1 2 3 26
|
ipcl |
⊢ ( ( 𝑊 ∈ PreHil ∧ 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) → ( 𝐴 , 𝐶 ) ∈ ( Base ‘ 𝐹 ) ) |
30 |
6 7 13 29
|
syl3anc |
⊢ ( ( 𝑊 ∈ PreHil ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → ( 𝐴 , 𝐶 ) ∈ ( Base ‘ 𝐹 ) ) |
31 |
1 2 3 26
|
ipcl |
⊢ ( ( 𝑊 ∈ PreHil ∧ 𝐴 ∈ 𝑉 ∧ ( 𝐵 − 𝐶 ) ∈ 𝑉 ) → ( 𝐴 , ( 𝐵 − 𝐶 ) ) ∈ ( Base ‘ 𝐹 ) ) |
32 |
6 7 15 31
|
syl3anc |
⊢ ( ( 𝑊 ∈ PreHil ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → ( 𝐴 , ( 𝐵 − 𝐶 ) ) ∈ ( Base ‘ 𝐹 ) ) |
33 |
26 17 5
|
grpsubadd |
⊢ ( ( 𝐹 ∈ Grp ∧ ( ( 𝐴 , 𝐵 ) ∈ ( Base ‘ 𝐹 ) ∧ ( 𝐴 , 𝐶 ) ∈ ( Base ‘ 𝐹 ) ∧ ( 𝐴 , ( 𝐵 − 𝐶 ) ) ∈ ( Base ‘ 𝐹 ) ) ) → ( ( ( 𝐴 , 𝐵 ) 𝑆 ( 𝐴 , 𝐶 ) ) = ( 𝐴 , ( 𝐵 − 𝐶 ) ) ↔ ( ( 𝐴 , ( 𝐵 − 𝐶 ) ) ( +g ‘ 𝐹 ) ( 𝐴 , 𝐶 ) ) = ( 𝐴 , 𝐵 ) ) ) |
34 |
25 28 30 32 33
|
syl13anc |
⊢ ( ( 𝑊 ∈ PreHil ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → ( ( ( 𝐴 , 𝐵 ) 𝑆 ( 𝐴 , 𝐶 ) ) = ( 𝐴 , ( 𝐵 − 𝐶 ) ) ↔ ( ( 𝐴 , ( 𝐵 − 𝐶 ) ) ( +g ‘ 𝐹 ) ( 𝐴 , 𝐶 ) ) = ( 𝐴 , 𝐵 ) ) ) |
35 |
23 34
|
mpbird |
⊢ ( ( 𝑊 ∈ PreHil ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → ( ( 𝐴 , 𝐵 ) 𝑆 ( 𝐴 , 𝐶 ) ) = ( 𝐴 , ( 𝐵 − 𝐶 ) ) ) |
36 |
35
|
eqcomd |
⊢ ( ( 𝑊 ∈ PreHil ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → ( 𝐴 , ( 𝐵 − 𝐶 ) ) = ( ( 𝐴 , 𝐵 ) 𝑆 ( 𝐴 , 𝐶 ) ) ) |