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