Metamath Proof Explorer

Theorem dochfl1

Description: The value of the explicit functional G is 1 at the X that determines it. (Contributed by NM, 27-Oct-2014)

Ref Expression
Hypotheses dochfl1.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
dochfl1.o ⊢ ⊥ = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
dochfl1.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
dochfl1.v ⊢ 𝑉 = ( Base ‘ 𝑈 )
dochfl1.a ⊢ + = ( +g ‘ 𝑈 )
dochfl1.t ⊢ · = ( ·𝑠 ‘ 𝑈 )
dochfl1.z ⊢ 0 = ( 0g ‘ 𝑈 )
dochfl1.d ⊢ 𝐷 = ( Scalar ‘ 𝑈 )
dochfl1.r ⊢ 𝑅 = ( Base ‘ 𝐷 )
dochfl1.i ⊢ 1 = ( 1r ‘ 𝐷 )
dochfl1.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
dochfl1.x ⊢ ( 𝜑 → 𝑋 ∈ ( 𝑉 ∖ { 0 } ) )
dochfl1.g ⊢ 𝐺 = ( 𝑣 ∈ 𝑉 ↦ ( ℩ 𝑘 ∈ 𝑅 ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑋 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑋 ) ) ) )
Assertion dochfl1 ( 𝜑 → ( 𝐺 ‘ 𝑋 ) = 1 )

Proof

