Metamath Proof Explorer

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 ∧ 𝑊 ∈ 𝐻 ) ∧ 𝐹 ∈ 𝑇 ) → ( 𝐼 ‘ ( 𝑅 ‘ 𝐹 ) ) = ( 𝑁 ‘ { ⟨ 𝐹 , 𝑂 ⟩ } ) )