baerlem5alem1

	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}\})$
	baerlem3.p	$⊢ \underset{˙}{+} = +_{W}$
	baerlem3.t	$⊢ \underset{˙}{\cdot} = \cdot_{W}$
	baerlem3.r	$⊢ R = Scalar (W)$
	baerlem3.b	$⊢ B = {Base}_{R}$
	baerlem3.a	$⊢ \underset{˙}{⨣} = +_{R}$
	baerlem3.l	$⊢ L = -_{R}$
	baerlem3.q	$⊢ Q = 0_{R}$
	baerlem3.i	$⊢ I = {inv}_{g} (R)$
	baerlem5a.a1	$⊢ φ \to a \in B$
	baerlem5a.b1	$⊢ φ \to b \in B$
	baerlem5a.d1	$⊢ φ \to d \in B$
	baerlem5a.e1	$⊢ φ \to e \in B$
	baerlem5a.j1	$⊢ φ \to j = (a \underset{˙}{\cdot} (X \underset{˙}{-} Y)) \underset{˙}{+} (b \underset{˙}{\cdot} Z)$
	baerlem5a.j2	$⊢ φ \to j = (d \underset{˙}{\cdot} (X \underset{˙}{-} Z)) \underset{˙}{+} (e \underset{˙}{\cdot} Y)$
