Metamath Proof Explorer

Theorem baerlem5blem1

Description: Lemma for baerlem5b . (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 ‘ 𝑅 )
baerlem5b.a1 ⊢ ( 𝜑 → 𝑎 ∈ 𝐵 )
baerlem5b.b1 ⊢ ( 𝜑 → 𝑏 ∈ 𝐵 )
baerlem5b.d1 ⊢ ( 𝜑 → 𝑑 ∈ 𝐵 )
baerlem5b.e1 ⊢ ( 𝜑 → 𝑒 ∈ 𝐵 )
baerlem5b.j1 ⊢ ( 𝜑 → 𝑗 = ( ( 𝑎 · 𝑌 ) + ( 𝑏 · 𝑍 ) ) )
baerlem5b.j2 ⊢ ( 𝜑 → 𝑗 = ( ( 𝑑 · ( 𝑋 − ( 𝑌 + 𝑍 ) ) ) + ( 𝑒 · 𝑋 ) ) )
Assertion baerlem5blem1 ( 𝜑 → 𝑗 = ( ( 𝐼 ‘ 𝑑 ) · ( 𝑌 + 𝑍 ) ) )

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 baerlem5b.a1 ⊢ ( 𝜑 → 𝑎 ∈ 𝐵 )
21 baerlem5b.b1 ⊢ ( 𝜑 → 𝑏 ∈ 𝐵 )
22 baerlem5b.d1 ⊢ ( 𝜑 → 𝑑 ∈ 𝐵 )
23 baerlem5b.e1 ⊢ ( 𝜑 → 𝑒 ∈ 𝐵 )
24 baerlem5b.j1 ⊢ ( 𝜑 → 𝑗 = ( ( 𝑎 · 𝑌 ) + ( 𝑏 · 𝑍 ) ) )
25 baerlem5b.j2 ⊢ ( 𝜑 → 𝑗 = ( ( 𝑑 · ( 𝑋 − ( 𝑌 + 𝑍 ) ) ) + ( 𝑒 · 𝑋 ) ) )
26 eqid ⊢ ( LSubSp ‘ 𝑊 ) = ( LSubSp ‘ 𝑊 )
27 lveclmod ⊢ ( 𝑊 ∈ LVec → 𝑊 ∈ LMod )
28 6 27 syl ⊢ ( 𝜑 → 𝑊 ∈ LMod )
29 10 eldifad ⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
30 11 eldifad ⊢ ( 𝜑 → 𝑍 ∈ 𝑉 )
31 1 26 5 28 29 30 lspprcl ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑌 , 𝑍 } ) ∈ ( LSubSp ‘ 𝑊 ) )
32 1 12 13 14 15 5 28 20 21 29 30 lsppreli ⊢ ( 𝜑 → ( ( 𝑎 · 𝑌 ) + ( 𝑏 · 𝑍 ) ) ∈ ( 𝑁 ‘ { 𝑌 , 𝑍 } ) )
33 14 lmodring ⊢ ( 𝑊 ∈ LMod → 𝑅 ∈ Ring )
34 28 33 syl ⊢ ( 𝜑 → 𝑅 ∈ Ring )
35 ringgrp ⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ Grp )
36 34 35 syl ⊢ ( 𝜑 → 𝑅 ∈ Grp )
37 15 19 grpinvcl ⊢ ( ( 𝑅 ∈ Grp ∧ 𝑑 ∈ 𝐵 ) → ( 𝐼 ‘ 𝑑 ) ∈ 𝐵 )
38 36 22 37 syl2anc ⊢ ( 𝜑 → ( 𝐼 ‘ 𝑑 ) ∈ 𝐵 )
39 1 12 13 14 15 5 28 38 38 29 30 lsppreli ⊢ ( 𝜑 → ( ( ( 𝐼 ‘ 𝑑 ) · 𝑌 ) + ( ( 𝐼 ‘ 𝑑 ) · 𝑍 ) ) ∈ ( 𝑁 ‘ { 𝑌 , 𝑍 } ) )
40 14 15 18 lmod0cl ⊢ ( 𝑊 ∈ LMod → 𝑄 ∈ 𝐵 )
41 28 40 syl ⊢ ( 𝜑 → 𝑄 ∈ 𝐵 )
42 14 15 16 lmodacl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝐵 ) → ( 𝑑 ⨣ 𝑒 ) ∈ 𝐵 )
43 28 22 23 42 syl3anc ⊢ ( 𝜑 → ( 𝑑 ⨣ 𝑒 ) ∈ 𝐵 )
44 1 14 13 15 lmodvscl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑎 ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) → ( 𝑎 · 𝑌 ) ∈ 𝑉 )
45 28 20 29 44 syl3anc ⊢ ( 𝜑 → ( 𝑎 · 𝑌 ) ∈ 𝑉 )
46 1 14 13 15 lmodvscl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑏 ∈ 𝐵 ∧ 𝑍 ∈ 𝑉 ) → ( 𝑏 · 𝑍 ) ∈ 𝑉 )
47 28 21 30 46 syl3anc ⊢ ( 𝜑 → ( 𝑏 · 𝑍 ) ∈ 𝑉 )
48 1 12 lmodvacl ⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝑎 · 𝑌 ) ∈ 𝑉 ∧ ( 𝑏 · 𝑍 ) ∈ 𝑉 ) → ( ( 𝑎 · 𝑌 ) + ( 𝑏 · 𝑍 ) ) ∈ 𝑉 )
49 28 45 47 48 syl3anc ⊢ ( 𝜑 → ( ( 𝑎 · 𝑌 ) + ( 𝑏 · 𝑍 ) ) ∈ 𝑉 )
50 1 12 3 lmod0vlid ⊢ ( ( 𝑊 ∈ LMod ∧ ( ( 𝑎 · 𝑌 ) + ( 𝑏 · 𝑍 ) ) ∈ 𝑉 ) → ( 0 + ( ( 𝑎 · 𝑌 ) + ( 𝑏 · 𝑍 ) ) ) = ( ( 𝑎 · 𝑌 ) + ( 𝑏 · 𝑍 ) ) )
51 28 49 50 syl2anc ⊢ ( 𝜑 → ( 0 + ( ( 𝑎 · 𝑌 ) + ( 𝑏 · 𝑍 ) ) ) = ( ( 𝑎 · 𝑌 ) + ( 𝑏 · 𝑍 ) ) )
52 1 14 13 18 3 lmod0vs ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ) → ( 𝑄 · 𝑋 ) = 0 )
53 28 7 52 syl2anc ⊢ ( 𝜑 → ( 𝑄 · 𝑋 ) = 0 )
54 53 oveq1d ⊢ ( 𝜑 → ( ( 𝑄 · 𝑋 ) + ( ( 𝑎 · 𝑌 ) + ( 𝑏 · 𝑍 ) ) ) = ( 0 + ( ( 𝑎 · 𝑌 ) + ( 𝑏 · 𝑍 ) ) ) )
55 51 54 24 3eqtr4d ⊢ ( 𝜑 → ( ( 𝑄 · 𝑋 ) + ( ( 𝑎 · 𝑌 ) + ( 𝑏 · 𝑍 ) ) ) = 𝑗 )
56 1 12 lmodvacl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑉 ) → ( 𝑌 + 𝑍 ) ∈ 𝑉 )
57 28 29 30 56 syl3anc ⊢ ( 𝜑 → ( 𝑌 + 𝑍 ) ∈ 𝑉 )
58 1 13 14 15 2 28 22 7 57 lmodsubdi ⊢ ( 𝜑 → ( 𝑑 · ( 𝑋 − ( 𝑌 + 𝑍 ) ) ) = ( ( 𝑑 · 𝑋 ) − ( 𝑑 · ( 𝑌 + 𝑍 ) ) ) )
59 1 14 13 15 lmodvscl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑑 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ) → ( 𝑑 · 𝑋 ) ∈ 𝑉 )
60 28 22 7 59 syl3anc ⊢ ( 𝜑 → ( 𝑑 · 𝑋 ) ∈ 𝑉 )
61 1 12 2 13 14 15 19 28 22 60 57 lmodsubvs ⊢ ( 𝜑 → ( ( 𝑑 · 𝑋 ) − ( 𝑑 · ( 𝑌 + 𝑍 ) ) ) = ( ( 𝑑 · 𝑋 ) + ( ( 𝐼 ‘ 𝑑 ) · ( 𝑌 + 𝑍 ) ) ) )
62 1 12 14 13 15 lmodvsdi ⊢ ( ( 𝑊 ∈ LMod ∧ ( ( 𝐼 ‘ 𝑑 ) ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑉 ) ) → ( ( 𝐼 ‘ 𝑑 ) · ( 𝑌 + 𝑍 ) ) = ( ( ( 𝐼 ‘ 𝑑 ) · 𝑌 ) + ( ( 𝐼 ‘ 𝑑 ) · 𝑍 ) ) )
63 28 38 29 30 62 syl13anc ⊢ ( 𝜑 → ( ( 𝐼 ‘ 𝑑 ) · ( 𝑌 + 𝑍 ) ) = ( ( ( 𝐼 ‘ 𝑑 ) · 𝑌 ) + ( ( 𝐼 ‘ 𝑑 ) · 𝑍 ) ) )
64 63 oveq2d ⊢ ( 𝜑 → ( ( 𝑑 · 𝑋 ) + ( ( 𝐼 ‘ 𝑑 ) · ( 𝑌 + 𝑍 ) ) ) = ( ( 𝑑 · 𝑋 ) + ( ( ( 𝐼 ‘ 𝑑 ) · 𝑌 ) + ( ( 𝐼 ‘ 𝑑 ) · 𝑍 ) ) ) )
65 58 61 64 3eqtrd ⊢ ( 𝜑 → ( 𝑑 · ( 𝑋 − ( 𝑌 + 𝑍 ) ) ) = ( ( 𝑑 · 𝑋 ) + ( ( ( 𝐼 ‘ 𝑑 ) · 𝑌 ) + ( ( 𝐼 ‘ 𝑑 ) · 𝑍 ) ) ) )
66 65 oveq1d ⊢ ( 𝜑 → ( ( 𝑑 · ( 𝑋 − ( 𝑌 + 𝑍 ) ) ) + ( 𝑒 · 𝑋 ) ) = ( ( ( 𝑑 · 𝑋 ) + ( ( ( 𝐼 ‘ 𝑑 ) · 𝑌 ) + ( ( 𝐼 ‘ 𝑑 ) · 𝑍 ) ) ) + ( 𝑒 · 𝑋 ) ) )
67 1 12 14 13 15 16 lmodvsdir ⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ) ) → ( ( 𝑑 ⨣ 𝑒 ) · 𝑋 ) = ( ( 𝑑 · 𝑋 ) + ( 𝑒 · 𝑋 ) ) )
68 28 22 23 7 67 syl13anc ⊢ ( 𝜑 → ( ( 𝑑 ⨣ 𝑒 ) · 𝑋 ) = ( ( 𝑑 · 𝑋 ) + ( 𝑒 · 𝑋 ) ) )
69 68 oveq1d ⊢ ( 𝜑 → ( ( ( 𝑑 ⨣ 𝑒 ) · 𝑋 ) + ( ( ( 𝐼 ‘ 𝑑 ) · 𝑌 ) + ( ( 𝐼 ‘ 𝑑 ) · 𝑍 ) ) ) = ( ( ( 𝑑 · 𝑋 ) + ( 𝑒 · 𝑋 ) ) + ( ( ( 𝐼 ‘ 𝑑 ) · 𝑌 ) + ( ( 𝐼 ‘ 𝑑 ) · 𝑍 ) ) ) )
70 lmodabl ⊢ ( 𝑊 ∈ LMod → 𝑊 ∈ Abel )
71 28 70 syl ⊢ ( 𝜑 → 𝑊 ∈ Abel )
72 1 14 13 15 lmodvscl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑒 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉 ) → ( 𝑒 · 𝑋 ) ∈ 𝑉 )
73 28 23 7 72 syl3anc ⊢ ( 𝜑 → ( 𝑒 · 𝑋 ) ∈ 𝑉 )
74 1 14 13 15 lmodvscl ⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝐼 ‘ 𝑑 ) ∈ 𝐵 ∧ 𝑌 ∈ 𝑉 ) → ( ( 𝐼 ‘ 𝑑 ) · 𝑌 ) ∈ 𝑉 )
75 28 38 29 74 syl3anc ⊢ ( 𝜑 → ( ( 𝐼 ‘ 𝑑 ) · 𝑌 ) ∈ 𝑉 )
76 1 14 13 15 lmodvscl ⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝐼 ‘ 𝑑 ) ∈ 𝐵 ∧ 𝑍 ∈ 𝑉 ) → ( ( 𝐼 ‘ 𝑑 ) · 𝑍 ) ∈ 𝑉 )
77 28 38 30 76 syl3anc ⊢ ( 𝜑 → ( ( 𝐼 ‘ 𝑑 ) · 𝑍 ) ∈ 𝑉 )
78 1 12 lmodvacl ⊢ ( ( 𝑊 ∈ LMod ∧ ( ( 𝐼 ‘ 𝑑 ) · 𝑌 ) ∈ 𝑉 ∧ ( ( 𝐼 ‘ 𝑑 ) · 𝑍 ) ∈ 𝑉 ) → ( ( ( 𝐼 ‘ 𝑑 ) · 𝑌 ) + ( ( 𝐼 ‘ 𝑑 ) · 𝑍 ) ) ∈ 𝑉 )
79 28 75 77 78 syl3anc ⊢ ( 𝜑 → ( ( ( 𝐼 ‘ 𝑑 ) · 𝑌 ) + ( ( 𝐼 ‘ 𝑑 ) · 𝑍 ) ) ∈ 𝑉 )
80 1 12 71 60 73 79 abl32 ⊢ ( 𝜑 → ( ( ( 𝑑 · 𝑋 ) + ( 𝑒 · 𝑋 ) ) + ( ( ( 𝐼 ‘ 𝑑 ) · 𝑌 ) + ( ( 𝐼 ‘ 𝑑 ) · 𝑍 ) ) ) = ( ( ( 𝑑 · 𝑋 ) + ( ( ( 𝐼 ‘ 𝑑 ) · 𝑌 ) + ( ( 𝐼 ‘ 𝑑 ) · 𝑍 ) ) ) + ( 𝑒 · 𝑋 ) ) )
81 69 80 eqtrd ⊢ ( 𝜑 → ( ( ( 𝑑 ⨣ 𝑒 ) · 𝑋 ) + ( ( ( 𝐼 ‘ 𝑑 ) · 𝑌 ) + ( ( 𝐼 ‘ 𝑑 ) · 𝑍 ) ) ) = ( ( ( 𝑑 · 𝑋 ) + ( ( ( 𝐼 ‘ 𝑑 ) · 𝑌 ) + ( ( 𝐼 ‘ 𝑑 ) · 𝑍 ) ) ) + ( 𝑒 · 𝑋 ) ) )
82 66 25 81 3eqtr4d ⊢ ( 𝜑 → 𝑗 = ( ( ( 𝑑 ⨣ 𝑒 ) · 𝑋 ) + ( ( ( 𝐼 ‘ 𝑑 ) · 𝑌 ) + ( ( 𝐼 ‘ 𝑑 ) · 𝑍 ) ) ) )
83 55 82 eqtrd ⊢ ( 𝜑 → ( ( 𝑄 · 𝑋 ) + ( ( 𝑎 · 𝑌 ) + ( 𝑏 · 𝑍 ) ) ) = ( ( ( 𝑑 ⨣ 𝑒 ) · 𝑋 ) + ( ( ( 𝐼 ‘ 𝑑 ) · 𝑌 ) + ( ( 𝐼 ‘ 𝑑 ) · 𝑍 ) ) ) )
84 1 12 14 15 13 26 6 31 7 8 32 39 41 43 83 lvecindp ⊢ ( 𝜑 → ( 𝑄 = ( 𝑑 ⨣ 𝑒 ) ∧ ( ( 𝑎 · 𝑌 ) + ( 𝑏 · 𝑍 ) ) = ( ( ( 𝐼 ‘ 𝑑 ) · 𝑌 ) + ( ( 𝐼 ‘ 𝑑 ) · 𝑍 ) ) ) )
85 84 simpld ⊢ ( 𝜑 → 𝑄 = ( 𝑑 ⨣ 𝑒 ) )
86 85 oveq1d ⊢ ( 𝜑 → ( 𝑄 · 𝑋 ) = ( ( 𝑑 ⨣ 𝑒 ) · 𝑋 ) )
87 86 53 eqtr3d ⊢ ( 𝜑 → ( ( 𝑑 ⨣ 𝑒 ) · 𝑋 ) = 0 )
88 87 oveq1d ⊢ ( 𝜑 → ( ( ( 𝑑 ⨣ 𝑒 ) · 𝑋 ) + ( ( ( 𝐼 ‘ 𝑑 ) · 𝑌 ) + ( ( 𝐼 ‘ 𝑑 ) · 𝑍 ) ) ) = ( 0 + ( ( ( 𝐼 ‘ 𝑑 ) · 𝑌 ) + ( ( 𝐼 ‘ 𝑑 ) · 𝑍 ) ) ) )
89 1 12 3 lmod0vlid ⊢ ( ( 𝑊 ∈ LMod ∧ ( ( ( 𝐼 ‘ 𝑑 ) · 𝑌 ) + ( ( 𝐼 ‘ 𝑑 ) · 𝑍 ) ) ∈ 𝑉 ) → ( 0 + ( ( ( 𝐼 ‘ 𝑑 ) · 𝑌 ) + ( ( 𝐼 ‘ 𝑑 ) · 𝑍 ) ) ) = ( ( ( 𝐼 ‘ 𝑑 ) · 𝑌 ) + ( ( 𝐼 ‘ 𝑑 ) · 𝑍 ) ) )
90 28 79 89 syl2anc ⊢ ( 𝜑 → ( 0 + ( ( ( 𝐼 ‘ 𝑑 ) · 𝑌 ) + ( ( 𝐼 ‘ 𝑑 ) · 𝑍 ) ) ) = ( ( ( 𝐼 ‘ 𝑑 ) · 𝑌 ) + ( ( 𝐼 ‘ 𝑑 ) · 𝑍 ) ) )
91 88 90 eqtrd ⊢ ( 𝜑 → ( ( ( 𝑑 ⨣ 𝑒 ) · 𝑋 ) + ( ( ( 𝐼 ‘ 𝑑 ) · 𝑌 ) + ( ( 𝐼 ‘ 𝑑 ) · 𝑍 ) ) ) = ( ( ( 𝐼 ‘ 𝑑 ) · 𝑌 ) + ( ( 𝐼 ‘ 𝑑 ) · 𝑍 ) ) )
92 91 82 63 3eqtr4d ⊢ ( 𝜑 → 𝑗 = ( ( 𝐼 ‘ 𝑑 ) · ( 𝑌 + 𝑍 ) ) )