Step | Hyp | Ref
| Expression |
1 | | colperpex.p |
. . . 4
β’ π = (BaseβπΊ) |
2 | | colperpex.d |
. . . 4
β’ β =
(distβπΊ) |
3 | | colperpex.i |
. . . 4
β’ πΌ = (ItvβπΊ) |
4 | | colperpex.l |
. . . 4
β’ πΏ = (LineGβπΊ) |
5 | | mideu.s |
. . . 4
β’ π = (pInvGβπΊ) |
6 | | colperpex.g |
. . . . 5
β’ (π β πΊ β TarskiG) |
7 | 6 | adantr 482 |
. . . 4
β’ ((π β§ (π₯ β π β§ (π₯ β (ππΌπ΅) β§ π₯ β (π
πΌπ)))) β πΊ β TarskiG) |
8 | | eqid 2733 |
. . . 4
β’ (πβπ₯) = (πβπ₯) |
9 | | mideu.2 |
. . . . 5
β’ (π β π΅ β π) |
10 | 9 | adantr 482 |
. . . 4
β’ ((π β§ (π₯ β π β§ (π₯ β (ππΌπ΅) β§ π₯ β (π
πΌπ)))) β π΅ β π) |
11 | | mideulem.3 |
. . . . 5
β’ (π β π β π) |
12 | 11 | adantr 482 |
. . . 4
β’ ((π β§ (π₯ β π β§ (π₯ β (ππΌπ΅) β§ π₯ β (π
πΌπ)))) β π β π) |
13 | | mideu.1 |
. . . . 5
β’ (π β π΄ β π) |
14 | 13 | adantr 482 |
. . . 4
β’ ((π β§ (π₯ β π β§ (π₯ β (ππΌπ΅) β§ π₯ β (π
πΌπ)))) β π΄ β π) |
15 | | opphllem.1 |
. . . . 5
β’ (π β π
β π) |
16 | 15 | adantr 482 |
. . . 4
β’ ((π β§ (π₯ β π β§ (π₯ β (ππΌπ΅) β§ π₯ β (π
πΌπ)))) β π
β π) |
17 | | simprl 770 |
. . . 4
β’ ((π β§ (π₯ β π β§ (π₯ β (ππΌπ΅) β§ π₯ β (π
πΌπ)))) β π₯ β π) |
18 | | mideulem.1 |
. . . . . . . . . . . . . 14
β’ (π β π΄ β π΅) |
19 | 18 | necomd 2996 |
. . . . . . . . . . . . 13
β’ (π β π΅ β π΄) |
20 | 19 | neneqd 2945 |
. . . . . . . . . . . 12
β’ (π β Β¬ π΅ = π΄) |
21 | 20 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ π β (π΅πΏπ΄)) β Β¬ π΅ = π΄) |
22 | | mideulem.6 |
. . . . . . . . . . . . . . . 16
β’ (π β (π΄πΏπ΅)(βGβπΊ)(π΄πΏπ)) |
23 | 4, 6, 22 | perpln2 27695 |
. . . . . . . . . . . . . . 15
β’ (π β (π΄πΏπ) β ran πΏ) |
24 | 1, 3, 4, 6, 13, 11, 23 | tglnne 27612 |
. . . . . . . . . . . . . 14
β’ (π β π΄ β π) |
25 | 24 | necomd 2996 |
. . . . . . . . . . . . 13
β’ (π β π β π΄) |
26 | 25 | neneqd 2945 |
. . . . . . . . . . . 12
β’ (π β Β¬ π = π΄) |
27 | 26 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ π β (π΅πΏπ΄)) β Β¬ π = π΄) |
28 | 21, 27 | jca 513 |
. . . . . . . . . 10
β’ ((π β§ π β (π΅πΏπ΄)) β (Β¬ π΅ = π΄ β§ Β¬ π = π΄)) |
29 | 6 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ π β (π΅πΏπ΄)) β πΊ β TarskiG) |
30 | 9 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ π β (π΅πΏπ΄)) β π΅ β π) |
31 | 13 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ π β (π΅πΏπ΄)) β π΄ β π) |
32 | 11 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ π β (π΅πΏπ΄)) β π β π) |
33 | 1, 3, 4, 6, 9, 13,
19 | tglinerflx2 27618 |
. . . . . . . . . . . . . 14
β’ (π β π΄ β (π΅πΏπ΄)) |
34 | 1, 3, 4, 6, 13, 9,
18 | tglinecom 27619 |
. . . . . . . . . . . . . . 15
β’ (π β (π΄πΏπ΅) = (π΅πΏπ΄)) |
35 | 34, 22 | eqbrtrrd 5130 |
. . . . . . . . . . . . . 14
β’ (π β (π΅πΏπ΄)(βGβπΊ)(π΄πΏπ)) |
36 | 1, 2, 3, 4, 6, 9, 13, 33, 11, 35 | perprag 27710 |
. . . . . . . . . . . . 13
β’ (π β β¨βπ΅π΄πββ© β (βGβπΊ)) |
37 | 36 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ π β (π΅πΏπ΄)) β β¨βπ΅π΄πββ© β (βGβπΊ)) |
38 | | simpr 486 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (π΅πΏπ΄)) β π β (π΅πΏπ΄)) |
39 | 38 | orcd 872 |
. . . . . . . . . . . 12
β’ ((π β§ π β (π΅πΏπ΄)) β (π β (π΅πΏπ΄) β¨ π΅ = π΄)) |
40 | 1, 2, 3, 4, 5, 29,
30, 31, 32, 37, 39 | ragflat3 27690 |
. . . . . . . . . . 11
β’ ((π β§ π β (π΅πΏπ΄)) β (π΅ = π΄ β¨ π = π΄)) |
41 | | oran 989 |
. . . . . . . . . . 11
β’ ((π΅ = π΄ β¨ π = π΄) β Β¬ (Β¬ π΅ = π΄ β§ Β¬ π = π΄)) |
42 | 40, 41 | sylib 217 |
. . . . . . . . . 10
β’ ((π β§ π β (π΅πΏπ΄)) β Β¬ (Β¬ π΅ = π΄ β§ Β¬ π = π΄)) |
43 | 28, 42 | pm2.65da 816 |
. . . . . . . . 9
β’ (π β Β¬ π β (π΅πΏπ΄)) |
44 | 43 | adantr 482 |
. . . . . . . 8
β’ ((π β§ (π₯ β π β§ (π₯ β (ππΌπ΅) β§ π₯ β (π
πΌπ)))) β Β¬ π β (π΅πΏπ΄)) |
45 | 34 | adantr 482 |
. . . . . . . 8
β’ ((π β§ (π₯ β π β§ (π₯ β (ππΌπ΅) β§ π₯ β (π
πΌπ)))) β (π΄πΏπ΅) = (π΅πΏπ΄)) |
46 | 44, 45 | neleqtrrd 2857 |
. . . . . . 7
β’ ((π β§ (π₯ β π β§ (π₯ β (ππΌπ΅) β§ π₯ β (π
πΌπ)))) β Β¬ π β (π΄πΏπ΅)) |
47 | 18 | adantr 482 |
. . . . . . . 8
β’ ((π β§ (π₯ β π β§ (π₯ β (ππΌπ΅) β§ π₯ β (π
πΌπ)))) β π΄ β π΅) |
48 | 47 | neneqd 2945 |
. . . . . . 7
β’ ((π β§ (π₯ β π β§ (π₯ β (ππΌπ΅) β§ π₯ β (π
πΌπ)))) β Β¬ π΄ = π΅) |
49 | 46, 48 | jca 513 |
. . . . . 6
β’ ((π β§ (π₯ β π β§ (π₯ β (ππΌπ΅) β§ π₯ β (π
πΌπ)))) β (Β¬ π β (π΄πΏπ΅) β§ Β¬ π΄ = π΅)) |
50 | | pm4.56 988 |
. . . . . 6
β’ ((Β¬
π β (π΄πΏπ΅) β§ Β¬ π΄ = π΅) β Β¬ (π β (π΄πΏπ΅) β¨ π΄ = π΅)) |
51 | 49, 50 | sylib 217 |
. . . . 5
β’ ((π β§ (π₯ β π β§ (π₯ β (ππΌπ΅) β§ π₯ β (π
πΌπ)))) β Β¬ (π β (π΄πΏπ΅) β¨ π΄ = π΅)) |
52 | 1, 4, 3, 7, 14, 10, 12, 51 | ncolrot2 27547 |
. . . 4
β’ ((π β§ (π₯ β π β§ (π₯ β (ππΌπ΅) β§ π₯ β (π
πΌπ)))) β Β¬ (π΅ β (ππΏπ΄) β¨ π = π΄)) |
53 | | simprrr 781 |
. . . . . 6
β’ ((π β§ (π₯ β π β§ (π₯ β (ππΌπ΅) β§ π₯ β (π
πΌπ)))) β π₯ β (π
πΌπ)) |
54 | 1, 2, 3, 7, 16, 17, 12, 53 | tgbtwncom 27472 |
. . . . 5
β’ ((π β§ (π₯ β π β§ (π₯ β (ππΌπ΅) β§ π₯ β (π
πΌπ)))) β π₯ β (ππΌπ
)) |
55 | | mideulem.4 |
. . . . . . . 8
β’ (π β π β π) |
56 | 55 | adantr 482 |
. . . . . . 7
β’ ((π β§ (π₯ β π β§ (π₯ β (ππΌπ΅) β§ π₯ β (π
πΌπ)))) β π β π) |
57 | | mideulem.7 |
. . . . . . . 8
β’ (π β π β (π΄πΏπ΅)) |
58 | 57 | adantr 482 |
. . . . . . 7
β’ ((π β§ (π₯ β π β§ (π₯ β (ππΌπ΅) β§ π₯ β (π
πΌπ)))) β π β (π΄πΏπ΅)) |
59 | | simprrl 780 |
. . . . . . 7
β’ ((π β§ (π₯ β π β§ (π₯ β (ππΌπ΅) β§ π₯ β (π
πΌπ)))) β π₯ β (ππΌπ΅)) |
60 | 1, 3, 4, 7, 56, 14, 10, 17, 58, 59 | coltr3 27632 |
. . . . . 6
β’ ((π β§ (π₯ β π β§ (π₯ β (ππΌπ΅) β§ π₯ β (π
πΌπ)))) β π₯ β (π΄πΏπ΅)) |
61 | 43, 34 | neleqtrrd 2857 |
. . . . . . 7
β’ (π β Β¬ π β (π΄πΏπ΅)) |
62 | 61 | adantr 482 |
. . . . . 6
β’ ((π β§ (π₯ β π β§ (π₯ β (ππΌπ΅) β§ π₯ β (π
πΌπ)))) β Β¬ π β (π΄πΏπ΅)) |
63 | | nelne2 3039 |
. . . . . 6
β’ ((π₯ β (π΄πΏπ΅) β§ Β¬ π β (π΄πΏπ΅)) β π₯ β π) |
64 | 60, 62, 63 | syl2anc 585 |
. . . . 5
β’ ((π β§ (π₯ β π β§ (π₯ β (ππΌπ΅) β§ π₯ β (π
πΌπ)))) β π₯ β π) |
65 | 1, 2, 3, 7, 12, 17, 16, 54, 64 | tgbtwnne 27474 |
. . . 4
β’ ((π β§ (π₯ β π β§ (π₯ β (ππΌπ΅) β§ π₯ β (π
πΌπ)))) β π β π
) |
66 | 1, 2, 3, 4, 5, 6, 9, 13, 11 | israg 27681 |
. . . . . . . 8
β’ (π β (β¨βπ΅π΄πββ© β (βGβπΊ) β (π΅ β π) = (π΅ β ((πβπ΄)βπ)))) |
67 | 36, 66 | mpbid 231 |
. . . . . . 7
β’ (π β (π΅ β π) = (π΅ β ((πβπ΄)βπ))) |
68 | 67 | ad3antrrr 729 |
. . . . . 6
β’ ((((π β§ (π₯ β π β§ (π₯ β (ππΌπ΅) β§ π₯ β (π
πΌπ)))) β§ π β π) β§ (π₯ β (((πβπ΄)βπ)πΌπ ) β§ (π₯ β π ) = (π₯ β π
))) β (π΅ β π) = (π΅ β ((πβπ΄)βπ))) |
69 | 6 | ad3antrrr 729 |
. . . . . . 7
β’ ((((π β§ (π₯ β π β§ (π₯ β (ππΌπ΅) β§ π₯ β (π
πΌπ)))) β§ π β π) β§ (π₯ β (((πβπ΄)βπ)πΌπ ) β§ (π₯ β π ) = (π₯ β π
))) β πΊ β TarskiG) |
70 | | eqid 2733 |
. . . . . . . . 9
β’ (πβπ΄) = (πβπ΄) |
71 | 1, 2, 3, 4, 5, 7, 14, 70, 12 | mircl 27645 |
. . . . . . . 8
β’ ((π β§ (π₯ β π β§ (π₯ β (ππΌπ΅) β§ π₯ β (π
πΌπ)))) β ((πβπ΄)βπ) β π) |
72 | 71 | ad2antrr 725 |
. . . . . . 7
β’ ((((π β§ (π₯ β π β§ (π₯ β (ππΌπ΅) β§ π₯ β (π
πΌπ)))) β§ π β π) β§ (π₯ β (((πβπ΄)βπ)πΌπ ) β§ (π₯ β π ) = (π₯ β π
))) β ((πβπ΄)βπ) β π) |
73 | 13 | ad3antrrr 729 |
. . . . . . 7
β’ ((((π β§ (π₯ β π β§ (π₯ β (ππΌπ΅) β§ π₯ β (π
πΌπ)))) β§ π β π) β§ (π₯ β (((πβπ΄)βπ)πΌπ ) β§ (π₯ β π ) = (π₯ β π
))) β π΄ β π) |
74 | 11 | ad3antrrr 729 |
. . . . . . 7
β’ ((((π β§ (π₯ β π β§ (π₯ β (ππΌπ΅) β§ π₯ β (π
πΌπ)))) β§ π β π) β§ (π₯ β (((πβπ΄)βπ)πΌπ ) β§ (π₯ β π ) = (π₯ β π
))) β π β π) |
75 | 15 | ad3antrrr 729 |
. . . . . . 7
β’ ((((π β§ (π₯ β π β§ (π₯ β (ππΌπ΅) β§ π₯ β (π
πΌπ)))) β§ π β π) β§ (π₯ β (((πβπ΄)βπ)πΌπ ) β§ (π₯ β π ) = (π₯ β π
))) β π
β π) |
76 | 9 | ad3antrrr 729 |
. . . . . . 7
β’ ((((π β§ (π₯ β π β§ (π₯ β (ππΌπ΅) β§ π₯ β (π
πΌπ)))) β§ π β π) β§ (π₯ β (((πβπ΄)βπ)πΌπ ) β§ (π₯ β π ) = (π₯ β π
))) β π΅ β π) |
77 | | simplr 768 |
. . . . . . 7
β’ ((((π β§ (π₯ β π β§ (π₯ β (ππΌπ΅) β§ π₯ β (π
πΌπ)))) β§ π β π) β§ (π₯ β (((πβπ΄)βπ)πΌπ ) β§ (π₯ β π ) = (π₯ β π
))) β π β π) |
78 | 1, 2, 3, 4, 5, 69,
73, 70, 74 | mirbtwn 27642 |
. . . . . . 7
β’ ((((π β§ (π₯ β π β§ (π₯ β (ππΌπ΅) β§ π₯ β (π
πΌπ)))) β§ π β π) β§ (π₯ β (((πβπ΄)βπ)πΌπ ) β§ (π₯ β π ) = (π₯ β π
))) β π΄ β (((πβπ΄)βπ)πΌπ)) |
79 | | eqid 2733 |
. . . . . . . . 9
β’ (πβπ΅) = (πβπ΅) |
80 | 1, 2, 3, 4, 5, 69,
76, 79, 77 | mirbtwn 27642 |
. . . . . . . 8
β’ ((((π β§ (π₯ β π β§ (π₯ β (ππΌπ΅) β§ π₯ β (π
πΌπ)))) β§ π β π) β§ (π₯ β (((πβπ΄)βπ)πΌπ ) β§ (π₯ β π ) = (π₯ β π
))) β π΅ β (((πβπ΅)βπ )πΌπ )) |
81 | | simpr 486 |
. . . . . . . . . . 11
β’
((((((π β§ (π₯ β π β§ (π₯ β (ππΌπ΅) β§ π₯ β (π
πΌπ)))) β§ π β π) β§ (π₯ β (((πβπ΄)βπ)πΌπ ) β§ (π₯ β π ) = (π₯ β π
))) β§ π β π) β§ π
= ((πβπ)βπ )) β π
= ((πβπ)βπ )) |
82 | 69 | ad2antrr 725 |
. . . . . . . . . . . . . . 15
β’
((((((π β§ (π₯ β π β§ (π₯ β (ππΌπ΅) β§ π₯ β (π
πΌπ)))) β§ π β π) β§ (π₯ β (((πβπ΄)βπ)πΌπ ) β§ (π₯ β π ) = (π₯ β π
))) β§ π β π) β§ π
= ((πβπ)βπ )) β πΊ β TarskiG) |
83 | 73 | ad2antrr 725 |
. . . . . . . . . . . . . . 15
β’
((((((π β§ (π₯ β π β§ (π₯ β (ππΌπ΅) β§ π₯ β (π
πΌπ)))) β§ π β π) β§ (π₯ β (((πβπ΄)βπ)πΌπ ) β§ (π₯ β π ) = (π₯ β π
))) β§ π β π) β§ π
= ((πβπ)βπ )) β π΄ β π) |
84 | 76 | ad2antrr 725 |
. . . . . . . . . . . . . . 15
β’
((((((π β§ (π₯ β π β§ (π₯ β (ππΌπ΅) β§ π₯ β (π
πΌπ)))) β§ π β π) β§ (π₯ β (((πβπ΄)βπ)πΌπ ) β§ (π₯ β π ) = (π₯ β π
))) β§ π β π) β§ π
= ((πβπ)βπ )) β π΅ β π) |
85 | 47 | ad4antr 731 |
. . . . . . . . . . . . . . 15
β’
((((((π β§ (π₯ β π β§ (π₯ β (ππΌπ΅) β§ π₯ β (π
πΌπ)))) β§ π β π) β§ (π₯ β (((πβπ΄)βπ)πΌπ ) β§ (π₯ β π ) = (π₯ β π
))) β§ π β π) β§ π
= ((πβπ)βπ )) β π΄ β π΅) |
86 | | mideulem.2 |
. . . . . . . . . . . . . . . 16
β’ (π β π β π) |
87 | 86 | ad5antr 733 |
. . . . . . . . . . . . . . 15
β’
((((((π β§ (π₯ β π β§ (π₯ β (ππΌπ΅) β§ π₯ β (π
πΌπ)))) β§ π β π) β§ (π₯ β (((πβπ΄)βπ)πΌπ ) β§ (π₯ β π ) = (π₯ β π
))) β§ π β π) β§ π
= ((πβπ)βπ )) β π β π) |
88 | 74 | ad2antrr 725 |
. . . . . . . . . . . . . . 15
β’
((((((π β§ (π₯ β π β§ (π₯ β (ππΌπ΅) β§ π₯ β (π
πΌπ)))) β§ π β π) β§ (π₯ β (((πβπ΄)βπ)πΌπ ) β§ (π₯ β π ) = (π₯ β π
))) β§ π β π) β§ π
= ((πβπ)βπ )) β π β π) |
89 | 56 | ad4antr 731 |
. . . . . . . . . . . . . . 15
β’
((((((π β§ (π₯ β π β§ (π₯ β (ππΌπ΅) β§ π₯ β (π
πΌπ)))) β§ π β π) β§ (π₯ β (((πβπ΄)βπ)πΌπ ) β§ (π₯ β π ) = (π₯ β π
))) β§ π β π) β§ π
= ((πβπ)βπ )) β π β π) |
90 | | mideulem.5 |
. . . . . . . . . . . . . . . 16
β’ (π β (π΄πΏπ΅)(βGβπΊ)(ππΏπ΅)) |
91 | 90 | ad5antr 733 |
. . . . . . . . . . . . . . 15
β’
((((((π β§ (π₯ β π β§ (π₯ β (ππΌπ΅) β§ π₯ β (π
πΌπ)))) β§ π β π) β§ (π₯ β (((πβπ΄)βπ)πΌπ ) β§ (π₯ β π ) = (π₯ β π
))) β§ π β π) β§ π
= ((πβπ)βπ )) β (π΄πΏπ΅)(βGβπΊ)(ππΏπ΅)) |
92 | 22 | ad5antr 733 |
. . . . . . . . . . . . . . 15
β’
((((((π β§ (π₯ β π β§ (π₯ β (ππΌπ΅) β§ π₯ β (π
πΌπ)))) β§ π β π) β§ (π₯ β (((πβπ΄)βπ)πΌπ ) β§ (π₯ β π ) = (π₯ β π
))) β§ π β π) β§ π
= ((πβπ)βπ )) β (π΄πΏπ΅)(βGβπΊ)(π΄πΏπ)) |
93 | 58 | ad4antr 731 |
. . . . . . . . . . . . . . 15
β’
((((((π β§ (π₯ β π β§ (π₯ β (ππΌπ΅) β§ π₯ β (π
πΌπ)))) β§ π β π) β§ (π₯ β (((πβπ΄)βπ)πΌπ ) β§ (π₯ β π ) = (π₯ β π
))) β§ π β π) β§ π
= ((πβπ)βπ )) β π β (π΄πΏπ΅)) |
94 | | mideulem.8 |
. . . . . . . . . . . . . . . 16
β’ (π β π β (ππΌπ)) |
95 | 94 | ad5antr 733 |
. . . . . . . . . . . . . . 15
β’
((((((π β§ (π₯ β π β§ (π₯ β (ππΌπ΅) β§ π₯ β (π
πΌπ)))) β§ π β π) β§ (π₯ β (((πβπ΄)βπ)πΌπ ) β§ (π₯ β π ) = (π₯ β π
))) β§ π β π) β§ π
= ((πβπ)βπ )) β π β (ππΌπ)) |
96 | 75 | ad2antrr 725 |
. . . . . . . . . . . . . . 15
β’
((((((π β§ (π₯ β π β§ (π₯ β (ππΌπ΅) β§ π₯ β (π
πΌπ)))) β§ π β π) β§ (π₯ β (((πβπ΄)βπ)πΌπ ) β§ (π₯ β π ) = (π₯ β π
))) β§ π β π) β§ π
= ((πβπ)βπ )) β π
β π) |
97 | | opphllem.2 |
. . . . . . . . . . . . . . . 16
β’ (π β π
β (π΅πΌπ)) |
98 | 97 | ad5antr 733 |
. . . . . . . . . . . . . . 15
β’
((((((π β§ (π₯ β π β§ (π₯ β (ππΌπ΅) β§ π₯ β (π
πΌπ)))) β§ π β π) β§ (π₯ β (((πβπ΄)βπ)πΌπ ) β§ (π₯ β π ) = (π₯ β π
))) β§ π β π) β§ π
= ((πβπ)βπ )) β π
β (π΅πΌπ)) |
99 | | opphllem.3 |
. . . . . . . . . . . . . . . 16
β’ (π β (π΄ β π) = (π΅ β π
)) |
100 | 99 | ad5antr 733 |
. . . . . . . . . . . . . . 15
β’
((((((π β§ (π₯ β π β§ (π₯ β (ππΌπ΅) β§ π₯ β (π
πΌπ)))) β§ π β π) β§ (π₯ β (((πβπ΄)βπ)πΌπ ) β§ (π₯ β π ) = (π₯ β π
))) β§ π β π) β§ π
= ((πβπ)βπ )) β (π΄ β π) = (π΅ β π
)) |
101 | 17 | ad2antrr 725 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ (π₯ β π β§ (π₯ β (ππΌπ΅) β§ π₯ β (π
πΌπ)))) β§ π β π) β§ (π₯ β (((πβπ΄)βπ)πΌπ ) β§ (π₯ β π ) = (π₯ β π
))) β π₯ β π) |
102 | 101 | ad2antrr 725 |
. . . . . . . . . . . . . . 15
β’
((((((π β§ (π₯ β π β§ (π₯ β (ππΌπ΅) β§ π₯ β (π
πΌπ)))) β§ π β π) β§ (π₯ β (((πβπ΄)βπ)πΌπ ) β§ (π₯ β π ) = (π₯ β π
))) β§ π β π) β§ π
= ((πβπ)βπ )) β π₯ β π) |
103 | | simp-5r 785 |
. . . . . . . . . . . . . . . . 17
β’
((((((π β§ (π₯ β π β§ (π₯ β (ππΌπ΅) β§ π₯ β (π
πΌπ)))) β§ π β π) β§ (π₯ β (((πβπ΄)βπ)πΌπ ) β§ (π₯ β π ) = (π₯ β π
))) β§ π β π) β§ π
= ((πβπ)βπ )) β (π₯ β π β§ (π₯ β (ππΌπ΅) β§ π₯ β (π
πΌπ)))) |
104 | 103 | simprd 497 |
. . . . . . . . . . . . . . . 16
β’
((((((π β§ (π₯ β π β§ (π₯ β (ππΌπ΅) β§ π₯ β (π
πΌπ)))) β§ π β π) β§ (π₯ β (((πβπ΄)βπ)πΌπ ) β§ (π₯ β π ) = (π₯ β π
))) β§ π β π) β§ π
= ((πβπ)βπ )) β (π₯ β (ππΌπ΅) β§ π₯ β (π
πΌπ))) |
105 | 104 | simpld 496 |
. . . . . . . . . . . . . . 15
β’
((((((π β§ (π₯ β π β§ (π₯ β (ππΌπ΅) β§ π₯ β (π
πΌπ)))) β§ π β π) β§ (π₯ β (((πβπ΄)βπ)πΌπ ) β§ (π₯ β π ) = (π₯ β π
))) β§ π β π) β§ π
= ((πβπ)βπ )) β π₯ β (ππΌπ΅)) |
106 | 104 | simprd 497 |
. . . . . . . . . . . . . . 15
β’
((((((π β§ (π₯ β π β§ (π₯ β (ππΌπ΅) β§ π₯ β (π
πΌπ)))) β§ π β π) β§ (π₯ β (((πβπ΄)βπ)πΌπ ) β§ (π₯ β π ) = (π₯ β π
))) β§ π β π) β§ π
= ((πβπ)βπ )) β π₯ β (π
πΌπ)) |
107 | 77 | ad2antrr 725 |
. . . . . . . . . . . . . . 15
β’
((((((π β§ (π₯ β π β§ (π₯ β (ππΌπ΅) β§ π₯ β (π
πΌπ)))) β§ π β π) β§ (π₯ β (((πβπ΄)βπ)πΌπ ) β§ (π₯ β π ) = (π₯ β π
))) β§ π β π) β§ π
= ((πβπ)βπ )) β π β π) |
108 | | simpllr 775 |
. . . . . . . . . . . . . . . 16
β’
((((((π β§ (π₯ β π β§ (π₯ β (ππΌπ΅) β§ π₯ β (π
πΌπ)))) β§ π β π) β§ (π₯ β (((πβπ΄)βπ)πΌπ ) β§ (π₯ β π ) = (π₯ β π
))) β§ π β π) β§ π
= ((πβπ)βπ )) β (π₯ β (((πβπ΄)βπ)πΌπ ) β§ (π₯ β π ) = (π₯ β π
))) |
109 | 108 | simpld 496 |
. . . . . . . . . . . . . . 15
β’
((((((π β§ (π₯ β π β§ (π₯ β (ππΌπ΅) β§ π₯ β (π
πΌπ)))) β§ π β π) β§ (π₯ β (((πβπ΄)βπ)πΌπ ) β§ (π₯ β π ) = (π₯ β π
))) β§ π β π) β§ π
= ((πβπ)βπ )) β π₯ β (((πβπ΄)βπ)πΌπ )) |
110 | | simprr 772 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ (π₯ β π β§ (π₯ β (ππΌπ΅) β§ π₯ β (π
πΌπ)))) β§ π β π) β§ (π₯ β (((πβπ΄)βπ)πΌπ ) β§ (π₯ β π ) = (π₯ β π
))) β (π₯ β π ) = (π₯ β π
)) |
111 | 110 | ad2antrr 725 |
. . . . . . . . . . . . . . 15
β’
((((((π β§ (π₯ β π β§ (π₯ β (ππΌπ΅) β§ π₯ β (π
πΌπ)))) β§ π β π) β§ (π₯ β (((πβπ΄)βπ)πΌπ ) β§ (π₯ β π ) = (π₯ β π
))) β§ π β π) β§ π
= ((πβπ)βπ )) β (π₯ β π ) = (π₯ β π
)) |
112 | | simplr 768 |
. . . . . . . . . . . . . . 15
β’
((((((π β§ (π₯ β π β§ (π₯ β (ππΌπ΅) β§ π₯ β (π
πΌπ)))) β§ π β π) β§ (π₯ β (((πβπ΄)βπ)πΌπ ) β§ (π₯ β π ) = (π₯ β π
))) β§ π β π) β§ π
= ((πβπ)βπ )) β π β π) |
113 | 1, 2, 3, 4, 82, 5,
83, 84, 85, 87, 88, 89, 91, 92, 93, 95, 96, 98, 100, 102, 105, 106, 107, 109, 111, 112, 81 | mideulem2 27718 |
. . . . . . . . . . . . . 14
β’
((((((π β§ (π₯ β π β§ (π₯ β (ππΌπ΅) β§ π₯ β (π
πΌπ)))) β§ π β π) β§ (π₯ β (((πβπ΄)βπ)πΌπ ) β§ (π₯ β π ) = (π₯ β π
))) β§ π β π) β§ π
= ((πβπ)βπ )) β π΅ = π) |
114 | 113 | eqcomd 2739 |
. . . . . . . . . . . . 13
β’
((((((π β§ (π₯ β π β§ (π₯ β (ππΌπ΅) β§ π₯ β (π
πΌπ)))) β§ π β π) β§ (π₯ β (((πβπ΄)βπ)πΌπ ) β§ (π₯ β π ) = (π₯ β π
))) β§ π β π) β§ π
= ((πβπ)βπ )) β π = π΅) |
115 | 114 | fveq2d 6847 |
. . . . . . . . . . . 12
β’
((((((π β§ (π₯ β π β§ (π₯ β (ππΌπ΅) β§ π₯ β (π
πΌπ)))) β§ π β π) β§ (π₯ β (((πβπ΄)βπ)πΌπ ) β§ (π₯ β π ) = (π₯ β π
))) β§ π β π) β§ π
= ((πβπ)βπ )) β (πβπ) = (πβπ΅)) |
116 | 115 | fveq1d 6845 |
. . . . . . . . . . 11
β’
((((((π β§ (π₯ β π β§ (π₯ β (ππΌπ΅) β§ π₯ β (π
πΌπ)))) β§ π β π) β§ (π₯ β (((πβπ΄)βπ)πΌπ ) β§ (π₯ β π ) = (π₯ β π
))) β§ π β π) β§ π
= ((πβπ)βπ )) β ((πβπ)βπ ) = ((πβπ΅)βπ )) |
117 | 81, 116 | eqtrd 2773 |
. . . . . . . . . 10
β’
((((((π β§ (π₯ β π β§ (π₯ β (ππΌπ΅) β§ π₯ β (π
πΌπ)))) β§ π β π) β§ (π₯ β (((πβπ΄)βπ)πΌπ ) β§ (π₯ β π ) = (π₯ β π
))) β§ π β π) β§ π
= ((πβπ)βπ )) β π
= ((πβπ΅)βπ )) |
118 | | eqid 2733 |
. . . . . . . . . . 11
β’ (πβπ) = (πβπ) |
119 | 1, 2, 3, 4, 5, 69,
118, 77, 75, 101, 110 | midexlem 27676 |
. . . . . . . . . 10
β’ ((((π β§ (π₯ β π β§ (π₯ β (ππΌπ΅) β§ π₯ β (π
πΌπ)))) β§ π β π) β§ (π₯ β (((πβπ΄)βπ)πΌπ ) β§ (π₯ β π ) = (π₯ β π
))) β βπ β π π
= ((πβπ)βπ )) |
120 | 117, 119 | r19.29a 3156 |
. . . . . . . . 9
β’ ((((π β§ (π₯ β π β§ (π₯ β (ππΌπ΅) β§ π₯ β (π
πΌπ)))) β§ π β π) β§ (π₯ β (((πβπ΄)βπ)πΌπ ) β§ (π₯ β π ) = (π₯ β π
))) β π
= ((πβπ΅)βπ )) |
121 | 120 | oveq1d 7373 |
. . . . . . . 8
β’ ((((π β§ (π₯ β π β§ (π₯ β (ππΌπ΅) β§ π₯ β (π
πΌπ)))) β§ π β π) β§ (π₯ β (((πβπ΄)βπ)πΌπ ) β§ (π₯ β π ) = (π₯ β π
))) β (π
πΌπ ) = (((πβπ΅)βπ )πΌπ )) |
122 | 80, 121 | eleqtrrd 2837 |
. . . . . . 7
β’ ((((π β§ (π₯ β π β§ (π₯ β (ππΌπ΅) β§ π₯ β (π
πΌπ)))) β§ π β π) β§ (π₯ β (((πβπ΄)βπ)πΌπ ) β§ (π₯ β π ) = (π₯ β π
))) β π΅ β (π
πΌπ )) |
123 | 1, 2, 3, 4, 5, 69,
73, 70, 74 | mircgr 27641 |
. . . . . . . . . 10
β’ ((((π β§ (π₯ β π β§ (π₯ β (ππΌπ΅) β§ π₯ β (π
πΌπ)))) β§ π β π) β§ (π₯ β (((πβπ΄)βπ)πΌπ ) β§ (π₯ β π ) = (π₯ β π
))) β (π΄ β ((πβπ΄)βπ)) = (π΄ β π)) |
124 | 99 | ad3antrrr 729 |
. . . . . . . . . 10
β’ ((((π β§ (π₯ β π β§ (π₯ β (ππΌπ΅) β§ π₯ β (π
πΌπ)))) β§ π β π) β§ (π₯ β (((πβπ΄)βπ)πΌπ ) β§ (π₯ β π ) = (π₯ β π
))) β (π΄ β π) = (π΅ β π
)) |
125 | 123, 124 | eqtrd 2773 |
. . . . . . . . 9
β’ ((((π β§ (π₯ β π β§ (π₯ β (ππΌπ΅) β§ π₯ β (π
πΌπ)))) β§ π β π) β§ (π₯ β (((πβπ΄)βπ)πΌπ ) β§ (π₯ β π ) = (π₯ β π
))) β (π΄ β ((πβπ΄)βπ)) = (π΅ β π
)) |
126 | 1, 2, 3, 69, 73, 72, 76, 75, 125 | tgcgrcomlr 27464 |
. . . . . . . 8
β’ ((((π β§ (π₯ β π β§ (π₯ β (ππΌπ΅) β§ π₯ β (π
πΌπ)))) β§ π β π) β§ (π₯ β (((πβπ΄)βπ)πΌπ ) β§ (π₯ β π ) = (π₯ β π
))) β (((πβπ΄)βπ) β π΄) = (π
β π΅)) |
127 | 120 | oveq2d 7374 |
. . . . . . . . 9
β’ ((((π β§ (π₯ β π β§ (π₯ β (ππΌπ΅) β§ π₯ β (π
πΌπ)))) β§ π β π) β§ (π₯ β (((πβπ΄)βπ)πΌπ ) β§ (π₯ β π ) = (π₯ β π
))) β (π΅ β π
) = (π΅ β ((πβπ΅)βπ ))) |
128 | 1, 2, 3, 4, 5, 69,
76, 79, 77 | mircgr 27641 |
. . . . . . . . 9
β’ ((((π β§ (π₯ β π β§ (π₯ β (ππΌπ΅) β§ π₯ β (π
πΌπ)))) β§ π β π) β§ (π₯ β (((πβπ΄)βπ)πΌπ ) β§ (π₯ β π ) = (π₯ β π
))) β (π΅ β ((πβπ΅)βπ )) = (π΅ β π )) |
129 | 124, 127,
128 | 3eqtrd 2777 |
. . . . . . . 8
β’ ((((π β§ (π₯ β π β§ (π₯ β (ππΌπ΅) β§ π₯ β (π
πΌπ)))) β§ π β π) β§ (π₯ β (((πβπ΄)βπ)πΌπ ) β§ (π₯ β π ) = (π₯ β π
))) β (π΄ β π) = (π΅ β π )) |
130 | 1, 2, 3, 69, 72, 73, 74, 75, 76, 77, 78, 122, 126, 129 | tgcgrextend 27469 |
. . . . . . 7
β’ ((((π β§ (π₯ β π β§ (π₯ β (ππΌπ΅) β§ π₯ β (π
πΌπ)))) β§ π β π) β§ (π₯ β (((πβπ΄)βπ)πΌπ ) β§ (π₯ β π ) = (π₯ β π
))) β (((πβπ΄)βπ) β π) = (π
β π )) |
131 | 1, 2, 3, 69, 72, 75 | axtgcgrrflx 27446 |
. . . . . . 7
β’ ((((π β§ (π₯ β π β§ (π₯ β (ππΌπ΅) β§ π₯ β (π
πΌπ)))) β§ π β π) β§ (π₯ β (((πβπ΄)βπ)πΌπ ) β§ (π₯ β π ) = (π₯ β π
))) β (((πβπ΄)βπ) β π
) = (π
β ((πβπ΄)βπ))) |
132 | 1, 2, 3, 69, 74, 75 | axtgcgrrflx 27446 |
. . . . . . . 8
β’ ((((π β§ (π₯ β π β§ (π₯ β (ππΌπ΅) β§ π₯ β (π
πΌπ)))) β§ π β π) β§ (π₯ β (((πβπ΄)βπ)πΌπ ) β§ (π₯ β π ) = (π₯ β π
))) β (π β π
) = (π
β π)) |
133 | 53 | ad2antrr 725 |
. . . . . . . . 9
β’ ((((π β§ (π₯ β π β§ (π₯ β (ππΌπ΅) β§ π₯ β (π
πΌπ)))) β§ π β π) β§ (π₯ β (((πβπ΄)βπ)πΌπ ) β§ (π₯ β π ) = (π₯ β π
))) β π₯ β (π
πΌπ)) |
134 | | simprl 770 |
. . . . . . . . . 10
β’ ((((π β§ (π₯ β π β§ (π₯ β (ππΌπ΅) β§ π₯ β (π
πΌπ)))) β§ π β π) β§ (π₯ β (((πβπ΄)βπ)πΌπ ) β§ (π₯ β π ) = (π₯ β π
))) β π₯ β (((πβπ΄)βπ)πΌπ )) |
135 | 1, 2, 3, 69, 72, 101, 77, 134 | tgbtwncom 27472 |
. . . . . . . . 9
β’ ((((π β§ (π₯ β π β§ (π₯ β (ππΌπ΅) β§ π₯ β (π
πΌπ)))) β§ π β π) β§ (π₯ β (((πβπ΄)βπ)πΌπ ) β§ (π₯ β π ) = (π₯ β π
))) β π₯ β (π πΌ((πβπ΄)βπ))) |
136 | 1, 2, 3, 69, 101, 77, 101, 75, 110 | tgcgrcomlr 27464 |
. . . . . . . . . 10
β’ ((((π β§ (π₯ β π β§ (π₯ β (ππΌπ΅) β§ π₯ β (π
πΌπ)))) β§ π β π) β§ (π₯ β (((πβπ΄)βπ)πΌπ ) β§ (π₯ β π ) = (π₯ β π
))) β (π β π₯) = (π
β π₯)) |
137 | 136 | eqcomd 2739 |
. . . . . . . . 9
β’ ((((π β§ (π₯ β π β§ (π₯ β (ππΌπ΅) β§ π₯ β (π
πΌπ)))) β§ π β π) β§ (π₯ β (((πβπ΄)βπ)πΌπ ) β§ (π₯ β π ) = (π₯ β π
))) β (π
β π₯) = (π β π₯)) |
138 | 36 | ad3antrrr 729 |
. . . . . . . . . . 11
β’ ((((π β§ (π₯ β π β§ (π₯ β (ππΌπ΅) β§ π₯ β (π
πΌπ)))) β§ π β π) β§ (π₯ β (((πβπ΄)βπ)πΌπ ) β§ (π₯ β π ) = (π₯ β π
))) β β¨βπ΅π΄πββ© β (βGβπΊ)) |
139 | 47 | necomd 2996 |
. . . . . . . . . . . 12
β’ ((π β§ (π₯ β π β§ (π₯ β (ππΌπ΅) β§ π₯ β (π
πΌπ)))) β π΅ β π΄) |
140 | 139 | ad2antrr 725 |
. . . . . . . . . . 11
β’ ((((π β§ (π₯ β π β§ (π₯ β (ππΌπ΅) β§ π₯ β (π
πΌπ)))) β§ π β π) β§ (π₯ β (((πβπ΄)βπ)πΌπ ) β§ (π₯ β π ) = (π₯ β π
))) β π΅ β π΄) |
141 | 60 | ad2antrr 725 |
. . . . . . . . . . . . . 14
β’ ((((π β§ (π₯ β π β§ (π₯ β (ππΌπ΅) β§ π₯ β (π
πΌπ)))) β§ π β π) β§ (π₯ β (((πβπ΄)βπ)πΌπ ) β§ (π₯ β π ) = (π₯ β π
))) β π₯ β (π΄πΏπ΅)) |
142 | 141 | orcd 872 |
. . . . . . . . . . . . 13
β’ ((((π β§ (π₯ β π β§ (π₯ β (ππΌπ΅) β§ π₯ β (π
πΌπ)))) β§ π β π) β§ (π₯ β (((πβπ΄)βπ)πΌπ ) β§ (π₯ β π ) = (π₯ β π
))) β (π₯ β (π΄πΏπ΅) β¨ π΄ = π΅)) |
143 | 1, 4, 3, 69, 73, 76, 101, 142 | colcom 27542 |
. . . . . . . . . . . 12
β’ ((((π β§ (π₯ β π β§ (π₯ β (ππΌπ΅) β§ π₯ β (π
πΌπ)))) β§ π β π) β§ (π₯ β (((πβπ΄)βπ)πΌπ ) β§ (π₯ β π ) = (π₯ β π
))) β (π₯ β (π΅πΏπ΄) β¨ π΅ = π΄)) |
144 | 1, 4, 3, 69, 76, 73, 101, 143 | colrot1 27543 |
. . . . . . . . . . 11
β’ ((((π β§ (π₯ β π β§ (π₯ β (ππΌπ΅) β§ π₯ β (π
πΌπ)))) β§ π β π) β§ (π₯ β (((πβπ΄)βπ)πΌπ ) β§ (π₯ β π ) = (π₯ β π
))) β (π΅ β (π΄πΏπ₯) β¨ π΄ = π₯)) |
145 | 1, 2, 3, 4, 5, 69,
76, 73, 74, 101, 138, 140, 144 | ragcol 27683 |
. . . . . . . . . 10
β’ ((((π β§ (π₯ β π β§ (π₯ β (ππΌπ΅) β§ π₯ β (π
πΌπ)))) β§ π β π) β§ (π₯ β (((πβπ΄)βπ)πΌπ ) β§ (π₯ β π ) = (π₯ β π
))) β β¨βπ₯π΄πββ© β (βGβπΊ)) |
146 | 1, 2, 3, 4, 5, 69,
101, 73, 74 | israg 27681 |
. . . . . . . . . 10
β’ ((((π β§ (π₯ β π β§ (π₯ β (ππΌπ΅) β§ π₯ β (π
πΌπ)))) β§ π β π) β§ (π₯ β (((πβπ΄)βπ)πΌπ ) β§ (π₯ β π ) = (π₯ β π
))) β (β¨βπ₯π΄πββ© β (βGβπΊ) β (π₯ β π) = (π₯ β ((πβπ΄)βπ)))) |
147 | 145, 146 | mpbid 231 |
. . . . . . . . 9
β’ ((((π β§ (π₯ β π β§ (π₯ β (ππΌπ΅) β§ π₯ β (π
πΌπ)))) β§ π β π) β§ (π₯ β (((πβπ΄)βπ)πΌπ ) β§ (π₯ β π ) = (π₯ β π
))) β (π₯ β π) = (π₯ β ((πβπ΄)βπ))) |
148 | 1, 2, 3, 69, 75, 101, 74, 77, 101, 72, 133, 135, 137, 147 | tgcgrextend 27469 |
. . . . . . . 8
β’ ((((π β§ (π₯ β π β§ (π₯ β (ππΌπ΅) β§ π₯ β (π
πΌπ)))) β§ π β π) β§ (π₯ β (((πβπ΄)βπ)πΌπ ) β§ (π₯ β π ) = (π₯ β π
))) β (π
β π) = (π β ((πβπ΄)βπ))) |
149 | 132, 148 | eqtrd 2773 |
. . . . . . 7
β’ ((((π β§ (π₯ β π β§ (π₯ β (ππΌπ΅) β§ π₯ β (π
πΌπ)))) β§ π β π) β§ (π₯ β (((πβπ΄)βπ)πΌπ ) β§ (π₯ β π ) = (π₯ β π
))) β (π β π
) = (π β ((πβπ΄)βπ))) |
150 | 1, 2, 3, 69, 72, 73, 74, 75, 75, 76, 77, 72, 78, 122, 130, 129, 131, 149 | tgifscgr 27492 |
. . . . . 6
β’ ((((π β§ (π₯ β π β§ (π₯ β (ππΌπ΅) β§ π₯ β (π
πΌπ)))) β§ π β π) β§ (π₯ β (((πβπ΄)βπ)πΌπ ) β§ (π₯ β π ) = (π₯ β π
))) β (π΄ β π
) = (π΅ β ((πβπ΄)βπ))) |
151 | 68, 150 | eqtr4d 2776 |
. . . . 5
β’ ((((π β§ (π₯ β π β§ (π₯ β (ππΌπ΅) β§ π₯ β (π
πΌπ)))) β§ π β π) β§ (π₯ β (((πβπ΄)βπ)πΌπ ) β§ (π₯ β π ) = (π₯ β π
))) β (π΅ β π) = (π΄ β π
)) |
152 | 1, 2, 3, 7, 71, 17, 17, 16 | axtgsegcon 27448 |
. . . . 5
β’ ((π β§ (π₯ β π β§ (π₯ β (ππΌπ΅) β§ π₯ β (π
πΌπ)))) β βπ β π (π₯ β (((πβπ΄)βπ)πΌπ ) β§ (π₯ β π ) = (π₯ β π
))) |
153 | 151, 152 | r19.29a 3156 |
. . . 4
β’ ((π β§ (π₯ β π β§ (π₯ β (ππΌπ΅) β§ π₯ β (π
πΌπ)))) β (π΅ β π) = (π΄ β π
)) |
154 | 99 | adantr 482 |
. . . . 5
β’ ((π β§ (π₯ β π β§ (π₯ β (ππΌπ΅) β§ π₯ β (π
πΌπ)))) β (π΄ β π) = (π΅ β π
)) |
155 | 1, 2, 3, 7, 14, 12, 10, 16, 154 | tgcgrcomlr 27464 |
. . . 4
β’ ((π β§ (π₯ β π β§ (π₯ β (ππΌπ΅) β§ π₯ β (π
πΌπ)))) β (π β π΄) = (π
β π΅)) |
156 | 143, 152 | r19.29a 3156 |
. . . 4
β’ ((π β§ (π₯ β π β§ (π₯ β (ππΌπ΅) β§ π₯ β (π
πΌπ)))) β (π₯ β (π΅πΏπ΄) β¨ π΅ = π΄)) |
157 | 1, 4, 3, 7, 12, 16, 17, 54 | btwncolg1 27539 |
. . . 4
β’ ((π β§ (π₯ β π β§ (π₯ β (ππΌπ΅) β§ π₯ β (π
πΌπ)))) β (π₯ β (ππΏπ
) β¨ π = π
)) |
158 | 1, 2, 3, 4, 5, 7, 8, 10, 12, 14, 16, 17, 52, 65, 153, 155, 156, 157 | symquadlem 27673 |
. . 3
β’ ((π β§ (π₯ β π β§ (π₯ β (ππΌπ΅) β§ π₯ β (π
πΌπ)))) β π΅ = ((πβπ₯)βπ΄)) |
159 | 1, 2, 3, 4, 5, 7, 17, 8, 14 | mirbtwn 27642 |
. . . . . . 7
β’ ((π β§ (π₯ β π β§ (π₯ β (ππΌπ΅) β§ π₯ β (π
πΌπ)))) β π₯ β (((πβπ₯)βπ΄)πΌπ΄)) |
160 | 158 | oveq1d 7373 |
. . . . . . 7
β’ ((π β§ (π₯ β π β§ (π₯ β (ππΌπ΅) β§ π₯ β (π
πΌπ)))) β (π΅πΌπ΄) = (((πβπ₯)βπ΄)πΌπ΄)) |
161 | 159, 160 | eleqtrrd 2837 |
. . . . . 6
β’ ((π β§ (π₯ β π β§ (π₯ β (ππΌπ΅) β§ π₯ β (π
πΌπ)))) β π₯ β (π΅πΌπ΄)) |
162 | 1, 2, 3, 7, 10, 17, 14, 161 | tgbtwncom 27472 |
. . . . 5
β’ ((π β§ (π₯ β π β§ (π₯ β (ππΌπ΅) β§ π₯ β (π
πΌπ)))) β π₯ β (π΄πΌπ΅)) |
163 | 1, 2, 3, 7, 14, 10 | axtgcgrrflx 27446 |
. . . . 5
β’ ((π β§ (π₯ β π β§ (π₯ β (ππΌπ΅) β§ π₯ β (π
πΌπ)))) β (π΄ β π΅) = (π΅ β π΄)) |
164 | 158 | oveq2d 7374 |
. . . . . 6
β’ ((π β§ (π₯ β π β§ (π₯ β (ππΌπ΅) β§ π₯ β (π
πΌπ)))) β (π₯ β π΅) = (π₯ β ((πβπ₯)βπ΄))) |
165 | 1, 2, 3, 4, 5, 7, 17, 8, 14 | mircgr 27641 |
. . . . . 6
β’ ((π β§ (π₯ β π β§ (π₯ β (ππΌπ΅) β§ π₯ β (π
πΌπ)))) β (π₯ β ((πβπ₯)βπ΄)) = (π₯ β π΄)) |
166 | 164, 165 | eqtrd 2773 |
. . . . 5
β’ ((π β§ (π₯ β π β§ (π₯ β (ππΌπ΅) β§ π₯ β (π
πΌπ)))) β (π₯ β π΅) = (π₯ β π΄)) |
167 | 1, 2, 3, 7, 14, 17, 10, 12, 10, 17, 14, 16, 162, 161, 163, 166, 154, 153 | tgifscgr 27492 |
. . . 4
β’ ((π β§ (π₯ β π β§ (π₯ β (ππΌπ΅) β§ π₯ β (π
πΌπ)))) β (π₯ β π) = (π₯ β π
)) |
168 | 1, 2, 3, 4, 5, 7, 17, 8, 16, 12, 167, 54 | ismir 27643 |
. . 3
β’ ((π β§ (π₯ β π β§ (π₯ β (ππΌπ΅) β§ π₯ β (π
πΌπ)))) β π = ((πβπ₯)βπ
)) |
169 | 158, 168 | jca 513 |
. 2
β’ ((π β§ (π₯ β π β§ (π₯ β (ππΌπ΅) β§ π₯ β (π
πΌπ)))) β (π΅ = ((πβπ₯)βπ΄) β§ π = ((πβπ₯)βπ
))) |
170 | 1, 2, 3, 6, 86, 55, 11, 94 | tgbtwncom 27472 |
. . 3
β’ (π β π β (ππΌπ)) |
171 | 1, 2, 3, 6, 11, 9,
86, 55, 15, 170, 97 | axtgpasch 27451 |
. 2
β’ (π β βπ₯ β π (π₯ β (ππΌπ΅) β§ π₯ β (π
πΌπ))) |
172 | 169, 171 | reximddv 3165 |
1
β’ (π β βπ₯ β π (π΅ = ((πβπ₯)βπ΄) β§ π = ((πβπ₯)βπ
))) |