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 ⊢ 𝑉 = ( Base ‘ 𝑊 )
lshpsmreu.a ⊢ + = ( +g ‘ 𝑊 )
lshpsmreu.n ⊢ 𝑁 = ( LSpan ‘ 𝑊 )
lshpsmreu.p ⊢ ⊕ = ( LSSum ‘ 𝑊 )
lshpsmreu.h ⊢ 𝐻 = ( LSHyp ‘ 𝑊 )
lshpsmreu.w ⊢ ( 𝜑 → 𝑊 ∈ LVec )
lshpsmreu.u ⊢ ( 𝜑 → 𝑈 ∈ 𝐻 )
lshpsmreu.z ⊢ ( 𝜑 → 𝑍 ∈ 𝑉 )
lshpsmreu.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
lshpsmreu.e ⊢ ( 𝜑 → ( 𝑈 ⊕ ( 𝑁 ‘ { 𝑍 } ) ) = 𝑉 )
lshpsmreu.d ⊢ 𝐷 = ( Scalar ‘ 𝑊 )
lshpsmreu.k ⊢ 𝐾 = ( Base ‘ 𝐷 )
lshpsmreu.t ⊢ · = ( ·𝑠 ‘ 𝑊 )
Assertion lshpsmreu ( 𝜑 → ∃! 𝑘 ∈ 𝐾 ∃ 𝑦 ∈ 𝑈 𝑋 = ( 𝑦 + ( 𝑘 · 𝑍 ) ) )

Proof

