Theorem dia1dim2

Description: Two expressions for a 1-dimensional subspace of partial vector space A (when F is a nonzero vector i.e. non-identity translation). (Contributed by NM, 15-Jan-2014) (Revised by Mario Carneiro, 22-Jun-2014)

	Ref	Expression
Hypotheses	dia1dim2.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	dia1dim2.t	⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
	dia1dim2.r	⊢ 𝑅 = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
	dva1dim2.u	⊢ 𝑈 = ( ( DVecA ‘ 𝐾 ) ‘ 𝑊 )
	dia1dim2.i	⊢ 𝐼 = ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 )
	dva1dim2.n	⊢ 𝑁 = ( LSpan ‘ 𝑈 )
Assertion	dia1dim2	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) → ( 𝐼 ‘ ( 𝑅 ‘ 𝐹 ) ) = ( 𝑁 ‘ { 𝐹 } ) )

Proof

Step	Hyp	Ref	Expression
1		dia1dim2.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2		dia1dim2.t	⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
3		dia1dim2.r	⊢ 𝑅 = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
4		dva1dim2.u	⊢ 𝑈 = ( ( DVecA ‘ 𝐾 ) ‘ 𝑊 )
5		dia1dim2.i	⊢ 𝐼 = ( ( DIsoA ‘ 𝐾 ) ‘ 𝑊 )
6		dva1dim2.n	⊢ 𝑁 = ( LSpan ‘ 𝑈 )
7		eqid	⊢ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 )
8		eqid	⊢ ( Scalar ‘ 𝑈 ) = ( Scalar ‘ 𝑈 )
9		eqid	⊢ ( Base ‘ ( Scalar ‘ 𝑈 ) ) = ( Base ‘ ( Scalar ‘ 𝑈 ) )
10	1 7 4 8 9	dvabase	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( Base ‘ ( Scalar ‘ 𝑈 ) ) = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) )
11	10	adantr	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) → ( Base ‘ ( Scalar ‘ 𝑈 ) ) = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) )
12	11	rexeqdv	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) → ( ∃ 𝑠 ∈ ( Base ‘ ( Scalar ‘ 𝑈 ) ) 𝑔 = ( 𝑠 ( ·𝑠 ‘ 𝑈 ) 𝐹 ) ↔ ∃ 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) 𝑔 = ( 𝑠 ( ·𝑠 ‘ 𝑈 ) 𝐹 ) ) )
13		eqid	⊢ ( ·𝑠 ‘ 𝑈 ) = ( ·𝑠 ‘ 𝑈 )
14	1 2 7 4 13	dvavsca	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ∧ 𝐹 ∈ 𝑇 ) ) → ( 𝑠 ( ·𝑠 ‘ 𝑈 ) 𝐹 ) = ( 𝑠 ‘ 𝐹 ) )
15	14	anass1rs	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) ∧ 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) → ( 𝑠 ( ·𝑠 ‘ 𝑈 ) 𝐹 ) = ( 𝑠 ‘ 𝐹 ) )
16	15	eqeq2d	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) ∧ 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) → ( 𝑔 = ( 𝑠 ( ·𝑠 ‘ 𝑈 ) 𝐹 ) ↔ 𝑔 = ( 𝑠 ‘ 𝐹 ) ) )
17	16	rexbidva	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) → ( ∃ 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) 𝑔 = ( 𝑠 ( ·𝑠 ‘ 𝑈 ) 𝐹 ) ↔ ∃ 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) 𝑔 = ( 𝑠 ‘ 𝐹 ) ) )
18	12 17	bitrd	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) → ( ∃ 𝑠 ∈ ( Base ‘ ( Scalar ‘ 𝑈 ) ) 𝑔 = ( 𝑠 ( ·𝑠 ‘ 𝑈 ) 𝐹 ) ↔ ∃ 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) 𝑔 = ( 𝑠 ‘ 𝐹 ) ) )
19	18	abbidv	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) → { 𝑔 ∣ ∃ 𝑠 ∈ ( Base ‘ ( Scalar ‘ 𝑈 ) ) 𝑔 = ( 𝑠 ( ·𝑠 ‘ 𝑈 ) 𝐹 ) } = { 𝑔 ∣ ∃ 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) 𝑔 = ( 𝑠 ‘ 𝐹 ) } )
20	1 4	dvalvec	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 𝑈 ∈ LVec )
21	20	adantr	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) → 𝑈 ∈ LVec )
22		lveclmod	⊢ ( 𝑈 ∈ LVec → 𝑈 ∈ LMod )
23	21 22	syl	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) → 𝑈 ∈ LMod )
24		simpr	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) → 𝐹 ∈ 𝑇 )
25		eqid	⊢ ( Base ‘ 𝑈 ) = ( Base ‘ 𝑈 )
26	1 2 4 25	dvavbase	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( Base ‘ 𝑈 ) = 𝑇 )
27	26	adantr	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) → ( Base ‘ 𝑈 ) = 𝑇 )
28	24 27	eleqtrrd	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) → 𝐹 ∈ ( Base ‘ 𝑈 ) )
29	8 9 25 13 6	lspsn	⊢ ( ( 𝑈 ∈ LMod ∧ 𝐹 ∈ ( Base ‘ 𝑈 ) ) → ( 𝑁 ‘ { 𝐹 } ) = { 𝑔 ∣ ∃ 𝑠 ∈ ( Base ‘ ( Scalar ‘ 𝑈 ) ) 𝑔 = ( 𝑠 ( ·𝑠 ‘ 𝑈 ) 𝐹 ) } )
30	23 28 29	syl2anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) → ( 𝑁 ‘ { 𝐹 } ) = { 𝑔 ∣ ∃ 𝑠 ∈ ( Base ‘ ( Scalar ‘ 𝑈 ) ) 𝑔 = ( 𝑠 ( ·𝑠 ‘ 𝑈 ) 𝐹 ) } )
31	1 2 3 7 5	dia1dim	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) → ( 𝐼 ‘ ( 𝑅 ‘ 𝐹 ) ) = { 𝑔 ∣ ∃ 𝑠 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) 𝑔 = ( 𝑠 ‘ 𝐹 ) } )
32	19 30 31	3eqtr4rd	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) → ( 𝐼 ‘ ( 𝑅 ‘ 𝐹 ) ) = ( 𝑁 ‘ { 𝐹 } ) )