ip2subdi

Description: Distributive law for inner product subtraction. (Contributed by Mario Carneiro, 8-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}$
	ip2subdi.p	$⊢ \underset{˙}{+} = +_{F}$
	ip2subdi.1	$⊢ φ \to W \in PreHil$
	ip2subdi.2	$⊢ φ \to A \in V$
	ip2subdi.3	$⊢ φ \to B \in V$
	ip2subdi.4	$⊢ φ \to C \in V$
	ip2subdi.5	$⊢ φ \to D \in V$
Assertion	ip2subdi	$⊢ φ \to (A \underset{˙}{-} B) \underset{˙}{,} (C \underset{˙}{-} D) = ((A \underset{˙}{,} C) \underset{˙}{+} (B \underset{˙}{,} D)) S ((A \underset{˙}{,} D) \underset{˙}{+} (B \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		ip2subdi.p	$⊢ \underset{˙}{+} = +_{F}$
7		ip2subdi.1	$⊢ φ \to W \in PreHil$
8		ip2subdi.2	$⊢ φ \to A \in V$
9		ip2subdi.3	$⊢ φ \to B \in V$
10		ip2subdi.4	$⊢ φ \to C \in V$
11		ip2subdi.5	$⊢ φ \to D \in V$
12		eqid	$⊢ {Base}_{F} = {Base}_{F}$
13		phllmod	$⊢ W \in PreHil \to W \in LMod$
14	7 13	syl	$⊢ φ \to W \in LMod$
15	1	lmodring	$⊢ W \in LMod \to F \in Ring$
16	14 15	syl	$⊢ φ \to F \in Ring$
17		ringabl	$⊢ F \in Ring \to F \in Abel$
18	16 17	syl	$⊢ φ \to F \in Abel$
19	1 2 3 12	ipcl	$⊢ (W \in PreHil \land A \in V \land C \in V) \to A \underset{˙}{,} C \in {Base}_{F}$
20	7 8 10 19	syl3anc	$⊢ φ \to A \underset{˙}{,} C \in {Base}_{F}$
21	1 2 3 12	ipcl	$⊢ (W \in PreHil \land A \in V \land D \in V) \to A \underset{˙}{,} D \in {Base}_{F}$
22	7 8 11 21	syl3anc	$⊢ φ \to A \underset{˙}{,} D \in {Base}_{F}$
23	1 2 3 12	ipcl	$⊢ (W \in PreHil \land B \in V \land C \in V) \to B \underset{˙}{,} C \in {Base}_{F}$
24	7 9 10 23	syl3anc	$⊢ φ \to B \underset{˙}{,} C \in {Base}_{F}$
25	12 6 5 18 20 22 24	ablsubsub4	$⊢ φ \to ((A \underset{˙}{,} C) S (A \underset{˙}{,} D)) S (B \underset{˙}{,} C) = (A \underset{˙}{,} C) S ((A \underset{˙}{,} D) \underset{˙}{+} (B \underset{˙}{,} C))$
26	25	oveq1d	$⊢ φ \to (((A \underset{˙}{,} C) S (A \underset{˙}{,} D)) S (B \underset{˙}{,} C)) \underset{˙}{+} (B \underset{˙}{,} D) = ((A \underset{˙}{,} C) S ((A \underset{˙}{,} D) \underset{˙}{+} (B \underset{˙}{,} C))) \underset{˙}{+} (B \underset{˙}{,} D)$
27	3 4	lmodvsubcl	$⊢ (W \in LMod \land C \in V \land D \in V) \to C \underset{˙}{-} D \in V$
28	14 10 11 27	syl3anc	$⊢ φ \to C \underset{˙}{-} D \in V$
29	1 2 3 4 5	ipsubdir	$⊢ (W \in PreHil \land (A \in V \land B \in V \land C \underset{˙}{-} D \in V)) \to (A \underset{˙}{-} B) \underset{˙}{,} (C \underset{˙}{-} D) = (A \underset{˙}{,} (C \underset{˙}{-} D)) S (B \underset{˙}{,} (C \underset{˙}{-} D))$
30	7 8 9 28 29	syl13anc	$⊢ φ \to (A \underset{˙}{-} B) \underset{˙}{,} (C \underset{˙}{-} D) = (A \underset{˙}{,} (C \underset{˙}{-} D)) S (B \underset{˙}{,} (C \underset{˙}{-} D))$
31	1 2 3 4 5	ipsubdi	$⊢ (W \in PreHil \land (A \in V \land C \in V \land D \in V)) \to A \underset{˙}{,} (C \underset{˙}{-} D) = (A \underset{˙}{,} C) S (A \underset{˙}{,} D)$
32	7 8 10 11 31	syl13anc	$⊢ φ \to A \underset{˙}{,} (C \underset{˙}{-} D) = (A \underset{˙}{,} C) S (A \underset{˙}{,} D)$
33	1 2 3 4 5	ipsubdi	$⊢ (W \in PreHil \land (B \in V \land C \in V \land D \in V)) \to B \underset{˙}{,} (C \underset{˙}{-} D) = (B \underset{˙}{,} C) S (B \underset{˙}{,} D)$
34	7 9 10 11 33	syl13anc	$⊢ φ \to B \underset{˙}{,} (C \underset{˙}{-} D) = (B \underset{˙}{,} C) S (B \underset{˙}{,} D)$
35	32 34	oveq12d	$⊢ φ \to (A \underset{˙}{,} (C \underset{˙}{-} D)) S (B \underset{˙}{,} (C \underset{˙}{-} D)) = ((A \underset{˙}{,} C) S (A \underset{˙}{,} D)) S ((B \underset{˙}{,} C) S (B \underset{˙}{,} D))$
36		ringgrp	$⊢ F \in Ring \to F \in Grp$
37	16 36	syl	$⊢ φ \to F \in Grp$
38	12 5	grpsubcl	$⊢ (F \in Grp \land A \underset{˙}{,} C \in {Base}_{F} \land A \underset{˙}{,} D \in {Base}_{F}) \to (A \underset{˙}{,} C) S (A \underset{˙}{,} D) \in {Base}_{F}$
39	37 20 22 38	syl3anc	$⊢ φ \to (A \underset{˙}{,} C) S (A \underset{˙}{,} D) \in {Base}_{F}$
40	1 2 3 12	ipcl	$⊢ (W \in PreHil \land B \in V \land D \in V) \to B \underset{˙}{,} D \in {Base}_{F}$
41	7 9 11 40	syl3anc	$⊢ φ \to B \underset{˙}{,} D \in {Base}_{F}$
42	12 6 5 18 39 24 41	ablsubsub	$⊢ φ \to ((A \underset{˙}{,} C) S (A \underset{˙}{,} D)) S ((B \underset{˙}{,} C) S (B \underset{˙}{,} D)) = (((A \underset{˙}{,} C) S (A \underset{˙}{,} D)) S (B \underset{˙}{,} C)) \underset{˙}{+} (B \underset{˙}{,} D)$
43	30 35 42	3eqtrd	$⊢ φ \to (A \underset{˙}{-} B) \underset{˙}{,} (C \underset{˙}{-} D) = (((A \underset{˙}{,} C) S (A \underset{˙}{,} D)) S (B \underset{˙}{,} C)) \underset{˙}{+} (B \underset{˙}{,} D)$
44	12 6	ringacl	$⊢ (F \in Ring \land A \underset{˙}{,} D \in {Base}_{F} \land B \underset{˙}{,} C \in {Base}_{F}) \to (A \underset{˙}{,} D) \underset{˙}{+} (B \underset{˙}{,} C) \in {Base}_{F}$
45	16 22 24 44	syl3anc	$⊢ φ \to (A \underset{˙}{,} D) \underset{˙}{+} (B \underset{˙}{,} C) \in {Base}_{F}$
46	12 6 5	abladdsub	$⊢ (F \in Abel \land (A \underset{˙}{,} C \in {Base}_{F} \land B \underset{˙}{,} D \in {Base}_{F} \land (A \underset{˙}{,} D) \underset{˙}{+} (B \underset{˙}{,} C) \in {Base}_{F})) \to ((A \underset{˙}{,} C) \underset{˙}{+} (B \underset{˙}{,} D)) S ((A \underset{˙}{,} D) \underset{˙}{+} (B \underset{˙}{,} C)) = ((A \underset{˙}{,} C) S ((A \underset{˙}{,} D) \underset{˙}{+} (B \underset{˙}{,} C))) \underset{˙}{+} (B \underset{˙}{,} D)$
47	18 20 41 45 46	syl13anc	$⊢ φ \to ((A \underset{˙}{,} C) \underset{˙}{+} (B \underset{˙}{,} D)) S ((A \underset{˙}{,} D) \underset{˙}{+} (B \underset{˙}{,} C)) = ((A \underset{˙}{,} C) S ((A \underset{˙}{,} D) \underset{˙}{+} (B \underset{˙}{,} C))) \underset{˙}{+} (B \underset{˙}{,} D)$
48	26 43 47	3eqtr4d	$⊢ φ \to (A \underset{˙}{-} B) \underset{˙}{,} (C \underset{˙}{-} D) = ((A \underset{˙}{,} C) \underset{˙}{+} (B \underset{˙}{,} D)) S ((A \underset{˙}{,} D) \underset{˙}{+} (B \underset{˙}{,} C))$

Metamath Proof Explorer

Theorem ip2subdi

Proof