Metamath Proof Explorer


Theorem lshpsmreu

Description: Lemma for lshpkrex . Show uniqueness of ring multiplier k when a vector X is broken down into components, one in a hyperplane and the other outside of it . TODO: do we need the cbvrexv for a to c ? (Contributed by NM, 4-Jan-2015)

Ref Expression
Hypotheses lshpsmreu.v V = Base W
lshpsmreu.a + ˙ = + W
lshpsmreu.n N = LSpan W
lshpsmreu.p ˙ = LSSum W
lshpsmreu.h H = LSHyp W
lshpsmreu.w φ W LVec
lshpsmreu.u φ U H
lshpsmreu.z φ Z V
lshpsmreu.x φ X V
lshpsmreu.e φ U ˙ N Z = V
lshpsmreu.d D = Scalar W
lshpsmreu.k K = Base D
lshpsmreu.t · ˙ = W
Assertion lshpsmreu φ ∃! k K y U X = y + ˙ k · ˙ Z

Proof

Step Hyp Ref Expression
1 lshpsmreu.v V = Base W
2 lshpsmreu.a + ˙ = + W
3 lshpsmreu.n N = LSpan W
4 lshpsmreu.p ˙ = LSSum W
5 lshpsmreu.h H = LSHyp W
6 lshpsmreu.w φ W LVec
7 lshpsmreu.u φ U H
8 lshpsmreu.z φ Z V
9 lshpsmreu.x φ X V
10 lshpsmreu.e φ U ˙ N Z = V
11 lshpsmreu.d D = Scalar W
12 lshpsmreu.k K = Base D
13 lshpsmreu.t · ˙ = W
14 9 10 eleqtrrd φ X U ˙ N Z
15 lveclmod W LVec W LMod
16 6 15 syl φ W LMod
17 eqid LSubSp W = LSubSp W
18 17 lsssssubg W LMod LSubSp W SubGrp W
19 16 18 syl φ LSubSp W SubGrp W
20 17 5 16 7 lshplss φ U LSubSp W
21 19 20 sseldd φ U SubGrp W
22 1 17 3 lspsncl W LMod Z V N Z LSubSp W
23 16 8 22 syl2anc φ N Z LSubSp W
24 19 23 sseldd φ N Z SubGrp W
25 2 4 lsmelval U SubGrp W N Z SubGrp W X U ˙ N Z c U z N Z X = c + ˙ z
26 21 24 25 syl2anc φ X U ˙ N Z c U z N Z X = c + ˙ z
27 14 26 mpbid φ c U z N Z X = c + ˙ z
28 df-rex z N Z X = c + ˙ z z z N Z X = c + ˙ z
29 11 12 1 13 3 lspsnel W LMod Z V z N Z b K z = b · ˙ Z
30 16 8 29 syl2anc φ z N Z b K z = b · ˙ Z
31 30 anbi1d φ z N Z X = c + ˙ z b K z = b · ˙ Z X = c + ˙ z
32 r19.41v b K z = b · ˙ Z X = c + ˙ z b K z = b · ˙ Z X = c + ˙ z
33 31 32 bitr4di φ z N Z X = c + ˙ z b K z = b · ˙ Z X = c + ˙ z
34 33 exbidv φ z z N Z X = c + ˙ z z b K z = b · ˙ Z X = c + ˙ z
35 rexcom4 b K z z = b · ˙ Z X = c + ˙ z z b K z = b · ˙ Z X = c + ˙ z
36 ovex b · ˙ Z V
37 oveq2 z = b · ˙ Z c + ˙ z = c + ˙ b · ˙ Z
38 37 eqeq2d z = b · ˙ Z X = c + ˙ z X = c + ˙ b · ˙ Z
39 36 38 ceqsexv z z = b · ˙ Z X = c + ˙ z X = c + ˙ b · ˙ Z
40 39 rexbii b K z z = b · ˙ Z X = c + ˙ z b K X = c + ˙ b · ˙ Z
41 35 40 bitr3i z b K z = b · ˙ Z X = c + ˙ z b K X = c + ˙ b · ˙ Z
42 34 41 bitrdi φ z z N Z X = c + ˙ z b K X = c + ˙ b · ˙ Z
43 28 42 syl5bb φ z N Z X = c + ˙ z b K X = c + ˙ b · ˙ Z
44 43 rexbidv φ c U z N Z X = c + ˙ z c U b K X = c + ˙ b · ˙ Z
45 27 44 mpbid φ c U b K X = c + ˙ b · ˙ Z
46 rexcom c U b K X = c + ˙ b · ˙ Z b K c U X = c + ˙ b · ˙ Z
47 45 46 sylib φ b K c U X = c + ˙ b · ˙ Z
48 oveq1 c = a c + ˙ b · ˙ Z = a + ˙ b · ˙ Z
49 48 eqeq2d c = a X = c + ˙ b · ˙ Z X = a + ˙ b · ˙ Z
50 49 cbvrexvw c U X = c + ˙ b · ˙ Z a U X = a + ˙ b · ˙ Z
51 eqid 0 W = 0 W
52 eqid Cntz W = Cntz W
53 simp11l φ b K l K a U X = a + ˙ b · ˙ Z c U X = c + ˙ l · ˙ Z φ
54 53 21 syl φ b K l K a U X = a + ˙ b · ˙ Z c U X = c + ˙ l · ˙ Z U SubGrp W
55 53 24 syl φ b K l K a U X = a + ˙ b · ˙ Z c U X = c + ˙ l · ˙ Z N Z SubGrp W
56 1 51 3 4 5 6 7 8 10 lshpdisj φ U N Z = 0 W
57 53 56 syl φ b K l K a U X = a + ˙ b · ˙ Z c U X = c + ˙ l · ˙ Z U N Z = 0 W
58 53 6 syl φ b K l K a U X = a + ˙ b · ˙ Z c U X = c + ˙ l · ˙ Z W LVec
59 58 15 syl φ b K l K a U X = a + ˙ b · ˙ Z c U X = c + ˙ l · ˙ Z W LMod
60 lmodabl W LMod W Abel
61 59 60 syl φ b K l K a U X = a + ˙ b · ˙ Z c U X = c + ˙ l · ˙ Z W Abel
62 52 61 54 55 ablcntzd φ b K l K a U X = a + ˙ b · ˙ Z c U X = c + ˙ l · ˙ Z U Cntz W N Z
63 simp12 φ b K l K a U X = a + ˙ b · ˙ Z c U X = c + ˙ l · ˙ Z a U
64 simp2 φ b K l K a U X = a + ˙ b · ˙ Z c U X = c + ˙ l · ˙ Z c U
65 simp1rl φ b K l K a U X = a + ˙ b · ˙ Z b K
66 65 3ad2ant1 φ b K l K a U X = a + ˙ b · ˙ Z c U X = c + ˙ l · ˙ Z b K
67 53 8 syl φ b K l K a U X = a + ˙ b · ˙ Z c U X = c + ˙ l · ˙ Z Z V
68 1 13 11 12 3 59 66 67 lspsneli φ b K l K a U X = a + ˙ b · ˙ Z c U X = c + ˙ l · ˙ Z b · ˙ Z N Z
69 simp1rr φ b K l K a U X = a + ˙ b · ˙ Z l K
70 69 3ad2ant1 φ b K l K a U X = a + ˙ b · ˙ Z c U X = c + ˙ l · ˙ Z l K
71 1 13 11 12 3 59 70 67 lspsneli φ b K l K a U X = a + ˙ b · ˙ Z c U X = c + ˙ l · ˙ Z l · ˙ Z N Z
72 simp13 φ b K l K a U X = a + ˙ b · ˙ Z c U X = c + ˙ l · ˙ Z X = a + ˙ b · ˙ Z
73 simp3 φ b K l K a U X = a + ˙ b · ˙ Z c U X = c + ˙ l · ˙ Z X = c + ˙ l · ˙ Z
74 72 73 eqtr3d φ b K l K a U X = a + ˙ b · ˙ Z c U X = c + ˙ l · ˙ Z a + ˙ b · ˙ Z = c + ˙ l · ˙ Z
75 2 51 52 54 55 57 62 63 64 68 71 74 subgdisj2 φ b K l K a U X = a + ˙ b · ˙ Z c U X = c + ˙ l · ˙ Z b · ˙ Z = l · ˙ Z
76 53 7 syl φ b K l K a U X = a + ˙ b · ˙ Z c U X = c + ˙ l · ˙ Z U H
77 53 10 syl φ b K l K a U X = a + ˙ b · ˙ Z c U X = c + ˙ l · ˙ Z U ˙ N Z = V
78 1 3 4 5 51 59 76 67 77 lshpne0 φ b K l K a U X = a + ˙ b · ˙ Z c U X = c + ˙ l · ˙ Z Z 0 W
79 1 13 11 12 51 58 66 70 67 78 lvecvscan2 φ b K l K a U X = a + ˙ b · ˙ Z c U X = c + ˙ l · ˙ Z b · ˙ Z = l · ˙ Z b = l
80 75 79 mpbid φ b K l K a U X = a + ˙ b · ˙ Z c U X = c + ˙ l · ˙ Z b = l
81 80 rexlimdv3a φ b K l K a U X = a + ˙ b · ˙ Z c U X = c + ˙ l · ˙ Z b = l
82 81 rexlimdv3a φ b K l K a U X = a + ˙ b · ˙ Z c U X = c + ˙ l · ˙ Z b = l
83 50 82 syl5bi φ b K l K c U X = c + ˙ b · ˙ Z c U X = c + ˙ l · ˙ Z b = l
84 83 impd φ b K l K c U X = c + ˙ b · ˙ Z c U X = c + ˙ l · ˙ Z b = l
85 84 ralrimivva φ b K l K c U X = c + ˙ b · ˙ Z c U X = c + ˙ l · ˙ Z b = l
86 oveq1 b = l b · ˙ Z = l · ˙ Z
87 86 oveq2d b = l c + ˙ b · ˙ Z = c + ˙ l · ˙ Z
88 87 eqeq2d b = l X = c + ˙ b · ˙ Z X = c + ˙ l · ˙ Z
89 88 rexbidv b = l c U X = c + ˙ b · ˙ Z c U X = c + ˙ l · ˙ Z
90 89 reu4 ∃! b K c U X = c + ˙ b · ˙ Z b K c U X = c + ˙ b · ˙ Z b K l K c U X = c + ˙ b · ˙ Z c U X = c + ˙ l · ˙ Z b = l
91 47 85 90 sylanbrc φ ∃! b K c U X = c + ˙ b · ˙ Z
92 oveq1 b = k b · ˙ Z = k · ˙ Z
93 92 oveq2d b = k c + ˙ b · ˙ Z = c + ˙ k · ˙ Z
94 93 eqeq2d b = k X = c + ˙ b · ˙ Z X = c + ˙ k · ˙ Z
95 94 rexbidv b = k c U X = c + ˙ b · ˙ Z c U X = c + ˙ k · ˙ Z
96 95 cbvreuvw ∃! b K c U X = c + ˙ b · ˙ Z ∃! k K c U X = c + ˙ k · ˙ Z
97 oveq1 c = y c + ˙ k · ˙ Z = y + ˙ k · ˙ Z
98 97 eqeq2d c = y X = c + ˙ k · ˙ Z X = y + ˙ k · ˙ Z
99 98 cbvrexvw c U X = c + ˙ k · ˙ Z y U X = y + ˙ k · ˙ Z
100 99 reubii ∃! k K c U X = c + ˙ k · ˙ Z ∃! k K y U X = y + ˙ k · ˙ Z
101 96 100 bitri ∃! b K c U X = c + ˙ b · ˙ Z ∃! k K y U X = y + ˙ k · ˙ Z
102 91 101 sylib φ ∃! k K y U X = y + ˙ k · ˙ Z