baerlem5amN

Description: An equality that holds when X , Y , Z are independent (non-colinear) vectors. Subtraction version of first equation of part (5) in Baer p. 46. TODO: This is the subtraction version, may not be needed. TODO: delete if baerlem5abmN is used. (Contributed by NM, 24-May-2015) (New usage is discouraged.)

	Ref	Expression
Hypotheses	baerlem3.v	$⊢ V = {Base}_{W}$
	baerlem3.m	$⊢ \underset{˙}{-} = -_{W}$
	baerlem3.o	$⊢ \underset{˙}{0} = 0_{W}$
	baerlem3.s	$⊢ \underset{˙}{\oplus} = LSSum (W)$
	baerlem3.n	$⊢ N = LSpan (W)$
	baerlem3.w	$⊢ φ \to W \in LVec$
	baerlem3.x	$⊢ φ \to X \in V$
	baerlem3.c	$⊢ φ \to \neg X \in N (\{Y, Z\})$
	baerlem3.d	$⊢ φ \to N (\{Y\}) \neq N (\{Z\})$
	baerlem3.y	$⊢ φ \to Y \in (V ∖ \{\underset{˙}{0}\})$
	baerlem3.z	$⊢ φ \to Z \in (V ∖ \{\underset{˙}{0}\})$
	baerlem5a.p	$⊢ \underset{˙}{+} = +_{W}$
Assertion	baerlem5amN	$⊢ φ \to N (\{X \underset{˙}{-} (Y \underset{˙}{-} Z)\}) = (N (\{X \underset{˙}{-} Y\}) \underset{˙}{\oplus} N (\{Z\})) \cap (N (\{X \underset{˙}{+} Z\}) \underset{˙}{\oplus} N (\{Y\}))$

Proof

