Step |
Hyp |
Ref |
Expression |
1 |
|
phlsrng.f |
⊢ 𝐹 = ( Scalar ‘ 𝑊 ) |
2 |
|
phllmhm.h |
⊢ , = ( ·𝑖 ‘ 𝑊 ) |
3 |
|
phllmhm.v |
⊢ 𝑉 = ( Base ‘ 𝑊 ) |
4 |
|
ipdir.g |
⊢ + = ( +g ‘ 𝑊 ) |
5 |
|
ipdir.p |
⊢ ⨣ = ( +g ‘ 𝐹 ) |
6 |
|
simpl |
⊢ ( ( 𝑊 ∈ PreHil ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → 𝑊 ∈ PreHil ) |
7 |
|
simpr2 |
⊢ ( ( 𝑊 ∈ PreHil ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → 𝐵 ∈ 𝑉 ) |
8 |
|
simpr3 |
⊢ ( ( 𝑊 ∈ PreHil ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → 𝐶 ∈ 𝑉 ) |
9 |
|
simpr1 |
⊢ ( ( 𝑊 ∈ PreHil ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → 𝐴 ∈ 𝑉 ) |
10 |
1 2 3 4 5
|
ipdir |
⊢ ( ( 𝑊 ∈ PreHil ∧ ( 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉 ) ) → ( ( 𝐵 + 𝐶 ) , 𝐴 ) = ( ( 𝐵 , 𝐴 ) ⨣ ( 𝐶 , 𝐴 ) ) ) |
11 |
6 7 8 9 10
|
syl13anc |
⊢ ( ( 𝑊 ∈ PreHil ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → ( ( 𝐵 + 𝐶 ) , 𝐴 ) = ( ( 𝐵 , 𝐴 ) ⨣ ( 𝐶 , 𝐴 ) ) ) |
12 |
11
|
fveq2d |
⊢ ( ( 𝑊 ∈ PreHil ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → ( ( *𝑟 ‘ 𝐹 ) ‘ ( ( 𝐵 + 𝐶 ) , 𝐴 ) ) = ( ( *𝑟 ‘ 𝐹 ) ‘ ( ( 𝐵 , 𝐴 ) ⨣ ( 𝐶 , 𝐴 ) ) ) ) |
13 |
1
|
phlsrng |
⊢ ( 𝑊 ∈ PreHil → 𝐹 ∈ *-Ring ) |
14 |
13
|
adantr |
⊢ ( ( 𝑊 ∈ PreHil ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → 𝐹 ∈ *-Ring ) |
15 |
|
eqid |
⊢ ( Base ‘ 𝐹 ) = ( Base ‘ 𝐹 ) |
16 |
1 2 3 15
|
ipcl |
⊢ ( ( 𝑊 ∈ PreHil ∧ 𝐵 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉 ) → ( 𝐵 , 𝐴 ) ∈ ( Base ‘ 𝐹 ) ) |
17 |
6 7 9 16
|
syl3anc |
⊢ ( ( 𝑊 ∈ PreHil ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → ( 𝐵 , 𝐴 ) ∈ ( Base ‘ 𝐹 ) ) |
18 |
1 2 3 15
|
ipcl |
⊢ ( ( 𝑊 ∈ PreHil ∧ 𝐶 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉 ) → ( 𝐶 , 𝐴 ) ∈ ( Base ‘ 𝐹 ) ) |
19 |
6 8 9 18
|
syl3anc |
⊢ ( ( 𝑊 ∈ PreHil ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → ( 𝐶 , 𝐴 ) ∈ ( Base ‘ 𝐹 ) ) |
20 |
|
eqid |
⊢ ( *𝑟 ‘ 𝐹 ) = ( *𝑟 ‘ 𝐹 ) |
21 |
20 15 5
|
srngadd |
⊢ ( ( 𝐹 ∈ *-Ring ∧ ( 𝐵 , 𝐴 ) ∈ ( Base ‘ 𝐹 ) ∧ ( 𝐶 , 𝐴 ) ∈ ( Base ‘ 𝐹 ) ) → ( ( *𝑟 ‘ 𝐹 ) ‘ ( ( 𝐵 , 𝐴 ) ⨣ ( 𝐶 , 𝐴 ) ) ) = ( ( ( *𝑟 ‘ 𝐹 ) ‘ ( 𝐵 , 𝐴 ) ) ⨣ ( ( *𝑟 ‘ 𝐹 ) ‘ ( 𝐶 , 𝐴 ) ) ) ) |
22 |
14 17 19 21
|
syl3anc |
⊢ ( ( 𝑊 ∈ PreHil ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → ( ( *𝑟 ‘ 𝐹 ) ‘ ( ( 𝐵 , 𝐴 ) ⨣ ( 𝐶 , 𝐴 ) ) ) = ( ( ( *𝑟 ‘ 𝐹 ) ‘ ( 𝐵 , 𝐴 ) ) ⨣ ( ( *𝑟 ‘ 𝐹 ) ‘ ( 𝐶 , 𝐴 ) ) ) ) |
23 |
12 22
|
eqtrd |
⊢ ( ( 𝑊 ∈ PreHil ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → ( ( *𝑟 ‘ 𝐹 ) ‘ ( ( 𝐵 + 𝐶 ) , 𝐴 ) ) = ( ( ( *𝑟 ‘ 𝐹 ) ‘ ( 𝐵 , 𝐴 ) ) ⨣ ( ( *𝑟 ‘ 𝐹 ) ‘ ( 𝐶 , 𝐴 ) ) ) ) |
24 |
|
phllmod |
⊢ ( 𝑊 ∈ PreHil → 𝑊 ∈ LMod ) |
25 |
24
|
adantr |
⊢ ( ( 𝑊 ∈ PreHil ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → 𝑊 ∈ LMod ) |
26 |
3 4
|
lmodvacl |
⊢ ( ( 𝑊 ∈ LMod ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) → ( 𝐵 + 𝐶 ) ∈ 𝑉 ) |
27 |
25 7 8 26
|
syl3anc |
⊢ ( ( 𝑊 ∈ PreHil ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → ( 𝐵 + 𝐶 ) ∈ 𝑉 ) |
28 |
1 2 3 20
|
ipcj |
⊢ ( ( 𝑊 ∈ PreHil ∧ ( 𝐵 + 𝐶 ) ∈ 𝑉 ∧ 𝐴 ∈ 𝑉 ) → ( ( *𝑟 ‘ 𝐹 ) ‘ ( ( 𝐵 + 𝐶 ) , 𝐴 ) ) = ( 𝐴 , ( 𝐵 + 𝐶 ) ) ) |
29 |
6 27 9 28
|
syl3anc |
⊢ ( ( 𝑊 ∈ PreHil ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → ( ( *𝑟 ‘ 𝐹 ) ‘ ( ( 𝐵 + 𝐶 ) , 𝐴 ) ) = ( 𝐴 , ( 𝐵 + 𝐶 ) ) ) |
30 |
1 2 3 20
|
ipcj |
⊢ ( ( 𝑊 ∈ PreHil ∧ 𝐵 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉 ) → ( ( *𝑟 ‘ 𝐹 ) ‘ ( 𝐵 , 𝐴 ) ) = ( 𝐴 , 𝐵 ) ) |
31 |
6 7 9 30
|
syl3anc |
⊢ ( ( 𝑊 ∈ PreHil ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → ( ( *𝑟 ‘ 𝐹 ) ‘ ( 𝐵 , 𝐴 ) ) = ( 𝐴 , 𝐵 ) ) |
32 |
1 2 3 20
|
ipcj |
⊢ ( ( 𝑊 ∈ PreHil ∧ 𝐶 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉 ) → ( ( *𝑟 ‘ 𝐹 ) ‘ ( 𝐶 , 𝐴 ) ) = ( 𝐴 , 𝐶 ) ) |
33 |
6 8 9 32
|
syl3anc |
⊢ ( ( 𝑊 ∈ PreHil ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → ( ( *𝑟 ‘ 𝐹 ) ‘ ( 𝐶 , 𝐴 ) ) = ( 𝐴 , 𝐶 ) ) |
34 |
31 33
|
oveq12d |
⊢ ( ( 𝑊 ∈ PreHil ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → ( ( ( *𝑟 ‘ 𝐹 ) ‘ ( 𝐵 , 𝐴 ) ) ⨣ ( ( *𝑟 ‘ 𝐹 ) ‘ ( 𝐶 , 𝐴 ) ) ) = ( ( 𝐴 , 𝐵 ) ⨣ ( 𝐴 , 𝐶 ) ) ) |
35 |
23 29 34
|
3eqtr3d |
⊢ ( ( 𝑊 ∈ PreHil ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → ( 𝐴 , ( 𝐵 + 𝐶 ) ) = ( ( 𝐴 , 𝐵 ) ⨣ ( 𝐴 , 𝐶 ) ) ) |