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 ⊢ H = LHyp ⁡ K
dvhvaddcl.t ⊢ T = LTrn ⁡ K ⁡ W
dvhvaddcl.e ⊢ E = TEndo ⁡ K ⁡ W
dvhvaddcl.u ⊢ U = DVecH ⁡ K ⁡ W
dvhvaddcl.d ⊢ D = Scalar ⁡ U
dvhvaddcl.p ⊢ ⨣ ˙ = + D
dvhvaddcl.a ⊢ + ˙ = + U
Assertion dvhvaddcl ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T × E ∧ G ∈ T × E → F + ˙ G ∈ T × E

Proof

Step Hyp Ref Expression
1 dvhvaddcl.h ⊢ H = LHyp ⁡ K
2 dvhvaddcl.t ⊢ T = LTrn ⁡ K ⁡ W
3 dvhvaddcl.e ⊢ E = TEndo ⁡ K ⁡ W
4 dvhvaddcl.u ⊢ U = DVecH ⁡ K ⁡ W
5 dvhvaddcl.d ⊢ D = Scalar ⁡ U
6 dvhvaddcl.p ⊢ ⨣ ˙ = + D
7 dvhvaddcl.a ⊢ + ˙ = + U
8 1 2 3 4 5 7 6 dvhvadd ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T × E ∧ G ∈ T × E → F + ˙ G = 1 st ⁡ F ∘ 1 st ⁡ G 2 nd ⁡ F ⨣ ˙ 2 nd ⁡ G
9 simpl ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T × E ∧ G ∈ T × E → K ∈ HL ∧ W ∈ H
10 xp1st ⊢ F ∈ T × E → 1 st ⁡ F ∈ T
11 10 ad2antrl ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T × E ∧ G ∈ T × E → 1 st ⁡ F ∈ T
12 xp1st ⊢ G ∈ T × E → 1 st ⁡ G ∈ T
13 12 ad2antll ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T × E ∧ G ∈ T × E → 1 st ⁡ G ∈ T
14 1 2 ltrnco ⊢ K ∈ HL ∧ W ∈ H ∧ 1 st ⁡ F ∈ T ∧ 1 st ⁡ G ∈ T → 1 st ⁡ F ∘ 1 st ⁡ G ∈ T
15 9 11 13 14 syl3anc ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T × E ∧ G ∈ T × E → 1 st ⁡ F ∘ 1 st ⁡ G ∈ T
16 eqid ⊢ a ∈ E , b ∈ E ⟼ c ∈ T ⟼ a ⁡ c ∘ b ⁡ c = a ∈ E , b ∈ E ⟼ c ∈ T ⟼ a ⁡ c ∘ b ⁡ c
17 1 2 3 4 5 16 6 dvhfplusr ⊢ K ∈ HL ∧ W ∈ H → ⨣ ˙ = a ∈ E , b ∈ E ⟼ c ∈ T ⟼ a ⁡ c ∘ b ⁡ c
18 17 adantr ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T × E ∧ G ∈ T × E → ⨣ ˙ = a ∈ E , b ∈ E ⟼ c ∈ T ⟼ a ⁡ c ∘ b ⁡ c
19 18 oveqd ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T × E ∧ G ∈ T × E → 2 nd ⁡ F ⨣ ˙ 2 nd ⁡ G = 2 nd ⁡ F a ∈ E , b ∈ E ⟼ c ∈ T ⟼ a ⁡ c ∘ b ⁡ c 2 nd ⁡ G
20 xp2nd ⊢ F ∈ T × E → 2 nd ⁡ F ∈ E
21 20 ad2antrl ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T × E ∧ G ∈ T × E → 2 nd ⁡ F ∈ E
22 xp2nd ⊢ G ∈ T × E → 2 nd ⁡ G ∈ E
23 22 ad2antll ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T × E ∧ G ∈ T × E → 2 nd ⁡ G ∈ E
24 1 2 3 16 tendoplcl ⊢ K ∈ HL ∧ W ∈ H ∧ 2 nd ⁡ F ∈ E ∧ 2 nd ⁡ G ∈ E → 2 nd ⁡ F a ∈ E , b ∈ E ⟼ c ∈ T ⟼ a ⁡ c ∘ b ⁡ c 2 nd ⁡ G ∈ E
25 9 21 23 24 syl3anc ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T × E ∧ G ∈ T × E → 2 nd ⁡ F a ∈ E , b ∈ E ⟼ c ∈ T ⟼ a ⁡ c ∘ b ⁡ c 2 nd ⁡ G ∈ E
26 19 25 eqeltrd ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T × E ∧ G ∈ T × E → 2 nd ⁡ F ⨣ ˙ 2 nd ⁡ G ∈ E
27 opelxpi ⊢ 1 st ⁡ F ∘ 1 st ⁡ G ∈ T ∧ 2 nd ⁡ F ⨣ ˙ 2 nd ⁡ G ∈ E → 1 st ⁡ F ∘ 1 st ⁡ G 2 nd ⁡ F ⨣ ˙ 2 nd ⁡ G ∈ T × E
28 15 26 27 syl2anc ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T × E ∧ G ∈ T × E → 1 st ⁡ F ∘ 1 st ⁡ G 2 nd ⁡ F ⨣ ˙ 2 nd ⁡ G ∈ T × E
29 8 28 eqeltrd ⊢ K ∈ HL ∧ W ∈ H ∧ F ∈ T × E ∧ G ∈ T × E → F + ˙ G ∈ T × E