Theorem baerlem3lem1

Description: Lemma for baerlem3 . (Contributed by NM, 9-Apr-2015)

	Ref	Expression
Hypotheses	baerlem3.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
	baerlem3.m	⊢ − = ( -g ‘ 𝑊 )
	baerlem3.o	⊢ 0 = ( 0g ‘ 𝑊 )
	baerlem3.s	⊢ ⊕ = ( LSSum ‘ 𝑊 )
	baerlem3.n	⊢ 𝑁 = ( LSpan ‘ 𝑊 )
	baerlem3.w	⊢ ( 𝜑 → 𝑊 ∈ LVec )
	baerlem3.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
	baerlem3.c	⊢ ( 𝜑 → ¬ 𝑋 ∈ ( 𝑁 ‘ { 𝑌 , 𝑍 } ) )
	baerlem3.d	⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑌 } ) ≠ ( 𝑁 ‘ { 𝑍 } ) )
	baerlem3.y	⊢ ( 𝜑 → 𝑌 ∈ ( 𝑉 ∖ { 0 } ) )
	baerlem3.z	⊢ ( 𝜑 → 𝑍 ∈ ( 𝑉 ∖ { 0 } ) )
	baerlem3.p	⊢ + = ( +g ‘ 𝑊 )
	baerlem3.t	⊢ · = ( ·𝑠 ‘ 𝑊 )
	baerlem3.r	⊢ 𝑅 = ( Scalar ‘ 𝑊 )
	baerlem3.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
	baerlem3.a	⊢ ⨣ = ( +g ‘ 𝑅 )
	baerlem3.l	⊢ 𝐿 = ( -g ‘ 𝑅 )
	baerlem3.q	⊢ 𝑄 = ( 0g ‘ 𝑅 )
	baerlem3.i	⊢ 𝐼 = ( invg ‘ 𝑅 )
	baerlem3.a1	⊢ ( 𝜑 → 𝑎 ∈ 𝐵 )
	baerlem3.b1	⊢ ( 𝜑 → 𝑏 ∈ 𝐵 )
	baerlem3.d1	⊢ ( 𝜑 → 𝑑 ∈ 𝐵 )
	baerlem3.e1	⊢ ( 𝜑 → 𝑒 ∈ 𝐵 )
	baerlem3.j1	⊢ ( 𝜑 → 𝑗 = ( ( 𝑎 · 𝑌 ) + ( 𝑏 · 𝑍 ) ) )
	baerlem3.j2	⊢ ( 𝜑 → 𝑗 = ( ( 𝑑 · ( 𝑋 − 𝑌 ) ) + ( 𝑒 · ( 𝑋 − 𝑍 ) ) ) )
Assertion	baerlem3lem1	⊢ ( 𝜑 → 𝑗 = ( 𝑎 · ( 𝑌 − 𝑍 ) ) )

Proof

