Metamath Proof Explorer

Theorem lshpkrlem1

Description: Lemma for lshpkrex . The value of tentative functional G is zero iff its argument belongs to hyperplane U . (Contributed by NM, 14-Jul-2014)

Ref Expression
Hypotheses lshpkrlem.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
lshpkrlem.a ⊢ + = ( +g ‘ 𝑊 )
lshpkrlem.n ⊢ 𝑁 = ( LSpan ‘ 𝑊 )
lshpkrlem.p ⊢ ⊕ = ( LSSum ‘ 𝑊 )
lshpkrlem.h ⊢ 𝐻 = ( LSHyp ‘ 𝑊 )
lshpkrlem.w ⊢ ( 𝜑 → 𝑊 ∈ LVec )
lshpkrlem.u ⊢ ( 𝜑 → 𝑈 ∈ 𝐻 )
lshpkrlem.z ⊢ ( 𝜑 → 𝑍 ∈ 𝑉 )
lshpkrlem.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
lshpkrlem.e ⊢ ( 𝜑 → ( 𝑈 ⊕ ( 𝑁 ‘ { 𝑍 } ) ) = 𝑉 )
lshpkrlem.d ⊢ 𝐷 = ( Scalar ‘ 𝑊 )
lshpkrlem.k ⊢ 𝐾 = ( Base ‘ 𝐷 )
lshpkrlem.t ⊢ · = ( ·𝑠 ‘ 𝑊 )
lshpkrlem.o ⊢ 0 = ( 0g ‘ 𝐷 )
lshpkrlem.g ⊢ 𝐺 = ( 𝑥 ∈ 𝑉 ↦ ( ℩ 𝑘 ∈ 𝐾 ∃ 𝑦 ∈ 𝑈 𝑥 = ( 𝑦 + ( 𝑘 · 𝑍 ) ) ) )
Assertion lshpkrlem1 ( 𝜑 → ( 𝑋 ∈ 𝑈 ↔ ( 𝐺 ‘ 𝑋 ) = 0 ) )

Proof