Assertion	baerlem5alem1	$⊢ φ \to j = a \underset{˙}{\cdot} (X \underset{˙}{-} (Y \underset{˙}{+} Z))$

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		baerlem3.p	$⊢ \underset{˙}{+} = +_{W}$
13		baerlem3.t	$⊢ \underset{˙}{\cdot} = \cdot_{W}$
14		baerlem3.r	$⊢ R = Scalar (W)$
15		baerlem3.b	$⊢ B = {Base}_{R}$
16		baerlem3.a	$⊢ \underset{˙}{⨣} = +_{R}$
17		baerlem3.l	$⊢ L = -_{R}$
18		baerlem3.q	$⊢ Q = 0_{R}$
19		baerlem3.i	$⊢ I = {inv}_{g} (R)$
20		baerlem5a.a1	$⊢ φ \to a \in B$
21		baerlem5a.b1	$⊢ φ \to b \in B$
22		baerlem5a.d1	$⊢ φ \to d \in B$
23		baerlem5a.e1	$⊢ φ \to e \in B$
24		baerlem5a.j1	$⊢ φ \to j = (a \underset{˙}{\cdot} (X \underset{˙}{-} Y)) \underset{˙}{+} (b \underset{˙}{\cdot} Z)$
25		baerlem5a.j2	$⊢ φ \to j = (d \underset{˙}{\cdot} (X \underset{˙}{-} Z)) \underset{˙}{+} (e \underset{˙}{\cdot} Y)$
26		lveclmod	$⊢ W \in LVec \to W \in LMod$
27	6 26	syl	$⊢ φ \to W \in LMod$
28	10	eldifad	$⊢ φ \to Y \in V$
29	1 13 14 15 2 27 20 7 28	lmodsubdi	$⊢ φ \to a \underset{˙}{\cdot} (X \underset{˙}{-} Y) = (a \underset{˙}{\cdot} X) \underset{˙}{-} (a \underset{˙}{\cdot} Y)$
30	1 14 13 15	lmodvscl	$⊢ (W \in LMod \land a \in B \land X \in V) \to a \underset{˙}{\cdot} X \in V$
31	27 20 7 30	syl3anc	$⊢ φ \to a \underset{˙}{\cdot} X \in V$
32	1 12 2 13 14 15 19 27 20 31 28	lmodsubvs	$⊢ φ \to (a \underset{˙}{\cdot} X) \underset{˙}{-} (a \underset{˙}{\cdot} Y) = (a \underset{˙}{\cdot} X) \underset{˙}{+} (I (a) \underset{˙}{\cdot} Y)$
33	29 32	eqtrd	$⊢ φ \to a \underset{˙}{\cdot} (X \underset{˙}{-} Y) = (a \underset{˙}{\cdot} X) \underset{˙}{+} (I (a) \underset{˙}{\cdot} Y)$
34	33	oveq1d	$⊢ φ \to (a \underset{˙}{\cdot} (X \underset{˙}{-} Y)) \underset{˙}{+} (b \underset{˙}{\cdot} Z) = ((a \underset{˙}{\cdot} X) \underset{˙}{+} (I (a) \underset{˙}{\cdot} Y)) \underset{˙}{+} (b \underset{˙}{\cdot} Z)$
35	14	lmodring	$⊢ W \in LMod \to R \in Ring$
36		ringgrp	$⊢ R \in Ring \to R \in Grp$
37	27 35 36	3syl	$⊢ φ \to R \in Grp$
38	15 19	grpinvcl	$⊢ (R \in Grp \land a \in B) \to I (a) \in B$
39	37 20 38	syl2anc	$⊢ φ \to I (a) \in B$
40	1 14 13 15	lmodvscl	$⊢ (W \in LMod \land I (a) \in B \land Y \in V) \to I (a) \underset{˙}{\cdot} Y \in V$
41	27 39 28 40	syl3anc	$⊢ φ \to I (a) \underset{˙}{\cdot} Y \in V$
42	11	eldifad	$⊢ φ \to Z \in V$
43	1 14 13 15	lmodvscl	$⊢ (W \in LMod \land b \in B \land Z \in V) \to b \underset{˙}{\cdot} Z \in V$
44	27 21 42 43	syl3anc	$⊢ φ \to b \underset{˙}{\cdot} Z \in V$
45	1 12	lmodass	$⊢ (W \in LMod \land (a \underset{˙}{\cdot} X \in V \land I (a) \underset{˙}{\cdot} Y \in V \land b \underset{˙}{\cdot} Z \in V)) \to ((a \underset{˙}{\cdot} X) \underset{˙}{+} (I (a) \underset{˙}{\cdot} Y)) \underset{˙}{+} (b \underset{˙}{\cdot} Z) = (a \underset{˙}{\cdot} X) \underset{˙}{+} ((I (a) \underset{˙}{\cdot} Y) \underset{˙}{+} (b \underset{˙}{\cdot} Z))$
46	27 31 41 44 45	syl13anc	$⊢ φ \to ((a \underset{˙}{\cdot} X) \underset{˙}{+} (I (a) \underset{˙}{\cdot} Y)) \underset{˙}{+} (b \underset{˙}{\cdot} Z) = (a \underset{˙}{\cdot} X) \underset{˙}{+} ((I (a) \underset{˙}{\cdot} Y) \underset{˙}{+} (b \underset{˙}{\cdot} Z))$
47	24 34 46	3eqtrd	$⊢ φ \to j = (a \underset{˙}{\cdot} X) \underset{˙}{+} ((I (a) \underset{˙}{\cdot} Y) \underset{˙}{+} (b \underset{˙}{\cdot} Z))$
48	1 12	lmodvacl	$⊢ (W \in LMod \land Y \in V \land Z \in V) \to Y \underset{˙}{+} Z \in V$
49	27 28 42 48	syl3anc	$⊢ φ \to Y \underset{˙}{+} Z \in V$
50	1 14 13 15	lmodvscl	$⊢ (W \in LMod \land a \in B \land Y \underset{˙}{+} Z \in V) \to a \underset{˙}{\cdot} (Y \underset{˙}{+} Z) \in V$
51	27 20 49 50	syl3anc	$⊢ φ \to a \underset{˙}{\cdot} (Y \underset{˙}{+} Z) \in V$
52		eqid	$⊢ {inv}_{g} (W) = {inv}_{g} (W)$
53	1 12 52 2	grpsubval	$⊢ (a \underset{˙}{\cdot} X \in V \land a \underset{˙}{\cdot} (Y \underset{˙}{+} Z) \in V) \to (a \underset{˙}{\cdot} X) \underset{˙}{-} (a \underset{˙}{\cdot} (Y \underset{˙}{+} Z)) = (a \underset{˙}{\cdot} X) \underset{˙}{+} {inv}_{g} (W) (a \underset{˙}{\cdot} (Y \underset{˙}{+} Z))$
54	31 51 53	syl2anc	$⊢ φ \to (a \underset{˙}{\cdot} X) \underset{˙}{-} (a \underset{˙}{\cdot} (Y \underset{˙}{+} Z)) = (a \underset{˙}{\cdot} X) \underset{˙}{+} {inv}_{g} (W) (a \underset{˙}{\cdot} (Y \underset{˙}{+} Z))$
55	1 13 14 15 2 27 20 7 49	lmodsubdi	$⊢ φ \to a \underset{˙}{\cdot} (X \underset{˙}{-} (Y \underset{˙}{+} Z)) = (a \underset{˙}{\cdot} X) \underset{˙}{-} (a \underset{˙}{\cdot} (Y \underset{˙}{+} Z))$
56	1 12 14 13 15	lmodvsdi	$⊢ (W \in LMod \land (I (a) \in B \land Y \in V \land Z \in V)) \to I (a) \underset{˙}{\cdot} (Y \underset{˙}{+} Z) = (I (a) \underset{˙}{\cdot} Y) \underset{˙}{+} (I (a) \underset{˙}{\cdot} Z)$
57	27 39 28 42 56	syl13anc	$⊢ φ \to I (a) \underset{˙}{\cdot} (Y \underset{˙}{+} Z) = (I (a) \underset{˙}{\cdot} Y) \underset{˙}{+} (I (a) \underset{˙}{\cdot} Z)$
58	1 14 13 52 15 19 27 49 20	lmodvsneg	$⊢ φ \to {inv}_{g} (W) (a \underset{˙}{\cdot} (Y \underset{˙}{+} Z)) = I (a) \underset{˙}{\cdot} (Y \underset{˙}{+} Z)$
59	15 19	grpinvcl	$⊢ (R \in Grp \land d \in B) \to I (d) \in B$
60	37 22 59	syl2anc	$⊢ φ \to I (d) \in B$
61		eqid	$⊢ LSubSp (W) = LSubSp (W)$
62	1 61 5 27 28 42	lspprcl	$⊢ φ \to N (\{Y, Z\}) \in LSubSp (W)$
63	1 12 13 14 15 5 27 39 21 28 42	lsppreli	$⊢ φ \to (I (a) \underset{˙}{\cdot} Y) \underset{˙}{+} (b \underset{˙}{\cdot} Z) \in N (\{Y, Z\})$
64	1 12 13 14 15 5 27 23 60 28 42	lsppreli	$⊢ φ \to (e \underset{˙}{\cdot} Y) \underset{˙}{+} (I (d) \underset{˙}{\cdot} Z) \in N (\{Y, Z\})$
65	1 13 14 15 2 27 22 7 42	lmodsubdi	$⊢ φ \to d \underset{˙}{\cdot} (X \underset{˙}{-} Z) = (d \underset{˙}{\cdot} X) \underset{˙}{-} (d \underset{˙}{\cdot} Z)$
66	1 14 13 15	lmodvscl	$⊢ (W \in LMod \land d \in B \land X \in V) \to d \underset{˙}{\cdot} X \in V$
67	27 22 7 66	syl3anc	$⊢ φ \to d \underset{˙}{\cdot} X \in V$
68	1 12 2 13 14 15 19 27 22 67 42	lmodsubvs	$⊢ φ \to (d \underset{˙}{\cdot} X) \underset{˙}{-} (d \underset{˙}{\cdot} Z) = (d \underset{˙}{\cdot} X) \underset{˙}{+} (I (d) \underset{˙}{\cdot} Z)$
69	65 68	eqtrd	$⊢ φ \to d \underset{˙}{\cdot} (X \underset{˙}{-} Z) = (d \underset{˙}{\cdot} X) \underset{˙}{+} (I (d) \underset{˙}{\cdot} Z)$
70	69	oveq1d	$⊢ φ \to (d \underset{˙}{\cdot} (X \underset{˙}{-} Z)) \underset{˙}{+} (e \underset{˙}{\cdot} Y) = ((d \underset{˙}{\cdot} X) \underset{˙}{+} (I (d) \underset{˙}{\cdot} Z)) \underset{˙}{+} (e \underset{˙}{\cdot} Y)$
71		lmodabl	$⊢ W \in LMod \to W \in Abel$
72	6 26 71	3syl	$⊢ φ \to W \in Abel$
73	1 14 13 15	lmodvscl	$⊢ (W \in LMod \land I (d) \in B \land Z \in V) \to I (d) \underset{˙}{\cdot} Z \in V$
74	27 60 42 73	syl3anc	$⊢ φ \to I (d) \underset{˙}{\cdot} Z \in V$
75	1 14 13 15	lmodvscl	$⊢ (W \in LMod \land e \in B \land Y \in V) \to e \underset{˙}{\cdot} Y \in V$
76	27 23 28 75	syl3anc	$⊢ φ \to e \underset{˙}{\cdot} Y \in V$
77	1 12 72 67 74 76	abl32	$⊢ φ \to ((d \underset{˙}{\cdot} X) \underset{˙}{+} (I (d) \underset{˙}{\cdot} Z)) \underset{˙}{+} (e \underset{˙}{\cdot} Y) = ((d \underset{˙}{\cdot} X) \underset{˙}{+} (e \underset{˙}{\cdot} Y)) \underset{˙}{+} (I (d) \underset{˙}{\cdot} Z)$
78	1 12	lmodass	$⊢ (W \in LMod \land (d \underset{˙}{\cdot} X \in V \land e \underset{˙}{\cdot} Y \in V \land I (d) \underset{˙}{\cdot} Z \in V)) \to ((d \underset{˙}{\cdot} X) \underset{˙}{+} (e \underset{˙}{\cdot} Y)) \underset{˙}{+} (I (d) \underset{˙}{\cdot} Z) = (d \underset{˙}{\cdot} X) \underset{˙}{+} ((e \underset{˙}{\cdot} Y) \underset{˙}{+} (I (d) \underset{˙}{\cdot} Z))$
79	27 67 76 74 78	syl13anc	$⊢ φ \to ((d \underset{˙}{\cdot} X) \underset{˙}{+} (e \underset{˙}{\cdot} Y)) \underset{˙}{+} (I (d) \underset{˙}{\cdot} Z) = (d \underset{˙}{\cdot} X) \underset{˙}{+} ((e \underset{˙}{\cdot} Y) \underset{˙}{+} (I (d) \underset{˙}{\cdot} Z))$
80	70 77 79	3eqtrd	$⊢ φ \to (d \underset{˙}{\cdot} (X \underset{˙}{-} Z)) \underset{˙}{+} (e \underset{˙}{\cdot} Y) = (d \underset{˙}{\cdot} X) \underset{˙}{+} ((e \underset{˙}{\cdot} Y) \underset{˙}{+} (I (d) \underset{˙}{\cdot} Z))$
81	25 47 80	3eqtr3d	$⊢ φ \to (a \underset{˙}{\cdot} X) \underset{˙}{+} ((I (a) \underset{˙}{\cdot} Y) \underset{˙}{+} (b \underset{˙}{\cdot} Z)) = (d \underset{˙}{\cdot} X) \underset{˙}{+} ((e \underset{˙}{\cdot} Y) \underset{˙}{+} (I (d) \underset{˙}{\cdot} Z))$
82	1 12 14 15 13 61 6 62 7 8 63 64 20 22 81	lvecindp	$⊢ φ \to (a = d \land (I (a) \underset{˙}{\cdot} Y) \underset{˙}{+} (b \underset{˙}{\cdot} Z) = (e \underset{˙}{\cdot} Y) \underset{˙}{+} (I (d) \underset{˙}{\cdot} Z))$
83	82	simprd	$⊢ φ \to (I (a) \underset{˙}{\cdot} Y) \underset{˙}{+} (b \underset{˙}{\cdot} Z) = (e \underset{˙}{\cdot} Y) \underset{˙}{+} (I (d) \underset{˙}{\cdot} Z)$
84	1 12 14 15 13 3 5 6 10 11 39 21 23 60 9 83	lvecindp2	$⊢ φ \to (I (a) = e \land b = I (d))$
85	84	simprd	$⊢ φ \to b = I (d)$
86	82	simpld	$⊢ φ \to a = d$
87	86	fveq2d	$⊢ φ \to I (a) = I (d)$
88	85 87	eqtr4d	$⊢ φ \to b = I (a)$
89	88	oveq1d	$⊢ φ \to b \underset{˙}{\cdot} Z = I (a) \underset{˙}{\cdot} Z$
90	89	oveq2d	$⊢ φ \to (I (a) \underset{˙}{\cdot} Y) \underset{˙}{+} (b \underset{˙}{\cdot} Z) = (I (a) \underset{˙}{\cdot} Y) \underset{˙}{+} (I (a) \underset{˙}{\cdot} Z)$
91	57 58 90	3eqtr4rd	$⊢ φ \to (I (a) \underset{˙}{\cdot} Y) \underset{˙}{+} (b \underset{˙}{\cdot} Z) = {inv}_{g} (W) (a \underset{˙}{\cdot} (Y \underset{˙}{+} Z))$
92	91	oveq2d	$⊢ φ \to (a \underset{˙}{\cdot} X) \underset{˙}{+} ((I (a) \underset{˙}{\cdot} Y) \underset{˙}{+} (b \underset{˙}{\cdot} Z)) = (a \underset{˙}{\cdot} X) \underset{˙}{+} {inv}_{g} (W) (a \underset{˙}{\cdot} (Y \underset{˙}{+} Z))$
93	54 55 92	3eqtr4rd	$⊢ φ \to (a \underset{˙}{\cdot} X) \underset{˙}{+} ((I (a) \underset{˙}{\cdot} Y) \underset{˙}{+} (b \underset{˙}{\cdot} Z)) = a \underset{˙}{\cdot} (X \underset{˙}{-} (Y \underset{˙}{+} Z))$
94	47 93	eqtrd	$⊢ φ \to j = a \underset{˙}{\cdot} (X \underset{˙}{-} (Y \underset{˙}{+} Z))$

Metamath Proof Explorer

Theorem baerlem5alem1

Proof