Step | Hyp | Ref
| Expression |
1 | | hypcgr.p |
. . 3
β’ π = (BaseβπΊ) |
2 | | hypcgr.m |
. . 3
β’ β =
(distβπΊ) |
3 | | hypcgr.i |
. . 3
β’ πΌ = (ItvβπΊ) |
4 | | hypcgr.g |
. . . 4
β’ (π β πΊ β TarskiG) |
5 | 4 | adantr 482 |
. . 3
β’ ((π β§ (π΄(midGβπΊ)π·) = π΅) β πΊ β TarskiG) |
6 | | hypcgr.c |
. . . 4
β’ (π β πΆ β π) |
7 | 6 | adantr 482 |
. . 3
β’ ((π β§ (π΄(midGβπΊ)π·) = π΅) β πΆ β π) |
8 | | hypcgr.a |
. . . 4
β’ (π β π΄ β π) |
9 | 8 | adantr 482 |
. . 3
β’ ((π β§ (π΄(midGβπΊ)π·) = π΅) β π΄ β π) |
10 | | hypcgr.f |
. . . 4
β’ (π β πΉ β π) |
11 | 10 | adantr 482 |
. . 3
β’ ((π β§ (π΄(midGβπΊ)π·) = π΅) β πΉ β π) |
12 | | hypcgr.d |
. . . 4
β’ (π β π· β π) |
13 | 12 | adantr 482 |
. . 3
β’ ((π β§ (π΄(midGβπΊ)π·) = π΅) β π· β π) |
14 | | eqid 2733 |
. . . . . . 7
β’
(LineGβπΊ) =
(LineGβπΊ) |
15 | | eqid 2733 |
. . . . . . 7
β’
(pInvGβπΊ) =
(pInvGβπΊ) |
16 | | hypcgr.b |
. . . . . . 7
β’ (π β π΅ β π) |
17 | | hypcgr.1 |
. . . . . . 7
β’ (π β β¨βπ΄π΅πΆββ© β (βGβπΊ)) |
18 | 1, 2, 3, 14, 15, 4, 8, 16, 6,
17 | ragcom 27949 |
. . . . . 6
β’ (π β β¨βπΆπ΅π΄ββ© β (βGβπΊ)) |
19 | 1, 2, 3, 14, 15, 4, 6, 16, 8 | israg 27948 |
. . . . . 6
β’ (π β (β¨βπΆπ΅π΄ββ© β (βGβπΊ) β (πΆ β π΄) = (πΆ β (((pInvGβπΊ)βπ΅)βπ΄)))) |
20 | 18, 19 | mpbid 231 |
. . . . 5
β’ (π β (πΆ β π΄) = (πΆ β (((pInvGβπΊ)βπ΅)βπ΄))) |
21 | 20 | adantr 482 |
. . . 4
β’ ((π β§ (π΄(midGβπΊ)π·) = π΅) β (πΆ β π΄) = (πΆ β (((pInvGβπΊ)βπ΅)βπ΄))) |
22 | | hypcgrlem1.a |
. . . . . . 7
β’ (π β πΆ = πΉ) |
23 | 22 | eqcomd 2739 |
. . . . . 6
β’ (π β πΉ = πΆ) |
24 | 23 | adantr 482 |
. . . . 5
β’ ((π β§ (π΄(midGβπΊ)π·) = π΅) β πΉ = πΆ) |
25 | | hypcgr.h |
. . . . . . 7
β’ (π β πΊDimTarskiGβ₯2) |
26 | 1, 2, 3, 4, 25, 8,
12, 15, 16 | ismidb 28029 |
. . . . . 6
β’ (π β (π· = (((pInvGβπΊ)βπ΅)βπ΄) β (π΄(midGβπΊ)π·) = π΅)) |
27 | 26 | biimpar 479 |
. . . . 5
β’ ((π β§ (π΄(midGβπΊ)π·) = π΅) β π· = (((pInvGβπΊ)βπ΅)βπ΄)) |
28 | 24, 27 | oveq12d 7427 |
. . . 4
β’ ((π β§ (π΄(midGβπΊ)π·) = π΅) β (πΉ β π·) = (πΆ β (((pInvGβπΊ)βπ΅)βπ΄))) |
29 | 21, 28 | eqtr4d 2776 |
. . 3
β’ ((π β§ (π΄(midGβπΊ)π·) = π΅) β (πΆ β π΄) = (πΉ β π·)) |
30 | 1, 2, 3, 5, 7, 9, 11, 13, 29 | tgcgrcomlr 27731 |
. 2
β’ ((π β§ (π΄(midGβπΊ)π·) = π΅) β (π΄ β πΆ) = (π· β πΉ)) |
31 | | simpr 486 |
. . . 4
β’ (((π β§ (π΄(midGβπΊ)π·) β π΅) β§ π΄ = π·) β π΄ = π·) |
32 | 22 | ad2antrr 725 |
. . . 4
β’ (((π β§ (π΄(midGβπΊ)π·) β π΅) β§ π΄ = π·) β πΆ = πΉ) |
33 | 31, 32 | oveq12d 7427 |
. . 3
β’ (((π β§ (π΄(midGβπΊ)π·) β π΅) β§ π΄ = π·) β (π΄ β πΆ) = (π· β πΉ)) |
34 | 17 | ad2antrr 725 |
. . . . . 6
β’ (((π β§ (π΄(midGβπΊ)π·) β π΅) β§ π΄ β π·) β β¨βπ΄π΅πΆββ© β (βGβπΊ)) |
35 | 4 | ad2antrr 725 |
. . . . . . 7
β’ (((π β§ (π΄(midGβπΊ)π·) β π΅) β§ π΄ β π·) β πΊ β TarskiG) |
36 | 8 | ad2antrr 725 |
. . . . . . 7
β’ (((π β§ (π΄(midGβπΊ)π·) β π΅) β§ π΄ β π·) β π΄ β π) |
37 | 16 | ad2antrr 725 |
. . . . . . 7
β’ (((π β§ (π΄(midGβπΊ)π·) β π΅) β§ π΄ β π·) β π΅ β π) |
38 | 6 | ad2antrr 725 |
. . . . . . 7
β’ (((π β§ (π΄(midGβπΊ)π·) β π΅) β§ π΄ β π·) β πΆ β π) |
39 | 1, 2, 3, 14, 15, 35, 36, 37, 38 | israg 27948 |
. . . . . 6
β’ (((π β§ (π΄(midGβπΊ)π·) β π΅) β§ π΄ β π·) β (β¨βπ΄π΅πΆββ© β (βGβπΊ) β (π΄ β πΆ) = (π΄ β (((pInvGβπΊ)βπ΅)βπΆ)))) |
40 | 34, 39 | mpbid 231 |
. . . . 5
β’ (((π β§ (π΄(midGβπΊ)π·) β π΅) β§ π΄ β π·) β (π΄ β πΆ) = (π΄ β (((pInvGβπΊ)βπ΅)βπΆ))) |
41 | 25 | ad2antrr 725 |
. . . . . . 7
β’ (((π β§ (π΄(midGβπΊ)π·) β π΅) β§ π΄ β π·) β πΊDimTarskiGβ₯2) |
42 | | hypcgrlem1.s |
. . . . . . 7
β’ π = ((lInvGβπΊ)β((π΄(midGβπΊ)π·)(LineGβπΊ)π΅)) |
43 | 12 | ad2antrr 725 |
. . . . . . . . 9
β’ (((π β§ (π΄(midGβπΊ)π·) β π΅) β§ π΄ β π·) β π· β π) |
44 | 1, 2, 3, 35, 41, 36, 43 | midcl 28028 |
. . . . . . . 8
β’ (((π β§ (π΄(midGβπΊ)π·) β π΅) β§ π΄ β π·) β (π΄(midGβπΊ)π·) β π) |
45 | | simplr 768 |
. . . . . . . 8
β’ (((π β§ (π΄(midGβπΊ)π·) β π΅) β§ π΄ β π·) β (π΄(midGβπΊ)π·) β π΅) |
46 | 1, 3, 14, 35, 44, 37, 45 | tgelrnln 27881 |
. . . . . . 7
β’ (((π β§ (π΄(midGβπΊ)π·) β π΅) β§ π΄ β π·) β ((π΄(midGβπΊ)π·)(LineGβπΊ)π΅) β ran (LineGβπΊ)) |
47 | | eqid 2733 |
. . . . . . 7
β’
((pInvGβπΊ)βπ΅) = ((pInvGβπΊ)βπ΅) |
48 | | eqid 2733 |
. . . . . . . . 9
β’
(cgrGβπΊ) =
(cgrGβπΊ) |
49 | 1, 2, 3, 14, 15, 35, 37, 47, 38 | mircl 27912 |
. . . . . . . . 9
β’ (((π β§ (π΄(midGβπΊ)π·) β π΅) β§ π΄ β π·) β (((pInvGβπΊ)βπ΅)βπΆ) β π) |
50 | | simpr 486 |
. . . . . . . . 9
β’ (((π β§ (π΄(midGβπΊ)π·) β π΅) β§ π΄ β π·) β π΄ β π·) |
51 | 1, 2, 3, 35, 41, 36, 43 | midbtwn 28030 |
. . . . . . . . . 10
β’ (((π β§ (π΄(midGβπΊ)π·) β π΅) β§ π΄ β π·) β (π΄(midGβπΊ)π·) β (π΄πΌπ·)) |
52 | 1, 14, 3, 35, 36, 44, 43, 51 | btwncolg3 27808 |
. . . . . . . . 9
β’ (((π β§ (π΄(midGβπΊ)π·) β π΅) β§ π΄ β π·) β (π· β (π΄(LineGβπΊ)(π΄(midGβπΊ)π·)) β¨ π΄ = (π΄(midGβπΊ)π·))) |
53 | | eqidd 2734 |
. . . . . . . . . . . . 13
β’ (π β π· = π·) |
54 | | hypcgrlem2.b |
. . . . . . . . . . . . 13
β’ (π β π΅ = πΈ) |
55 | 53, 54, 22 | s3eqd 14815 |
. . . . . . . . . . . 12
β’ (π β β¨βπ·π΅πΆββ© = β¨βπ·πΈπΉββ©) |
56 | 55 | ad2antrr 725 |
. . . . . . . . . . 11
β’ (((π β§ (π΄(midGβπΊ)π·) β π΅) β§ π΄ β π·) β β¨βπ·π΅πΆββ© = β¨βπ·πΈπΉββ©) |
57 | | hypcgr.2 |
. . . . . . . . . . . 12
β’ (π β β¨βπ·πΈπΉββ© β (βGβπΊ)) |
58 | 57 | ad2antrr 725 |
. . . . . . . . . . 11
β’ (((π β§ (π΄(midGβπΊ)π·) β π΅) β§ π΄ β π·) β β¨βπ·πΈπΉββ© β (βGβπΊ)) |
59 | 56, 58 | eqeltrd 2834 |
. . . . . . . . . 10
β’ (((π β§ (π΄(midGβπΊ)π·) β π΅) β§ π΄ β π·) β β¨βπ·π΅πΆββ© β (βGβπΊ)) |
60 | 1, 2, 3, 14, 15, 35, 43, 37, 38 | israg 27948 |
. . . . . . . . . 10
β’ (((π β§ (π΄(midGβπΊ)π·) β π΅) β§ π΄ β π·) β (β¨βπ·π΅πΆββ© β (βGβπΊ) β (π· β πΆ) = (π· β (((pInvGβπΊ)βπ΅)βπΆ)))) |
61 | 59, 60 | mpbid 231 |
. . . . . . . . 9
β’ (((π β§ (π΄(midGβπΊ)π·) β π΅) β§ π΄ β π·) β (π· β πΆ) = (π· β (((pInvGβπΊ)βπ΅)βπΆ))) |
62 | 1, 14, 3, 35, 36, 43, 44, 48, 38, 49, 2, 50, 52, 40, 61 | lncgr 27820 |
. . . . . . . 8
β’ (((π β§ (π΄(midGβπΊ)π·) β π΅) β§ π΄ β π·) β ((π΄(midGβπΊ)π·) β πΆ) = ((π΄(midGβπΊ)π·) β (((pInvGβπΊ)βπ΅)βπΆ))) |
63 | 1, 2, 3, 14, 15, 35, 44, 37, 38 | israg 27948 |
. . . . . . . 8
β’ (((π β§ (π΄(midGβπΊ)π·) β π΅) β§ π΄ β π·) β (β¨β(π΄(midGβπΊ)π·)π΅πΆββ© β (βGβπΊ) β ((π΄(midGβπΊ)π·) β πΆ) = ((π΄(midGβπΊ)π·) β (((pInvGβπΊ)βπ΅)βπΆ)))) |
64 | 62, 63 | mpbird 257 |
. . . . . . 7
β’ (((π β§ (π΄(midGβπΊ)π·) β π΅) β§ π΄ β π·) β β¨β(π΄(midGβπΊ)π·)π΅πΆββ© β (βGβπΊ)) |
65 | 1, 3, 14, 35, 44, 37, 45 | tglinerflx1 27884 |
. . . . . . 7
β’ (((π β§ (π΄(midGβπΊ)π·) β π΅) β§ π΄ β π·) β (π΄(midGβπΊ)π·) β ((π΄(midGβπΊ)π·)(LineGβπΊ)π΅)) |
66 | 1, 3, 14, 35, 44, 37, 45 | tglinerflx2 27885 |
. . . . . . 7
β’ (((π β§ (π΄(midGβπΊ)π·) β π΅) β§ π΄ β π·) β π΅ β ((π΄(midGβπΊ)π·)(LineGβπΊ)π΅)) |
67 | 1, 2, 3, 35, 41, 42, 14, 46, 44, 47, 64, 65, 66, 38, 45 | lmimid 28045 |
. . . . . 6
β’ (((π β§ (π΄(midGβπΊ)π·) β π΅) β§ π΄ β π·) β (πβπΆ) = (((pInvGβπΊ)βπ΅)βπΆ)) |
68 | 67 | oveq2d 7425 |
. . . . 5
β’ (((π β§ (π΄(midGβπΊ)π·) β π΅) β§ π΄ β π·) β (π΄ β (πβπΆ)) = (π΄ β (((pInvGβπΊ)βπ΅)βπΆ))) |
69 | 40, 68 | eqtr4d 2776 |
. . . 4
β’ (((π β§ (π΄(midGβπΊ)π·) β π΅) β§ π΄ β π·) β (π΄ β πΆ) = (π΄ β (πβπΆ))) |
70 | 1, 2, 3, 35, 41, 43, 36 | midcom 28033 |
. . . . . . . 8
β’ (((π β§ (π΄(midGβπΊ)π·) β π΅) β§ π΄ β π·) β (π·(midGβπΊ)π΄) = (π΄(midGβπΊ)π·)) |
71 | 70, 65 | eqeltrd 2834 |
. . . . . . 7
β’ (((π β§ (π΄(midGβπΊ)π·) β π΅) β§ π΄ β π·) β (π·(midGβπΊ)π΄) β ((π΄(midGβπΊ)π·)(LineGβπΊ)π΅)) |
72 | 50 | necomd 2997 |
. . . . . . . . . 10
β’ (((π β§ (π΄(midGβπΊ)π·) β π΅) β§ π΄ β π·) β π· β π΄) |
73 | 1, 3, 14, 35, 43, 36, 72 | tgelrnln 27881 |
. . . . . . . . 9
β’ (((π β§ (π΄(midGβπΊ)π·) β π΅) β§ π΄ β π·) β (π·(LineGβπΊ)π΄) β ran (LineGβπΊ)) |
74 | 1, 2, 3, 35, 36, 44, 43, 51 | tgbtwncom 27739 |
. . . . . . . . . . 11
β’ (((π β§ (π΄(midGβπΊ)π·) β π΅) β§ π΄ β π·) β (π΄(midGβπΊ)π·) β (π·πΌπ΄)) |
75 | 1, 3, 14, 35, 43, 36, 44, 72, 74 | btwnlng1 27870 |
. . . . . . . . . 10
β’ (((π β§ (π΄(midGβπΊ)π·) β π΅) β§ π΄ β π·) β (π΄(midGβπΊ)π·) β (π·(LineGβπΊ)π΄)) |
76 | 65, 75 | elind 4195 |
. . . . . . . . 9
β’ (((π β§ (π΄(midGβπΊ)π·) β π΅) β§ π΄ β π·) β (π΄(midGβπΊ)π·) β (((π΄(midGβπΊ)π·)(LineGβπΊ)π΅) β© (π·(LineGβπΊ)π΄))) |
77 | 1, 3, 14, 35, 43, 36, 72 | tglinerflx2 27885 |
. . . . . . . . 9
β’ (((π β§ (π΄(midGβπΊ)π·) β π΅) β§ π΄ β π·) β π΄ β (π·(LineGβπΊ)π΄)) |
78 | 45 | necomd 2997 |
. . . . . . . . 9
β’ (((π β§ (π΄(midGβπΊ)π·) β π΅) β§ π΄ β π·) β π΅ β (π΄(midGβπΊ)π·)) |
79 | 4 | ad2antrr 725 |
. . . . . . . . . . . . 13
β’ (((π β§ (π΄(midGβπΊ)π·) β π΅) β§ π΄ = (π΄(midGβπΊ)π·)) β πΊ β TarskiG) |
80 | 8 | ad2antrr 725 |
. . . . . . . . . . . . 13
β’ (((π β§ (π΄(midGβπΊ)π·) β π΅) β§ π΄ = (π΄(midGβπΊ)π·)) β π΄ β π) |
81 | 12 | ad2antrr 725 |
. . . . . . . . . . . . 13
β’ (((π β§ (π΄(midGβπΊ)π·) β π΅) β§ π΄ = (π΄(midGβπΊ)π·)) β π· β π) |
82 | 25 | ad2antrr 725 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (π΄(midGβπΊ)π·) β π΅) β§ π΄ = (π΄(midGβπΊ)π·)) β πΊDimTarskiGβ₯2) |
83 | | simpr 486 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ (π΄(midGβπΊ)π·) β π΅) β§ π΄ = (π΄(midGβπΊ)π·)) β π΄ = (π΄(midGβπΊ)π·)) |
84 | 83 | eqcomd 2739 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (π΄(midGβπΊ)π·) β π΅) β§ π΄ = (π΄(midGβπΊ)π·)) β (π΄(midGβπΊ)π·) = π΄) |
85 | 1, 2, 3, 79, 82, 80, 81, 84 | midcgr 28031 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π΄(midGβπΊ)π·) β π΅) β§ π΄ = (π΄(midGβπΊ)π·)) β (π΄ β π΄) = (π΄ β π·)) |
86 | 85 | eqcomd 2739 |
. . . . . . . . . . . . 13
β’ (((π β§ (π΄(midGβπΊ)π·) β π΅) β§ π΄ = (π΄(midGβπΊ)π·)) β (π΄ β π·) = (π΄ β π΄)) |
87 | 1, 2, 3, 79, 80, 81, 80, 86 | axtgcgrid 27714 |
. . . . . . . . . . . 12
β’ (((π β§ (π΄(midGβπΊ)π·) β π΅) β§ π΄ = (π΄(midGβπΊ)π·)) β π΄ = π·) |
88 | 87 | ex 414 |
. . . . . . . . . . 11
β’ ((π β§ (π΄(midGβπΊ)π·) β π΅) β (π΄ = (π΄(midGβπΊ)π·) β π΄ = π·)) |
89 | 88 | necon3d 2962 |
. . . . . . . . . 10
β’ ((π β§ (π΄(midGβπΊ)π·) β π΅) β (π΄ β π· β π΄ β (π΄(midGβπΊ)π·))) |
90 | 89 | imp 408 |
. . . . . . . . 9
β’ (((π β§ (π΄(midGβπΊ)π·) β π΅) β§ π΄ β π·) β π΄ β (π΄(midGβπΊ)π·)) |
91 | | hypcgr.e |
. . . . . . . . . . . . . 14
β’ (π β πΈ β π) |
92 | | hypcgr.3 |
. . . . . . . . . . . . . 14
β’ (π β (π΄ β π΅) = (π· β πΈ)) |
93 | 1, 2, 3, 4, 8, 16,
12, 91, 92 | tgcgrcomlr 27731 |
. . . . . . . . . . . . 13
β’ (π β (π΅ β π΄) = (πΈ β π·)) |
94 | 54 | oveq1d 7424 |
. . . . . . . . . . . . 13
β’ (π β (π΅ β π·) = (πΈ β π·)) |
95 | 93, 94 | eqtr4d 2776 |
. . . . . . . . . . . 12
β’ (π β (π΅ β π΄) = (π΅ β π·)) |
96 | 95 | ad2antrr 725 |
. . . . . . . . . . 11
β’ (((π β§ (π΄(midGβπΊ)π·) β π΅) β§ π΄ β π·) β (π΅ β π΄) = (π΅ β π·)) |
97 | | eqidd 2734 |
. . . . . . . . . . . . 13
β’ (((π β§ (π΄(midGβπΊ)π·) β π΅) β§ π΄ β π·) β (π΄(midGβπΊ)π·) = (π΄(midGβπΊ)π·)) |
98 | 1, 2, 3, 35, 41, 36, 43, 15, 44 | ismidb 28029 |
. . . . . . . . . . . . 13
β’ (((π β§ (π΄(midGβπΊ)π·) β π΅) β§ π΄ β π·) β (π· = (((pInvGβπΊ)β(π΄(midGβπΊ)π·))βπ΄) β (π΄(midGβπΊ)π·) = (π΄(midGβπΊ)π·))) |
99 | 97, 98 | mpbird 257 |
. . . . . . . . . . . 12
β’ (((π β§ (π΄(midGβπΊ)π·) β π΅) β§ π΄ β π·) β π· = (((pInvGβπΊ)β(π΄(midGβπΊ)π·))βπ΄)) |
100 | 99 | oveq2d 7425 |
. . . . . . . . . . 11
β’ (((π β§ (π΄(midGβπΊ)π·) β π΅) β§ π΄ β π·) β (π΅ β π·) = (π΅ β (((pInvGβπΊ)β(π΄(midGβπΊ)π·))βπ΄))) |
101 | 96, 100 | eqtrd 2773 |
. . . . . . . . . 10
β’ (((π β§ (π΄(midGβπΊ)π·) β π΅) β§ π΄ β π·) β (π΅ β π΄) = (π΅ β (((pInvGβπΊ)β(π΄(midGβπΊ)π·))βπ΄))) |
102 | 1, 2, 3, 14, 15, 35, 37, 44, 36 | israg 27948 |
. . . . . . . . . 10
β’ (((π β§ (π΄(midGβπΊ)π·) β π΅) β§ π΄ β π·) β (β¨βπ΅(π΄(midGβπΊ)π·)π΄ββ© β (βGβπΊ) β (π΅ β π΄) = (π΅ β (((pInvGβπΊ)β(π΄(midGβπΊ)π·))βπ΄)))) |
103 | 101, 102 | mpbird 257 |
. . . . . . . . 9
β’ (((π β§ (π΄(midGβπΊ)π·) β π΅) β§ π΄ β π·) β β¨βπ΅(π΄(midGβπΊ)π·)π΄ββ© β (βGβπΊ)) |
104 | 1, 2, 3, 14, 35, 46, 73, 76, 66, 77, 78, 90, 103 | ragperp 27968 |
. . . . . . . 8
β’ (((π β§ (π΄(midGβπΊ)π·) β π΅) β§ π΄ β π·) β ((π΄(midGβπΊ)π·)(LineGβπΊ)π΅)(βGβπΊ)(π·(LineGβπΊ)π΄)) |
105 | 104 | orcd 872 |
. . . . . . 7
β’ (((π β§ (π΄(midGβπΊ)π·) β π΅) β§ π΄ β π·) β (((π΄(midGβπΊ)π·)(LineGβπΊ)π΅)(βGβπΊ)(π·(LineGβπΊ)π΄) β¨ π· = π΄)) |
106 | 1, 2, 3, 35, 41, 42, 14, 46, 43, 36 | islmib 28038 |
. . . . . . 7
β’ (((π β§ (π΄(midGβπΊ)π·) β π΅) β§ π΄ β π·) β (π΄ = (πβπ·) β ((π·(midGβπΊ)π΄) β ((π΄(midGβπΊ)π·)(LineGβπΊ)π΅) β§ (((π΄(midGβπΊ)π·)(LineGβπΊ)π΅)(βGβπΊ)(π·(LineGβπΊ)π΄) β¨ π· = π΄)))) |
107 | 71, 105, 106 | mpbir2and 712 |
. . . . . 6
β’ (((π β§ (π΄(midGβπΊ)π·) β π΅) β§ π΄ β π·) β π΄ = (πβπ·)) |
108 | 107 | oveq1d 7424 |
. . . . 5
β’ (((π β§ (π΄(midGβπΊ)π·) β π΅) β§ π΄ β π·) β (π΄ β (πβπΆ)) = ((πβπ·) β (πβπΆ))) |
109 | 1, 2, 3, 35, 41, 42, 14, 46, 43, 38 | lmiiso 28048 |
. . . . 5
β’ (((π β§ (π΄(midGβπΊ)π·) β π΅) β§ π΄ β π·) β ((πβπ·) β (πβπΆ)) = (π· β πΆ)) |
110 | 22 | oveq2d 7425 |
. . . . . 6
β’ (π β (π· β πΆ) = (π· β πΉ)) |
111 | 110 | ad2antrr 725 |
. . . . 5
β’ (((π β§ (π΄(midGβπΊ)π·) β π΅) β§ π΄ β π·) β (π· β πΆ) = (π· β πΉ)) |
112 | 108, 109,
111 | 3eqtrd 2777 |
. . . 4
β’ (((π β§ (π΄(midGβπΊ)π·) β π΅) β§ π΄ β π·) β (π΄ β (πβπΆ)) = (π· β πΉ)) |
113 | 69, 112 | eqtrd 2773 |
. . 3
β’ (((π β§ (π΄(midGβπΊ)π·) β π΅) β§ π΄ β π·) β (π΄ β πΆ) = (π· β πΉ)) |
114 | 33, 113 | pm2.61dane 3030 |
. 2
β’ ((π β§ (π΄(midGβπΊ)π·) β π΅) β (π΄ β πΆ) = (π· β πΉ)) |
115 | 30, 114 | pm2.61dane 3030 |
1
β’ (π β (π΄ β πΆ) = (π· β πΉ)) |