Step |
Hyp |
Ref |
Expression |
1 |
|
dvhvadd.h |
⊢ 𝐻 = ( LHyp ‘ 𝐾 ) |
2 |
|
dvhvadd.t |
⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) |
3 |
|
dvhvadd.e |
⊢ 𝐸 = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 ) |
4 |
|
dvhvadd.u |
⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 ) |
5 |
|
dvhvadd.f |
⊢ 𝐷 = ( Scalar ‘ 𝑈 ) |
6 |
|
dvhvadd.s |
⊢ + = ( +g ‘ 𝑈 ) |
7 |
|
dvhvadd.p |
⊢ ⨣ = ( +g ‘ 𝐷 ) |
8 |
|
simp1 |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝑄 ∈ 𝐸 ) ∧ ( 𝐺 ∈ 𝑇 ∧ 𝑅 ∈ 𝐸 ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ) |
9 |
|
opelxpi |
⊢ ( ( 𝐹 ∈ 𝑇 ∧ 𝑄 ∈ 𝐸 ) → 〈 𝐹 , 𝑄 〉 ∈ ( 𝑇 × 𝐸 ) ) |
10 |
9
|
3ad2ant2 |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝑄 ∈ 𝐸 ) ∧ ( 𝐺 ∈ 𝑇 ∧ 𝑅 ∈ 𝐸 ) ) → 〈 𝐹 , 𝑄 〉 ∈ ( 𝑇 × 𝐸 ) ) |
11 |
|
opelxpi |
⊢ ( ( 𝐺 ∈ 𝑇 ∧ 𝑅 ∈ 𝐸 ) → 〈 𝐺 , 𝑅 〉 ∈ ( 𝑇 × 𝐸 ) ) |
12 |
11
|
3ad2ant3 |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝑄 ∈ 𝐸 ) ∧ ( 𝐺 ∈ 𝑇 ∧ 𝑅 ∈ 𝐸 ) ) → 〈 𝐺 , 𝑅 〉 ∈ ( 𝑇 × 𝐸 ) ) |
13 |
1 2 3 4 5 6 7
|
dvhvadd |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 〈 𝐹 , 𝑄 〉 ∈ ( 𝑇 × 𝐸 ) ∧ 〈 𝐺 , 𝑅 〉 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 〈 𝐹 , 𝑄 〉 + 〈 𝐺 , 𝑅 〉 ) = 〈 ( ( 1st ‘ 〈 𝐹 , 𝑄 〉 ) ∘ ( 1st ‘ 〈 𝐺 , 𝑅 〉 ) ) , ( ( 2nd ‘ 〈 𝐹 , 𝑄 〉 ) ⨣ ( 2nd ‘ 〈 𝐺 , 𝑅 〉 ) ) 〉 ) |
14 |
8 10 12 13
|
syl12anc |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝑄 ∈ 𝐸 ) ∧ ( 𝐺 ∈ 𝑇 ∧ 𝑅 ∈ 𝐸 ) ) → ( 〈 𝐹 , 𝑄 〉 + 〈 𝐺 , 𝑅 〉 ) = 〈 ( ( 1st ‘ 〈 𝐹 , 𝑄 〉 ) ∘ ( 1st ‘ 〈 𝐺 , 𝑅 〉 ) ) , ( ( 2nd ‘ 〈 𝐹 , 𝑄 〉 ) ⨣ ( 2nd ‘ 〈 𝐺 , 𝑅 〉 ) ) 〉 ) |
15 |
|
op1stg |
⊢ ( ( 𝐹 ∈ 𝑇 ∧ 𝑄 ∈ 𝐸 ) → ( 1st ‘ 〈 𝐹 , 𝑄 〉 ) = 𝐹 ) |
16 |
15
|
3ad2ant2 |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝑄 ∈ 𝐸 ) ∧ ( 𝐺 ∈ 𝑇 ∧ 𝑅 ∈ 𝐸 ) ) → ( 1st ‘ 〈 𝐹 , 𝑄 〉 ) = 𝐹 ) |
17 |
|
op1stg |
⊢ ( ( 𝐺 ∈ 𝑇 ∧ 𝑅 ∈ 𝐸 ) → ( 1st ‘ 〈 𝐺 , 𝑅 〉 ) = 𝐺 ) |
18 |
17
|
3ad2ant3 |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝑄 ∈ 𝐸 ) ∧ ( 𝐺 ∈ 𝑇 ∧ 𝑅 ∈ 𝐸 ) ) → ( 1st ‘ 〈 𝐺 , 𝑅 〉 ) = 𝐺 ) |
19 |
16 18
|
coeq12d |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝑄 ∈ 𝐸 ) ∧ ( 𝐺 ∈ 𝑇 ∧ 𝑅 ∈ 𝐸 ) ) → ( ( 1st ‘ 〈 𝐹 , 𝑄 〉 ) ∘ ( 1st ‘ 〈 𝐺 , 𝑅 〉 ) ) = ( 𝐹 ∘ 𝐺 ) ) |
20 |
|
op2ndg |
⊢ ( ( 𝐹 ∈ 𝑇 ∧ 𝑄 ∈ 𝐸 ) → ( 2nd ‘ 〈 𝐹 , 𝑄 〉 ) = 𝑄 ) |
21 |
20
|
3ad2ant2 |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝑄 ∈ 𝐸 ) ∧ ( 𝐺 ∈ 𝑇 ∧ 𝑅 ∈ 𝐸 ) ) → ( 2nd ‘ 〈 𝐹 , 𝑄 〉 ) = 𝑄 ) |
22 |
|
op2ndg |
⊢ ( ( 𝐺 ∈ 𝑇 ∧ 𝑅 ∈ 𝐸 ) → ( 2nd ‘ 〈 𝐺 , 𝑅 〉 ) = 𝑅 ) |
23 |
22
|
3ad2ant3 |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝑄 ∈ 𝐸 ) ∧ ( 𝐺 ∈ 𝑇 ∧ 𝑅 ∈ 𝐸 ) ) → ( 2nd ‘ 〈 𝐺 , 𝑅 〉 ) = 𝑅 ) |
24 |
21 23
|
oveq12d |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝑄 ∈ 𝐸 ) ∧ ( 𝐺 ∈ 𝑇 ∧ 𝑅 ∈ 𝐸 ) ) → ( ( 2nd ‘ 〈 𝐹 , 𝑄 〉 ) ⨣ ( 2nd ‘ 〈 𝐺 , 𝑅 〉 ) ) = ( 𝑄 ⨣ 𝑅 ) ) |
25 |
19 24
|
opeq12d |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝑄 ∈ 𝐸 ) ∧ ( 𝐺 ∈ 𝑇 ∧ 𝑅 ∈ 𝐸 ) ) → 〈 ( ( 1st ‘ 〈 𝐹 , 𝑄 〉 ) ∘ ( 1st ‘ 〈 𝐺 , 𝑅 〉 ) ) , ( ( 2nd ‘ 〈 𝐹 , 𝑄 〉 ) ⨣ ( 2nd ‘ 〈 𝐺 , 𝑅 〉 ) ) 〉 = 〈 ( 𝐹 ∘ 𝐺 ) , ( 𝑄 ⨣ 𝑅 ) 〉 ) |
26 |
14 25
|
eqtrd |
⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐹 ∈ 𝑇 ∧ 𝑄 ∈ 𝐸 ) ∧ ( 𝐺 ∈ 𝑇 ∧ 𝑅 ∈ 𝐸 ) ) → ( 〈 𝐹 , 𝑄 〉 + 〈 𝐺 , 𝑅 〉 ) = 〈 ( 𝐹 ∘ 𝐺 ) , ( 𝑄 ⨣ 𝑅 ) 〉 ) |