Metamath Proof Explorer

Theorem lshpkrlem3

Description: Lemma for lshpkrex . Defining property of GX . (Contributed by NM, 15-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 lshpkrlem3 ( 𝜑 → ∃ 𝑧 ∈ 𝑈 𝑋 = ( 𝑧 + ( ( 𝐺 ‘ 𝑋 ) · 𝑍 ) ) )

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 1 2 3 4 5 6 7 8 9 10 11 12 13 lshpsmreu ⊢ ( 𝜑 → ∃! 𝑙 ∈ 𝐾 ∃ 𝑧 ∈ 𝑈 𝑋 = ( 𝑧 + ( 𝑙 · 𝑍 ) ) )
17 riotasbc ⊢ ( ∃! 𝑙 ∈ 𝐾 ∃ 𝑧 ∈ 𝑈 𝑋 = ( 𝑧 + ( 𝑙 · 𝑍 ) ) → [ ( ℩ 𝑙 ∈ 𝐾 ∃ 𝑧 ∈ 𝑈 𝑋 = ( 𝑧 + ( 𝑙 · 𝑍 ) ) ) / 𝑙 ] ∃ 𝑧 ∈ 𝑈 𝑋 = ( 𝑧 + ( 𝑙 · 𝑍 ) ) )
18 16 17 syl ⊢ ( 𝜑 → [ ( ℩ 𝑙 ∈ 𝐾 ∃ 𝑧 ∈ 𝑈 𝑋 = ( 𝑧 + ( 𝑙 · 𝑍 ) ) ) / 𝑙 ] ∃ 𝑧 ∈ 𝑈 𝑋 = ( 𝑧 + ( 𝑙 · 𝑍 ) ) )
19 eqeq1 ⊢ ( 𝑥 = 𝑋 → ( 𝑥 = ( 𝑧 + ( 𝑙 · 𝑍 ) ) ↔ 𝑋 = ( 𝑧 + ( 𝑙 · 𝑍 ) ) ) )
20 19 rexbidv ⊢ ( 𝑥 = 𝑋 → ( ∃ 𝑧 ∈ 𝑈 𝑥 = ( 𝑧 + ( 𝑙 · 𝑍 ) ) ↔ ∃ 𝑧 ∈ 𝑈 𝑋 = ( 𝑧 + ( 𝑙 · 𝑍 ) ) ) )
21 20 riotabidv ⊢ ( 𝑥 = 𝑋 → ( ℩ 𝑙 ∈ 𝐾 ∃ 𝑧 ∈ 𝑈 𝑥 = ( 𝑧 + ( 𝑙 · 𝑍 ) ) ) = ( ℩ 𝑙 ∈ 𝐾 ∃ 𝑧 ∈ 𝑈 𝑋 = ( 𝑧 + ( 𝑙 · 𝑍 ) ) ) )
22 oveq1 ⊢ ( 𝑘 = 𝑙 → ( 𝑘 · 𝑍 ) = ( 𝑙 · 𝑍 ) )
23 22 oveq2d ⊢ ( 𝑘 = 𝑙 → ( 𝑦 + ( 𝑘 · 𝑍 ) ) = ( 𝑦 + ( 𝑙 · 𝑍 ) ) )
24 23 eqeq2d ⊢ ( 𝑘 = 𝑙 → ( 𝑥 = ( 𝑦 + ( 𝑘 · 𝑍 ) ) ↔ 𝑥 = ( 𝑦 + ( 𝑙 · 𝑍 ) ) ) )
25 24 rexbidv ⊢ ( 𝑘 = 𝑙 → ( ∃ 𝑦 ∈ 𝑈 𝑥 = ( 𝑦 + ( 𝑘 · 𝑍 ) ) ↔ ∃ 𝑦 ∈ 𝑈 𝑥 = ( 𝑦 + ( 𝑙 · 𝑍 ) ) ) )
26 oveq1 ⊢ ( 𝑦 = 𝑧 → ( 𝑦 + ( 𝑙 · 𝑍 ) ) = ( 𝑧 + ( 𝑙 · 𝑍 ) ) )
27 26 eqeq2d ⊢ ( 𝑦 = 𝑧 → ( 𝑥 = ( 𝑦 + ( 𝑙 · 𝑍 ) ) ↔ 𝑥 = ( 𝑧 + ( 𝑙 · 𝑍 ) ) ) )
28 27 cbvrexvw ⊢ ( ∃ 𝑦 ∈ 𝑈 𝑥 = ( 𝑦 + ( 𝑙 · 𝑍 ) ) ↔ ∃ 𝑧 ∈ 𝑈 𝑥 = ( 𝑧 + ( 𝑙 · 𝑍 ) ) )
29 25 28 bitrdi ⊢ ( 𝑘 = 𝑙 → ( ∃ 𝑦 ∈ 𝑈 𝑥 = ( 𝑦 + ( 𝑘 · 𝑍 ) ) ↔ ∃ 𝑧 ∈ 𝑈 𝑥 = ( 𝑧 + ( 𝑙 · 𝑍 ) ) ) )
30 29 cbvriotavw ⊢ ( ℩ 𝑘 ∈ 𝐾 ∃ 𝑦 ∈ 𝑈 𝑥 = ( 𝑦 + ( 𝑘 · 𝑍 ) ) ) = ( ℩ 𝑙 ∈ 𝐾 ∃ 𝑧 ∈ 𝑈 𝑥 = ( 𝑧 + ( 𝑙 · 𝑍 ) ) )
31 30 mpteq2i ⊢ ( 𝑥 ∈ 𝑉 ↦ ( ℩ 𝑘 ∈ 𝐾 ∃ 𝑦 ∈ 𝑈 𝑥 = ( 𝑦 + ( 𝑘 · 𝑍 ) ) ) ) = ( 𝑥 ∈ 𝑉 ↦ ( ℩ 𝑙 ∈ 𝐾 ∃ 𝑧 ∈ 𝑈 𝑥 = ( 𝑧 + ( 𝑙 · 𝑍 ) ) ) )
32 15 31 eqtri ⊢ 𝐺 = ( 𝑥 ∈ 𝑉 ↦ ( ℩ 𝑙 ∈ 𝐾 ∃ 𝑧 ∈ 𝑈 𝑥 = ( 𝑧 + ( 𝑙 · 𝑍 ) ) ) )
33 riotaex ⊢ ( ℩ 𝑙 ∈ 𝐾 ∃ 𝑧 ∈ 𝑈 𝑋 = ( 𝑧 + ( 𝑙 · 𝑍 ) ) ) ∈ V
34 21 32 33 fvmpt ⊢ ( 𝑋 ∈ 𝑉 → ( 𝐺 ‘ 𝑋 ) = ( ℩ 𝑙 ∈ 𝐾 ∃ 𝑧 ∈ 𝑈 𝑋 = ( 𝑧 + ( 𝑙 · 𝑍 ) ) ) )
35 dfsbcq ⊢ ( ( 𝐺 ‘ 𝑋 ) = ( ℩ 𝑙 ∈ 𝐾 ∃ 𝑧 ∈ 𝑈 𝑋 = ( 𝑧 + ( 𝑙 · 𝑍 ) ) ) → ( [ ( 𝐺 ‘ 𝑋 ) / 𝑙 ] ∃ 𝑧 ∈ 𝑈 𝑋 = ( 𝑧 + ( 𝑙 · 𝑍 ) ) ↔ [ ( ℩ 𝑙 ∈ 𝐾 ∃ 𝑧 ∈ 𝑈 𝑋 = ( 𝑧 + ( 𝑙 · 𝑍 ) ) ) / 𝑙 ] ∃ 𝑧 ∈ 𝑈 𝑋 = ( 𝑧 + ( 𝑙 · 𝑍 ) ) ) )
36 9 34 35 3syl ⊢ ( 𝜑 → ( [ ( 𝐺 ‘ 𝑋 ) / 𝑙 ] ∃ 𝑧 ∈ 𝑈 𝑋 = ( 𝑧 + ( 𝑙 · 𝑍 ) ) ↔ [ ( ℩ 𝑙 ∈ 𝐾 ∃ 𝑧 ∈ 𝑈 𝑋 = ( 𝑧 + ( 𝑙 · 𝑍 ) ) ) / 𝑙 ] ∃ 𝑧 ∈ 𝑈 𝑋 = ( 𝑧 + ( 𝑙 · 𝑍 ) ) ) )
37 18 36 mpbird ⊢ ( 𝜑 → [ ( 𝐺 ‘ 𝑋 ) / 𝑙 ] ∃ 𝑧 ∈ 𝑈 𝑋 = ( 𝑧 + ( 𝑙 · 𝑍 ) ) )
38 fvex ⊢ ( 𝐺 ‘ 𝑋 ) ∈ V
39 oveq1 ⊢ ( 𝑙 = ( 𝐺 ‘ 𝑋 ) → ( 𝑙 · 𝑍 ) = ( ( 𝐺 ‘ 𝑋 ) · 𝑍 ) )
40 39 oveq2d ⊢ ( 𝑙 = ( 𝐺 ‘ 𝑋 ) → ( 𝑧 + ( 𝑙 · 𝑍 ) ) = ( 𝑧 + ( ( 𝐺 ‘ 𝑋 ) · 𝑍 ) ) )
41 40 eqeq2d ⊢ ( 𝑙 = ( 𝐺 ‘ 𝑋 ) → ( 𝑋 = ( 𝑧 + ( 𝑙 · 𝑍 ) ) ↔ 𝑋 = ( 𝑧 + ( ( 𝐺 ‘ 𝑋 ) · 𝑍 ) ) ) )
42 41 rexbidv ⊢ ( 𝑙 = ( 𝐺 ‘ 𝑋 ) → ( ∃ 𝑧 ∈ 𝑈 𝑋 = ( 𝑧 + ( 𝑙 · 𝑍 ) ) ↔ ∃ 𝑧 ∈ 𝑈 𝑋 = ( 𝑧 + ( ( 𝐺 ‘ 𝑋 ) · 𝑍 ) ) ) )
43 38 42 sbcie ⊢ ( [ ( 𝐺 ‘ 𝑋 ) / 𝑙 ] ∃ 𝑧 ∈ 𝑈 𝑋 = ( 𝑧 + ( 𝑙 · 𝑍 ) ) ↔ ∃ 𝑧 ∈ 𝑈 𝑋 = ( 𝑧 + ( ( 𝐺 ‘ 𝑋 ) · 𝑍 ) ) )
44 37 43 sylib ⊢ ( 𝜑 → ∃ 𝑧 ∈ 𝑈 𝑋 = ( 𝑧 + ( ( 𝐺 ‘ 𝑋 ) · 𝑍 ) ) )