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	$⊢ \underset{˙}{,} = \cdot_{𝑖} (W)$
	phllmhm.v	$⊢ V = {Base}_{W}$
	ipsubdir.m	$⊢ \underset{˙}{-} = -_{W}$
	ipsubdir.s	$⊢ S = -_{F}$
Assertion	ipsubdi	$⊢ (W \in PreHil \land (A \in V \land B \in V \land C \in V)) \to A \underset{˙}{,} (B \underset{˙}{-} C) = (A \underset{˙}{,} B) S (A \underset{˙}{,} C)$

Proof

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

Metamath Proof Explorer

Theorem ipsubdi

Proof