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 )