Theorem dib1dim2

Description: Two expressions for a 1-dimensional subspace of vector space H (when F is a nonzero vector i.e. non-identity translation). (Contributed by NM, 24-Feb-2014)

	Ref	Expression
Hypotheses	dib1dim2.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
	dib1dim2.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	dib1dim2.t	⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
	dib1dim2.r	⊢ 𝑅 = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
	dib1dim2.o	⊢ 𝑂 = ( ℎ ∈ 𝑇 ↦ ( I ↾ 𝐵 ) )
	dib1dim2.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
	dib1dim2.i	⊢ 𝐼 = ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 )
	dib1dim2.n	⊢ 𝑁 = ( LSpan ‘ 𝑈 )
Assertion	dib1dim2	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) → ( 𝐼 ‘ ( 𝑅 ‘ 𝐹 ) ) = ( 𝑁 ‘ { ⟨ 𝐹 , 𝑂 ⟩ } ) )

Proof

Step	Hyp	Ref	Expression
1		dib1dim2.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
2		dib1dim2.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
3		dib1dim2.t	⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
4		dib1dim2.r	⊢ 𝑅 = ( ( trL ‘ 𝐾 ) ‘ 𝑊 )
5		dib1dim2.o	⊢ 𝑂 = ( ℎ ∈ 𝑇 ↦ ( I ↾ 𝐵 ) )
6		dib1dim2.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
7		dib1dim2.i	⊢ 𝐼 = ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 )
8		dib1dim2.n	⊢ 𝑁 = ( LSpan ‘ 𝑈 )
9		df-rab	⊢ { 𝑢 ∈ ( 𝑇 × ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) ∣ ∃ 𝑣 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) 𝑢 = ⟨ ( 𝑣 ‘ 𝐹 ) , 𝑂 ⟩ } = { 𝑢 ∣ ( 𝑢 ∈ ( 𝑇 × ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) ∧ ∃ 𝑣 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) 𝑢 = ⟨ ( 𝑣 ‘ 𝐹 ) , 𝑂 ⟩ ) }
10		eqid	⊢ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 )
11	1 2 3 4 10 5 7	dib1dim	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) → ( 𝐼 ‘ ( 𝑅 ‘ 𝐹 ) ) = { 𝑢 ∈ ( 𝑇 × ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) ∣ ∃ 𝑣 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) 𝑢 = ⟨ ( 𝑣 ‘ 𝐹 ) , 𝑂 ⟩ } )
12		eqid	⊢ ( Scalar ‘ 𝑈 ) = ( Scalar ‘ 𝑈 )
13		eqid	⊢ ( Base ‘ ( Scalar ‘ 𝑈 ) ) = ( Base ‘ ( Scalar ‘ 𝑈 ) )
14	2 10 6 12 13	dvhbase	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( Base ‘ ( Scalar ‘ 𝑈 ) ) = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) )
15	14	adantr	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) → ( Base ‘ ( Scalar ‘ 𝑈 ) ) = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) )
16	15	rexeqdv	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) → ( ∃ 𝑣 ∈ ( Base ‘ ( Scalar ‘ 𝑈 ) ) 𝑢 = ( 𝑣 ( ·𝑠 ‘ 𝑈 ) ⟨ 𝐹 , 𝑂 ⟩ ) ↔ ∃ 𝑣 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) 𝑢 = ( 𝑣 ( ·𝑠 ‘ 𝑈 ) ⟨ 𝐹 , 𝑂 ⟩ ) ) )
17		simpll	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) ∧ 𝑣 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
18		simpr	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) ∧ 𝑣 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) → 𝑣 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) )
19		simplr	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) ∧ 𝑣 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) → 𝐹 ∈ 𝑇 )
20	1 2 3 10 5	tendo0cl	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 𝑂 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) )
21	20	ad2antrr	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) ∧ 𝑣 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) → 𝑂 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) )
22		eqid	⊢ ( ·𝑠 ‘ 𝑈 ) = ( ·𝑠 ‘ 𝑈 )
23	2 3 10 6 22	dvhopvsca	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑣 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ∧ 𝐹 ∈ 𝑇 ∧ 𝑂 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) ) → ( 𝑣 ( ·𝑠 ‘ 𝑈 ) ⟨ 𝐹 , 𝑂 ⟩ ) = ⟨ ( 𝑣 ‘ 𝐹 ) , ( 𝑣 ∘ 𝑂 ) ⟩ )
24	17 18 19 21 23	syl13anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) ∧ 𝑣 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) → ( 𝑣 ( ·𝑠 ‘ 𝑈 ) ⟨ 𝐹 , 𝑂 ⟩ ) = ⟨ ( 𝑣 ‘ 𝐹 ) , ( 𝑣 ∘ 𝑂 ) ⟩ )
25	1 2 3 10 5	tendo0mulr	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑣 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) → ( 𝑣 ∘ 𝑂 ) = 𝑂 )
26	25	adantlr	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) ∧ 𝑣 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) → ( 𝑣 ∘ 𝑂 ) = 𝑂 )
27	26	opeq2d	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) ∧ 𝑣 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) → ⟨ ( 𝑣 ‘ 𝐹 ) , ( 𝑣 ∘ 𝑂 ) ⟩ = ⟨ ( 𝑣 ‘ 𝐹 ) , 𝑂 ⟩ )
28	24 27	eqtrd	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) ∧ 𝑣 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) → ( 𝑣 ( ·𝑠 ‘ 𝑈 ) ⟨ 𝐹 , 𝑂 ⟩ ) = ⟨ ( 𝑣 ‘ 𝐹 ) , 𝑂 ⟩ )
29	28	eqeq2d	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) ∧ 𝑣 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) → ( 𝑢 = ( 𝑣 ( ·𝑠 ‘ 𝑈 ) ⟨ 𝐹 , 𝑂 ⟩ ) ↔ 𝑢 = ⟨ ( 𝑣 ‘ 𝐹 ) , 𝑂 ⟩ ) )
30	29	rexbidva	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) → ( ∃ 𝑣 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) 𝑢 = ( 𝑣 ( ·𝑠 ‘ 𝑈 ) ⟨ 𝐹 , 𝑂 ⟩ ) ↔ ∃ 𝑣 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) 𝑢 = ⟨ ( 𝑣 ‘ 𝐹 ) , 𝑂 ⟩ ) )
31	2 3 10	tendocl	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑣 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ∧ 𝐹 ∈ 𝑇 ) → ( 𝑣 ‘ 𝐹 ) ∈ 𝑇 )
32	31	3expa	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑣 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) ∧ 𝐹 ∈ 𝑇 ) → ( 𝑣 ‘ 𝐹 ) ∈ 𝑇 )
33	32	an32s	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) ∧ 𝑣 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) → ( 𝑣 ‘ 𝐹 ) ∈ 𝑇 )
34		opelxpi	⊢ ( ( ( 𝑣 ‘ 𝐹 ) ∈ 𝑇 ∧ 𝑂 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) → ⟨ ( 𝑣 ‘ 𝐹 ) , 𝑂 ⟩ ∈ ( 𝑇 × ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) )
35	33 21 34	syl2anc	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) ∧ 𝑣 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) → ⟨ ( 𝑣 ‘ 𝐹 ) , 𝑂 ⟩ ∈ ( 𝑇 × ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) )
36		eleq1a	⊢ ( ⟨ ( 𝑣 ‘ 𝐹 ) , 𝑂 ⟩ ∈ ( 𝑇 × ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) → ( 𝑢 = ⟨ ( 𝑣 ‘ 𝐹 ) , 𝑂 ⟩ → 𝑢 ∈ ( 𝑇 × ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) ) )
37	35 36	syl	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) ∧ 𝑣 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) → ( 𝑢 = ⟨ ( 𝑣 ‘ 𝐹 ) , 𝑂 ⟩ → 𝑢 ∈ ( 𝑇 × ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) ) )
38	37	rexlimdva	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) → ( ∃ 𝑣 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) 𝑢 = ⟨ ( 𝑣 ‘ 𝐹 ) , 𝑂 ⟩ → 𝑢 ∈ ( 𝑇 × ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) ) )
39	38	pm4.71rd	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) → ( ∃ 𝑣 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) 𝑢 = ⟨ ( 𝑣 ‘ 𝐹 ) , 𝑂 ⟩ ↔ ( 𝑢 ∈ ( 𝑇 × ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) ∧ ∃ 𝑣 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) 𝑢 = ⟨ ( 𝑣 ‘ 𝐹 ) , 𝑂 ⟩ ) ) )
40	16 30 39	3bitrd	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) → ( ∃ 𝑣 ∈ ( Base ‘ ( Scalar ‘ 𝑈 ) ) 𝑢 = ( 𝑣 ( ·𝑠 ‘ 𝑈 ) ⟨ 𝐹 , 𝑂 ⟩ ) ↔ ( 𝑢 ∈ ( 𝑇 × ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) ∧ ∃ 𝑣 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) 𝑢 = ⟨ ( 𝑣 ‘ 𝐹 ) , 𝑂 ⟩ ) ) )
41	40	abbidv	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) → { 𝑢 ∣ ∃ 𝑣 ∈ ( Base ‘ ( Scalar ‘ 𝑈 ) ) 𝑢 = ( 𝑣 ( ·𝑠 ‘ 𝑈 ) ⟨ 𝐹 , 𝑂 ⟩ ) } = { 𝑢 ∣ ( 𝑢 ∈ ( 𝑇 × ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) ∧ ∃ 𝑣 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) 𝑢 = ⟨ ( 𝑣 ‘ 𝐹 ) , 𝑂 ⟩ ) } )
42	9 11 41	3eqtr4a	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) → ( 𝐼 ‘ ( 𝑅 ‘ 𝐹 ) ) = { 𝑢 ∣ ∃ 𝑣 ∈ ( Base ‘ ( Scalar ‘ 𝑈 ) ) 𝑢 = ( 𝑣 ( ·𝑠 ‘ 𝑈 ) ⟨ 𝐹 , 𝑂 ⟩ ) } )
43		simpl	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
44	2 6 43	dvhlmod	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) → 𝑈 ∈ LMod )
45		simpr	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) → 𝐹 ∈ 𝑇 )
46	20	adantr	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) → 𝑂 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) )
47		eqid	⊢ ( Base ‘ 𝑈 ) = ( Base ‘ 𝑈 )
48	2 3 10 6 47	dvhelvbasei	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝑂 ∈ ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) ) ) → ⟨ 𝐹 , 𝑂 ⟩ ∈ ( Base ‘ 𝑈 ) )
49	43 45 46 48	syl12anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) → ⟨ 𝐹 , 𝑂 ⟩ ∈ ( Base ‘ 𝑈 ) )
50	12 13 47 22 8	lspsn	⊢ ( ( 𝑈 ∈ LMod ∧ ⟨ 𝐹 , 𝑂 ⟩ ∈ ( Base ‘ 𝑈 ) ) → ( 𝑁 ‘ { ⟨ 𝐹 , 𝑂 ⟩ } ) = { 𝑢 ∣ ∃ 𝑣 ∈ ( Base ‘ ( Scalar ‘ 𝑈 ) ) 𝑢 = ( 𝑣 ( ·𝑠 ‘ 𝑈 ) ⟨ 𝐹 , 𝑂 ⟩ ) } )
51	44 49 50	syl2anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) → ( 𝑁 ‘ { ⟨ 𝐹 , 𝑂 ⟩ } ) = { 𝑢 ∣ ∃ 𝑣 ∈ ( Base ‘ ( Scalar ‘ 𝑈 ) ) 𝑢 = ( 𝑣 ( ·𝑠 ‘ 𝑈 ) ⟨ 𝐹 , 𝑂 ⟩ ) } )
52	42 51	eqtr4d	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) → ( 𝐼 ‘ ( 𝑅 ‘ 𝐹 ) ) = ( 𝑁 ‘ { ⟨ 𝐹 , 𝑂 ⟩ } ) )