Metamath Proof Explorer


Theorem ipsubdi

Description: Distributive law for inner product subtraction. (Contributed by NM, 20-Nov-2007) (Revised by Mario Carneiro, 7-Oct-2015)

Ref Expression
Hypotheses phlsrng.f 𝐹 = ( Scalar ‘ 𝑊 )
phllmhm.h , = ( ·𝑖𝑊 )
phllmhm.v 𝑉 = ( Base ‘ 𝑊 )
ipsubdir.m = ( -g𝑊 )
ipsubdir.s 𝑆 = ( -g𝐹 )
Assertion ipsubdi ( ( 𝑊 ∈ PreHil ∧ ( 𝐴𝑉𝐵𝑉𝐶𝑉 ) ) → ( 𝐴 , ( 𝐵 𝐶 ) ) = ( ( 𝐴 , 𝐵 ) 𝑆 ( 𝐴 , 𝐶 ) ) )

Proof

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 ∧ ( 𝐴𝑉𝐵𝑉𝐶𝑉 ) ) → ( 𝐴 , ( 𝐵 𝐶 ) ) = ( ( 𝐴 , 𝐵 ) 𝑆 ( 𝐴 , 𝐶 ) ) )