Theorem dochsnkr2cl

Description: The X determining functional G belongs to the atom formed by the orthocomplement of the kernel. (Contributed by NM, 4-Jan-2015)

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

Proof

Step	Hyp	Ref	Expression
1		dochsnkr2.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2		dochsnkr2.o	⊢ ⊥ = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
3		dochsnkr2.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
4		dochsnkr2.v	⊢ 𝑉 = ( Base ‘ 𝑈 )
5		dochsnkr2.z	⊢ 0 = ( 0g ‘ 𝑈 )
6		dochsnkr2.a	⊢ + = ( +g ‘ 𝑈 )
7		dochsnkr2.t	⊢ · = ( ·𝑠 ‘ 𝑈 )
8		dochsnkr2.l	⊢ 𝐿 = ( LKer ‘ 𝑈 )
9		dochsnkr2.d	⊢ 𝐷 = ( Scalar ‘ 𝑈 )
10		dochsnkr2.r	⊢ 𝑅 = ( Base ‘ 𝐷 )
11		dochsnkr2.g	⊢ 𝐺 = ( 𝑣 ∈ 𝑉 ↦ ( ℩ 𝑘 ∈ 𝑅 ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑋 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑋 ) ) ) )
12		dochsnkr2.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
13		dochsnkr2.x	⊢ ( 𝜑 → 𝑋 ∈ ( 𝑉 ∖ { 0 } ) )
14	1 3 12	dvhlmod	⊢ ( 𝜑 → 𝑈 ∈ LMod )
15	13	eldifad	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
16		eqid	⊢ ( LSpan ‘ 𝑈 ) = ( LSpan ‘ 𝑈 )
17	4 16	lspsnid	⊢ ( ( 𝑈 ∈ LMod ∧ 𝑋 ∈ 𝑉 ) → 𝑋 ∈ ( ( LSpan ‘ 𝑈 ) ‘ { 𝑋 } ) )
18	14 15 17	syl2anc	⊢ ( 𝜑 → 𝑋 ∈ ( ( LSpan ‘ 𝑈 ) ‘ { 𝑋 } ) )
19	1 2 3 4 5 6 7 8 9 10 11 12 13	dochsnkr2	⊢ ( 𝜑 → ( 𝐿 ‘ 𝐺 ) = ( ⊥ ‘ { 𝑋 } ) )
20	15	snssd	⊢ ( 𝜑 → { 𝑋 } ⊆ 𝑉 )
21	1 3 2 4 16 12 20	dochocsp	⊢ ( 𝜑 → ( ⊥ ‘ ( ( LSpan ‘ 𝑈 ) ‘ { 𝑋 } ) ) = ( ⊥ ‘ { 𝑋 } ) )
22	19 21	eqtr4d	⊢ ( 𝜑 → ( 𝐿 ‘ 𝐺 ) = ( ⊥ ‘ ( ( LSpan ‘ 𝑈 ) ‘ { 𝑋 } ) ) )
23	22	fveq2d	⊢ ( 𝜑 → ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) = ( ⊥ ‘ ( ⊥ ‘ ( ( LSpan ‘ 𝑈 ) ‘ { 𝑋 } ) ) ) )
24		eqid	⊢ ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
25	1 3 4 16 24	dihlsprn	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ∈ 𝑉 ) → ( ( LSpan ‘ 𝑈 ) ‘ { 𝑋 } ) ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) )
26	12 15 25	syl2anc	⊢ ( 𝜑 → ( ( LSpan ‘ 𝑈 ) ‘ { 𝑋 } ) ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) )
27	1 24 2	dochoc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( LSpan ‘ 𝑈 ) ‘ { 𝑋 } ) ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ) → ( ⊥ ‘ ( ⊥ ‘ ( ( LSpan ‘ 𝑈 ) ‘ { 𝑋 } ) ) ) = ( ( LSpan ‘ 𝑈 ) ‘ { 𝑋 } ) )
28	12 26 27	syl2anc	⊢ ( 𝜑 → ( ⊥ ‘ ( ⊥ ‘ ( ( LSpan ‘ 𝑈 ) ‘ { 𝑋 } ) ) ) = ( ( LSpan ‘ 𝑈 ) ‘ { 𝑋 } ) )
29	23 28	eqtr2d	⊢ ( 𝜑 → ( ( LSpan ‘ 𝑈 ) ‘ { 𝑋 } ) = ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) )
30	18 29	eleqtrd	⊢ ( 𝜑 → 𝑋 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) )
31		eldifsni	⊢ ( 𝑋 ∈ ( 𝑉 ∖ { 0 } ) → 𝑋 ≠ 0 )
32	13 31	syl	⊢ ( 𝜑 → 𝑋 ≠ 0 )
33		eldifsn	⊢ ( 𝑋 ∈ ( ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ∖ { 0 } ) ↔ ( 𝑋 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ∧ 𝑋 ≠ 0 ) )
34	30 32 33	sylanbrc	⊢ ( 𝜑 → 𝑋 ∈ ( ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ∖ { 0 } ) )