Step | Hyp | Ref
| Expression |
1 | | elex 3461 |
. 2
β’ (πΎ β π β πΎ β V) |
2 | | fveq2 6839 |
. . . . 5
β’ (π = πΎ β (LHypβπ) = (LHypβπΎ)) |
3 | | djhval.h |
. . . . 5
β’ π» = (LHypβπΎ) |
4 | 2, 3 | eqtr4di 2795 |
. . . 4
β’ (π = πΎ β (LHypβπ) = π») |
5 | | fveq2 6839 |
. . . . . . . 8
β’ (π = πΎ β (DVecHβπ) = (DVecHβπΎ)) |
6 | 5 | fveq1d 6841 |
. . . . . . 7
β’ (π = πΎ β ((DVecHβπ)βπ€) = ((DVecHβπΎ)βπ€)) |
7 | 6 | fveq2d 6843 |
. . . . . 6
β’ (π = πΎ β (Baseβ((DVecHβπ)βπ€)) = (Baseβ((DVecHβπΎ)βπ€))) |
8 | 7 | pweqd 4575 |
. . . . 5
β’ (π = πΎ β π«
(Baseβ((DVecHβπ)βπ€)) = π«
(Baseβ((DVecHβπΎ)βπ€))) |
9 | | fveq2 6839 |
. . . . . . 7
β’ (π = πΎ β (ocHβπ) = (ocHβπΎ)) |
10 | 9 | fveq1d 6841 |
. . . . . 6
β’ (π = πΎ β ((ocHβπ)βπ€) = ((ocHβπΎ)βπ€)) |
11 | 10 | fveq1d 6841 |
. . . . . . 7
β’ (π = πΎ β (((ocHβπ)βπ€)βπ₯) = (((ocHβπΎ)βπ€)βπ₯)) |
12 | 10 | fveq1d 6841 |
. . . . . . 7
β’ (π = πΎ β (((ocHβπ)βπ€)βπ¦) = (((ocHβπΎ)βπ€)βπ¦)) |
13 | 11, 12 | ineq12d 4171 |
. . . . . 6
β’ (π = πΎ β ((((ocHβπ)βπ€)βπ₯) β© (((ocHβπ)βπ€)βπ¦)) = ((((ocHβπΎ)βπ€)βπ₯) β© (((ocHβπΎ)βπ€)βπ¦))) |
14 | 10, 13 | fveq12d 6846 |
. . . . 5
β’ (π = πΎ β (((ocHβπ)βπ€)β((((ocHβπ)βπ€)βπ₯) β© (((ocHβπ)βπ€)βπ¦))) = (((ocHβπΎ)βπ€)β((((ocHβπΎ)βπ€)βπ₯) β© (((ocHβπΎ)βπ€)βπ¦)))) |
15 | 8, 8, 14 | mpoeq123dv 7426 |
. . . 4
β’ (π = πΎ β (π₯ β π«
(Baseβ((DVecHβπ)βπ€)), π¦ β π«
(Baseβ((DVecHβπ)βπ€)) β¦ (((ocHβπ)βπ€)β((((ocHβπ)βπ€)βπ₯) β© (((ocHβπ)βπ€)βπ¦)))) = (π₯ β π«
(Baseβ((DVecHβπΎ)βπ€)), π¦ β π«
(Baseβ((DVecHβπΎ)βπ€)) β¦ (((ocHβπΎ)βπ€)β((((ocHβπΎ)βπ€)βπ₯) β© (((ocHβπΎ)βπ€)βπ¦))))) |
16 | 4, 15 | mpteq12dv 5194 |
. . 3
β’ (π = πΎ β (π€ β (LHypβπ) β¦ (π₯ β π«
(Baseβ((DVecHβπ)βπ€)), π¦ β π«
(Baseβ((DVecHβπ)βπ€)) β¦ (((ocHβπ)βπ€)β((((ocHβπ)βπ€)βπ₯) β© (((ocHβπ)βπ€)βπ¦))))) = (π€ β π» β¦ (π₯ β π«
(Baseβ((DVecHβπΎ)βπ€)), π¦ β π«
(Baseβ((DVecHβπΎ)βπ€)) β¦ (((ocHβπΎ)βπ€)β((((ocHβπΎ)βπ€)βπ₯) β© (((ocHβπΎ)βπ€)βπ¦)))))) |
17 | | df-djh 39796 |
. . 3
β’ joinH =
(π β V β¦ (π€ β (LHypβπ) β¦ (π₯ β π«
(Baseβ((DVecHβπ)βπ€)), π¦ β π«
(Baseβ((DVecHβπ)βπ€)) β¦ (((ocHβπ)βπ€)β((((ocHβπ)βπ€)βπ₯) β© (((ocHβπ)βπ€)βπ¦)))))) |
18 | 16, 17, 3 | mptfvmpt 7174 |
. 2
β’ (πΎ β V β
(joinHβπΎ) = (π€ β π» β¦ (π₯ β π«
(Baseβ((DVecHβπΎ)βπ€)), π¦ β π«
(Baseβ((DVecHβπΎ)βπ€)) β¦ (((ocHβπΎ)βπ€)β((((ocHβπΎ)βπ€)βπ₯) β© (((ocHβπΎ)βπ€)βπ¦)))))) |
19 | 1, 18 | syl 17 |
1
β’ (πΎ β π β (joinHβπΎ) = (π€ β π» β¦ (π₯ β π«
(Baseβ((DVecHβπΎ)βπ€)), π¦ β π«
(Baseβ((DVecHβπΎ)βπ€)) β¦ (((ocHβπΎ)βπ€)β((((ocHβπΎ)βπ€)βπ₯) β© (((ocHβπΎ)βπ€)βπ¦)))))) |