This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dvhvscacl

Description: Closure of the scalar product operation for the constructed full vector space H. (Contributed by NM, 12-Feb-2014)

Ref Expression
Hypotheses dvhfvsca.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
dvhfvsca.t ⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
dvhfvsca.e ⊢ 𝐸 = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 )
dvhfvsca.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
dvhfvsca.s ⊢ · = ( ·𝑠 ‘ 𝑈 )
Assertion dvhvscacl ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑅 ∈ 𝐸 ∧ 𝐹 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 𝑅 · 𝐹 ) ∈ ( 𝑇 × 𝐸 ) )

Proof

Step Hyp Ref Expression
1 dvhfvsca.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2 dvhfvsca.t ⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
3 dvhfvsca.e ⊢ 𝐸 = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 )
4 dvhfvsca.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
5 dvhfvsca.s ⊢ · = ( ·𝑠 ‘ 𝑈 )
6 1 2 3 4 5 dvhvsca ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑅 ∈ 𝐸 ∧ 𝐹 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 𝑅 · 𝐹 ) = ⟨ ( 𝑅 ‘ ( 1st ‘ 𝐹 ) ) , ( 𝑅 ∘ ( 2nd ‘ 𝐹 ) ) ⟩ )
7 simpl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑅 ∈ 𝐸 ∧ 𝐹 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
8 simprl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑅 ∈ 𝐸 ∧ 𝐹 ∈ ( 𝑇 × 𝐸 ) ) ) → 𝑅 ∈ 𝐸 )
9 xp1st ⊢ ( 𝐹 ∈ ( 𝑇 × 𝐸 ) → ( 1st ‘ 𝐹 ) ∈ 𝑇 )
10 9 ad2antll ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑅 ∈ 𝐸 ∧ 𝐹 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 1st ‘ 𝐹 ) ∈ 𝑇 )
11 1 2 3 tendocl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑅 ∈ 𝐸 ∧ ( 1st ‘ 𝐹 ) ∈ 𝑇 ) → ( 𝑅 ‘ ( 1st ‘ 𝐹 ) ) ∈ 𝑇 )
12 7 8 10 11 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑅 ∈ 𝐸 ∧ 𝐹 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 𝑅 ‘ ( 1st ‘ 𝐹 ) ) ∈ 𝑇 )
13 xp2nd ⊢ ( 𝐹 ∈ ( 𝑇 × 𝐸 ) → ( 2nd ‘ 𝐹 ) ∈ 𝐸 )
14 13 ad2antll ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑅 ∈ 𝐸 ∧ 𝐹 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 2nd ‘ 𝐹 ) ∈ 𝐸 )
15 1 3 tendococl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑅 ∈ 𝐸 ∧ ( 2nd ‘ 𝐹 ) ∈ 𝐸 ) → ( 𝑅 ∘ ( 2nd ‘ 𝐹 ) ) ∈ 𝐸 )
16 7 8 14 15 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑅 ∈ 𝐸 ∧ 𝐹 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 𝑅 ∘ ( 2nd ‘ 𝐹 ) ) ∈ 𝐸 )
17 opelxpi ⊢ ( ( ( 𝑅 ‘ ( 1st ‘ 𝐹 ) ) ∈ 𝑇 ∧ ( 𝑅 ∘ ( 2nd ‘ 𝐹 ) ) ∈ 𝐸 ) → ⟨ ( 𝑅 ‘ ( 1st ‘ 𝐹 ) ) , ( 𝑅 ∘ ( 2nd ‘ 𝐹 ) ) ⟩ ∈ ( 𝑇 × 𝐸 ) )
18 12 16 17 syl2anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑅 ∈ 𝐸 ∧ 𝐹 ∈ ( 𝑇 × 𝐸 ) ) ) → ⟨ ( 𝑅 ‘ ( 1st ‘ 𝐹 ) ) , ( 𝑅 ∘ ( 2nd ‘ 𝐹 ) ) ⟩ ∈ ( 𝑇 × 𝐸 ) )
19 6 18 eqeltrd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑅 ∈ 𝐸 ∧ 𝐹 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 𝑅 · 𝐹 ) ∈ ( 𝑇 × 𝐸 ) )