baerlem5bmN

Description: An equality that holds when X , Y , Z are independent (non-colinear) vectors. Subtraction version of second 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	baerlem5bmN	$⊢ φ \to N (\{Y \underset{˙}{-} Z\}) = (N (\{Y\}) \underset{˙}{\oplus} N (\{Z\})) \cap (N (\{X \underset{˙}{-} (Y \underset{˙}{-} Z)\}) \underset{˙}{\oplus} N (\{X\}))$

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	sneqd	$⊢ φ \to \{Y \underset{˙}{-} Z\} = \{Y \underset{˙}{+} {inv}_{g} (W) (Z)\}$
19	18	fveq2d	$⊢ φ \to N (\{Y \underset{˙}{-} Z\}) = N (\{Y \underset{˙}{+} {inv}_{g} (W) (Z)\})$
20		lveclmod	$⊢ W \in LVec \to W \in LMod$
21	6 20	syl	$⊢ φ \to W \in LMod$
22	1 15	lmodvnegcl	$⊢ (W \in LMod \land Z \in V) \to {inv}_{g} (W) (Z) \in V$
23	21 14 22	syl2anc	$⊢ φ \to {inv}_{g} (W) (Z) \in V$
24		eqid	$⊢ LSubSp (W) = LSubSp (W)$
25	1 24 5 21 13 14	lspprcl	$⊢ φ \to N (\{Y, Z\}) \in LSubSp (W)$
26	3 24 21 25 7 8	lssneln0	$⊢ φ \to X \in (V ∖ \{\underset{˙}{0}\})$
27	1 5 6 7 13 14 8	lspindpi	$⊢ φ \to (N (\{X\}) \neq N (\{Y\}) \land N (\{X\}) \neq N (\{Z\}))$
28	27	simpld	$⊢ φ \to N (\{X\}) \neq N (\{Y\})$
29	1 3 5 6 26 13 28	lspsnne1	$⊢ φ \to \neg X \in N (\{Y\})$
30	9	necomd	$⊢ φ \to N (\{Z\}) \neq N (\{Y\})$
31	1 3 5 6 11 13 30	lspsnne1	$⊢ φ \to \neg Z \in N (\{Y\})$
32	1 5 6 7 14 13 31 8	lspexchn2	$⊢ φ \to \neg Z \in N (\{Y, X\})$
33		lmodgrp	$⊢ W \in LMod \to W \in Grp$
34	21 33	syl	$⊢ φ \to W \in Grp$
35	34	adantr	$⊢ (φ \land {inv}_{g} (W) (Z) \in N (\{Y, X\})) \to W \in Grp$
36	14	adantr	$⊢ (φ \land {inv}_{g} (W) (Z) \in N (\{Y, X\})) \to Z \in V$
37	1 15	grpinvinv	$⊢ (W \in Grp \land Z \in V) \to {inv}_{g} (W) ({inv}_{g} (W) (Z)) = Z$
38	35 36 37	syl2anc	$⊢ (φ \land {inv}_{g} (W) (Z) \in N (\{Y, X\})) \to {inv}_{g} (W) ({inv}_{g} (W) (Z)) = Z$
39	21	adantr	$⊢ (φ \land {inv}_{g} (W) (Z) \in N (\{Y, X\})) \to W \in LMod$
40	1 24 5 21 13 7	lspprcl	$⊢ φ \to N (\{Y, X\}) \in LSubSp (W)$
41	40	adantr	$⊢ (φ \land {inv}_{g} (W) (Z) \in N (\{Y, X\})) \to N (\{Y, X\}) \in LSubSp (W)$
42		simpr	$⊢ (φ \land {inv}_{g} (W) (Z) \in N (\{Y, X\})) \to {inv}_{g} (W) (Z) \in N (\{Y, X\})$
43	24 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\})$
44	39 41 42 43	syl3anc	$⊢ (φ \land {inv}_{g} (W) (Z) \in N (\{Y, X\})) \to {inv}_{g} (W) ({inv}_{g} (W) (Z)) \in N (\{Y, X\})$
45	38 44	eqeltrrd	$⊢ (φ \land {inv}_{g} (W) (Z) \in N (\{Y, X\})) \to Z \in N (\{Y, X\})$
46	32 45	mtand	$⊢ φ \to \neg {inv}_{g} (W) (Z) \in N (\{Y, X\})$
47	1 5 6 23 7 13 29 46	lspexchn2	$⊢ φ \to \neg X \in N (\{Y, {inv}_{g} (W) (Z)\})$
48	1 15 5	lspsnneg	$⊢ (W \in LMod \land Z \in V) \to N (\{{inv}_{g} (W) (Z)\}) = N (\{Z\})$
49	21 14 48	syl2anc	$⊢ φ \to N (\{{inv}_{g} (W) (Z)\}) = N (\{Z\})$
50	9 49	neeqtrrd	$⊢ φ \to N (\{Y\}) \neq N (\{{inv}_{g} (W) (Z)\})$
51	1 3 15	grpinvnzcl	$⊢ (W \in Grp \land Z \in (V ∖ \{\underset{˙}{0}\})) \to {inv}_{g} (W) (Z) \in (V ∖ \{\underset{˙}{0}\})$
52	34 11 51	syl2anc	$⊢ φ \to {inv}_{g} (W) (Z) \in (V ∖ \{\underset{˙}{0}\})$
53	1 2 3 4 5 6 7 47 50 10 52 12	baerlem5b	$⊢ φ \to N (\{Y \underset{˙}{+} {inv}_{g} (W) (Z)\}) = (N (\{Y\}) \underset{˙}{\oplus} N (\{{inv}_{g} (W) (Z)\})) \cap (N (\{X \underset{˙}{-} (Y \underset{˙}{+} {inv}_{g} (W) (Z))\}) \underset{˙}{\oplus} N (\{X\}))$
54	49	oveq2d	$⊢ φ \to N (\{Y\}) \underset{˙}{\oplus} N (\{{inv}_{g} (W) (Z)\}) = N (\{Y\}) \underset{˙}{\oplus} N (\{Z\})$
55	17	eqcomd	$⊢ φ \to Y \underset{˙}{+} {inv}_{g} (W) (Z) = Y \underset{˙}{-} Z$
56	55	oveq2d	$⊢ φ \to X \underset{˙}{-} (Y \underset{˙}{+} {inv}_{g} (W) (Z)) = X \underset{˙}{-} (Y \underset{˙}{-} Z)$
57	56	sneqd	$⊢ φ \to \{X \underset{˙}{-} (Y \underset{˙}{+} {inv}_{g} (W) (Z))\} = \{X \underset{˙}{-} (Y \underset{˙}{-} Z)\}$
58	57	fveq2d	$⊢ φ \to N (\{X \underset{˙}{-} (Y \underset{˙}{+} {inv}_{g} (W) (Z))\}) = N (\{X \underset{˙}{-} (Y \underset{˙}{-} Z)\})$
59	58	oveq1d	$⊢ φ \to N (\{X \underset{˙}{-} (Y \underset{˙}{+} {inv}_{g} (W) (Z))\}) \underset{˙}{\oplus} N (\{X\}) = N (\{X \underset{˙}{-} (Y \underset{˙}{-} Z)\}) \underset{˙}{\oplus} N (\{X\})$
60	54 59	ineq12d	$⊢ φ \to (N (\{Y\}) \underset{˙}{\oplus} N (\{{inv}_{g} (W) (Z)\})) \cap (N (\{X \underset{˙}{-} (Y \underset{˙}{+} {inv}_{g} (W) (Z))\}) \underset{˙}{\oplus} N (\{X\})) = (N (\{Y\}) \underset{˙}{\oplus} N (\{Z\})) \cap (N (\{X \underset{˙}{-} (Y \underset{˙}{-} Z)\}) \underset{˙}{\oplus} N (\{X\}))$
61	19 53 60	3eqtrd	$⊢ φ \to N (\{Y \underset{˙}{-} Z\}) = (N (\{Y\}) \underset{˙}{\oplus} N (\{Z\})) \cap (N (\{X \underset{˙}{-} (Y \underset{˙}{-} Z)\}) \underset{˙}{\oplus} N (\{X\}))$

Metamath Proof Explorer

Theorem baerlem5bmN

Proof