Step Hyp Ref Expression
1 lshpsmreu.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
2 lshpsmreu.a ⊢ + = ( +g ‘ 𝑊 )
3 lshpsmreu.n ⊢ 𝑁 = ( LSpan ‘ 𝑊 )
4 lshpsmreu.p ⊢ ⊕ = ( LSSum ‘ 𝑊 )
5 lshpsmreu.h ⊢ 𝐻 = ( LSHyp ‘ 𝑊 )
6 lshpsmreu.w ⊢ ( 𝜑 → 𝑊 ∈ LVec )
7 lshpsmreu.u ⊢ ( 𝜑 → 𝑈 ∈ 𝐻 )
8 lshpsmreu.z ⊢ ( 𝜑 → 𝑍 ∈ 𝑉 )
9 lshpsmreu.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
10 lshpsmreu.e ⊢ ( 𝜑 → ( 𝑈 ⊕ ( 𝑁 ‘ { 𝑍 } ) ) = 𝑉 )
11 lshpsmreu.d ⊢ 𝐷 = ( Scalar ‘ 𝑊 )
12 lshpsmreu.k ⊢ 𝐾 = ( Base ‘ 𝐷 )
13 lshpsmreu.t ⊢ · = ( ·𝑠 ‘ 𝑊 )
14 9 10 eleqtrrd ⊢ ( 𝜑 → 𝑋 ∈ ( 𝑈 ⊕ ( 𝑁 ‘ { 𝑍 } ) ) )
15 lveclmod ⊢ ( 𝑊 ∈ LVec → 𝑊 ∈ LMod )
16 6 15 syl ⊢ ( 𝜑 → 𝑊 ∈ LMod )
17 eqid ⊢ ( LSubSp ‘ 𝑊 ) = ( LSubSp ‘ 𝑊 )
18 17 lsssssubg ⊢ ( 𝑊 ∈ LMod → ( LSubSp ‘ 𝑊 ) ⊆ ( SubGrp ‘ 𝑊 ) )
19 16 18 syl ⊢ ( 𝜑 → ( LSubSp ‘ 𝑊 ) ⊆ ( SubGrp ‘ 𝑊 ) )
20 17 5 16 7 lshplss ⊢ ( 𝜑 → 𝑈 ∈ ( LSubSp ‘ 𝑊 ) )
21 19 20 sseldd ⊢ ( 𝜑 → 𝑈 ∈ ( SubGrp ‘ 𝑊 ) )
22 1 17 3 lspsncl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑍 ∈ 𝑉 ) → ( 𝑁 ‘ { 𝑍 } ) ∈ ( LSubSp ‘ 𝑊 ) )
23 16 8 22 syl2anc ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑍 } ) ∈ ( LSubSp ‘ 𝑊 ) )
24 19 23 sseldd ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑍 } ) ∈ ( SubGrp ‘ 𝑊 ) )
25 2 4 lsmelval ⊢ ( ( 𝑈 ∈ ( SubGrp ‘ 𝑊 ) ∧ ( 𝑁 ‘ { 𝑍 } ) ∈ ( SubGrp ‘ 𝑊 ) ) → ( 𝑋 ∈ ( 𝑈 ⊕ ( 𝑁 ‘ { 𝑍 } ) ) ↔ ∃ 𝑐 ∈ 𝑈 ∃ 𝑧 ∈ ( 𝑁 ‘ { 𝑍 } ) 𝑋 = ( 𝑐 + 𝑧 ) ) )
26 21 24 25 syl2anc ⊢ ( 𝜑 → ( 𝑋 ∈ ( 𝑈 ⊕ ( 𝑁 ‘ { 𝑍 } ) ) ↔ ∃ 𝑐 ∈ 𝑈 ∃ 𝑧 ∈ ( 𝑁 ‘ { 𝑍 } ) 𝑋 = ( 𝑐 + 𝑧 ) ) )
27 14 26 mpbid ⊢ ( 𝜑 → ∃ 𝑐 ∈ 𝑈 ∃ 𝑧 ∈ ( 𝑁 ‘ { 𝑍 } ) 𝑋 = ( 𝑐 + 𝑧 ) )
28 df-rex ⊢ ( ∃ 𝑧 ∈ ( 𝑁 ‘ { 𝑍 } ) 𝑋 = ( 𝑐 + 𝑧 ) ↔ ∃ 𝑧 ( 𝑧 ∈ ( 𝑁 ‘ { 𝑍 } ) ∧ 𝑋 = ( 𝑐 + 𝑧 ) ) )
29 11 12 1 13 3 ellspsn ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑍 ∈ 𝑉 ) → ( 𝑧 ∈ ( 𝑁 ‘ { 𝑍 } ) ↔ ∃ 𝑏 ∈ 𝐾 𝑧 = ( 𝑏 · 𝑍 ) ) )
30 16 8 29 syl2anc ⊢ ( 𝜑 → ( 𝑧 ∈ ( 𝑁 ‘ { 𝑍 } ) ↔ ∃ 𝑏 ∈ 𝐾 𝑧 = ( 𝑏 · 𝑍 ) ) )
31 30 anbi1d ⊢ ( 𝜑 → ( ( 𝑧 ∈ ( 𝑁 ‘ { 𝑍 } ) ∧ 𝑋 = ( 𝑐 + 𝑧 ) ) ↔ ( ∃ 𝑏 ∈ 𝐾 𝑧 = ( 𝑏 · 𝑍 ) ∧ 𝑋 = ( 𝑐 + 𝑧 ) ) ) )
32 r19.41v ⊢ ( ∃ 𝑏 ∈ 𝐾 ( 𝑧 = ( 𝑏 · 𝑍 ) ∧ 𝑋 = ( 𝑐 + 𝑧 ) ) ↔ ( ∃ 𝑏 ∈ 𝐾 𝑧 = ( 𝑏 · 𝑍 ) ∧ 𝑋 = ( 𝑐 + 𝑧 ) ) )
33 31 32 bitr4di ⊢ ( 𝜑 → ( ( 𝑧 ∈ ( 𝑁 ‘ { 𝑍 } ) ∧ 𝑋 = ( 𝑐 + 𝑧 ) ) ↔ ∃ 𝑏 ∈ 𝐾 ( 𝑧 = ( 𝑏 · 𝑍 ) ∧ 𝑋 = ( 𝑐 + 𝑧 ) ) ) )
34 33 exbidv ⊢ ( 𝜑 → ( ∃ 𝑧 ( 𝑧 ∈ ( 𝑁 ‘ { 𝑍 } ) ∧ 𝑋 = ( 𝑐 + 𝑧 ) ) ↔ ∃ 𝑧 ∃ 𝑏 ∈ 𝐾 ( 𝑧 = ( 𝑏 · 𝑍 ) ∧ 𝑋 = ( 𝑐 + 𝑧 ) ) ) )
35 rexcom4 ⊢ ( ∃ 𝑏 ∈ 𝐾 ∃ 𝑧 ( 𝑧 = ( 𝑏 · 𝑍 ) ∧ 𝑋 = ( 𝑐 + 𝑧 ) ) ↔ ∃ 𝑧 ∃ 𝑏 ∈ 𝐾 ( 𝑧 = ( 𝑏 · 𝑍 ) ∧ 𝑋 = ( 𝑐 + 𝑧 ) ) )
36 ovex ⊢ ( 𝑏 · 𝑍 ) ∈ V
37 oveq2 ⊢ ( 𝑧 = ( 𝑏 · 𝑍 ) → ( 𝑐 + 𝑧 ) = ( 𝑐 + ( 𝑏 · 𝑍 ) ) )
38 37 eqeq2d ⊢ ( 𝑧 = ( 𝑏 · 𝑍 ) → ( 𝑋 = ( 𝑐 + 𝑧 ) ↔ 𝑋 = ( 𝑐 + ( 𝑏 · 𝑍 ) ) ) )
39 36 38 ceqsexv ⊢ ( ∃ 𝑧 ( 𝑧 = ( 𝑏 · 𝑍 ) ∧ 𝑋 = ( 𝑐 + 𝑧 ) ) ↔ 𝑋 = ( 𝑐 + ( 𝑏 · 𝑍 ) ) )
40 39 rexbii ⊢ ( ∃ 𝑏 ∈ 𝐾 ∃ 𝑧 ( 𝑧 = ( 𝑏 · 𝑍 ) ∧ 𝑋 = ( 𝑐 + 𝑧 ) ) ↔ ∃ 𝑏 ∈ 𝐾 𝑋 = ( 𝑐 + ( 𝑏 · 𝑍 ) ) )
41 35 40 bitr3i ⊢ ( ∃ 𝑧 ∃ 𝑏 ∈ 𝐾 ( 𝑧 = ( 𝑏 · 𝑍 ) ∧ 𝑋 = ( 𝑐 + 𝑧 ) ) ↔ ∃ 𝑏 ∈ 𝐾 𝑋 = ( 𝑐 + ( 𝑏 · 𝑍 ) ) )
42 34 41 bitrdi ⊢ ( 𝜑 → ( ∃ 𝑧 ( 𝑧 ∈ ( 𝑁 ‘ { 𝑍 } ) ∧ 𝑋 = ( 𝑐 + 𝑧 ) ) ↔ ∃ 𝑏 ∈ 𝐾 𝑋 = ( 𝑐 + ( 𝑏 · 𝑍 ) ) ) )
43 28 42 bitrid ⊢ ( 𝜑 → ( ∃ 𝑧 ∈ ( 𝑁 ‘ { 𝑍 } ) 𝑋 = ( 𝑐 + 𝑧 ) ↔ ∃ 𝑏 ∈ 𝐾 𝑋 = ( 𝑐 + ( 𝑏 · 𝑍 ) ) ) )
44 43 rexbidv ⊢ ( 𝜑 → ( ∃ 𝑐 ∈ 𝑈 ∃ 𝑧 ∈ ( 𝑁 ‘ { 𝑍 } ) 𝑋 = ( 𝑐 + 𝑧 ) ↔ ∃ 𝑐 ∈ 𝑈 ∃ 𝑏 ∈ 𝐾 𝑋 = ( 𝑐 + ( 𝑏 · 𝑍 ) ) ) )
45 27 44 mpbid ⊢ ( 𝜑 → ∃ 𝑐 ∈ 𝑈 ∃ 𝑏 ∈ 𝐾 𝑋 = ( 𝑐 + ( 𝑏 · 𝑍 ) ) )
46 rexcom ⊢ ( ∃ 𝑐 ∈ 𝑈 ∃ 𝑏 ∈ 𝐾 𝑋 = ( 𝑐 + ( 𝑏 · 𝑍 ) ) ↔ ∃ 𝑏 ∈ 𝐾 ∃ 𝑐 ∈ 𝑈 𝑋 = ( 𝑐 + ( 𝑏 · 𝑍 ) ) )
47 45 46 sylib ⊢ ( 𝜑 → ∃ 𝑏 ∈ 𝐾 ∃ 𝑐 ∈ 𝑈 𝑋 = ( 𝑐 + ( 𝑏 · 𝑍 ) ) )
48 oveq1 ⊢ ( 𝑐 = 𝑎 → ( 𝑐 + ( 𝑏 · 𝑍 ) ) = ( 𝑎 + ( 𝑏 · 𝑍 ) ) )
49 48 eqeq2d ⊢ ( 𝑐 = 𝑎 → ( 𝑋 = ( 𝑐 + ( 𝑏 · 𝑍 ) ) ↔ 𝑋 = ( 𝑎 + ( 𝑏 · 𝑍 ) ) ) )
50 49 cbvrexvw ⊢ ( ∃ 𝑐 ∈ 𝑈 𝑋 = ( 𝑐 + ( 𝑏 · 𝑍 ) ) ↔ ∃ 𝑎 ∈ 𝑈 𝑋 = ( 𝑎 + ( 𝑏 · 𝑍 ) ) )
51 eqid ⊢ ( 0g ‘ 𝑊 ) = ( 0g ‘ 𝑊 )
52 eqid ⊢ ( Cntz ‘ 𝑊 ) = ( Cntz ‘ 𝑊 )
53 simp11l ⊢ ( ( ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐾 ∧ 𝑙 ∈ 𝐾 ) ) ∧ 𝑎 ∈ 𝑈 ∧ 𝑋 = ( 𝑎 + ( 𝑏 · 𝑍 ) ) ) ∧ 𝑐 ∈ 𝑈 ∧ 𝑋 = ( 𝑐 + ( 𝑙 · 𝑍 ) ) ) → 𝜑 )
54 53 21 syl ⊢ ( ( ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐾 ∧ 𝑙 ∈ 𝐾 ) ) ∧ 𝑎 ∈ 𝑈 ∧ 𝑋 = ( 𝑎 + ( 𝑏 · 𝑍 ) ) ) ∧ 𝑐 ∈ 𝑈 ∧ 𝑋 = ( 𝑐 + ( 𝑙 · 𝑍 ) ) ) → 𝑈 ∈ ( SubGrp ‘ 𝑊 ) )
55 53 24 syl ⊢ ( ( ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐾 ∧ 𝑙 ∈ 𝐾 ) ) ∧ 𝑎 ∈ 𝑈 ∧ 𝑋 = ( 𝑎 + ( 𝑏 · 𝑍 ) ) ) ∧ 𝑐 ∈ 𝑈 ∧ 𝑋 = ( 𝑐 + ( 𝑙 · 𝑍 ) ) ) → ( 𝑁 ‘ { 𝑍 } ) ∈ ( SubGrp ‘ 𝑊 ) )
56 1 51 3 4 5 6 7 8 10 lshpdisj ⊢ ( 𝜑 → ( 𝑈 ∩ ( 𝑁 ‘ { 𝑍 } ) ) = { ( 0g ‘ 𝑊 ) } )
57 53 56 syl ⊢ ( ( ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐾 ∧ 𝑙 ∈ 𝐾 ) ) ∧ 𝑎 ∈ 𝑈 ∧ 𝑋 = ( 𝑎 + ( 𝑏 · 𝑍 ) ) ) ∧ 𝑐 ∈ 𝑈 ∧ 𝑋 = ( 𝑐 + ( 𝑙 · 𝑍 ) ) ) → ( 𝑈 ∩ ( 𝑁 ‘ { 𝑍 } ) ) = { ( 0g ‘ 𝑊 ) } )
58 53 6 syl ⊢ ( ( ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐾 ∧ 𝑙 ∈ 𝐾 ) ) ∧ 𝑎 ∈ 𝑈 ∧ 𝑋 = ( 𝑎 + ( 𝑏 · 𝑍 ) ) ) ∧ 𝑐 ∈ 𝑈 ∧ 𝑋 = ( 𝑐 + ( 𝑙 · 𝑍 ) ) ) → 𝑊 ∈ LVec )
59 58 15 syl ⊢ ( ( ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐾 ∧ 𝑙 ∈ 𝐾 ) ) ∧ 𝑎 ∈ 𝑈 ∧ 𝑋 = ( 𝑎 + ( 𝑏 · 𝑍 ) ) ) ∧ 𝑐 ∈ 𝑈 ∧ 𝑋 = ( 𝑐 + ( 𝑙 · 𝑍 ) ) ) → 𝑊 ∈ LMod )
60 lmodabl ⊢ ( 𝑊 ∈ LMod → 𝑊 ∈ Abel )
61 59 60 syl ⊢ ( ( ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐾 ∧ 𝑙 ∈ 𝐾 ) ) ∧ 𝑎 ∈ 𝑈 ∧ 𝑋 = ( 𝑎 + ( 𝑏 · 𝑍 ) ) ) ∧ 𝑐 ∈ 𝑈 ∧ 𝑋 = ( 𝑐 + ( 𝑙 · 𝑍 ) ) ) → 𝑊 ∈ Abel )
62 52 61 54 55 ablcntzd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐾 ∧ 𝑙 ∈ 𝐾 ) ) ∧ 𝑎 ∈ 𝑈 ∧ 𝑋 = ( 𝑎 + ( 𝑏 · 𝑍 ) ) ) ∧ 𝑐 ∈ 𝑈 ∧ 𝑋 = ( 𝑐 + ( 𝑙 · 𝑍 ) ) ) → 𝑈 ⊆ ( ( Cntz ‘ 𝑊 ) ‘ ( 𝑁 ‘ { 𝑍 } ) ) )
63 simp12 ⊢ ( ( ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐾 ∧ 𝑙 ∈ 𝐾 ) ) ∧ 𝑎 ∈ 𝑈 ∧ 𝑋 = ( 𝑎 + ( 𝑏 · 𝑍 ) ) ) ∧ 𝑐 ∈ 𝑈 ∧ 𝑋 = ( 𝑐 + ( 𝑙 · 𝑍 ) ) ) → 𝑎 ∈ 𝑈 )
64 simp2 ⊢ ( ( ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐾 ∧ 𝑙 ∈ 𝐾 ) ) ∧ 𝑎 ∈ 𝑈 ∧ 𝑋 = ( 𝑎 + ( 𝑏 · 𝑍 ) ) ) ∧ 𝑐 ∈ 𝑈 ∧ 𝑋 = ( 𝑐 + ( 𝑙 · 𝑍 ) ) ) → 𝑐 ∈ 𝑈 )
65 simp1rl ⊢ ( ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐾 ∧ 𝑙 ∈ 𝐾 ) ) ∧ 𝑎 ∈ 𝑈 ∧ 𝑋 = ( 𝑎 + ( 𝑏 · 𝑍 ) ) ) → 𝑏 ∈ 𝐾 )
66 65 3ad2ant1 ⊢ ( ( ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐾 ∧ 𝑙 ∈ 𝐾 ) ) ∧ 𝑎 ∈ 𝑈 ∧ 𝑋 = ( 𝑎 + ( 𝑏 · 𝑍 ) ) ) ∧ 𝑐 ∈ 𝑈 ∧ 𝑋 = ( 𝑐 + ( 𝑙 · 𝑍 ) ) ) → 𝑏 ∈ 𝐾 )
67 53 8 syl ⊢ ( ( ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐾 ∧ 𝑙 ∈ 𝐾 ) ) ∧ 𝑎 ∈ 𝑈 ∧ 𝑋 = ( 𝑎 + ( 𝑏 · 𝑍 ) ) ) ∧ 𝑐 ∈ 𝑈 ∧ 𝑋 = ( 𝑐 + ( 𝑙 · 𝑍 ) ) ) → 𝑍 ∈ 𝑉 )
68 1 13 11 12 3 59 66 67 ellspsni ⊢ ( ( ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐾 ∧ 𝑙 ∈ 𝐾 ) ) ∧ 𝑎 ∈ 𝑈 ∧ 𝑋 = ( 𝑎 + ( 𝑏 · 𝑍 ) ) ) ∧ 𝑐 ∈ 𝑈 ∧ 𝑋 = ( 𝑐 + ( 𝑙 · 𝑍 ) ) ) → ( 𝑏 · 𝑍 ) ∈ ( 𝑁 ‘ { 𝑍 } ) )
69 simp1rr ⊢ ( ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐾 ∧ 𝑙 ∈ 𝐾 ) ) ∧ 𝑎 ∈ 𝑈 ∧ 𝑋 = ( 𝑎 + ( 𝑏 · 𝑍 ) ) ) → 𝑙 ∈ 𝐾 )
70 69 3ad2ant1 ⊢ ( ( ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐾 ∧ 𝑙 ∈ 𝐾 ) ) ∧ 𝑎 ∈ 𝑈 ∧ 𝑋 = ( 𝑎 + ( 𝑏 · 𝑍 ) ) ) ∧ 𝑐 ∈ 𝑈 ∧ 𝑋 = ( 𝑐 + ( 𝑙 · 𝑍 ) ) ) → 𝑙 ∈ 𝐾 )
71 1 13 11 12 3 59 70 67 ellspsni ⊢ ( ( ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐾 ∧ 𝑙 ∈ 𝐾 ) ) ∧ 𝑎 ∈ 𝑈 ∧ 𝑋 = ( 𝑎 + ( 𝑏 · 𝑍 ) ) ) ∧ 𝑐 ∈ 𝑈 ∧ 𝑋 = ( 𝑐 + ( 𝑙 · 𝑍 ) ) ) → ( 𝑙 · 𝑍 ) ∈ ( 𝑁 ‘ { 𝑍 } ) )
72 simp13 ⊢ ( ( ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐾 ∧ 𝑙 ∈ 𝐾 ) ) ∧ 𝑎 ∈ 𝑈 ∧ 𝑋 = ( 𝑎 + ( 𝑏 · 𝑍 ) ) ) ∧ 𝑐 ∈ 𝑈 ∧ 𝑋 = ( 𝑐 + ( 𝑙 · 𝑍 ) ) ) → 𝑋 = ( 𝑎 + ( 𝑏 · 𝑍 ) ) )
73 simp3 ⊢ ( ( ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐾 ∧ 𝑙 ∈ 𝐾 ) ) ∧ 𝑎 ∈ 𝑈 ∧ 𝑋 = ( 𝑎 + ( 𝑏 · 𝑍 ) ) ) ∧ 𝑐 ∈ 𝑈 ∧ 𝑋 = ( 𝑐 + ( 𝑙 · 𝑍 ) ) ) → 𝑋 = ( 𝑐 + ( 𝑙 · 𝑍 ) ) )
74 72 73 eqtr3d ⊢ ( ( ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐾 ∧ 𝑙 ∈ 𝐾 ) ) ∧ 𝑎 ∈ 𝑈 ∧ 𝑋 = ( 𝑎 + ( 𝑏 · 𝑍 ) ) ) ∧ 𝑐 ∈ 𝑈 ∧ 𝑋 = ( 𝑐 + ( 𝑙 · 𝑍 ) ) ) → ( 𝑎 + ( 𝑏 · 𝑍 ) ) = ( 𝑐 + ( 𝑙 · 𝑍 ) ) )
75 2 51 52 54 55 57 62 63 64 68 71 74 subgdisj2 ⊢ ( ( ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐾 ∧ 𝑙 ∈ 𝐾 ) ) ∧ 𝑎 ∈ 𝑈 ∧ 𝑋 = ( 𝑎 + ( 𝑏 · 𝑍 ) ) ) ∧ 𝑐 ∈ 𝑈 ∧ 𝑋 = ( 𝑐 + ( 𝑙 · 𝑍 ) ) ) → ( 𝑏 · 𝑍 ) = ( 𝑙 · 𝑍 ) )
76 53 7 syl ⊢ ( ( ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐾 ∧ 𝑙 ∈ 𝐾 ) ) ∧ 𝑎 ∈ 𝑈 ∧ 𝑋 = ( 𝑎 + ( 𝑏 · 𝑍 ) ) ) ∧ 𝑐 ∈ 𝑈 ∧ 𝑋 = ( 𝑐 + ( 𝑙 · 𝑍 ) ) ) → 𝑈 ∈ 𝐻 )
77 53 10 syl ⊢ ( ( ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐾 ∧ 𝑙 ∈ 𝐾 ) ) ∧ 𝑎 ∈ 𝑈 ∧ 𝑋 = ( 𝑎 + ( 𝑏 · 𝑍 ) ) ) ∧ 𝑐 ∈ 𝑈 ∧ 𝑋 = ( 𝑐 + ( 𝑙 · 𝑍 ) ) ) → ( 𝑈 ⊕ ( 𝑁 ‘ { 𝑍 } ) ) = 𝑉 )
78 1 3 4 5 51 59 76 67 77 lshpne0 ⊢ ( ( ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐾 ∧ 𝑙 ∈ 𝐾 ) ) ∧ 𝑎 ∈ 𝑈 ∧ 𝑋 = ( 𝑎 + ( 𝑏 · 𝑍 ) ) ) ∧ 𝑐 ∈ 𝑈 ∧ 𝑋 = ( 𝑐 + ( 𝑙 · 𝑍 ) ) ) → 𝑍 ≠ ( 0g ‘ 𝑊 ) )
79 1 13 11 12 51 58 66 70 67 78 lvecvscan2 ⊢ ( ( ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐾 ∧ 𝑙 ∈ 𝐾 ) ) ∧ 𝑎 ∈ 𝑈 ∧ 𝑋 = ( 𝑎 + ( 𝑏 · 𝑍 ) ) ) ∧ 𝑐 ∈ 𝑈 ∧ 𝑋 = ( 𝑐 + ( 𝑙 · 𝑍 ) ) ) → ( ( 𝑏 · 𝑍 ) = ( 𝑙 · 𝑍 ) ↔ 𝑏 = 𝑙 ) )
80 75 79 mpbid ⊢ ( ( ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐾 ∧ 𝑙 ∈ 𝐾 ) ) ∧ 𝑎 ∈ 𝑈 ∧ 𝑋 = ( 𝑎 + ( 𝑏 · 𝑍 ) ) ) ∧ 𝑐 ∈ 𝑈 ∧ 𝑋 = ( 𝑐 + ( 𝑙 · 𝑍 ) ) ) → 𝑏 = 𝑙 )
81 80 rexlimdv3a ⊢ ( ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐾 ∧ 𝑙 ∈ 𝐾 ) ) ∧ 𝑎 ∈ 𝑈 ∧ 𝑋 = ( 𝑎 + ( 𝑏 · 𝑍 ) ) ) → ( ∃ 𝑐 ∈ 𝑈 𝑋 = ( 𝑐 + ( 𝑙 · 𝑍 ) ) → 𝑏 = 𝑙 ) )
82 81 rexlimdv3a ⊢ ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐾 ∧ 𝑙 ∈ 𝐾 ) ) → ( ∃ 𝑎 ∈ 𝑈 𝑋 = ( 𝑎 + ( 𝑏 · 𝑍 ) ) → ( ∃ 𝑐 ∈ 𝑈 𝑋 = ( 𝑐 + ( 𝑙 · 𝑍 ) ) → 𝑏 = 𝑙 ) ) )
83 50 82 biimtrid ⊢ ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐾 ∧ 𝑙 ∈ 𝐾 ) ) → ( ∃ 𝑐 ∈ 𝑈 𝑋 = ( 𝑐 + ( 𝑏 · 𝑍 ) ) → ( ∃ 𝑐 ∈ 𝑈 𝑋 = ( 𝑐 + ( 𝑙 · 𝑍 ) ) → 𝑏 = 𝑙 ) ) )
84 83 impd ⊢ ( ( 𝜑 ∧ ( 𝑏 ∈ 𝐾 ∧ 𝑙 ∈ 𝐾 ) ) → ( ( ∃ 𝑐 ∈ 𝑈 𝑋 = ( 𝑐 + ( 𝑏 · 𝑍 ) ) ∧ ∃ 𝑐 ∈ 𝑈 𝑋 = ( 𝑐 + ( 𝑙 · 𝑍 ) ) ) → 𝑏 = 𝑙 ) )
85 84 ralrimivva ⊢ ( 𝜑 → ∀ 𝑏 ∈ 𝐾 ∀ 𝑙 ∈ 𝐾 ( ( ∃ 𝑐 ∈ 𝑈 𝑋 = ( 𝑐 + ( 𝑏 · 𝑍 ) ) ∧ ∃ 𝑐 ∈ 𝑈 𝑋 = ( 𝑐 + ( 𝑙 · 𝑍 ) ) ) → 𝑏 = 𝑙 ) )
86 oveq1 ⊢ ( 𝑏 = 𝑙 → ( 𝑏 · 𝑍 ) = ( 𝑙 · 𝑍 ) )
87 86 oveq2d ⊢ ( 𝑏 = 𝑙 → ( 𝑐 + ( 𝑏 · 𝑍 ) ) = ( 𝑐 + ( 𝑙 · 𝑍 ) ) )
88 87 eqeq2d ⊢ ( 𝑏 = 𝑙 → ( 𝑋 = ( 𝑐 + ( 𝑏 · 𝑍 ) ) ↔ 𝑋 = ( 𝑐 + ( 𝑙 · 𝑍 ) ) ) )
89 88 rexbidv ⊢ ( 𝑏 = 𝑙 → ( ∃ 𝑐 ∈ 𝑈 𝑋 = ( 𝑐 + ( 𝑏 · 𝑍 ) ) ↔ ∃ 𝑐 ∈ 𝑈 𝑋 = ( 𝑐 + ( 𝑙 · 𝑍 ) ) ) )
90 89 reu4 ⊢ ( ∃! 𝑏 ∈ 𝐾 ∃ 𝑐 ∈ 𝑈 𝑋 = ( 𝑐 + ( 𝑏 · 𝑍 ) ) ↔ ( ∃ 𝑏 ∈ 𝐾 ∃ 𝑐 ∈ 𝑈 𝑋 = ( 𝑐 + ( 𝑏 · 𝑍 ) ) ∧ ∀ 𝑏 ∈ 𝐾 ∀ 𝑙 ∈ 𝐾 ( ( ∃ 𝑐 ∈ 𝑈 𝑋 = ( 𝑐 + ( 𝑏 · 𝑍 ) ) ∧ ∃ 𝑐 ∈ 𝑈 𝑋 = ( 𝑐 + ( 𝑙 · 𝑍 ) ) ) → 𝑏 = 𝑙 ) ) )
91 47 85 90 sylanbrc ⊢ ( 𝜑 → ∃! 𝑏 ∈ 𝐾 ∃ 𝑐 ∈ 𝑈 𝑋 = ( 𝑐 + ( 𝑏 · 𝑍 ) ) )
92 oveq1 ⊢ ( 𝑏 = 𝑘 → ( 𝑏 · 𝑍 ) = ( 𝑘 · 𝑍 ) )
93 92 oveq2d ⊢ ( 𝑏 = 𝑘 → ( 𝑐 + ( 𝑏 · 𝑍 ) ) = ( 𝑐 + ( 𝑘 · 𝑍 ) ) )
94 93 eqeq2d ⊢ ( 𝑏 = 𝑘 → ( 𝑋 = ( 𝑐 + ( 𝑏 · 𝑍 ) ) ↔ 𝑋 = ( 𝑐 + ( 𝑘 · 𝑍 ) ) ) )
95 94 rexbidv ⊢ ( 𝑏 = 𝑘 → ( ∃ 𝑐 ∈ 𝑈 𝑋 = ( 𝑐 + ( 𝑏 · 𝑍 ) ) ↔ ∃ 𝑐 ∈ 𝑈 𝑋 = ( 𝑐 + ( 𝑘 · 𝑍 ) ) ) )
96 95 cbvreuvw ⊢ ( ∃! 𝑏 ∈ 𝐾 ∃ 𝑐 ∈ 𝑈 𝑋 = ( 𝑐 + ( 𝑏 · 𝑍 ) ) ↔ ∃! 𝑘 ∈ 𝐾 ∃ 𝑐 ∈ 𝑈 𝑋 = ( 𝑐 + ( 𝑘 · 𝑍 ) ) )
97 oveq1 ⊢ ( 𝑐 = 𝑦 → ( 𝑐 + ( 𝑘 · 𝑍 ) ) = ( 𝑦 + ( 𝑘 · 𝑍 ) ) )
98 97 eqeq2d ⊢ ( 𝑐 = 𝑦 → ( 𝑋 = ( 𝑐 + ( 𝑘 · 𝑍 ) ) ↔ 𝑋 = ( 𝑦 + ( 𝑘 · 𝑍 ) ) ) )
99 98 cbvrexvw ⊢ ( ∃ 𝑐 ∈ 𝑈 𝑋 = ( 𝑐 + ( 𝑘 · 𝑍 ) ) ↔ ∃ 𝑦 ∈ 𝑈 𝑋 = ( 𝑦 + ( 𝑘 · 𝑍 ) ) )
100 99 reubii ⊢ ( ∃! 𝑘 ∈ 𝐾 ∃ 𝑐 ∈ 𝑈 𝑋 = ( 𝑐 + ( 𝑘 · 𝑍 ) ) ↔ ∃! 𝑘 ∈ 𝐾 ∃ 𝑦 ∈ 𝑈 𝑋 = ( 𝑦 + ( 𝑘 · 𝑍 ) ) )
101 96 100 bitri ⊢ ( ∃! 𝑏 ∈ 𝐾 ∃ 𝑐 ∈ 𝑈 𝑋 = ( 𝑐 + ( 𝑏 · 𝑍 ) ) ↔ ∃! 𝑘 ∈ 𝐾 ∃ 𝑦 ∈ 𝑈 𝑋 = ( 𝑦 + ( 𝑘 · 𝑍 ) ) )
102 91 101 sylib ⊢ ( 𝜑 → ∃! 𝑘 ∈ 𝐾 ∃ 𝑦 ∈ 𝑈 𝑋 = ( 𝑦 + ( 𝑘 · 𝑍 ) ) )