# Metamath Proof Explorer

## Theorem ipsubdir

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 ipsubdir

### 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 phllmod ${⊢}{W}\in \mathrm{PreHil}\to {W}\in \mathrm{LMod}$
8 7 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}$
9 lmodgrp ${⊢}{W}\in \mathrm{LMod}\to {W}\in \mathrm{Grp}$
10 8 9 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}$
11 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}$
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 3 4 grpsubcl
14 10 11 12 13 syl3anc
15 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}$
16 eqid ${⊢}{+}_{{W}}={+}_{{W}}$
17 eqid ${⊢}{+}_{{F}}={+}_{{F}}$
18 1 2 3 16 17 ipdir
19 6 14 12 15 18 syl13anc
20 3 16 4 grpnpcan
21 10 11 12 20 syl3anc
22 21 oveq1d
23 19 22 eqtr3d
24 1 lmodfgrp ${⊢}{W}\in \mathrm{LMod}\to {F}\in \mathrm{Grp}$
25 8 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 11 15 27 syl3anc
29 1 2 3 26 ipcl
30 6 12 15 29 syl3anc
31 1 2 3 26 ipcl
32 6 14 15 31 syl3anc