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 ∧ 𝑊 ∈ ðŧ ) ∧ ( ðđ ∈ ( 𝑇 × ðļ ) ∧ 𝐚 ∈ ( 𝑇 × ðļ ) ) ) → ( ðđ + 𝐚 ) ∈ ( 𝑇 × ðļ ) )