Metamath Proof Explorer

Theorem dvhvaddcl

Description: Closure of the vector sum operation for the constructed full vector space H. (Contributed by NM, 26-Oct-2013) (Revised by Mario Carneiro, 23-Jun-2014)

Ref Expression
Hypotheses dvhvaddcl.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
dvhvaddcl.t ⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
dvhvaddcl.e ⊢ 𝐸 = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 )
dvhvaddcl.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
dvhvaddcl.d ⊢ 𝐷 = ( Scalar ‘ 𝑈 )
dvhvaddcl.p ⊢ ⨣ = ( +g ‘ 𝐷 )
dvhvaddcl.a ⊢ + = ( +g ‘ 𝑈 )
Assertion dvhvaddcl ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ ( 𝑇 × 𝐸 ) ∧ 𝐺 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 𝐹 + 𝐺 ) ∈ ( 𝑇 × 𝐸 ) )

Proof

Step Hyp Ref Expression
1 dvhvaddcl.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2 dvhvaddcl.t ⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
3 dvhvaddcl.e ⊢ 𝐸 = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 )
4 dvhvaddcl.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
5 dvhvaddcl.d ⊢ 𝐷 = ( Scalar ‘ 𝑈 )
6 dvhvaddcl.p ⊢ ⨣ = ( +g ‘ 𝐷 )
7 dvhvaddcl.a ⊢ + = ( +g ‘ 𝑈 )
8 1 2 3 4 5 7 6 dvhvadd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ ( 𝑇 × 𝐸 ) ∧ 𝐺 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 𝐹 + 𝐺 ) = ⟨ ( ( 1st ‘ 𝐹 ) ∘ ( 1st ‘ 𝐺 ) ) , ( ( 2nd ‘ 𝐹 ) ⨣ ( 2nd ‘ 𝐺 ) ) ⟩ )
9 simpl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ ( 𝑇 × 𝐸 ) ∧ 𝐺 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
10 xp1st ⊢ ( 𝐹 ∈ ( 𝑇 × 𝐸 ) → ( 1st ‘ 𝐹 ) ∈ 𝑇 )
11 10 ad2antrl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ ( 𝑇 × 𝐸 ) ∧ 𝐺 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 1st ‘ 𝐹 ) ∈ 𝑇 )
12 xp1st ⊢ ( 𝐺 ∈ ( 𝑇 × 𝐸 ) → ( 1st ‘ 𝐺 ) ∈ 𝑇 )
13 12 ad2antll ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ ( 𝑇 × 𝐸 ) ∧ 𝐺 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 1st ‘ 𝐺 ) ∈ 𝑇 )
14 1 2 ltrnco ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 1st ‘ 𝐹 ) ∈ 𝑇 ∧ ( 1st ‘ 𝐺 ) ∈ 𝑇 ) → ( ( 1st ‘ 𝐹 ) ∘ ( 1st ‘ 𝐺 ) ) ∈ 𝑇 )
15 9 11 13 14 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ ( 𝑇 × 𝐸 ) ∧ 𝐺 ∈ ( 𝑇 × 𝐸 ) ) ) → ( ( 1st ‘ 𝐹 ) ∘ ( 1st ‘ 𝐺 ) ) ∈ 𝑇 )
16 eqid ⊢ ( 𝑎 ∈ 𝐸 , 𝑏 ∈ 𝐸 ↦ ( 𝑐 ∈ 𝑇 ↦ ( ( 𝑎 ‘ 𝑐 ) ∘ ( 𝑏 ‘ 𝑐 ) ) ) ) = ( 𝑎 ∈ 𝐸 , 𝑏 ∈ 𝐸 ↦ ( 𝑐 ∈ 𝑇 ↦ ( ( 𝑎 ‘ 𝑐 ) ∘ ( 𝑏 ‘ 𝑐 ) ) ) )
17 1 2 3 4 5 16 6 dvhfplusr ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ⨣ = ( 𝑎 ∈ 𝐸 , 𝑏 ∈ 𝐸 ↦ ( 𝑐 ∈ 𝑇 ↦ ( ( 𝑎 ‘ 𝑐 ) ∘ ( 𝑏 ‘ 𝑐 ) ) ) ) )
18 17 adantr ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ ( 𝑇 × 𝐸 ) ∧ 𝐺 ∈ ( 𝑇 × 𝐸 ) ) ) → ⨣ = ( 𝑎 ∈ 𝐸 , 𝑏 ∈ 𝐸 ↦ ( 𝑐 ∈ 𝑇 ↦ ( ( 𝑎 ‘ 𝑐 ) ∘ ( 𝑏 ‘ 𝑐 ) ) ) ) )
19 18 oveqd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ ( 𝑇 × 𝐸 ) ∧ 𝐺 ∈ ( 𝑇 × 𝐸 ) ) ) → ( ( 2nd ‘ 𝐹 ) ⨣ ( 2nd ‘ 𝐺 ) ) = ( ( 2nd ‘ 𝐹 ) ( 𝑎 ∈ 𝐸 , 𝑏 ∈ 𝐸 ↦ ( 𝑐 ∈ 𝑇 ↦ ( ( 𝑎 ‘ 𝑐 ) ∘ ( 𝑏 ‘ 𝑐 ) ) ) ) ( 2nd ‘ 𝐺 ) ) )
20 xp2nd ⊢ ( 𝐹 ∈ ( 𝑇 × 𝐸 ) → ( 2nd ‘ 𝐹 ) ∈ 𝐸 )
21 20 ad2antrl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ ( 𝑇 × 𝐸 ) ∧ 𝐺 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 2nd ‘ 𝐹 ) ∈ 𝐸 )
22 xp2nd ⊢ ( 𝐺 ∈ ( 𝑇 × 𝐸 ) → ( 2nd ‘ 𝐺 ) ∈ 𝐸 )
23 22 ad2antll ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ ( 𝑇 × 𝐸 ) ∧ 𝐺 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 2nd ‘ 𝐺 ) ∈ 𝐸 )
24 1 2 3 16 tendoplcl ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 2nd ‘ 𝐹 ) ∈ 𝐸 ∧ ( 2nd ‘ 𝐺 ) ∈ 𝐸 ) → ( ( 2nd ‘ 𝐹 ) ( 𝑎 ∈ 𝐸 , 𝑏 ∈ 𝐸 ↦ ( 𝑐 ∈ 𝑇 ↦ ( ( 𝑎 ‘ 𝑐 ) ∘ ( 𝑏 ‘ 𝑐 ) ) ) ) ( 2nd ‘ 𝐺 ) ) ∈ 𝐸 )
25 9 21 23 24 syl3anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ ( 𝑇 × 𝐸 ) ∧ 𝐺 ∈ ( 𝑇 × 𝐸 ) ) ) → ( ( 2nd ‘ 𝐹 ) ( 𝑎 ∈ 𝐸 , 𝑏 ∈ 𝐸 ↦ ( 𝑐 ∈ 𝑇 ↦ ( ( 𝑎 ‘ 𝑐 ) ∘ ( 𝑏 ‘ 𝑐 ) ) ) ) ( 2nd ‘ 𝐺 ) ) ∈ 𝐸 )
26 19 25 eqeltrd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ ( 𝑇 × 𝐸 ) ∧ 𝐺 ∈ ( 𝑇 × 𝐸 ) ) ) → ( ( 2nd ‘ 𝐹 ) ⨣ ( 2nd ‘ 𝐺 ) ) ∈ 𝐸 )
27 opelxpi ⊢ ( ( ( ( 1st ‘ 𝐹 ) ∘ ( 1st ‘ 𝐺 ) ) ∈ 𝑇 ∧ ( ( 2nd ‘ 𝐹 ) ⨣ ( 2nd ‘ 𝐺 ) ) ∈ 𝐸 ) → ⟨ ( ( 1st ‘ 𝐹 ) ∘ ( 1st ‘ 𝐺 ) ) , ( ( 2nd ‘ 𝐹 ) ⨣ ( 2nd ‘ 𝐺 ) ) ⟩ ∈ ( 𝑇 × 𝐸 ) )
28 15 26 27 syl2anc ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ ( 𝑇 × 𝐸 ) ∧ 𝐺 ∈ ( 𝑇 × 𝐸 ) ) ) → ⟨ ( ( 1st ‘ 𝐹 ) ∘ ( 1st ‘ 𝐺 ) ) , ( ( 2nd ‘ 𝐹 ) ⨣ ( 2nd ‘ 𝐺 ) ) ⟩ ∈ ( 𝑇 × 𝐸 ) )
29 8 28 eqeltrd ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ ( 𝑇 × 𝐸 ) ∧ 𝐺 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 𝐹 + 𝐺 ) ∈ ( 𝑇 × 𝐸 ) )