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 ∧ 𝑊𝐻 ) ∧ ( 𝐹 ∈ ( 𝑇 × 𝐸 ) ∧ 𝐺 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 𝐹 + 𝐺 ) ∈ ( 𝑇 × 𝐸 ) )