baerlem5blem1

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

Metamath Proof Explorer

Theorem baerlem5blem1

Proof