# Metamath Proof Explorer

## Theorem ip2subdi

Description: Distributive law for inner product subtraction. (Contributed by Mario Carneiro, 8-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}}$
ip2subdi.p
ip2subdi.1 ${⊢}{\phi }\to {W}\in \mathrm{PreHil}$
ip2subdi.2 ${⊢}{\phi }\to {A}\in {V}$
ip2subdi.3 ${⊢}{\phi }\to {B}\in {V}$
ip2subdi.4 ${⊢}{\phi }\to {C}\in {V}$
ip2subdi.5 ${⊢}{\phi }\to {D}\in {V}$
Assertion ip2subdi

### 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 ip2subdi.p
7 ip2subdi.1 ${⊢}{\phi }\to {W}\in \mathrm{PreHil}$
8 ip2subdi.2 ${⊢}{\phi }\to {A}\in {V}$
9 ip2subdi.3 ${⊢}{\phi }\to {B}\in {V}$
10 ip2subdi.4 ${⊢}{\phi }\to {C}\in {V}$
11 ip2subdi.5 ${⊢}{\phi }\to {D}\in {V}$
12 eqid ${⊢}{\mathrm{Base}}_{{F}}={\mathrm{Base}}_{{F}}$
13 phllmod ${⊢}{W}\in \mathrm{PreHil}\to {W}\in \mathrm{LMod}$
14 7 13 syl ${⊢}{\phi }\to {W}\in \mathrm{LMod}$
15 1 lmodring ${⊢}{W}\in \mathrm{LMod}\to {F}\in \mathrm{Ring}$
16 14 15 syl ${⊢}{\phi }\to {F}\in \mathrm{Ring}$
17 ringabl ${⊢}{F}\in \mathrm{Ring}\to {F}\in \mathrm{Abel}$
18 16 17 syl ${⊢}{\phi }\to {F}\in \mathrm{Abel}$
19 1 2 3 12 ipcl
20 7 8 10 19 syl3anc
21 1 2 3 12 ipcl
22 7 8 11 21 syl3anc
23 1 2 3 12 ipcl
24 7 9 10 23 syl3anc
25 12 6 5 18 20 22 24 ablsubsub4
26 25 oveq1d
27 3 4 lmodvsubcl
28 14 10 11 27 syl3anc
29 1 2 3 4 5 ipsubdir
30 7 8 9 28 29 syl13anc
31 1 2 3 4 5 ipsubdi
32 7 8 10 11 31 syl13anc
33 1 2 3 4 5 ipsubdi
34 7 9 10 11 33 syl13anc
35 32 34 oveq12d
36 ringgrp ${⊢}{F}\in \mathrm{Ring}\to {F}\in \mathrm{Grp}$
37 16 36 syl ${⊢}{\phi }\to {F}\in \mathrm{Grp}$
38 12 5 grpsubcl
39 37 20 22 38 syl3anc
40 1 2 3 12 ipcl
41 7 9 11 40 syl3anc
42 12 6 5 18 39 24 41 ablsubsub
43 30 35 42 3eqtrd
44 12 6 ringacl
45 16 22 24 44 syl3anc