Step | Hyp | Ref
| Expression |
1 | | simp1 1137 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ π β πΈ) β§ (πΊ β π β§ π
β πΈ)) β (πΎ β HL β§ π β π»)) |
2 | | opelxpi 5671 |
. . . 4
β’ ((πΉ β π β§ π β πΈ) β β¨πΉ, πβ© β (π Γ πΈ)) |
3 | 2 | 3ad2ant2 1135 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ π β πΈ) β§ (πΊ β π β§ π
β πΈ)) β β¨πΉ, πβ© β (π Γ πΈ)) |
4 | | opelxpi 5671 |
. . . 4
β’ ((πΊ β π β§ π
β πΈ) β β¨πΊ, π
β© β (π Γ πΈ)) |
5 | 4 | 3ad2ant3 1136 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ π β πΈ) β§ (πΊ β π β§ π
β πΈ)) β β¨πΊ, π
β© β (π Γ πΈ)) |
6 | | dvhvadd.h |
. . . 4
β’ π» = (LHypβπΎ) |
7 | | dvhvadd.t |
. . . 4
β’ π = ((LTrnβπΎ)βπ) |
8 | | dvhvadd.e |
. . . 4
β’ πΈ = ((TEndoβπΎ)βπ) |
9 | | dvhvadd.u |
. . . 4
β’ π = ((DVecHβπΎ)βπ) |
10 | | dvhvadd.f |
. . . 4
β’ π· = (Scalarβπ) |
11 | | dvhvadd.s |
. . . 4
β’ + =
(+gβπ) |
12 | | dvhvadd.p |
. . . 4
⒠⨣ =
(+gβπ·) |
13 | 6, 7, 8, 9, 10, 11, 12 | dvhvadd 39558 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (β¨πΉ, πβ© β (π Γ πΈ) β§ β¨πΊ, π
β© β (π Γ πΈ))) β (β¨πΉ, πβ© + β¨πΊ, π
β©) = β¨((1st
ββ¨πΉ, πβ©) β (1st
ββ¨πΊ, π
β©)), ((2nd
ββ¨πΉ, πβ©) ⨣ (2nd
ββ¨πΊ, π
β©))β©) |
14 | 1, 3, 5, 13 | syl12anc 836 |
. 2
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ π β πΈ) β§ (πΊ β π β§ π
β πΈ)) β (β¨πΉ, πβ© + β¨πΊ, π
β©) = β¨((1st
ββ¨πΉ, πβ©) β (1st
ββ¨πΊ, π
β©)), ((2nd
ββ¨πΉ, πβ©) ⨣ (2nd
ββ¨πΊ, π
β©))β©) |
15 | | op1stg 7934 |
. . . . 5
β’ ((πΉ β π β§ π β πΈ) β (1st ββ¨πΉ, πβ©) = πΉ) |
16 | 15 | 3ad2ant2 1135 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ π β πΈ) β§ (πΊ β π β§ π
β πΈ)) β (1st ββ¨πΉ, πβ©) = πΉ) |
17 | | op1stg 7934 |
. . . . 5
β’ ((πΊ β π β§ π
β πΈ) β (1st ββ¨πΊ, π
β©) = πΊ) |
18 | 17 | 3ad2ant3 1136 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ π β πΈ) β§ (πΊ β π β§ π
β πΈ)) β (1st ββ¨πΊ, π
β©) = πΊ) |
19 | 16, 18 | coeq12d 5821 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ π β πΈ) β§ (πΊ β π β§ π
β πΈ)) β ((1st
ββ¨πΉ, πβ©) β (1st
ββ¨πΊ, π
β©)) = (πΉ β πΊ)) |
20 | | op2ndg 7935 |
. . . . 5
β’ ((πΉ β π β§ π β πΈ) β (2nd ββ¨πΉ, πβ©) = π) |
21 | 20 | 3ad2ant2 1135 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ π β πΈ) β§ (πΊ β π β§ π
β πΈ)) β (2nd ββ¨πΉ, πβ©) = π) |
22 | | op2ndg 7935 |
. . . . 5
β’ ((πΊ β π β§ π
β πΈ) β (2nd ββ¨πΊ, π
β©) = π
) |
23 | 22 | 3ad2ant3 1136 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ π β πΈ) β§ (πΊ β π β§ π
β πΈ)) β (2nd ββ¨πΊ, π
β©) = π
) |
24 | 21, 23 | oveq12d 7376 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ π β πΈ) β§ (πΊ β π β§ π
β πΈ)) β ((2nd
ββ¨πΉ, πβ©) ⨣ (2nd
ββ¨πΊ, π
β©)) = (π ⨣ π
)) |
25 | 19, 24 | opeq12d 4839 |
. 2
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ π β πΈ) β§ (πΊ β π β§ π
β πΈ)) β β¨((1st
ββ¨πΉ, πβ©) β (1st
ββ¨πΊ, π
β©)), ((2nd
ββ¨πΉ, πβ©) ⨣ (2nd
ββ¨πΊ, π
β©))β© = β¨(πΉ β πΊ), (π ⨣ π
)β©) |
26 | 14, 25 | eqtrd 2777 |
1
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ π β πΈ) β§ (πΊ β π β§ π
β πΈ)) β (β¨πΉ, πβ© + β¨πΊ, π
β©) = β¨(πΉ β πΊ), (π ⨣ π
)β©) |