Step | Hyp | Ref
| Expression |
1 | | simprl 770 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (π β π β§ π β πΈ) β§ π β π) β§ (π = (πβπΊ) β§ π β πΈ)) β π = (πβπΊ)) |
2 | | simpl1 1192 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ (π β π β§ π β πΈ) β§ π β π) β§ (π = (πβπΊ) β§ π β πΈ)) β (πΎ β HL β§ π β π»)) |
3 | | simprr 772 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ (π β π β§ π β πΈ) β§ π β π) β§ (π = (πβπΊ) β§ π β πΈ)) β π β πΈ) |
4 | | dih1dimat.l |
. . . . . . . 8
β’ β€ =
(leβπΎ) |
5 | | dih1dimat.c |
. . . . . . . 8
β’ πΆ = (AtomsβπΎ) |
6 | | dih1dimat.h |
. . . . . . . 8
β’ π» = (LHypβπΎ) |
7 | | dih1dimat.p |
. . . . . . . 8
β’ π = ((ocβπΎ)βπ) |
8 | 4, 5, 6, 7 | lhpocnel2 38532 |
. . . . . . 7
β’ ((πΎ β HL β§ π β π») β (π β πΆ β§ Β¬ π β€ π)) |
9 | 2, 8 | syl 17 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ (π β π β§ π β πΈ) β§ π β π) β§ (π = (πβπΊ) β§ π β πΈ)) β (π β πΆ β§ Β¬ π β€ π)) |
10 | | simpl2r 1228 |
. . . . . . . . 9
β’ ((((πΎ β HL β§ π β π») β§ (π β π β§ π β πΈ) β§ π β π) β§ (π = (πβπΊ) β§ π β πΈ)) β π β πΈ) |
11 | | simpl3 1194 |
. . . . . . . . 9
β’ ((((πΎ β HL β§ π β π») β§ (π β π β§ π β πΈ) β§ π β π) β§ (π = (πβπΊ) β§ π β πΈ)) β π β π) |
12 | | dih1dimat.b |
. . . . . . . . . . 11
β’ π΅ = (BaseβπΎ) |
13 | | dih1dimat.t |
. . . . . . . . . . 11
β’ π = ((LTrnβπΎ)βπ) |
14 | | dih1dimat.e |
. . . . . . . . . . 11
β’ πΈ = ((TEndoβπΎ)βπ) |
15 | | dih1dimat.o |
. . . . . . . . . . 11
β’ π = (β β π β¦ ( I βΎ π΅)) |
16 | | dih1dimat.u |
. . . . . . . . . . 11
β’ π = ((DVecHβπΎ)βπ) |
17 | | dih1dimat.d |
. . . . . . . . . . 11
β’ πΉ = (Scalarβπ) |
18 | | dih1dimat.j |
. . . . . . . . . . 11
β’ π½ = (invrβπΉ) |
19 | 12, 6, 13, 14, 15, 16, 17, 18 | tendoinvcl 39617 |
. . . . . . . . . 10
β’ (((πΎ β HL β§ π β π») β§ π β πΈ β§ π β π) β ((π½βπ ) β πΈ β§ (π½βπ ) β π)) |
20 | 19 | simpld 496 |
. . . . . . . . 9
β’ (((πΎ β HL β§ π β π») β§ π β πΈ β§ π β π) β (π½βπ ) β πΈ) |
21 | 2, 10, 11, 20 | syl3anc 1372 |
. . . . . . . 8
β’ ((((πΎ β HL β§ π β π») β§ (π β π β§ π β πΈ) β§ π β π) β§ (π = (πβπΊ) β§ π β πΈ)) β (π½βπ ) β πΈ) |
22 | | simpl2l 1227 |
. . . . . . . 8
β’ ((((πΎ β HL β§ π β π») β§ (π β π β§ π β πΈ) β§ π β π) β§ (π = (πβπΊ) β§ π β πΈ)) β π β π) |
23 | 6, 13, 14 | tendocl 39280 |
. . . . . . . 8
β’ (((πΎ β HL β§ π β π») β§ (π½βπ ) β πΈ β§ π β π) β ((π½βπ )βπ) β π) |
24 | 2, 21, 22, 23 | syl3anc 1372 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π») β§ (π β π β§ π β πΈ) β§ π β π) β§ (π = (πβπΊ) β§ π β πΈ)) β ((π½βπ )βπ) β π) |
25 | 4, 5, 6, 13 | ltrnel 38652 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ ((π½βπ )βπ) β π β§ (π β πΆ β§ Β¬ π β€ π)) β ((((π½βπ )βπ)βπ) β πΆ β§ Β¬ (((π½βπ )βπ)βπ) β€ π)) |
26 | 2, 24, 9, 25 | syl3anc 1372 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ (π β π β§ π β πΈ) β§ π β π) β§ (π = (πβπΊ) β§ π β πΈ)) β ((((π½βπ )βπ)βπ) β πΆ β§ Β¬ (((π½βπ )βπ)βπ) β€ π)) |
27 | | dih1dimat.g |
. . . . . . 7
β’ πΊ = (β©β β π (ββπ) = (((π½βπ )βπ)βπ)) |
28 | 4, 5, 6, 13, 27 | ltrniotacl 39092 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ (π β πΆ β§ Β¬ π β€ π) β§ ((((π½βπ )βπ)βπ) β πΆ β§ Β¬ (((π½βπ )βπ)βπ) β€ π)) β πΊ β π) |
29 | 2, 9, 26, 28 | syl3anc 1372 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ (π β π β§ π β πΈ) β§ π β π) β§ (π = (πβπΊ) β§ π β πΈ)) β πΊ β π) |
30 | 6, 13, 14 | tendocl 39280 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ π β πΈ β§ πΊ β π) β (πβπΊ) β π) |
31 | 2, 3, 29, 30 | syl3anc 1372 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (π β π β§ π β πΈ) β§ π β π) β§ (π = (πβπΊ) β§ π β πΈ)) β (πβπΊ) β π) |
32 | 1, 31 | eqeltrd 2834 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ (π β π β§ π β πΈ) β§ π β π) β§ (π = (πβπΊ) β§ π β πΈ)) β π β π) |
33 | 6, 14 | tendococl 39285 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ π β πΈ β§ (π½βπ ) β πΈ) β (π β (π½βπ )) β πΈ) |
34 | 2, 3, 21, 33 | syl3anc 1372 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (π β π β§ π β πΈ) β§ π β π) β§ (π = (πβπΊ) β§ π β πΈ)) β (π β (π½βπ )) β πΈ) |
35 | | simp1 1137 |
. . . . . . . 8
β’ (((πΎ β HL β§ π β π») β§ (π β π β§ π β πΈ) β§ π β π) β (πΎ β HL β§ π β π»)) |
36 | 8 | 3ad2ant1 1134 |
. . . . . . . . 9
β’ (((πΎ β HL β§ π β π») β§ (π β π β§ π β πΈ) β§ π β π) β (π β πΆ β§ Β¬ π β€ π)) |
37 | 20 | 3adant2l 1179 |
. . . . . . . . . . 11
β’ (((πΎ β HL β§ π β π») β§ (π β π β§ π β πΈ) β§ π β π) β (π½βπ ) β πΈ) |
38 | | simp2l 1200 |
. . . . . . . . . . 11
β’ (((πΎ β HL β§ π β π») β§ (π β π β§ π β πΈ) β§ π β π) β π β π) |
39 | 35, 37, 38, 23 | syl3anc 1372 |
. . . . . . . . . 10
β’ (((πΎ β HL β§ π β π») β§ (π β π β§ π β πΈ) β§ π β π) β ((π½βπ )βπ) β π) |
40 | 35, 39, 36, 25 | syl3anc 1372 |
. . . . . . . . 9
β’ (((πΎ β HL β§ π β π») β§ (π β π β§ π β πΈ) β§ π β π) β ((((π½βπ )βπ)βπ) β πΆ β§ Β¬ (((π½βπ )βπ)βπ) β€ π)) |
41 | 35, 36, 40, 28 | syl3anc 1372 |
. . . . . . . 8
β’ (((πΎ β HL β§ π β π») β§ (π β π β§ π β πΈ) β§ π β π) β πΊ β π) |
42 | 4, 5, 6, 13, 27 | ltrniotaval 39094 |
. . . . . . . . 9
β’ (((πΎ β HL β§ π β π») β§ (π β πΆ β§ Β¬ π β€ π) β§ ((((π½βπ )βπ)βπ) β πΆ β§ Β¬ (((π½βπ )βπ)βπ) β€ π)) β (πΊβπ) = (((π½βπ )βπ)βπ)) |
43 | 35, 36, 40, 42 | syl3anc 1372 |
. . . . . . . 8
β’ (((πΎ β HL β§ π β π») β§ (π β π β§ π β πΈ) β§ π β π) β (πΊβπ) = (((π½βπ )βπ)βπ)) |
44 | 4, 5, 6, 13 | cdlemd 38720 |
. . . . . . . 8
β’ ((((πΎ β HL β§ π β π») β§ πΊ β π β§ ((π½βπ )βπ) β π) β§ (π β πΆ β§ Β¬ π β€ π) β§ (πΊβπ) = (((π½βπ )βπ)βπ)) β πΊ = ((π½βπ )βπ)) |
45 | 35, 41, 39, 36, 43, 44 | syl311anc 1385 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ (π β π β§ π β πΈ) β§ π β π) β πΊ = ((π½βπ )βπ)) |
46 | 45 | adantr 482 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ (π β π β§ π β πΈ) β§ π β π) β§ (π = (πβπΊ) β§ π β πΈ)) β πΊ = ((π½βπ )βπ)) |
47 | 46 | fveq2d 6850 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ (π β π β§ π β πΈ) β§ π β π) β§ (π = (πβπΊ) β§ π β πΈ)) β (πβπΊ) = (πβ((π½βπ )βπ))) |
48 | 6, 13, 14 | tendocoval 39279 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ (π½βπ ) β πΈ) β§ π β π) β ((π β (π½βπ ))βπ) = (πβ((π½βπ )βπ))) |
49 | 2, 3, 21, 22, 48 | syl121anc 1376 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ (π β π β§ π β πΈ) β§ π β π) β§ (π = (πβπΊ) β§ π β πΈ)) β ((π β (π½βπ ))βπ) = (πβ((π½βπ )βπ))) |
50 | 47, 1, 49 | 3eqtr4d 2783 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (π β π β§ π β πΈ) β§ π β π) β§ (π = (πβπΊ) β§ π β πΈ)) β π = ((π β (π½βπ ))βπ)) |
51 | | coass 6221 |
. . . . 5
β’ ((π β (π½βπ )) β π ) = (π β ((π½βπ ) β π )) |
52 | 12, 6, 13, 14, 15, 16, 17, 18 | tendolinv 39618 |
. . . . . . . 8
β’ (((πΎ β HL β§ π β π») β§ π β πΈ β§ π β π) β ((π½βπ ) β π ) = ( I βΎ π)) |
53 | 2, 10, 11, 52 | syl3anc 1372 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π») β§ (π β π β§ π β πΈ) β§ π β π) β§ (π = (πβπΊ) β§ π β πΈ)) β ((π½βπ ) β π ) = ( I βΎ π)) |
54 | 53 | coeq2d 5822 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ (π β π β§ π β πΈ) β§ π β π) β§ (π = (πβπΊ) β§ π β πΈ)) β (π β ((π½βπ ) β π )) = (π β ( I βΎ π))) |
55 | 6, 13, 14 | tendo1mulr 39284 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ π β πΈ) β (π β ( I βΎ π)) = π) |
56 | 2, 3, 55 | syl2anc 585 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ (π β π β§ π β πΈ) β§ π β π) β§ (π = (πβπΊ) β§ π β πΈ)) β (π β ( I βΎ π)) = π) |
57 | 54, 56 | eqtrd 2773 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ (π β π β§ π β πΈ) β§ π β π) β§ (π = (πβπΊ) β§ π β πΈ)) β (π β ((π½βπ ) β π )) = π) |
58 | 51, 57 | eqtr2id 2786 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (π β π β§ π β πΈ) β§ π β π) β§ (π = (πβπΊ) β§ π β πΈ)) β π = ((π β (π½βπ )) β π )) |
59 | | fveq1 6845 |
. . . . . . 7
β’ (π‘ = (π β (π½βπ )) β (π‘βπ) = ((π β (π½βπ ))βπ)) |
60 | 59 | eqeq2d 2744 |
. . . . . 6
β’ (π‘ = (π β (π½βπ )) β (π = (π‘βπ) β π = ((π β (π½βπ ))βπ))) |
61 | | coeq1 5817 |
. . . . . . 7
β’ (π‘ = (π β (π½βπ )) β (π‘ β π ) = ((π β (π½βπ )) β π )) |
62 | 61 | eqeq2d 2744 |
. . . . . 6
β’ (π‘ = (π β (π½βπ )) β (π = (π‘ β π ) β π = ((π β (π½βπ )) β π ))) |
63 | 60, 62 | anbi12d 632 |
. . . . 5
β’ (π‘ = (π β (π½βπ )) β ((π = (π‘βπ) β§ π = (π‘ β π )) β (π = ((π β (π½βπ ))βπ) β§ π = ((π β (π½βπ )) β π )))) |
64 | 63 | rspcev 3583 |
. . . 4
β’ (((π β (π½βπ )) β πΈ β§ (π = ((π β (π½βπ ))βπ) β§ π = ((π β (π½βπ )) β π ))) β βπ‘ β πΈ (π = (π‘βπ) β§ π = (π‘ β π ))) |
65 | 34, 50, 58, 64 | syl12anc 836 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ (π β π β§ π β πΈ) β§ π β π) β§ (π = (πβπΊ) β§ π β πΈ)) β βπ‘ β πΈ (π = (π‘βπ) β§ π = (π‘ β π ))) |
66 | 32, 3, 65 | jca31 516 |
. 2
β’ ((((πΎ β HL β§ π β π») β§ (π β π β§ π β πΈ) β§ π β π) β§ (π = (πβπΊ) β§ π β πΈ)) β ((π β π β§ π β πΈ) β§ βπ‘ β πΈ (π = (π‘βπ) β§ π = (π‘ β π )))) |
67 | | simp3r 1203 |
. . . . . . . 8
β’
(((((πΎ β HL
β§ π β π») β§ (π β π β§ π β πΈ) β§ π β π) β§ (π β π β§ π β πΈ)) β§ π‘ β πΈ β§ (π = (π‘βπ) β§ π = (π‘ β π ))) β π = (π‘ β π )) |
68 | 67 | fveq1d 6848 |
. . . . . . 7
β’
(((((πΎ β HL
β§ π β π») β§ (π β π β§ π β πΈ) β§ π β π) β§ (π β π β§ π β πΈ)) β§ π‘ β πΈ β§ (π = (π‘βπ) β§ π = (π‘ β π ))) β (πβ((π½βπ )βπ)) = ((π‘ β π )β((π½βπ )βπ))) |
69 | | simp1l1 1267 |
. . . . . . . 8
β’
(((((πΎ β HL
β§ π β π») β§ (π β π β§ π β πΈ) β§ π β π) β§ (π β π β§ π β πΈ)) β§ π‘ β πΈ β§ (π = (π‘βπ) β§ π = (π‘ β π ))) β (πΎ β HL β§ π β π»)) |
70 | | simp2 1138 |
. . . . . . . . 9
β’
(((((πΎ β HL
β§ π β π») β§ (π β π β§ π β πΈ) β§ π β π) β§ (π β π β§ π β πΈ)) β§ π‘ β πΈ β§ (π = (π‘βπ) β§ π = (π‘ β π ))) β π‘ β πΈ) |
71 | | simpl2r 1228 |
. . . . . . . . . 10
β’ ((((πΎ β HL β§ π β π») β§ (π β π β§ π β πΈ) β§ π β π) β§ (π β π β§ π β πΈ)) β π β πΈ) |
72 | 71 | 3ad2ant1 1134 |
. . . . . . . . 9
β’
(((((πΎ β HL
β§ π β π») β§ (π β π β§ π β πΈ) β§ π β π) β§ (π β π β§ π β πΈ)) β§ π‘ β πΈ β§ (π = (π‘βπ) β§ π = (π‘ β π ))) β π β πΈ) |
73 | 6, 14 | tendococl 39285 |
. . . . . . . . 9
β’ (((πΎ β HL β§ π β π») β§ π‘ β πΈ β§ π β πΈ) β (π‘ β π ) β πΈ) |
74 | 69, 70, 72, 73 | syl3anc 1372 |
. . . . . . . 8
β’
(((((πΎ β HL
β§ π β π») β§ (π β π β§ π β πΈ) β§ π β π) β§ (π β π β§ π β πΈ)) β§ π‘ β πΈ β§ (π = (π‘βπ) β§ π = (π‘ β π ))) β (π‘ β π ) β πΈ) |
75 | | simp1l3 1269 |
. . . . . . . . 9
β’
(((((πΎ β HL
β§ π β π») β§ (π β π β§ π β πΈ) β§ π β π) β§ (π β π β§ π β πΈ)) β§ π‘ β πΈ β§ (π = (π‘βπ) β§ π = (π‘ β π ))) β π β π) |
76 | 69, 72, 75, 20 | syl3anc 1372 |
. . . . . . . 8
β’
(((((πΎ β HL
β§ π β π») β§ (π β π β§ π β πΈ) β§ π β π) β§ (π β π β§ π β πΈ)) β§ π‘ β πΈ β§ (π = (π‘βπ) β§ π = (π‘ β π ))) β (π½βπ ) β πΈ) |
77 | | simpl2l 1227 |
. . . . . . . . 9
β’ ((((πΎ β HL β§ π β π») β§ (π β π β§ π β πΈ) β§ π β π) β§ (π β π β§ π β πΈ)) β π β π) |
78 | 77 | 3ad2ant1 1134 |
. . . . . . . 8
β’
(((((πΎ β HL
β§ π β π») β§ (π β π β§ π β πΈ) β§ π β π) β§ (π β π β§ π β πΈ)) β§ π‘ β πΈ β§ (π = (π‘βπ) β§ π = (π‘ β π ))) β π β π) |
79 | 6, 13, 14 | tendocoval 39279 |
. . . . . . . 8
β’ (((πΎ β HL β§ π β π») β§ ((π‘ β π ) β πΈ β§ (π½βπ ) β πΈ) β§ π β π) β (((π‘ β π ) β (π½βπ ))βπ) = ((π‘ β π )β((π½βπ )βπ))) |
80 | 69, 74, 76, 78, 79 | syl121anc 1376 |
. . . . . . 7
β’
(((((πΎ β HL
β§ π β π») β§ (π β π β§ π β πΈ) β§ π β π) β§ (π β π β§ π β πΈ)) β§ π‘ β πΈ β§ (π = (π‘βπ) β§ π = (π‘ β π ))) β (((π‘ β π ) β (π½βπ ))βπ) = ((π‘ β π )β((π½βπ )βπ))) |
81 | | coass 6221 |
. . . . . . . . 9
β’ ((π‘ β π ) β (π½βπ )) = (π‘ β (π β (π½βπ ))) |
82 | 12, 6, 13, 14, 15, 16, 17, 18 | tendorinv 39619 |
. . . . . . . . . . . 12
β’ (((πΎ β HL β§ π β π») β§ π β πΈ β§ π β π) β (π β (π½βπ )) = ( I βΎ π)) |
83 | 69, 72, 75, 82 | syl3anc 1372 |
. . . . . . . . . . 11
β’
(((((πΎ β HL
β§ π β π») β§ (π β π β§ π β πΈ) β§ π β π) β§ (π β π β§ π β πΈ)) β§ π‘ β πΈ β§ (π = (π‘βπ) β§ π = (π‘ β π ))) β (π β (π½βπ )) = ( I βΎ π)) |
84 | 83 | coeq2d 5822 |
. . . . . . . . . 10
β’
(((((πΎ β HL
β§ π β π») β§ (π β π β§ π β πΈ) β§ π β π) β§ (π β π β§ π β πΈ)) β§ π‘ β πΈ β§ (π = (π‘βπ) β§ π = (π‘ β π ))) β (π‘ β (π β (π½βπ ))) = (π‘ β ( I βΎ π))) |
85 | 6, 13, 14 | tendo1mulr 39284 |
. . . . . . . . . . 11
β’ (((πΎ β HL β§ π β π») β§ π‘ β πΈ) β (π‘ β ( I βΎ π)) = π‘) |
86 | 69, 70, 85 | syl2anc 585 |
. . . . . . . . . 10
β’
(((((πΎ β HL
β§ π β π») β§ (π β π β§ π β πΈ) β§ π β π) β§ (π β π β§ π β πΈ)) β§ π‘ β πΈ β§ (π = (π‘βπ) β§ π = (π‘ β π ))) β (π‘ β ( I βΎ π)) = π‘) |
87 | 84, 86 | eqtrd 2773 |
. . . . . . . . 9
β’
(((((πΎ β HL
β§ π β π») β§ (π β π β§ π β πΈ) β§ π β π) β§ (π β π β§ π β πΈ)) β§ π‘ β πΈ β§ (π = (π‘βπ) β§ π = (π‘ β π ))) β (π‘ β (π β (π½βπ ))) = π‘) |
88 | 81, 87 | eqtrid 2785 |
. . . . . . . 8
β’
(((((πΎ β HL
β§ π β π») β§ (π β π β§ π β πΈ) β§ π β π) β§ (π β π β§ π β πΈ)) β§ π‘ β πΈ β§ (π = (π‘βπ) β§ π = (π‘ β π ))) β ((π‘ β π ) β (π½βπ )) = π‘) |
89 | 88 | fveq1d 6848 |
. . . . . . 7
β’
(((((πΎ β HL
β§ π β π») β§ (π β π β§ π β πΈ) β§ π β π) β§ (π β π β§ π β πΈ)) β§ π‘ β πΈ β§ (π = (π‘βπ) β§ π = (π‘ β π ))) β (((π‘ β π ) β (π½βπ ))βπ) = (π‘βπ)) |
90 | 68, 80, 89 | 3eqtr2rd 2780 |
. . . . . 6
β’
(((((πΎ β HL
β§ π β π») β§ (π β π β§ π β πΈ) β§ π β π) β§ (π β π β§ π β πΈ)) β§ π‘ β πΈ β§ (π = (π‘βπ) β§ π = (π‘ β π ))) β (π‘βπ) = (πβ((π½βπ )βπ))) |
91 | | simp3l 1202 |
. . . . . 6
β’
(((((πΎ β HL
β§ π β π») β§ (π β π β§ π β πΈ) β§ π β π) β§ (π β π β§ π β πΈ)) β§ π‘ β πΈ β§ (π = (π‘βπ) β§ π = (π‘ β π ))) β π = (π‘βπ)) |
92 | 45 | adantr 482 |
. . . . . . . 8
β’ ((((πΎ β HL β§ π β π») β§ (π β π β§ π β πΈ) β§ π β π) β§ (π β π β§ π β πΈ)) β πΊ = ((π½βπ )βπ)) |
93 | 92 | 3ad2ant1 1134 |
. . . . . . 7
β’
(((((πΎ β HL
β§ π β π») β§ (π β π β§ π β πΈ) β§ π β π) β§ (π β π β§ π β πΈ)) β§ π‘ β πΈ β§ (π = (π‘βπ) β§ π = (π‘ β π ))) β πΊ = ((π½βπ )βπ)) |
94 | 93 | fveq2d 6850 |
. . . . . 6
β’
(((((πΎ β HL
β§ π β π») β§ (π β π β§ π β πΈ) β§ π β π) β§ (π β π β§ π β πΈ)) β§ π‘ β πΈ β§ (π = (π‘βπ) β§ π = (π‘ β π ))) β (πβπΊ) = (πβ((π½βπ )βπ))) |
95 | 90, 91, 94 | 3eqtr4d 2783 |
. . . . 5
β’
(((((πΎ β HL
β§ π β π») β§ (π β π β§ π β πΈ) β§ π β π) β§ (π β π β§ π β πΈ)) β§ π‘ β πΈ β§ (π = (π‘βπ) β§ π = (π‘ β π ))) β π = (πβπΊ)) |
96 | 95 | rexlimdv3a 3153 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (π β π β§ π β πΈ) β§ π β π) β§ (π β π β§ π β πΈ)) β (βπ‘ β πΈ (π = (π‘βπ) β§ π = (π‘ β π )) β π = (πβπΊ))) |
97 | 96 | impr 456 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ (π β π β§ π β πΈ) β§ π β π) β§ ((π β π β§ π β πΈ) β§ βπ‘ β πΈ (π = (π‘βπ) β§ π = (π‘ β π )))) β π = (πβπΊ)) |
98 | | simprlr 779 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ (π β π β§ π β πΈ) β§ π β π) β§ ((π β π β§ π β πΈ) β§ βπ‘ β πΈ (π = (π‘βπ) β§ π = (π‘ β π )))) β π β πΈ) |
99 | 97, 98 | jca 513 |
. 2
β’ ((((πΎ β HL β§ π β π») β§ (π β π β§ π β πΈ) β§ π β π) β§ ((π β π β§ π β πΈ) β§ βπ‘ β πΈ (π = (π‘βπ) β§ π = (π‘ β π )))) β (π = (πβπΊ) β§ π β πΈ)) |
100 | 66, 99 | impbida 800 |
1
β’ (((πΎ β HL β§ π β π») β§ (π β π β§ π β πΈ) β§ π β π) β ((π = (πβπΊ) β§ π β πΈ) β ((π β π β§ π β πΈ) β§ βπ‘ β πΈ (π = (π‘βπ) β§ π = (π‘ β π ))))) |