# 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}=\mathrm{Scalar}\left({W}\right)$
phllmhm.h
phllmhm.v ${⊢}{V}={\mathrm{Base}}_{{W}}$
ipsubdir.m
ipsubdir.s ${⊢}{S}={-}_{{F}}$
Assertion ipsubdi

### Proof

Step Hyp Ref Expression
1 phlsrng.f ${⊢}{F}=\mathrm{Scalar}\left({W}\right)$
2 phllmhm.h
3 phllmhm.v ${⊢}{V}={\mathrm{Base}}_{{W}}$
4 ipsubdir.m
5 ipsubdir.s ${⊢}{S}={-}_{{F}}$
6 simpl ${⊢}\left({W}\in \mathrm{PreHil}\wedge \left({A}\in {V}\wedge {B}\in {V}\wedge {C}\in {V}\right)\right)\to {W}\in \mathrm{PreHil}$
7 simpr1 ${⊢}\left({W}\in \mathrm{PreHil}\wedge \left({A}\in {V}\wedge {B}\in {V}\wedge {C}\in {V}\right)\right)\to {A}\in {V}$
8 phllmod ${⊢}{W}\in \mathrm{PreHil}\to {W}\in \mathrm{LMod}$
9 8 adantr ${⊢}\left({W}\in \mathrm{PreHil}\wedge \left({A}\in {V}\wedge {B}\in {V}\wedge {C}\in {V}\right)\right)\to {W}\in \mathrm{LMod}$
10 lmodgrp ${⊢}{W}\in \mathrm{LMod}\to {W}\in \mathrm{Grp}$
11 9 10 syl ${⊢}\left({W}\in \mathrm{PreHil}\wedge \left({A}\in {V}\wedge {B}\in {V}\wedge {C}\in {V}\right)\right)\to {W}\in \mathrm{Grp}$
12 simpr2 ${⊢}\left({W}\in \mathrm{PreHil}\wedge \left({A}\in {V}\wedge {B}\in {V}\wedge {C}\in {V}\right)\right)\to {B}\in {V}$
13 simpr3 ${⊢}\left({W}\in \mathrm{PreHil}\wedge \left({A}\in {V}\wedge {B}\in {V}\wedge {C}\in {V}\right)\right)\to {C}\in {V}$
14 3 4 grpsubcl
15 11 12 13 14 syl3anc
16 eqid ${⊢}{+}_{{W}}={+}_{{W}}$
17 eqid ${⊢}{+}_{{F}}={+}_{{F}}$
18 1 2 3 16 17 ipdi
19 6 7 15 13 18 syl13anc
20 3 16 4 grpnpcan
21 11 12 13 20 syl3anc
22 21 oveq2d
23 19 22 eqtr3d
24 1 lmodfgrp ${⊢}{W}\in \mathrm{LMod}\to {F}\in \mathrm{Grp}$
25 9 24 syl ${⊢}\left({W}\in \mathrm{PreHil}\wedge \left({A}\in {V}\wedge {B}\in {V}\wedge {C}\in {V}\right)\right)\to {F}\in \mathrm{Grp}$
26 eqid ${⊢}{\mathrm{Base}}_{{F}}={\mathrm{Base}}_{{F}}$
27 1 2 3 26 ipcl
28 6 7 12 27 syl3anc
29 1 2 3 26 ipcl
30 6 7 13 29 syl3anc
31 1 2 3 26 ipcl
32 6 7 15 31 syl3anc