Step Hyp Ref Expression
1 dochfl1.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2 dochfl1.o ⊢ ⊥ = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
3 dochfl1.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
4 dochfl1.v ⊢ 𝑉 = ( Base ‘ 𝑈 )
5 dochfl1.a ⊢ + = ( +g ‘ 𝑈 )
6 dochfl1.t ⊢ · = ( ·𝑠 ‘ 𝑈 )
7 dochfl1.z ⊢ 0 = ( 0g ‘ 𝑈 )
8 dochfl1.d ⊢ 𝐷 = ( Scalar ‘ 𝑈 )
9 dochfl1.r ⊢ 𝑅 = ( Base ‘ 𝐷 )
10 dochfl1.i ⊢ 1 = ( 1r ‘ 𝐷 )
11 dochfl1.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
12 dochfl1.x ⊢ ( 𝜑 → 𝑋 ∈ ( 𝑉 ∖ { 0 } ) )
13 dochfl1.g ⊢ 𝐺 = ( 𝑣 ∈ 𝑉 ↦ ( ℩ 𝑘 ∈ 𝑅 ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑋 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑋 ) ) ) )
14 12 eldifad ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
15 eqeq1 ⊢ ( 𝑣 = 𝑋 → ( 𝑣 = ( 𝑤 + ( 𝑘 · 𝑋 ) ) ↔ 𝑋 = ( 𝑤 + ( 𝑘 · 𝑋 ) ) ) )
16 15 rexbidv ⊢ ( 𝑣 = 𝑋 → ( ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑋 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑋 ) ) ↔ ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑋 } ) 𝑋 = ( 𝑤 + ( 𝑘 · 𝑋 ) ) ) )
17 16 riotabidv ⊢ ( 𝑣 = 𝑋 → ( ℩ 𝑘 ∈ 𝑅 ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑋 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑋 ) ) ) = ( ℩ 𝑘 ∈ 𝑅 ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑋 } ) 𝑋 = ( 𝑤 + ( 𝑘 · 𝑋 ) ) ) )
18 riotaex ⊢ ( ℩ 𝑘 ∈ 𝑅 ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑋 } ) 𝑋 = ( 𝑤 + ( 𝑘 · 𝑋 ) ) ) ∈ V
19 17 13 18 fvmpt ⊢ ( 𝑋 ∈ 𝑉 → ( 𝐺 ‘ 𝑋 ) = ( ℩ 𝑘 ∈ 𝑅 ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑋 } ) 𝑋 = ( 𝑤 + ( 𝑘 · 𝑋 ) ) ) )
20 14 19 syl ⊢ ( 𝜑 → ( 𝐺 ‘ 𝑋 ) = ( ℩ 𝑘 ∈ 𝑅 ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑋 } ) 𝑋 = ( 𝑤 + ( 𝑘 · 𝑋 ) ) ) )
21 1 3 11 dvhlmod ⊢ ( 𝜑 → 𝑈 ∈ LMod )
22 14 snssd ⊢ ( 𝜑 → { 𝑋 } ⊆ 𝑉 )
23 eqid ⊢ ( LSubSp ‘ 𝑈 ) = ( LSubSp ‘ 𝑈 )
24 1 3 4 23 2 dochlss ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ { 𝑋 } ⊆ 𝑉 ) → ( ⊥ ‘ { 𝑋 } ) ∈ ( LSubSp ‘ 𝑈 ) )
25 11 22 24 syl2anc ⊢ ( 𝜑 → ( ⊥ ‘ { 𝑋 } ) ∈ ( LSubSp ‘ 𝑈 ) )
26 7 23 lss0cl ⊢ ( ( 𝑈 ∈ LMod ∧ ( ⊥ ‘ { 𝑋 } ) ∈ ( LSubSp ‘ 𝑈 ) ) → 0 ∈ ( ⊥ ‘ { 𝑋 } ) )
27 21 25 26 syl2anc ⊢ ( 𝜑 → 0 ∈ ( ⊥ ‘ { 𝑋 } ) )
28 4 8 6 10 lmodvs1 ⊢ ( ( 𝑈 ∈ LMod ∧ 𝑋 ∈ 𝑉 ) → ( 1 · 𝑋 ) = 𝑋 )
29 21 14 28 syl2anc ⊢ ( 𝜑 → ( 1 · 𝑋 ) = 𝑋 )
30 29 oveq2d ⊢ ( 𝜑 → ( 0 + ( 1 · 𝑋 ) ) = ( 0 + 𝑋 ) )
31 4 5 7 lmod0vlid ⊢ ( ( 𝑈 ∈ LMod ∧ 𝑋 ∈ 𝑉 ) → ( 0 + 𝑋 ) = 𝑋 )
32 21 14 31 syl2anc ⊢ ( 𝜑 → ( 0 + 𝑋 ) = 𝑋 )
33 30 32 eqtr2d ⊢ ( 𝜑 → 𝑋 = ( 0 + ( 1 · 𝑋 ) ) )
34 oveq1 ⊢ ( 𝑤 = 0 → ( 𝑤 + ( 1 · 𝑋 ) ) = ( 0 + ( 1 · 𝑋 ) ) )
35 34 rspceeqv ⊢ ( ( 0 ∈ ( ⊥ ‘ { 𝑋 } ) ∧ 𝑋 = ( 0 + ( 1 · 𝑋 ) ) ) → ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑋 } ) 𝑋 = ( 𝑤 + ( 1 · 𝑋 ) ) )
36 27 33 35 syl2anc ⊢ ( 𝜑 → ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑋 } ) 𝑋 = ( 𝑤 + ( 1 · 𝑋 ) ) )
37 8 lmodring ⊢ ( 𝑈 ∈ LMod → 𝐷 ∈ Ring )
38 9 10 ringidcl ⊢ ( 𝐷 ∈ Ring → 1 ∈ 𝑅 )
39 21 37 38 3syl ⊢ ( 𝜑 → 1 ∈ 𝑅 )
40 eqid ⊢ ( LSpan ‘ 𝑈 ) = ( LSpan ‘ 𝑈 )
41 eqid ⊢ ( LSSum ‘ 𝑈 ) = ( LSSum ‘ 𝑈 )
42 eqid ⊢ ( LSHyp ‘ 𝑈 ) = ( LSHyp ‘ 𝑈 )
43 1 3 11 dvhlvec ⊢ ( 𝜑 → 𝑈 ∈ LVec )
44 1 2 3 4 7 42 11 12 dochsnshp ⊢ ( 𝜑 → ( ⊥ ‘ { 𝑋 } ) ∈ ( LSHyp ‘ 𝑈 ) )
45 1 2 3 4 7 40 41 11 12 dochexmidat ⊢ ( 𝜑 → ( ( ⊥ ‘ { 𝑋 } ) ( LSSum ‘ 𝑈 ) ( ( LSpan ‘ 𝑈 ) ‘ { 𝑋 } ) ) = 𝑉 )
46 4 5 40 41 42 43 44 14 14 45 8 9 6 lshpsmreu ⊢ ( 𝜑 → ∃! 𝑘 ∈ 𝑅 ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑋 } ) 𝑋 = ( 𝑤 + ( 𝑘 · 𝑋 ) ) )
47 oveq1 ⊢ ( 𝑘 = 1 → ( 𝑘 · 𝑋 ) = ( 1 · 𝑋 ) )
48 47 oveq2d ⊢ ( 𝑘 = 1 → ( 𝑤 + ( 𝑘 · 𝑋 ) ) = ( 𝑤 + ( 1 · 𝑋 ) ) )
49 48 eqeq2d ⊢ ( 𝑘 = 1 → ( 𝑋 = ( 𝑤 + ( 𝑘 · 𝑋 ) ) ↔ 𝑋 = ( 𝑤 + ( 1 · 𝑋 ) ) ) )
50 49 rexbidv ⊢ ( 𝑘 = 1 → ( ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑋 } ) 𝑋 = ( 𝑤 + ( 𝑘 · 𝑋 ) ) ↔ ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑋 } ) 𝑋 = ( 𝑤 + ( 1 · 𝑋 ) ) ) )
51 50 riota2 ⊢ ( ( 1 ∈ 𝑅 ∧ ∃! 𝑘 ∈ 𝑅 ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑋 } ) 𝑋 = ( 𝑤 + ( 𝑘 · 𝑋 ) ) ) → ( ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑋 } ) 𝑋 = ( 𝑤 + ( 1 · 𝑋 ) ) ↔ ( ℩ 𝑘 ∈ 𝑅 ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑋 } ) 𝑋 = ( 𝑤 + ( 𝑘 · 𝑋 ) ) ) = 1 ) )
52 39 46 51 syl2anc ⊢ ( 𝜑 → ( ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑋 } ) 𝑋 = ( 𝑤 + ( 1 · 𝑋 ) ) ↔ ( ℩ 𝑘 ∈ 𝑅 ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑋 } ) 𝑋 = ( 𝑤 + ( 𝑘 · 𝑋 ) ) ) = 1 ) )
53 36 52 mpbid ⊢ ( 𝜑 → ( ℩ 𝑘 ∈ 𝑅 ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑋 } ) 𝑋 = ( 𝑤 + ( 𝑘 · 𝑋 ) ) ) = 1 )
54 20 53 eqtrd ⊢ ( 𝜑 → ( 𝐺 ‘ 𝑋 ) = 1 )