Step	Hyp	Ref	Expression
1		baerlem3.v	$⊢ V = {Base}_{W}$
2		baerlem3.m	$⊢ \underset{˙}{-} = -_{W}$
3		baerlem3.o	$⊢ \underset{˙}{0} = 0_{W}$
4		baerlem3.s	$⊢ \underset{˙}{\oplus} = LSSum (W)$
5		baerlem3.n	$⊢ N = LSpan (W)$
6		baerlem3.w	$⊢ φ \to W \in LVec$
7		baerlem3.x	$⊢ φ \to X \in V$
8		baerlem3.c	$⊢ φ \to \neg X \in N (\{Y, Z\})$
9		baerlem3.d	$⊢ φ \to N (\{Y\}) \neq N (\{Z\})$
10		baerlem3.y	$⊢ φ \to Y \in (V ∖ \{\underset{˙}{0}\})$
11		baerlem3.z	$⊢ φ \to Z \in (V ∖ \{\underset{˙}{0}\})$
12		baerlem5a.p	$⊢ \underset{˙}{+} = +_{W}$
13	10	eldifad	$⊢ φ \to Y \in V$
14	11	eldifad	$⊢ φ \to Z \in V$
15		eqid	$⊢ {inv}_{g} (W) = {inv}_{g} (W)$
16	1 12 15 2	grpsubval	$⊢ (Y \in V \land Z \in V) \to Y \underset{˙}{-} Z = Y \underset{˙}{+} {inv}_{g} (W) (Z)$
17	13 14 16	syl2anc	$⊢ φ \to Y \underset{˙}{-} Z = Y \underset{˙}{+} {inv}_{g} (W) (Z)$
18	17	oveq2d	$⊢ φ \to X \underset{˙}{-} (Y \underset{˙}{-} Z) = X \underset{˙}{-} (Y \underset{˙}{+} {inv}_{g} (W) (Z))$
19	18	sneqd	$⊢ φ \to \{X \underset{˙}{-} (Y \underset{˙}{-} Z)\} = \{X \underset{˙}{-} (Y \underset{˙}{+} {inv}_{g} (W) (Z))\}$
20	19	fveq2d	$⊢ φ \to N (\{X \underset{˙}{-} (Y \underset{˙}{-} Z)\}) = N (\{X \underset{˙}{-} (Y \underset{˙}{+} {inv}_{g} (W) (Z))\})$
21		lveclmod	$⊢ W \in LVec \to W \in LMod$
22	6 21	syl	$⊢ φ \to W \in LMod$
23	1 15	lmodvnegcl	$⊢ (W \in LMod \land Z \in V) \to {inv}_{g} (W) (Z) \in V$
24	22 14 23	syl2anc	$⊢ φ \to {inv}_{g} (W) (Z) \in V$
25		eqid	$⊢ LSubSp (W) = LSubSp (W)$
26	1 25 5 22 13 14	lspprcl	$⊢ φ \to N (\{Y, Z\}) \in LSubSp (W)$
27	3 25 22 26 7 8	lssneln0	$⊢ φ \to X \in (V ∖ \{\underset{˙}{0}\})$
28	1 5 6 7 13 14 8	lspindpi	$⊢ φ \to (N (\{X\}) \neq N (\{Y\}) \land N (\{X\}) \neq N (\{Z\}))$
29	28	simpld	$⊢ φ \to N (\{X\}) \neq N (\{Y\})$
30	1 3 5 6 27 13 29	lspsnne1	$⊢ φ \to \neg X \in N (\{Y\})$
31	9	necomd	$⊢ φ \to N (\{Z\}) \neq N (\{Y\})$
32	1 3 5 6 11 13 31	lspsnne1	$⊢ φ \to \neg Z \in N (\{Y\})$
33	1 5 6 7 14 13 32 8	lspexchn2	$⊢ φ \to \neg Z \in N (\{Y, X\})$
34		lmodgrp	$⊢ W \in LMod \to W \in Grp$
35	6 21 34	3syl	$⊢ φ \to W \in Grp$
36	35	adantr	$⊢ (φ \land {inv}_{g} (W) (Z) \in N (\{Y, X\})) \to W \in Grp$
37	14	adantr	$⊢ (φ \land {inv}_{g} (W) (Z) \in N (\{Y, X\})) \to Z \in V$
38	1 15	grpinvinv	$⊢ (W \in Grp \land Z \in V) \to {inv}_{g} (W) ({inv}_{g} (W) (Z)) = Z$
39	36 37 38	syl2anc	$⊢ (φ \land {inv}_{g} (W) (Z) \in N (\{Y, X\})) \to {inv}_{g} (W) ({inv}_{g} (W) (Z)) = Z$
40	22	adantr	$⊢ (φ \land {inv}_{g} (W) (Z) \in N (\{Y, X\})) \to W \in LMod$
41	1 25 5 22 13 7	lspprcl	$⊢ φ \to N (\{Y, X\}) \in LSubSp (W)$
42	41	adantr	$⊢ (φ \land {inv}_{g} (W) (Z) \in N (\{Y, X\})) \to N (\{Y, X\}) \in LSubSp (W)$
43		simpr	$⊢ (φ \land {inv}_{g} (W) (Z) \in N (\{Y, X\})) \to {inv}_{g} (W) (Z) \in N (\{Y, X\})$
44	25 15	lssvnegcl	$⊢ (W \in LMod \land N (\{Y, X\}) \in LSubSp (W) \land {inv}_{g} (W) (Z) \in N (\{Y, X\})) \to {inv}_{g} (W) ({inv}_{g} (W) (Z)) \in N (\{Y, X\})$
45	40 42 43 44	syl3anc	$⊢ (φ \land {inv}_{g} (W) (Z) \in N (\{Y, X\})) \to {inv}_{g} (W) ({inv}_{g} (W) (Z)) \in N (\{Y, X\})$
46	39 45	eqeltrrd	$⊢ (φ \land {inv}_{g} (W) (Z) \in N (\{Y, X\})) \to Z \in N (\{Y, X\})$
47	33 46	mtand	$⊢ φ \to \neg {inv}_{g} (W) (Z) \in N (\{Y, X\})$
48	1 5 6 24 7 13 30 47	lspexchn2	$⊢ φ \to \neg X \in N (\{Y, {inv}_{g} (W) (Z)\})$
49	1 15 5	lspsnneg	$⊢ (W \in LMod \land Z \in V) \to N (\{{inv}_{g} (W) (Z)\}) = N (\{Z\})$
50	22 14 49	syl2anc	$⊢ φ \to N (\{{inv}_{g} (W) (Z)\}) = N (\{Z\})$
51	9 50	neeqtrrd	$⊢ φ \to N (\{Y\}) \neq N (\{{inv}_{g} (W) (Z)\})$
52	1 3 15	grpinvnzcl	$⊢ (W \in Grp \land Z \in (V ∖ \{\underset{˙}{0}\})) \to {inv}_{g} (W) (Z) \in (V ∖ \{\underset{˙}{0}\})$
53	35 11 52	syl2anc	$⊢ φ \to {inv}_{g} (W) (Z) \in (V ∖ \{\underset{˙}{0}\})$
54	1 2 3 4 5 6 7 48 51 10 53 12	baerlem5a	$⊢ φ \to N (\{X \underset{˙}{-} (Y \underset{˙}{+} {inv}_{g} (W) (Z))\}) = (N (\{X \underset{˙}{-} Y\}) \underset{˙}{\oplus} N (\{{inv}_{g} (W) (Z)\})) \cap (N (\{X \underset{˙}{-} {inv}_{g} (W) (Z)\}) \underset{˙}{\oplus} N (\{Y\}))$
55	50	oveq2d	$⊢ φ \to N (\{X \underset{˙}{-} Y\}) \underset{˙}{\oplus} N (\{{inv}_{g} (W) (Z)\}) = N (\{X \underset{˙}{-} Y\}) \underset{˙}{\oplus} N (\{Z\})$
56	1 12 2 15 35 7 14	grpsubinv	$⊢ φ \to X \underset{˙}{-} {inv}_{g} (W) (Z) = X \underset{˙}{+} Z$
57	56	sneqd	$⊢ φ \to \{X \underset{˙}{-} {inv}_{g} (W) (Z)\} = \{X \underset{˙}{+} Z\}$
58	57	fveq2d	$⊢ φ \to N (\{X \underset{˙}{-} {inv}_{g} (W) (Z)\}) = N (\{X \underset{˙}{+} Z\})$
59	58	oveq1d	$⊢ φ \to N (\{X \underset{˙}{-} {inv}_{g} (W) (Z)\}) \underset{˙}{\oplus} N (\{Y\}) = N (\{X \underset{˙}{+} Z\}) \underset{˙}{\oplus} N (\{Y\})$
60	55 59	ineq12d	$⊢ φ \to (N (\{X \underset{˙}{-} Y\}) \underset{˙}{\oplus} N (\{{inv}_{g} (W) (Z)\})) \cap (N (\{X \underset{˙}{-} {inv}_{g} (W) (Z)\}) \underset{˙}{\oplus} N (\{Y\})) = (N (\{X \underset{˙}{-} Y\}) \underset{˙}{\oplus} N (\{Z\})) \cap (N (\{X \underset{˙}{+} Z\}) \underset{˙}{\oplus} N (\{Y\}))$
61	20 54 60	3eqtrd	$⊢ φ \to N (\{X \underset{˙}{-} (Y \underset{˙}{-} Z)\}) = (N (\{X \underset{˙}{-} Y\}) \underset{˙}{\oplus} N (\{Z\})) \cap (N (\{X \underset{˙}{+} Z\}) \underset{˙}{\oplus} N (\{Y\}))$

Metamath Proof Explorer

Theorem baerlem5amN

Proof