Step	Hyp	Ref	Expression
1		baerlem3.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
2		baerlem3.m	⊢ − = ( -g ‘ 𝑊 )
3		baerlem3.o	⊢ 0 = ( 0g ‘ 𝑊 )
4		baerlem3.s	⊢ ⊕ = ( LSSum ‘ 𝑊 )
5		baerlem3.n	⊢ 𝑁 = ( LSpan ‘ 𝑊 )
6		baerlem3.w	⊢ ( 𝜑 → 𝑊 ∈ LVec )
7		baerlem3.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
8		baerlem3.c	⊢ ( 𝜑 → ¬ 𝑋 ∈ ( 𝑁 ‘ { 𝑌 , 𝑍 } ) )
9		baerlem3.d	⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑌 } ) ≠ ( 𝑁 ‘ { 𝑍 } ) )
10		baerlem3.y	⊢ ( 𝜑 → 𝑌 ∈ ( 𝑉 ∖ { 0 } ) )
11		baerlem3.z	⊢ ( 𝜑 → 𝑍 ∈ ( 𝑉 ∖ { 0 } ) )
12		baerlem3.p	⊢ + = ( +g ‘ 𝑊 )
13		baerlem3.t	⊢ · = ( ·𝑠 ‘ 𝑊 )
14		baerlem3.r	⊢ 𝑅 = ( Scalar ‘ 𝑊 )
15		baerlem3.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
16		baerlem3.a	⊢ ⨣ = ( +g ‘ 𝑅 )
17		baerlem3.l	⊢ 𝐿 = ( -g ‘ 𝑅 )
18		baerlem3.q	⊢ 𝑄 = ( 0g ‘ 𝑅 )
19		baerlem3.i	⊢ 𝐼 = ( invg ‘ 𝑅 )
20		baerlem3.a1	⊢ ( 𝜑 → 𝑎 ∈ 𝐵 )
21		baerlem3.b1	⊢ ( 𝜑 → 𝑏 ∈ 𝐵 )
22		baerlem3.d1	⊢ ( 𝜑 → 𝑑 ∈ 𝐵 )
23		baerlem3.e1	⊢ ( 𝜑 → 𝑒 ∈ 𝐵 )
24		baerlem3.j1	⊢ ( 𝜑 → 𝑗 = ( ( 𝑎 · 𝑌 ) + ( 𝑏 · 𝑍 ) ) )
25		baerlem3.j2	⊢ ( 𝜑 → 𝑗 = ( ( 𝑑 · ( 𝑋 − 𝑌 ) ) + ( 𝑒 · ( 𝑋 − 𝑍 ) ) ) )
26		lveclmod	⊢ ( 𝑊 ∈ LVec → 𝑊 ∈ LMod )
27	6 26	syl	⊢ ( 𝜑 → 𝑊 ∈ LMod )
28	10	eldifad	⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
29	1 14 13 15	lmodvscl	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑎 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) → ( 𝑎 · 𝑌 ) ∈ 𝑉 )
30	27 20 28 29	syl3anc	⊢ ( 𝜑 → ( 𝑎 · 𝑌 ) ∈ 𝑉 )
31	11	eldifad	⊢ ( 𝜑 → 𝑍 ∈ 𝑉 )
32	1 14 13 15	lmodvscl	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑎 ∈ 𝐵 ∧ 𝑍 ∈ 𝑉 ) → ( 𝑎 · 𝑍 ) ∈ 𝑉 )
33	27 20 31 32	syl3anc	⊢ ( 𝜑 → ( 𝑎 · 𝑍 ) ∈ 𝑉 )
34		eqid	⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
35	1 12 2 14 13 19 34	lmodvsubval2	⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝑎 · 𝑌 ) ∈ 𝑉 ∧ ( 𝑎 · 𝑍 ) ∈ 𝑉 ) → ( ( 𝑎 · 𝑌 ) − ( 𝑎 · 𝑍 ) ) = ( ( 𝑎 · 𝑌 ) + ( ( 𝐼 ‘ ( 1r ‘ 𝑅 ) ) · ( 𝑎 · 𝑍 ) ) ) )
36	27 30 33 35	syl3anc	⊢ ( 𝜑 → ( ( 𝑎 · 𝑌 ) − ( 𝑎 · 𝑍 ) ) = ( ( 𝑎 · 𝑌 ) + ( ( 𝐼 ‘ ( 1r ‘ 𝑅 ) ) · ( 𝑎 · 𝑍 ) ) ) )
37	1 13 14 15 2 27 20 28 31	lmodsubdi	⊢ ( 𝜑 → ( 𝑎 · ( 𝑌 − 𝑍 ) ) = ( ( 𝑎 · 𝑌 ) − ( 𝑎 · 𝑍 ) ) )
38	14	lmodring	⊢ ( 𝑊 ∈ LMod → 𝑅 ∈ Ring )
39	27 38	syl	⊢ ( 𝜑 → 𝑅 ∈ Ring )
40		ringgrp	⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ Grp )
41	39 40	syl	⊢ ( 𝜑 → 𝑅 ∈ Grp )
42	14 15 34	lmod1cl	⊢ ( 𝑊 ∈ LMod → ( 1r ‘ 𝑅 ) ∈ 𝐵 )
43	27 42	syl	⊢ ( 𝜑 → ( 1r ‘ 𝑅 ) ∈ 𝐵 )
44	15 19	grpinvcl	⊢ ( ( 𝑅 ∈ Grp ∧ ( 1r ‘ 𝑅 ) ∈ 𝐵 ) → ( 𝐼 ‘ ( 1r ‘ 𝑅 ) ) ∈ 𝐵 )
45	41 43 44	syl2anc	⊢ ( 𝜑 → ( 𝐼 ‘ ( 1r ‘ 𝑅 ) ) ∈ 𝐵 )
46		eqid	⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
47	1 14 13 15 46	lmodvsass	⊢ ( ( 𝑊 ∈ LMod ∧ ( ( 𝐼 ‘ ( 1r ‘ 𝑅 ) ) ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ∧ 𝑍 ∈ 𝑉 ) ) → ( ( ( 𝐼 ‘ ( 1r ‘ 𝑅 ) ) ( .r ‘ 𝑅 ) 𝑎 ) · 𝑍 ) = ( ( 𝐼 ‘ ( 1r ‘ 𝑅 ) ) · ( 𝑎 · 𝑍 ) ) )
48	27 45 20 31 47	syl13anc	⊢ ( 𝜑 → ( ( ( 𝐼 ‘ ( 1r ‘ 𝑅 ) ) ( .r ‘ 𝑅 ) 𝑎 ) · 𝑍 ) = ( ( 𝐼 ‘ ( 1r ‘ 𝑅 ) ) · ( 𝑎 · 𝑍 ) ) )
49	15 46 34 19 39 20	ringnegl	⊢ ( 𝜑 → ( ( 𝐼 ‘ ( 1r ‘ 𝑅 ) ) ( .r ‘ 𝑅 ) 𝑎 ) = ( 𝐼 ‘ 𝑎 ) )
50		ringabl	⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ Abel )
51	39 50	syl	⊢ ( 𝜑 → 𝑅 ∈ Abel )
52	15 16 19	ablinvadd	⊢ ( ( 𝑅 ∈ Abel ∧ 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝐵 ) → ( 𝐼 ‘ ( 𝑑 ⨣ 𝑒 ) ) = ( ( 𝐼 ‘ 𝑑 ) ⨣ ( 𝐼 ‘ 𝑒 ) ) )
53	51 22 23 52	syl3anc	⊢ ( 𝜑 → ( 𝐼 ‘ ( 𝑑 ⨣ 𝑒 ) ) = ( ( 𝐼 ‘ 𝑑 ) ⨣ ( 𝐼 ‘ 𝑒 ) ) )
54		eqid	⊢ ( LSubSp ‘ 𝑊 ) = ( LSubSp ‘ 𝑊 )
55	1 54 5 27 28 31	lspprcl	⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑌 , 𝑍 } ) ∈ ( LSubSp ‘ 𝑊 ) )
56	1 12 13 14 15 5 27 20 21 28 31	lsppreli	⊢ ( 𝜑 → ( ( 𝑎 · 𝑌 ) + ( 𝑏 · 𝑍 ) ) ∈ ( 𝑁 ‘ { 𝑌 , 𝑍 } ) )
57	1 12 13 14 15 5 27 22 23 28 31	lsppreli	⊢ ( 𝜑 → ( ( 𝑑 · 𝑌 ) + ( 𝑒 · 𝑍 ) ) ∈ ( 𝑁 ‘ { 𝑌 , 𝑍 } ) )
58		eqid	⊢ ( invg ‘ 𝑊 ) = ( invg ‘ 𝑊 )
59	54 58	lssvnegcl	⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝑁 ‘ { 𝑌 , 𝑍 } ) ∈ ( LSubSp ‘ 𝑊 ) ∧ ( ( 𝑑 · 𝑌 ) + ( 𝑒 · 𝑍 ) ) ∈ ( 𝑁 ‘ { 𝑌 , 𝑍 } ) ) → ( ( invg ‘ 𝑊 ) ‘ ( ( 𝑑 · 𝑌 ) + ( 𝑒 · 𝑍 ) ) ) ∈ ( 𝑁 ‘ { 𝑌 , 𝑍 } ) )
60	27 55 57 59	syl3anc	⊢ ( 𝜑 → ( ( invg ‘ 𝑊 ) ‘ ( ( 𝑑 · 𝑌 ) + ( 𝑒 · 𝑍 ) ) ) ∈ ( 𝑁 ‘ { 𝑌 , 𝑍 } ) )
61	15 18	ring0cl	⊢ ( 𝑅 ∈ Ring → 𝑄 ∈ 𝐵 )
62	39 61	syl	⊢ ( 𝜑 → 𝑄 ∈ 𝐵 )
63	15 16	ringacl	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝐵 ) → ( 𝑑 ⨣ 𝑒 ) ∈ 𝐵 )
64	39 22 23 63	syl3anc	⊢ ( 𝜑 → ( 𝑑 ⨣ 𝑒 ) ∈ 𝐵 )
65	1 14 13 18 3	lmod0vs	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ) → ( 𝑄 · 𝑋 ) = 0 )
66	27 7 65	syl2anc	⊢ ( 𝜑 → ( 𝑄 · 𝑋 ) = 0 )
67	66	oveq1d	⊢ ( 𝜑 → ( ( 𝑄 · 𝑋 ) + ( ( 𝑎 · 𝑌 ) + ( 𝑏 · 𝑍 ) ) ) = ( 0 + ( ( 𝑎 · 𝑌 ) + ( 𝑏 · 𝑍 ) ) ) )
68		lmodgrp	⊢ ( 𝑊 ∈ LMod → 𝑊 ∈ Grp )
69	27 68	syl	⊢ ( 𝜑 → 𝑊 ∈ Grp )
70	1 14 13 15	lmodvscl	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑏 ∈ 𝐵 ∧ 𝑍 ∈ 𝑉 ) → ( 𝑏 · 𝑍 ) ∈ 𝑉 )
71	27 21 31 70	syl3anc	⊢ ( 𝜑 → ( 𝑏 · 𝑍 ) ∈ 𝑉 )
72	1 12	lmodvacl	⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝑎 · 𝑌 ) ∈ 𝑉 ∧ ( 𝑏 · 𝑍 ) ∈ 𝑉 ) → ( ( 𝑎 · 𝑌 ) + ( 𝑏 · 𝑍 ) ) ∈ 𝑉 )
73	27 30 71 72	syl3anc	⊢ ( 𝜑 → ( ( 𝑎 · 𝑌 ) + ( 𝑏 · 𝑍 ) ) ∈ 𝑉 )
74	1 12 3	grplid	⊢ ( ( 𝑊 ∈ Grp ∧ ( ( 𝑎 · 𝑌 ) + ( 𝑏 · 𝑍 ) ) ∈ 𝑉 ) → ( 0 + ( ( 𝑎 · 𝑌 ) + ( 𝑏 · 𝑍 ) ) ) = ( ( 𝑎 · 𝑌 ) + ( 𝑏 · 𝑍 ) ) )
75	69 73 74	syl2anc	⊢ ( 𝜑 → ( 0 + ( ( 𝑎 · 𝑌 ) + ( 𝑏 · 𝑍 ) ) ) = ( ( 𝑎 · 𝑌 ) + ( 𝑏 · 𝑍 ) ) )
76		lmodabl	⊢ ( 𝑊 ∈ LMod → 𝑊 ∈ Abel )
77	27 76	syl	⊢ ( 𝜑 → 𝑊 ∈ Abel )
78	1 14 13 15	lmodvscl	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑑 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ) → ( 𝑑 · 𝑋 ) ∈ 𝑉 )
79	27 22 7 78	syl3anc	⊢ ( 𝜑 → ( 𝑑 · 𝑋 ) ∈ 𝑉 )
80	1 14 13 15	lmodvscl	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑒 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ) → ( 𝑒 · 𝑋 ) ∈ 𝑉 )
81	27 23 7 80	syl3anc	⊢ ( 𝜑 → ( 𝑒 · 𝑋 ) ∈ 𝑉 )
82	1 14 13 15	lmodvscl	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑑 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) → ( 𝑑 · 𝑌 ) ∈ 𝑉 )
83	27 22 28 82	syl3anc	⊢ ( 𝜑 → ( 𝑑 · 𝑌 ) ∈ 𝑉 )
84	1 14 13 15	lmodvscl	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑒 ∈ 𝐵 ∧ 𝑍 ∈ 𝑉 ) → ( 𝑒 · 𝑍 ) ∈ 𝑉 )
85	27 23 31 84	syl3anc	⊢ ( 𝜑 → ( 𝑒 · 𝑍 ) ∈ 𝑉 )
86	1 12 2	ablsub4	⊢ ( ( 𝑊 ∈ Abel ∧ ( ( 𝑑 · 𝑋 ) ∈ 𝑉 ∧ ( 𝑒 · 𝑋 ) ∈ 𝑉 ) ∧ ( ( 𝑑 · 𝑌 ) ∈ 𝑉 ∧ ( 𝑒 · 𝑍 ) ∈ 𝑉 ) ) → ( ( ( 𝑑 · 𝑋 ) + ( 𝑒 · 𝑋 ) ) − ( ( 𝑑 · 𝑌 ) + ( 𝑒 · 𝑍 ) ) ) = ( ( ( 𝑑 · 𝑋 ) − ( 𝑑 · 𝑌 ) ) + ( ( 𝑒 · 𝑋 ) − ( 𝑒 · 𝑍 ) ) ) )
87	77 79 81 83 85 86	syl122anc	⊢ ( 𝜑 → ( ( ( 𝑑 · 𝑋 ) + ( 𝑒 · 𝑋 ) ) − ( ( 𝑑 · 𝑌 ) + ( 𝑒 · 𝑍 ) ) ) = ( ( ( 𝑑 · 𝑋 ) − ( 𝑑 · 𝑌 ) ) + ( ( 𝑒 · 𝑋 ) − ( 𝑒 · 𝑍 ) ) ) )
88	1 12 14 13 15 16	lmodvsdir	⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ) ) → ( ( 𝑑 ⨣ 𝑒 ) · 𝑋 ) = ( ( 𝑑 · 𝑋 ) + ( 𝑒 · 𝑋 ) ) )
89	27 22 23 7 88	syl13anc	⊢ ( 𝜑 → ( ( 𝑑 ⨣ 𝑒 ) · 𝑋 ) = ( ( 𝑑 · 𝑋 ) + ( 𝑒 · 𝑋 ) ) )
90	89	oveq1d	⊢ ( 𝜑 → ( ( ( 𝑑 ⨣ 𝑒 ) · 𝑋 ) − ( ( 𝑑 · 𝑌 ) + ( 𝑒 · 𝑍 ) ) ) = ( ( ( 𝑑 · 𝑋 ) + ( 𝑒 · 𝑋 ) ) − ( ( 𝑑 · 𝑌 ) + ( 𝑒 · 𝑍 ) ) ) )
91	1 13 14 15 2 27 22 7 28	lmodsubdi	⊢ ( 𝜑 → ( 𝑑 · ( 𝑋 − 𝑌 ) ) = ( ( 𝑑 · 𝑋 ) − ( 𝑑 · 𝑌 ) ) )
92	1 13 14 15 2 27 23 7 31	lmodsubdi	⊢ ( 𝜑 → ( 𝑒 · ( 𝑋 − 𝑍 ) ) = ( ( 𝑒 · 𝑋 ) − ( 𝑒 · 𝑍 ) ) )
93	91 92	oveq12d	⊢ ( 𝜑 → ( ( 𝑑 · ( 𝑋 − 𝑌 ) ) + ( 𝑒 · ( 𝑋 − 𝑍 ) ) ) = ( ( ( 𝑑 · 𝑋 ) − ( 𝑑 · 𝑌 ) ) + ( ( 𝑒 · 𝑋 ) − ( 𝑒 · 𝑍 ) ) ) )
94	25 93	eqtrd	⊢ ( 𝜑 → 𝑗 = ( ( ( 𝑑 · 𝑋 ) − ( 𝑑 · 𝑌 ) ) + ( ( 𝑒 · 𝑋 ) − ( 𝑒 · 𝑍 ) ) ) )
95	87 90 94	3eqtr4rd	⊢ ( 𝜑 → 𝑗 = ( ( ( 𝑑 ⨣ 𝑒 ) · 𝑋 ) − ( ( 𝑑 · 𝑌 ) + ( 𝑒 · 𝑍 ) ) ) )
96	1 14 13 15	lmodvscl	⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝑑 ⨣ 𝑒 ) ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ) → ( ( 𝑑 ⨣ 𝑒 ) · 𝑋 ) ∈ 𝑉 )
97	27 64 7 96	syl3anc	⊢ ( 𝜑 → ( ( 𝑑 ⨣ 𝑒 ) · 𝑋 ) ∈ 𝑉 )
98	1 12	lmodvacl	⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝑑 · 𝑌 ) ∈ 𝑉 ∧ ( 𝑒 · 𝑍 ) ∈ 𝑉 ) → ( ( 𝑑 · 𝑌 ) + ( 𝑒 · 𝑍 ) ) ∈ 𝑉 )
99	27 83 85 98	syl3anc	⊢ ( 𝜑 → ( ( 𝑑 · 𝑌 ) + ( 𝑒 · 𝑍 ) ) ∈ 𝑉 )
100	1 12 58 2	grpsubval	⊢ ( ( ( ( 𝑑 ⨣ 𝑒 ) · 𝑋 ) ∈ 𝑉 ∧ ( ( 𝑑 · 𝑌 ) + ( 𝑒 · 𝑍 ) ) ∈ 𝑉 ) → ( ( ( 𝑑 ⨣ 𝑒 ) · 𝑋 ) − ( ( 𝑑 · 𝑌 ) + ( 𝑒 · 𝑍 ) ) ) = ( ( ( 𝑑 ⨣ 𝑒 ) · 𝑋 ) + ( ( invg ‘ 𝑊 ) ‘ ( ( 𝑑 · 𝑌 ) + ( 𝑒 · 𝑍 ) ) ) ) )
101	97 99 100	syl2anc	⊢ ( 𝜑 → ( ( ( 𝑑 ⨣ 𝑒 ) · 𝑋 ) − ( ( 𝑑 · 𝑌 ) + ( 𝑒 · 𝑍 ) ) ) = ( ( ( 𝑑 ⨣ 𝑒 ) · 𝑋 ) + ( ( invg ‘ 𝑊 ) ‘ ( ( 𝑑 · 𝑌 ) + ( 𝑒 · 𝑍 ) ) ) ) )
102	95 24 101	3eqtr3d	⊢ ( 𝜑 → ( ( 𝑎 · 𝑌 ) + ( 𝑏 · 𝑍 ) ) = ( ( ( 𝑑 ⨣ 𝑒 ) · 𝑋 ) + ( ( invg ‘ 𝑊 ) ‘ ( ( 𝑑 · 𝑌 ) + ( 𝑒 · 𝑍 ) ) ) ) )
103	67 75 102	3eqtrd	⊢ ( 𝜑 → ( ( 𝑄 · 𝑋 ) + ( ( 𝑎 · 𝑌 ) + ( 𝑏 · 𝑍 ) ) ) = ( ( ( 𝑑 ⨣ 𝑒 ) · 𝑋 ) + ( ( invg ‘ 𝑊 ) ‘ ( ( 𝑑 · 𝑌 ) + ( 𝑒 · 𝑍 ) ) ) ) )
104	1 12 14 15 13 54 6 55 7 8 56 60 62 64 103	lvecindp	⊢ ( 𝜑 → ( 𝑄 = ( 𝑑 ⨣ 𝑒 ) ∧ ( ( 𝑎 · 𝑌 ) + ( 𝑏 · 𝑍 ) ) = ( ( invg ‘ 𝑊 ) ‘ ( ( 𝑑 · 𝑌 ) + ( 𝑒 · 𝑍 ) ) ) ) )
105	104	simpld	⊢ ( 𝜑 → 𝑄 = ( 𝑑 ⨣ 𝑒 ) )
106	105	fveq2d	⊢ ( 𝜑 → ( 𝐼 ‘ 𝑄 ) = ( 𝐼 ‘ ( 𝑑 ⨣ 𝑒 ) ) )
107	15 19	grpinvcl	⊢ ( ( 𝑅 ∈ Grp ∧ 𝑑 ∈ 𝐵 ) → ( 𝐼 ‘ 𝑑 ) ∈ 𝐵 )
108	41 22 107	syl2anc	⊢ ( 𝜑 → ( 𝐼 ‘ 𝑑 ) ∈ 𝐵 )
109	15 19	grpinvcl	⊢ ( ( 𝑅 ∈ Grp ∧ 𝑒 ∈ 𝐵 ) → ( 𝐼 ‘ 𝑒 ) ∈ 𝐵 )
110	41 23 109	syl2anc	⊢ ( 𝜑 → ( 𝐼 ‘ 𝑒 ) ∈ 𝐵 )
111	104	simprd	⊢ ( 𝜑 → ( ( 𝑎 · 𝑌 ) + ( 𝑏 · 𝑍 ) ) = ( ( invg ‘ 𝑊 ) ‘ ( ( 𝑑 · 𝑌 ) + ( 𝑒 · 𝑍 ) ) ) )
112	1 12 13 58 14 15 19 27 22 23 28 31	lmodnegadd	⊢ ( 𝜑 → ( ( invg ‘ 𝑊 ) ‘ ( ( 𝑑 · 𝑌 ) + ( 𝑒 · 𝑍 ) ) ) = ( ( ( 𝐼 ‘ 𝑑 ) · 𝑌 ) + ( ( 𝐼 ‘ 𝑒 ) · 𝑍 ) ) )
113	111 112	eqtrd	⊢ ( 𝜑 → ( ( 𝑎 · 𝑌 ) + ( 𝑏 · 𝑍 ) ) = ( ( ( 𝐼 ‘ 𝑑 ) · 𝑌 ) + ( ( 𝐼 ‘ 𝑒 ) · 𝑍 ) ) )
114	1 12 14 15 13 3 5 6 10 11 20 21 108 110 9 113	lvecindp2	⊢ ( 𝜑 → ( 𝑎 = ( 𝐼 ‘ 𝑑 ) ∧ 𝑏 = ( 𝐼 ‘ 𝑒 ) ) )
115		oveq12	⊢ ( ( 𝑎 = ( 𝐼 ‘ 𝑑 ) ∧ 𝑏 = ( 𝐼 ‘ 𝑒 ) ) → ( 𝑎 ⨣ 𝑏 ) = ( ( 𝐼 ‘ 𝑑 ) ⨣ ( 𝐼 ‘ 𝑒 ) ) )
116	114 115	syl	⊢ ( 𝜑 → ( 𝑎 ⨣ 𝑏 ) = ( ( 𝐼 ‘ 𝑑 ) ⨣ ( 𝐼 ‘ 𝑒 ) ) )
117	53 106 116	3eqtr4rd	⊢ ( 𝜑 → ( 𝑎 ⨣ 𝑏 ) = ( 𝐼 ‘ 𝑄 ) )
118	18 19	grpinvid	⊢ ( 𝑅 ∈ Grp → ( 𝐼 ‘ 𝑄 ) = 𝑄 )
119	41 118	syl	⊢ ( 𝜑 → ( 𝐼 ‘ 𝑄 ) = 𝑄 )
120	117 119	eqtrd	⊢ ( 𝜑 → ( 𝑎 ⨣ 𝑏 ) = 𝑄 )
121	15 16 18 19	grpinvid1	⊢ ( ( 𝑅 ∈ Grp ∧ 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) → ( ( 𝐼 ‘ 𝑎 ) = 𝑏 ↔ ( 𝑎 ⨣ 𝑏 ) = 𝑄 ) )
122	41 20 21 121	syl3anc	⊢ ( 𝜑 → ( ( 𝐼 ‘ 𝑎 ) = 𝑏 ↔ ( 𝑎 ⨣ 𝑏 ) = 𝑄 ) )
123	120 122	mpbird	⊢ ( 𝜑 → ( 𝐼 ‘ 𝑎 ) = 𝑏 )
124	49 123	eqtrd	⊢ ( 𝜑 → ( ( 𝐼 ‘ ( 1r ‘ 𝑅 ) ) ( .r ‘ 𝑅 ) 𝑎 ) = 𝑏 )
125	124	oveq1d	⊢ ( 𝜑 → ( ( ( 𝐼 ‘ ( 1r ‘ 𝑅 ) ) ( .r ‘ 𝑅 ) 𝑎 ) · 𝑍 ) = ( 𝑏 · 𝑍 ) )
126	48 125	eqtr3d	⊢ ( 𝜑 → ( ( 𝐼 ‘ ( 1r ‘ 𝑅 ) ) · ( 𝑎 · 𝑍 ) ) = ( 𝑏 · 𝑍 ) )
127	126	oveq2d	⊢ ( 𝜑 → ( ( 𝑎 · 𝑌 ) + ( ( 𝐼 ‘ ( 1r ‘ 𝑅 ) ) · ( 𝑎 · 𝑍 ) ) ) = ( ( 𝑎 · 𝑌 ) + ( 𝑏 · 𝑍 ) ) )
128	24 127	eqtr4d	⊢ ( 𝜑 → 𝑗 = ( ( 𝑎 · 𝑌 ) + ( ( 𝐼 ‘ ( 1r ‘ 𝑅 ) ) · ( 𝑎 · 𝑍 ) ) ) )
129	36 37 128	3eqtr4rd	⊢ ( 𝜑 → 𝑗 = ( 𝑎 · ( 𝑌 − 𝑍 ) ) )