Step Hyp Ref Expression
1 lshpkrlem.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
2 lshpkrlem.a ⊢ + = ( +g ‘ 𝑊 )
3 lshpkrlem.n ⊢ 𝑁 = ( LSpan ‘ 𝑊 )
4 lshpkrlem.p ⊢ ⊕ = ( LSSum ‘ 𝑊 )
5 lshpkrlem.h ⊢ 𝐻 = ( LSHyp ‘ 𝑊 )
6 lshpkrlem.w ⊢ ( 𝜑 → 𝑊 ∈ LVec )
7 lshpkrlem.u ⊢ ( 𝜑 → 𝑈 ∈ 𝐻 )
8 lshpkrlem.z ⊢ ( 𝜑 → 𝑍 ∈ 𝑉 )
9 lshpkrlem.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
10 lshpkrlem.e ⊢ ( 𝜑 → ( 𝑈 ⊕ ( 𝑁 ‘ { 𝑍 } ) ) = 𝑉 )
11 lshpkrlem.d ⊢ 𝐷 = ( Scalar ‘ 𝑊 )
12 lshpkrlem.k ⊢ 𝐾 = ( Base ‘ 𝐷 )
13 lshpkrlem.t ⊢ · = ( ·𝑠 ‘ 𝑊 )
14 lshpkrlem.o ⊢ 0 = ( 0g ‘ 𝐷 )
15 lshpkrlem.g ⊢ 𝐺 = ( 𝑥 ∈ 𝑉 ↦ ( ℩ 𝑘 ∈ 𝐾 ∃ 𝑦 ∈ 𝑈 𝑥 = ( 𝑦 + ( 𝑘 · 𝑍 ) ) ) )
16 lveclmod ⊢ ( 𝑊 ∈ LVec → 𝑊 ∈ LMod )
17 6 16 syl ⊢ ( 𝜑 → 𝑊 ∈ LMod )
18 11 lmodfgrp ⊢ ( 𝑊 ∈ LMod → 𝐷 ∈ Grp )
19 12 14 grpidcl ⊢ ( 𝐷 ∈ Grp → 0 ∈ 𝐾 )
20 17 18 19 3syl ⊢ ( 𝜑 → 0 ∈ 𝐾 )
21 1 2 3 4 5 6 7 8 9 10 11 12 13 lshpsmreu ⊢ ( 𝜑 → ∃! 𝑘 ∈ 𝐾 ∃ 𝑏 ∈ 𝑈 𝑋 = ( 𝑏 + ( 𝑘 · 𝑍 ) ) )
22 oveq1 ⊢ ( 𝑘 = 0 → ( 𝑘 · 𝑍 ) = ( 0 · 𝑍 ) )
23 22 oveq2d ⊢ ( 𝑘 = 0 → ( 𝑏 + ( 𝑘 · 𝑍 ) ) = ( 𝑏 + ( 0 · 𝑍 ) ) )
24 23 eqeq2d ⊢ ( 𝑘 = 0 → ( 𝑋 = ( 𝑏 + ( 𝑘 · 𝑍 ) ) ↔ 𝑋 = ( 𝑏 + ( 0 · 𝑍 ) ) ) )
25 24 rexbidv ⊢ ( 𝑘 = 0 → ( ∃ 𝑏 ∈ 𝑈 𝑋 = ( 𝑏 + ( 𝑘 · 𝑍 ) ) ↔ ∃ 𝑏 ∈ 𝑈 𝑋 = ( 𝑏 + ( 0 · 𝑍 ) ) ) )
26 25 riota2 ⊢ ( ( 0 ∈ 𝐾 ∧ ∃! 𝑘 ∈ 𝐾 ∃ 𝑏 ∈ 𝑈 𝑋 = ( 𝑏 + ( 𝑘 · 𝑍 ) ) ) → ( ∃ 𝑏 ∈ 𝑈 𝑋 = ( 𝑏 + ( 0 · 𝑍 ) ) ↔ ( ℩ 𝑘 ∈ 𝐾 ∃ 𝑏 ∈ 𝑈 𝑋 = ( 𝑏 + ( 𝑘 · 𝑍 ) ) ) = 0 ) )
27 20 21 26 syl2anc ⊢ ( 𝜑 → ( ∃ 𝑏 ∈ 𝑈 𝑋 = ( 𝑏 + ( 0 · 𝑍 ) ) ↔ ( ℩ 𝑘 ∈ 𝐾 ∃ 𝑏 ∈ 𝑈 𝑋 = ( 𝑏 + ( 𝑘 · 𝑍 ) ) ) = 0 ) )
28 simpr ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑈 ) → 𝑋 ∈ 𝑈 )
29 eqidd ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑈 ) → 𝑋 = 𝑋 )
30 eqeq2 ⊢ ( 𝑏 = 𝑋 → ( 𝑋 = 𝑏 ↔ 𝑋 = 𝑋 ) )
31 30 rspcev ⊢ ( ( 𝑋 ∈ 𝑈 ∧ 𝑋 = 𝑋 ) → ∃ 𝑏 ∈ 𝑈 𝑋 = 𝑏 )
32 28 29 31 syl2anc ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑈 ) → ∃ 𝑏 ∈ 𝑈 𝑋 = 𝑏 )
33 32 ex ⊢ ( 𝜑 → ( 𝑋 ∈ 𝑈 → ∃ 𝑏 ∈ 𝑈 𝑋 = 𝑏 ) )
34 eleq1a ⊢ ( 𝑏 ∈ 𝑈 → ( 𝑋 = 𝑏 → 𝑋 ∈ 𝑈 ) )
35 34 a1i ⊢ ( 𝜑 → ( 𝑏 ∈ 𝑈 → ( 𝑋 = 𝑏 → 𝑋 ∈ 𝑈 ) ) )
36 35 rexlimdv ⊢ ( 𝜑 → ( ∃ 𝑏 ∈ 𝑈 𝑋 = 𝑏 → 𝑋 ∈ 𝑈 ) )
37 33 36 impbid ⊢ ( 𝜑 → ( 𝑋 ∈ 𝑈 ↔ ∃ 𝑏 ∈ 𝑈 𝑋 = 𝑏 ) )
38 eqid ⊢ ( 0g ‘ 𝑊 ) = ( 0g ‘ 𝑊 )
39 1 11 13 14 38 lmod0vs ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑍 ∈ 𝑉 ) → ( 0 · 𝑍 ) = ( 0g ‘ 𝑊 ) )
40 17 8 39 syl2anc ⊢ ( 𝜑 → ( 0 · 𝑍 ) = ( 0g ‘ 𝑊 ) )
41 40 adantr ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝑈 ) → ( 0 · 𝑍 ) = ( 0g ‘ 𝑊 ) )
42 41 oveq2d ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝑈 ) → ( 𝑏 + ( 0 · 𝑍 ) ) = ( 𝑏 + ( 0g ‘ 𝑊 ) ) )
43 6 adantr ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝑈 ) → 𝑊 ∈ LVec )
44 43 16 syl ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝑈 ) → 𝑊 ∈ LMod )
45 eqid ⊢ ( LSubSp ‘ 𝑊 ) = ( LSubSp ‘ 𝑊 )
46 45 5 17 7 lshplss ⊢ ( 𝜑 → 𝑈 ∈ ( LSubSp ‘ 𝑊 ) )
47 1 45 lssel ⊢ ( ( 𝑈 ∈ ( LSubSp ‘ 𝑊 ) ∧ 𝑏 ∈ 𝑈 ) → 𝑏 ∈ 𝑉 )
48 46 47 sylan ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝑈 ) → 𝑏 ∈ 𝑉 )
49 1 2 38 lmod0vrid ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑏 ∈ 𝑉 ) → ( 𝑏 + ( 0g ‘ 𝑊 ) ) = 𝑏 )
50 44 48 49 syl2anc ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝑈 ) → ( 𝑏 + ( 0g ‘ 𝑊 ) ) = 𝑏 )
51 42 50 eqtrd ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝑈 ) → ( 𝑏 + ( 0 · 𝑍 ) ) = 𝑏 )
52 51 eqeq2d ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝑈 ) → ( 𝑋 = ( 𝑏 + ( 0 · 𝑍 ) ) ↔ 𝑋 = 𝑏 ) )
53 52 bicomd ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝑈 ) → ( 𝑋 = 𝑏 ↔ 𝑋 = ( 𝑏 + ( 0 · 𝑍 ) ) ) )
54 53 rexbidva ⊢ ( 𝜑 → ( ∃ 𝑏 ∈ 𝑈 𝑋 = 𝑏 ↔ ∃ 𝑏 ∈ 𝑈 𝑋 = ( 𝑏 + ( 0 · 𝑍 ) ) ) )
55 37 54 bitrd ⊢ ( 𝜑 → ( 𝑋 ∈ 𝑈 ↔ ∃ 𝑏 ∈ 𝑈 𝑋 = ( 𝑏 + ( 0 · 𝑍 ) ) ) )
56 eqeq1 ⊢ ( 𝑥 = 𝑋 → ( 𝑥 = ( 𝑦 + ( 𝑘 · 𝑍 ) ) ↔ 𝑋 = ( 𝑦 + ( 𝑘 · 𝑍 ) ) ) )
57 56 rexbidv ⊢ ( 𝑥 = 𝑋 → ( ∃ 𝑦 ∈ 𝑈 𝑥 = ( 𝑦 + ( 𝑘 · 𝑍 ) ) ↔ ∃ 𝑦 ∈ 𝑈 𝑋 = ( 𝑦 + ( 𝑘 · 𝑍 ) ) ) )
58 57 riotabidv ⊢ ( 𝑥 = 𝑋 → ( ℩ 𝑘 ∈ 𝐾 ∃ 𝑦 ∈ 𝑈 𝑥 = ( 𝑦 + ( 𝑘 · 𝑍 ) ) ) = ( ℩ 𝑘 ∈ 𝐾 ∃ 𝑦 ∈ 𝑈 𝑋 = ( 𝑦 + ( 𝑘 · 𝑍 ) ) ) )
59 riotaex ⊢ ( ℩ 𝑘 ∈ 𝐾 ∃ 𝑦 ∈ 𝑈 𝑋 = ( 𝑦 + ( 𝑘 · 𝑍 ) ) ) ∈ V
60 58 15 59 fvmpt ⊢ ( 𝑋 ∈ 𝑉 → ( 𝐺 ‘ 𝑋 ) = ( ℩ 𝑘 ∈ 𝐾 ∃ 𝑦 ∈ 𝑈 𝑋 = ( 𝑦 + ( 𝑘 · 𝑍 ) ) ) )
61 oveq1 ⊢ ( 𝑦 = 𝑏 → ( 𝑦 + ( 𝑘 · 𝑍 ) ) = ( 𝑏 + ( 𝑘 · 𝑍 ) ) )
62 61 eqeq2d ⊢ ( 𝑦 = 𝑏 → ( 𝑋 = ( 𝑦 + ( 𝑘 · 𝑍 ) ) ↔ 𝑋 = ( 𝑏 + ( 𝑘 · 𝑍 ) ) ) )
63 62 cbvrexvw ⊢ ( ∃ 𝑦 ∈ 𝑈 𝑋 = ( 𝑦 + ( 𝑘 · 𝑍 ) ) ↔ ∃ 𝑏 ∈ 𝑈 𝑋 = ( 𝑏 + ( 𝑘 · 𝑍 ) ) )
64 63 a1i ⊢ ( 𝑘 ∈ 𝐾 → ( ∃ 𝑦 ∈ 𝑈 𝑋 = ( 𝑦 + ( 𝑘 · 𝑍 ) ) ↔ ∃ 𝑏 ∈ 𝑈 𝑋 = ( 𝑏 + ( 𝑘 · 𝑍 ) ) ) )
65 64 riotabiia ⊢ ( ℩ 𝑘 ∈ 𝐾 ∃ 𝑦 ∈ 𝑈 𝑋 = ( 𝑦 + ( 𝑘 · 𝑍 ) ) ) = ( ℩ 𝑘 ∈ 𝐾 ∃ 𝑏 ∈ 𝑈 𝑋 = ( 𝑏 + ( 𝑘 · 𝑍 ) ) )
66 60 65 eqtrdi ⊢ ( 𝑋 ∈ 𝑉 → ( 𝐺 ‘ 𝑋 ) = ( ℩ 𝑘 ∈ 𝐾 ∃ 𝑏 ∈ 𝑈 𝑋 = ( 𝑏 + ( 𝑘 · 𝑍 ) ) ) )
67 9 66 syl ⊢ ( 𝜑 → ( 𝐺 ‘ 𝑋 ) = ( ℩ 𝑘 ∈ 𝐾 ∃ 𝑏 ∈ 𝑈 𝑋 = ( 𝑏 + ( 𝑘 · 𝑍 ) ) ) )
68 67 eqeq1d ⊢ ( 𝜑 → ( ( 𝐺 ‘ 𝑋 ) = 0 ↔ ( ℩ 𝑘 ∈ 𝐾 ∃ 𝑏 ∈ 𝑈 𝑋 = ( 𝑏 + ( 𝑘 · 𝑍 ) ) ) = 0 ) )
69 27 55 68 3bitr4d ⊢ ( 𝜑 → ( 𝑋 ∈ 𝑈 ↔ ( 𝐺 ‘ 𝑋 ) = 0 ) )