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 ⊢ F = Scalar ⁡ W
phllmhm.h ⊢ , ˙ = ⋅ 𝑖 ⁡ W
phllmhm.v ⊢ V = Base W
ipsubdir.m ⊢ - ˙ = - W
ipsubdir.s ⊢ S = - F
Assertion ipsubdi ⊢ W ∈ PreHil ∧ A ∈ V ∧ B ∈ V ∧ C ∈ V → A , ˙ B - ˙ C = A , ˙ B S A , ˙ C

Proof

Step Hyp Ref Expression
1 phlsrng.f ⊢ F = Scalar ⁡ W
2 phllmhm.h ⊢ , ˙ = ⋅ 𝑖 ⁡ W
3 phllmhm.v ⊢ V = Base W
4 ipsubdir.m ⊢ - ˙ = - W
5 ipsubdir.s ⊢ S = - F
6 simpl ⊢ W ∈ PreHil ∧ A ∈ V ∧ B ∈ V ∧ C ∈ V → W ∈ PreHil
7 simpr1 ⊢ W ∈ PreHil ∧ A ∈ V ∧ B ∈ V ∧ C ∈ V → A ∈ V
8 phllmod ⊢ W ∈ PreHil → W ∈ LMod
9 8 adantr ⊢ W ∈ PreHil ∧ A ∈ V ∧ B ∈ V ∧ C ∈ V → W ∈ LMod
10 lmodgrp ⊢ W ∈ LMod → W ∈ Grp
11 9 10 syl ⊢ W ∈ PreHil ∧ A ∈ V ∧ B ∈ V ∧ C ∈ V → W ∈ Grp
12 simpr2 ⊢ W ∈ PreHil ∧ A ∈ V ∧ B ∈ V ∧ C ∈ V → B ∈ V
13 simpr3 ⊢ W ∈ PreHil ∧ A ∈ V ∧ B ∈ V ∧ C ∈ V → C ∈ V
14 3 4 grpsubcl ⊢ W ∈ Grp ∧ B ∈ V ∧ C ∈ V → B - ˙ C ∈ V
15 11 12 13 14 syl3anc ⊢ W ∈ PreHil ∧ A ∈ V ∧ B ∈ V ∧ C ∈ V → B - ˙ C ∈ V
16 eqid ⊢ + W = + W
17 eqid ⊢ + F = + F
18 1 2 3 16 17 ipdi ⊢ W ∈ PreHil ∧ A ∈ V ∧ B - ˙ C ∈ V ∧ C ∈ V → A , ˙ B - ˙ C + W C = A , ˙ B - ˙ C + F A , ˙ C
19 6 7 15 13 18 syl13anc ⊢ W ∈ PreHil ∧ A ∈ V ∧ B ∈ V ∧ C ∈ V → A , ˙ B - ˙ C + W C = A , ˙ B - ˙ C + F A , ˙ C
20 3 16 4 grpnpcan ⊢ W ∈ Grp ∧ B ∈ V ∧ C ∈ V → B - ˙ C + W C = B
21 11 12 13 20 syl3anc ⊢ W ∈ PreHil ∧ A ∈ V ∧ B ∈ V ∧ C ∈ V → B - ˙ C + W C = B
22 21 oveq2d ⊢ W ∈ PreHil ∧ A ∈ V ∧ B ∈ V ∧ C ∈ V → A , ˙ B - ˙ C + W C = A , ˙ B
23 19 22 eqtr3d ⊢ W ∈ PreHil ∧ A ∈ V ∧ B ∈ V ∧ C ∈ V → A , ˙ B - ˙ C + F A , ˙ C = A , ˙ B
24 1 lmodfgrp ⊢ W ∈ LMod → F ∈ Grp
25 9 24 syl ⊢ W ∈ PreHil ∧ A ∈ V ∧ B ∈ V ∧ C ∈ V → F ∈ Grp
26 eqid ⊢ Base F = Base F
27 1 2 3 26 ipcl ⊢ W ∈ PreHil ∧ A ∈ V ∧ B ∈ V → A , ˙ B ∈ Base F
28 6 7 12 27 syl3anc ⊢ W ∈ PreHil ∧ A ∈ V ∧ B ∈ V ∧ C ∈ V → A , ˙ B ∈ Base F
29 1 2 3 26 ipcl ⊢ W ∈ PreHil ∧ A ∈ V ∧ C ∈ V → A , ˙ C ∈ Base F
30 6 7 13 29 syl3anc ⊢ W ∈ PreHil ∧ A ∈ V ∧ B ∈ V ∧ C ∈ V → A , ˙ C ∈ Base F
31 1 2 3 26 ipcl ⊢ W ∈ PreHil ∧ A ∈ V ∧ B - ˙ C ∈ V → A , ˙ B - ˙ C ∈ Base F
32 6 7 15 31 syl3anc ⊢ W ∈ PreHil ∧ A ∈ V ∧ B ∈ V ∧ C ∈ V → A , ˙ B - ˙ C ∈ Base F
33 26 17 5 grpsubadd ⊢ F ∈ Grp ∧ A , ˙ B ∈ Base F ∧ A , ˙ C ∈ Base F ∧ A , ˙ B - ˙ C ∈ Base F → A , ˙ B S A , ˙ C = A , ˙ B - ˙ C ↔ A , ˙ B - ˙ C + F A , ˙ C = A , ˙ B
34 25 28 30 32 33 syl13anc ⊢ W ∈ PreHil ∧ A ∈ V ∧ B ∈ V ∧ C ∈ V → A , ˙ B S A , ˙ C = A , ˙ B - ˙ C ↔ A , ˙ B - ˙ C + F A , ˙ C = A , ˙ B
35 23 34 mpbird ⊢ W ∈ PreHil ∧ A ∈ V ∧ B ∈ V ∧ C ∈ V → A , ˙ B S A , ˙ C = A , ˙ B - ˙ C
36 35 eqcomd ⊢ W ∈ PreHil ∧ A ∈ V ∧ B ∈ V ∧ C ∈ V → A , ˙ B - ˙ C = A , ˙ B S A , ˙ C