Step | Hyp | Ref
| Expression |
1 | | isperp.p |
. . . . . . . . 9
β’ π = (BaseβπΊ) |
2 | | isperp.d |
. . . . . . . . 9
β’ β =
(distβπΊ) |
3 | | isperp.i |
. . . . . . . . 9
β’ πΌ = (ItvβπΊ) |
4 | | isperp.l |
. . . . . . . . 9
β’ πΏ = (LineGβπΊ) |
5 | | eqid 2732 |
. . . . . . . . 9
β’
(pInvGβπΊ) =
(pInvGβπΊ) |
6 | | isperp.g |
. . . . . . . . . . . . . . 15
β’ (π β πΊ β TarskiG) |
7 | 6 | ad3antrrr 728 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β πΊ β TarskiG) |
8 | 7 | ad2antrr 724 |
. . . . . . . . . . . . 13
β’
((((((π β§ π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β πΊ β TarskiG) |
9 | 8 | ad2antrr 724 |
. . . . . . . . . . . 12
β’
((((((((π β§ π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β§ π β π) β§ πΆ = (((pInvGβπΊ)βπ)βπ¦)) β πΊ β TarskiG) |
10 | 9 | ad2antrr 724 |
. . . . . . . . . . 11
β’
((((((((((π β§
π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β§ π β π) β§ πΆ = (((pInvGβπΊ)βπ)βπ¦)) β§ π§ β π) β§ (π¦ β (ππΌπ§) β§ (π¦ β π§) = (π¦ β π))) β πΊ β TarskiG) |
11 | 10 | ad2antrr 724 |
. . . . . . . . . 10
β’
((((((((((((π β§
π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β§ π β π) β§ πΆ = (((pInvGβπΊ)βπ)βπ¦)) β§ π§ β π) β§ (π¦ β (ππΌπ§) β§ (π¦ β π§) = (π¦ β π))) β§ π β π) β§ (π¦ β (ππΌπ) β§ (π¦ β π) = (π¦ β π))) β πΊ β TarskiG) |
12 | 11 | ad2antrr 724 |
. . . . . . . . 9
β’
((((((((((((((π β§
π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β§ π β π) β§ πΆ = (((pInvGβπΊ)βπ)βπ¦)) β§ π§ β π) β§ (π¦ β (ππΌπ§) β§ (π¦ β π§) = (π¦ β π))) β§ π β π) β§ (π¦ β (ππΌπ) β§ (π¦ β π) = (π¦ β π))) β§ π β π) β§ (π¦ β ((((pInvGβπΊ)βπ§)βπ)πΌπ) β§ (π¦ β π) = (π¦ β πΆ))) β πΊ β TarskiG) |
13 | | eqid 2732 |
. . . . . . . . 9
β’
((pInvGβπΊ)βπ₯) = ((pInvGβπΊ)βπ₯) |
14 | | foot.x |
. . . . . . . . . . . . 13
β’ (π β πΆ β π) |
15 | 14 | ad3antrrr 728 |
. . . . . . . . . . . 12
β’ ((((π β§ π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β πΆ β π) |
16 | 15 | ad2antrr 724 |
. . . . . . . . . . 11
β’
((((((π β§ π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β πΆ β π) |
17 | 16 | ad6antr 734 |
. . . . . . . . . 10
β’
((((((((((((π β§
π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β§ π β π) β§ πΆ = (((pInvGβπΊ)βπ)βπ¦)) β§ π§ β π) β§ (π¦ β (ππΌπ§) β§ (π¦ β π§) = (π¦ β π))) β§ π β π) β§ (π¦ β (ππΌπ) β§ (π¦ β π) = (π¦ β π))) β πΆ β π) |
18 | 17 | ad2antrr 724 |
. . . . . . . . 9
β’
((((((((((((((π β§
π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β§ π β π) β§ πΆ = (((pInvGβπΊ)βπ)βπ¦)) β§ π§ β π) β§ (π¦ β (ππΌπ§) β§ (π¦ β π§) = (π¦ β π))) β§ π β π) β§ (π¦ β (ππΌπ) β§ (π¦ β π) = (π¦ β π))) β§ π β π) β§ (π¦ β ((((pInvGβπΊ)βπ§)βπ)πΌπ) β§ (π¦ β π) = (π¦ β πΆ))) β πΆ β π) |
19 | | simplr 767 |
. . . . . . . . 9
β’
((((((((((((((π β§
π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β§ π β π) β§ πΆ = (((pInvGβπΊ)βπ)βπ¦)) β§ π§ β π) β§ (π¦ β (ππΌπ§) β§ (π¦ β π§) = (π¦ β π))) β§ π β π) β§ (π¦ β (ππΌπ) β§ (π¦ β π) = (π¦ β π))) β§ π β π) β§ (π¦ β ((((pInvGβπΊ)βπ§)βπ)πΌπ) β§ (π¦ β π) = (π¦ β πΆ))) β π β π) |
20 | | simp-4r 782 |
. . . . . . . . . . . 12
β’
((((((((π β§ π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β§ π β π) β§ πΆ = (((pInvGβπΊ)βπ)βπ¦)) β π¦ β π) |
21 | 20 | ad2antrr 724 |
. . . . . . . . . . 11
β’
((((((((((π β§
π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β§ π β π) β§ πΆ = (((pInvGβπΊ)βπ)βπ¦)) β§ π§ β π) β§ (π¦ β (ππΌπ§) β§ (π¦ β π§) = (π¦ β π))) β π¦ β π) |
22 | 21 | ad2antrr 724 |
. . . . . . . . . 10
β’
((((((((((((π β§
π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β§ π β π) β§ πΆ = (((pInvGβπΊ)βπ)βπ¦)) β§ π§ β π) β§ (π¦ β (ππΌπ§) β§ (π¦ β π§) = (π¦ β π))) β§ π β π) β§ (π¦ β (ππΌπ) β§ (π¦ β π) = (π¦ β π))) β π¦ β π) |
23 | 22 | ad2antrr 724 |
. . . . . . . . 9
β’
((((((((((((((π β§
π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β§ π β π) β§ πΆ = (((pInvGβπΊ)βπ)βπ¦)) β§ π§ β π) β§ (π¦ β (ππΌπ§) β§ (π¦ β π§) = (π¦ β π))) β§ π β π) β§ (π¦ β (ππΌπ) β§ (π¦ β π) = (π¦ β π))) β§ π β π) β§ (π¦ β ((((pInvGβπΊ)βπ§)βπ)πΌπ) β§ (π¦ β π) = (π¦ β πΆ))) β π¦ β π) |
24 | | simprr 771 |
. . . . . . . . . 10
β’
((((((((((((((π β§
π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β§ π β π) β§ πΆ = (((pInvGβπΊ)βπ)βπ¦)) β§ π§ β π) β§ (π¦ β (ππΌπ§) β§ (π¦ β π§) = (π¦ β π))) β§ π β π) β§ (π¦ β (ππΌπ) β§ (π¦ β π) = (π¦ β π))) β§ π β π) β§ (π¦ β ((((pInvGβπΊ)βπ§)βπ)πΌπ) β§ (π¦ β π) = (π¦ β πΆ))) β (π¦ β π) = (π¦ β πΆ)) |
25 | 24 | eqcomd 2738 |
. . . . . . . . 9
β’
((((((((((((((π β§
π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β§ π β π) β§ πΆ = (((pInvGβπΊ)βπ)βπ¦)) β§ π§ β π) β§ (π¦ β (ππΌπ§) β§ (π¦ β π§) = (π¦ β π))) β§ π β π) β§ (π¦ β (ππΌπ) β§ (π¦ β π) = (π¦ β π))) β§ π β π) β§ (π¦ β ((((pInvGβπΊ)βπ§)βπ)πΌπ) β§ (π¦ β π) = (π¦ β πΆ))) β (π¦ β πΆ) = (π¦ β π)) |
26 | 1, 2, 3, 4, 5, 12,
13, 18, 19, 23, 25 | midexlem 27932 |
. . . . . . . 8
β’
((((((((((((((π β§
π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β§ π β π) β§ πΆ = (((pInvGβπΊ)βπ)βπ¦)) β§ π§ β π) β§ (π¦ β (ππΌπ§) β§ (π¦ β π§) = (π¦ β π))) β§ π β π) β§ (π¦ β (ππΌπ) β§ (π¦ β π) = (π¦ β π))) β§ π β π) β§ (π¦ β ((((pInvGβπΊ)βπ§)βπ)πΌπ) β§ (π¦ β π) = (π¦ β πΆ))) β βπ₯ β π π = (((pInvGβπΊ)βπ₯)βπΆ)) |
27 | 12 | adantr 481 |
. . . . . . . . . 10
β’
(((((((((((((((π β§
π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β§ π β π) β§ πΆ = (((pInvGβπΊ)βπ)βπ¦)) β§ π§ β π) β§ (π¦ β (ππΌπ§) β§ (π¦ β π§) = (π¦ β π))) β§ π β π) β§ (π¦ β (ππΌπ) β§ (π¦ β π) = (π¦ β π))) β§ π β π) β§ (π¦ β ((((pInvGβπΊ)βπ§)βπ)πΌπ) β§ (π¦ β π) = (π¦ β πΆ))) β§ (π₯ β π β§ π = (((pInvGβπΊ)βπ₯)βπΆ))) β πΊ β TarskiG) |
28 | 23 | adantr 481 |
. . . . . . . . . 10
β’
(((((((((((((((π β§
π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β§ π β π) β§ πΆ = (((pInvGβπΊ)βπ)βπ¦)) β§ π§ β π) β§ (π¦ β (ππΌπ§) β§ (π¦ β π§) = (π¦ β π))) β§ π β π) β§ (π¦ β (ππΌπ) β§ (π¦ β π) = (π¦ β π))) β§ π β π) β§ (π¦ β ((((pInvGβπΊ)βπ§)βπ)πΌπ) β§ (π¦ β π) = (π¦ β πΆ))) β§ (π₯ β π β§ π = (((pInvGβπΊ)βπ₯)βπΆ))) β π¦ β π) |
29 | | simp-6r 786 |
. . . . . . . . . . 11
β’
((((((((((((((π β§
π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β§ π β π) β§ πΆ = (((pInvGβπΊ)βπ)βπ¦)) β§ π§ β π) β§ (π¦ β (ππΌπ§) β§ (π¦ β π§) = (π¦ β π))) β§ π β π) β§ (π¦ β (ππΌπ) β§ (π¦ β π) = (π¦ β π))) β§ π β π) β§ (π¦ β ((((pInvGβπΊ)βπ§)βπ)πΌπ) β§ (π¦ β π) = (π¦ β πΆ))) β π§ β π) |
30 | 29 | adantr 481 |
. . . . . . . . . 10
β’
(((((((((((((((π β§
π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β§ π β π) β§ πΆ = (((pInvGβπΊ)βπ)βπ¦)) β§ π§ β π) β§ (π¦ β (ππΌπ§) β§ (π¦ β π§) = (π¦ β π))) β§ π β π) β§ (π¦ β (ππΌπ) β§ (π¦ β π) = (π¦ β π))) β§ π β π) β§ (π¦ β ((((pInvGβπΊ)βπ§)βπ)πΌπ) β§ (π¦ β π) = (π¦ β πΆ))) β§ (π₯ β π β§ π = (((pInvGβπΊ)βπ₯)βπΆ))) β π§ β π) |
31 | | simprl 769 |
. . . . . . . . . 10
β’
(((((((((((((((π β§
π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β§ π β π) β§ πΆ = (((pInvGβπΊ)βπ)βπ¦)) β§ π§ β π) β§ (π¦ β (ππΌπ§) β§ (π¦ β π§) = (π¦ β π))) β§ π β π) β§ (π¦ β (ππΌπ) β§ (π¦ β π) = (π¦ β π))) β§ π β π) β§ (π¦ β ((((pInvGβπΊ)βπ§)βπ)πΌπ) β§ (π¦ β π) = (π¦ β πΆ))) β§ (π₯ β π β§ π = (((pInvGβπΊ)βπ₯)βπΆ))) β π₯ β π) |
32 | | simp-4r 782 |
. . . . . . . . . . . . 13
β’
((((((((((π β§
π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β§ π β π) β§ πΆ = (((pInvGβπΊ)βπ)βπ¦)) β§ π§ β π) β§ (π¦ β (ππΌπ§) β§ (π¦ β π§) = (π¦ β π))) β π β π) |
33 | 32 | ad4antr 730 |
. . . . . . . . . . . 12
β’
((((((((((((((π β§
π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β§ π β π) β§ πΆ = (((pInvGβπΊ)βπ)βπ¦)) β§ π§ β π) β§ (π¦ β (ππΌπ§) β§ (π¦ β π§) = (π¦ β π))) β§ π β π) β§ (π¦ β (ππΌπ) β§ (π¦ β π) = (π¦ β π))) β§ π β π) β§ (π¦ β ((((pInvGβπΊ)βπ§)βπ)πΌπ) β§ (π¦ β π) = (π¦ β πΆ))) β π β π) |
34 | 33 | adantr 481 |
. . . . . . . . . . 11
β’
(((((((((((((((π β§
π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β§ π β π) β§ πΆ = (((pInvGβπΊ)βπ)βπ¦)) β§ π§ β π) β§ (π¦ β (ππΌπ§) β§ (π¦ β π§) = (π¦ β π))) β§ π β π) β§ (π¦ β (ππΌπ) β§ (π¦ β π) = (π¦ β π))) β§ π β π) β§ (π¦ β ((((pInvGβπΊ)βπ§)βπ)πΌπ) β§ (π¦ β π) = (π¦ β πΆ))) β§ (π₯ β π β§ π = (((pInvGβπΊ)βπ₯)βπΆ))) β π β π) |
35 | | simp-5r 784 |
. . . . . . . . . . . . . 14
β’
((((((((((((((π β§
π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β§ π β π) β§ πΆ = (((pInvGβπΊ)βπ)βπ¦)) β§ π§ β π) β§ (π¦ β (ππΌπ§) β§ (π¦ β π§) = (π¦ β π))) β§ π β π) β§ (π¦ β (ππΌπ) β§ (π¦ β π) = (π¦ β π))) β§ π β π) β§ (π¦ β ((((pInvGβπΊ)βπ§)βπ)πΌπ) β§ (π¦ β π) = (π¦ β πΆ))) β (π¦ β (ππΌπ§) β§ (π¦ β π§) = (π¦ β π))) |
36 | 35 | simprd 496 |
. . . . . . . . . . . . 13
β’
((((((((((((((π β§
π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β§ π β π) β§ πΆ = (((pInvGβπΊ)βπ)βπ¦)) β§ π§ β π) β§ (π¦ β (ππΌπ§) β§ (π¦ β π§) = (π¦ β π))) β§ π β π) β§ (π¦ β (ππΌπ) β§ (π¦ β π) = (π¦ β π))) β§ π β π) β§ (π¦ β ((((pInvGβπΊ)βπ§)βπ)πΌπ) β§ (π¦ β π) = (π¦ β πΆ))) β (π¦ β π§) = (π¦ β π)) |
37 | 36 | eqcomd 2738 |
. . . . . . . . . . . 12
β’
((((((((((((((π β§
π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β§ π β π) β§ πΆ = (((pInvGβπΊ)βπ)βπ¦)) β§ π§ β π) β§ (π¦ β (ππΌπ§) β§ (π¦ β π§) = (π¦ β π))) β§ π β π) β§ (π¦ β (ππΌπ) β§ (π¦ β π) = (π¦ β π))) β§ π β π) β§ (π¦ β ((((pInvGβπΊ)βπ§)βπ)πΌπ) β§ (π¦ β π) = (π¦ β πΆ))) β (π¦ β π) = (π¦ β π§)) |
38 | 37 | adantr 481 |
. . . . . . . . . . 11
β’
(((((((((((((((π β§
π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β§ π β π) β§ πΆ = (((pInvGβπΊ)βπ)βπ¦)) β§ π§ β π) β§ (π¦ β (ππΌπ§) β§ (π¦ β π§) = (π¦ β π))) β§ π β π) β§ (π¦ β (ππΌπ) β§ (π¦ β π) = (π¦ β π))) β§ π β π) β§ (π¦ β ((((pInvGβπΊ)βπ§)βπ)πΌπ) β§ (π¦ β π) = (π¦ β πΆ))) β§ (π₯ β π β§ π = (((pInvGβπΊ)βπ₯)βπΆ))) β (π¦ β π) = (π¦ β π§)) |
39 | | simp-7r 788 |
. . . . . . . . . . . . . . 15
β’
((((((((((((((π β§
π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β§ π β π) β§ πΆ = (((pInvGβπΊ)βπ)βπ¦)) β§ π§ β π) β§ (π¦ β (ππΌπ§) β§ (π¦ β π§) = (π¦ β π))) β§ π β π) β§ (π¦ β (ππΌπ) β§ (π¦ β π) = (π¦ β π))) β§ π β π) β§ (π¦ β ((((pInvGβπΊ)βπ§)βπ)πΌπ) β§ (π¦ β π) = (π¦ β πΆ))) β πΆ = (((pInvGβπΊ)βπ)βπ¦)) |
40 | 39 | adantr 481 |
. . . . . . . . . . . . . 14
β’
(((((((((((((((π β§
π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β§ π β π) β§ πΆ = (((pInvGβπΊ)βπ)βπ¦)) β§ π§ β π) β§ (π¦ β (ππΌπ§) β§ (π¦ β π§) = (π¦ β π))) β§ π β π) β§ (π¦ β (ππΌπ) β§ (π¦ β π) = (π¦ β π))) β§ π β π) β§ (π¦ β ((((pInvGβπΊ)βπ§)βπ)πΌπ) β§ (π¦ β π) = (π¦ β πΆ))) β§ (π₯ β π β§ π = (((pInvGβπΊ)βπ₯)βπΆ))) β πΆ = (((pInvGβπΊ)βπ)βπ¦)) |
41 | | simpllr 774 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((π β§ π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β π β π) |
42 | 41 | ad2antrr 724 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
((((((π β§ π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β π β π) |
43 | 42 | ad2antrr 724 |
. . . . . . . . . . . . . . . . . . . . 21
β’
((((((((π β§ π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β§ π β π) β§ πΆ = (((pInvGβπΊ)βπ)βπ¦)) β π β π) |
44 | 43 | ad2antrr 724 |
. . . . . . . . . . . . . . . . . . . 20
β’
((((((((((π β§
π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β§ π β π) β§ πΆ = (((pInvGβπΊ)βπ)βπ¦)) β§ π§ β π) β§ (π¦ β (ππΌπ§) β§ (π¦ β π§) = (π¦ β π))) β π β π) |
45 | 44 | ad4antr 730 |
. . . . . . . . . . . . . . . . . . 19
β’
((((((((((((((π β§
π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β§ π β π) β§ πΆ = (((pInvGβπΊ)βπ)βπ¦)) β§ π§ β π) β§ (π¦ β (ππΌπ§) β§ (π¦ β π§) = (π¦ β π))) β§ π β π) β§ (π¦ β (ππΌπ) β§ (π¦ β π) = (π¦ β π))) β§ π β π) β§ (π¦ β ((((pInvGβπΊ)βπ§)βπ)πΌπ) β§ (π¦ β π) = (π¦ β πΆ))) β π β π) |
46 | | simplr 767 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β π β π) |
47 | 46 | ad10antr 742 |
. . . . . . . . . . . . . . . . . . 19
β’
((((((((((((((π β§
π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β§ π β π) β§ πΆ = (((pInvGβπΊ)βπ)βπ¦)) β§ π§ β π) β§ (π¦ β (ππΌπ§) β§ (π¦ β π§) = (π¦ β π))) β§ π β π) β§ (π¦ β (ππΌπ) β§ (π¦ β π) = (π¦ β π))) β§ π β π) β§ (π¦ β ((((pInvGβπΊ)βπ§)βπ)πΌπ) β§ (π¦ β π) = (π¦ β πΆ))) β π β π) |
48 | | simp-11r 796 |
. . . . . . . . . . . . . . . . . . . 20
β’
((((((((((((((π β§
π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β§ π β π) β§ πΆ = (((pInvGβπΊ)βπ)βπ¦)) β§ π§ β π) β§ (π¦ β (ππΌπ§) β§ (π¦ β π§) = (π¦ β π))) β§ π β π) β§ (π¦ β (ππΌπ) β§ (π¦ β π) = (π¦ β π))) β§ π β π) β§ (π¦ β ((((pInvGβπΊ)βπ§)βπ)πΌπ) β§ (π¦ β π) = (π¦ β πΆ))) β (π΄ = (ππΏπ) β§ π β π)) |
49 | 48 | simprd 496 |
. . . . . . . . . . . . . . . . . . 19
β’
((((((((((((((π β§
π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β§ π β π) β§ πΆ = (((pInvGβπΊ)βπ)βπ¦)) β§ π§ β π) β§ (π¦ β (ππΌπ§) β§ (π¦ β π§) = (π¦ β π))) β§ π β π) β§ (π¦ β (ππΌπ) β§ (π¦ β π) = (π¦ β π))) β§ π β π) β§ (π¦ β ((((pInvGβπΊ)βπ§)βπ)πΌπ) β§ (π¦ β π) = (π¦ β πΆ))) β π β π) |
50 | 49 | necomd 2996 |
. . . . . . . . . . . . . . . . . . . 20
β’
((((((((((((((π β§
π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β§ π β π) β§ πΆ = (((pInvGβπΊ)βπ)βπ¦)) β§ π§ β π) β§ (π¦ β (ππΌπ§) β§ (π¦ β π§) = (π¦ β π))) β§ π β π) β§ (π¦ β (ππΌπ) β§ (π¦ β π) = (π¦ β π))) β§ π β π) β§ (π¦ β ((((pInvGβπΊ)βπ§)βπ)πΌπ) β§ (π¦ β π) = (π¦ β πΆ))) β π β π) |
51 | | simp-9r 792 |
. . . . . . . . . . . . . . . . . . . . 21
β’
((((((((((((((π β§
π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β§ π β π) β§ πΆ = (((pInvGβπΊ)βπ)βπ¦)) β§ π§ β π) β§ (π¦ β (ππΌπ§) β§ (π¦ β π§) = (π¦ β π))) β§ π β π) β§ (π¦ β (ππΌπ) β§ (π¦ β π) = (π¦ β π))) β§ π β π) β§ (π¦ β ((((pInvGβπΊ)βπ§)βπ)πΌπ) β§ (π¦ β π) = (π¦ β πΆ))) β (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) |
52 | 51 | simpld 495 |
. . . . . . . . . . . . . . . . . . . 20
β’
((((((((((((((π β§
π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β§ π β π) β§ πΆ = (((pInvGβπΊ)βπ)βπ¦)) β§ π§ β π) β§ (π¦ β (ππΌπ§) β§ (π¦ β π§) = (π¦ β π))) β§ π β π) β§ (π¦ β (ππΌπ) β§ (π¦ β π) = (π¦ β π))) β§ π β π) β§ (π¦ β ((((pInvGβπΊ)βπ§)βπ)πΌπ) β§ (π¦ β π) = (π¦ β πΆ))) β π β (ππΌπ¦)) |
53 | 1, 3, 4, 12, 47, 45, 23, 50, 52 | btwnlng3 27861 |
. . . . . . . . . . . . . . . . . . 19
β’
((((((((((((((π β§
π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β§ π β π) β§ πΆ = (((pInvGβπΊ)βπ)βπ¦)) β§ π§ β π) β§ (π¦ β (ππΌπ§) β§ (π¦ β π§) = (π¦ β π))) β§ π β π) β§ (π¦ β (ππΌπ) β§ (π¦ β π) = (π¦ β π))) β§ π β π) β§ (π¦ β ((((pInvGβπΊ)βπ§)βπ)πΌπ) β§ (π¦ β π) = (π¦ β πΆ))) β π¦ β (ππΏπ)) |
54 | 1, 3, 4, 12, 45, 47, 23, 49, 53 | lncom 27862 |
. . . . . . . . . . . . . . . . . 18
β’
((((((((((((((π β§
π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β§ π β π) β§ πΆ = (((pInvGβπΊ)βπ)βπ¦)) β§ π§ β π) β§ (π¦ β (ππΌπ§) β§ (π¦ β π§) = (π¦ β π))) β§ π β π) β§ (π¦ β (ππΌπ) β§ (π¦ β π) = (π¦ β π))) β§ π β π) β§ (π¦ β ((((pInvGβπΊ)βπ§)βπ)πΌπ) β§ (π¦ β π) = (π¦ β πΆ))) β π¦ β (ππΏπ)) |
55 | 48 | simpld 495 |
. . . . . . . . . . . . . . . . . 18
β’
((((((((((((((π β§
π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β§ π β π) β§ πΆ = (((pInvGβπΊ)βπ)βπ¦)) β§ π§ β π) β§ (π¦ β (ππΌπ§) β§ (π¦ β π§) = (π¦ β π))) β§ π β π) β§ (π¦ β (ππΌπ) β§ (π¦ β π) = (π¦ β π))) β§ π β π) β§ (π¦ β ((((pInvGβπΊ)βπ§)βπ)πΌπ) β§ (π¦ β π) = (π¦ β πΆ))) β π΄ = (ππΏπ)) |
56 | 54, 55 | eleqtrrd 2836 |
. . . . . . . . . . . . . . . . 17
β’
((((((((((((((π β§
π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β§ π β π) β§ πΆ = (((pInvGβπΊ)βπ)βπ¦)) β§ π§ β π) β§ (π¦ β (ππΌπ§) β§ (π¦ β π§) = (π¦ β π))) β§ π β π) β§ (π¦ β (ππΌπ) β§ (π¦ β π) = (π¦ β π))) β§ π β π) β§ (π¦ β ((((pInvGβπΊ)βπ§)βπ)πΌπ) β§ (π¦ β π) = (π¦ β πΆ))) β π¦ β π΄) |
57 | 56 | adantr 481 |
. . . . . . . . . . . . . . . 16
β’
(((((((((((((((π β§
π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β§ π β π) β§ πΆ = (((pInvGβπΊ)βπ)βπ¦)) β§ π§ β π) β§ (π¦ β (ππΌπ§) β§ (π¦ β π§) = (π¦ β π))) β§ π β π) β§ (π¦ β (ππΌπ) β§ (π¦ β π) = (π¦ β π))) β§ π β π) β§ (π¦ β ((((pInvGβπΊ)βπ§)βπ)πΌπ) β§ (π¦ β π) = (π¦ β πΆ))) β§ (π₯ β π β§ π = (((pInvGβπΊ)βπ₯)βπΆ))) β π¦ β π΄) |
58 | | foot.y |
. . . . . . . . . . . . . . . . . . 19
β’ (π β Β¬ πΆ β π΄) |
59 | 58 | ad3antrrr 728 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β Β¬ πΆ β π΄) |
60 | 59 | ad10antr 742 |
. . . . . . . . . . . . . . . . 17
β’
((((((((((((((π β§
π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β§ π β π) β§ πΆ = (((pInvGβπΊ)βπ)βπ¦)) β§ π§ β π) β§ (π¦ β (ππΌπ§) β§ (π¦ β π§) = (π¦ β π))) β§ π β π) β§ (π¦ β (ππΌπ) β§ (π¦ β π) = (π¦ β π))) β§ π β π) β§ (π¦ β ((((pInvGβπΊ)βπ§)βπ)πΌπ) β§ (π¦ β π) = (π¦ β πΆ))) β Β¬ πΆ β π΄) |
61 | 60 | adantr 481 |
. . . . . . . . . . . . . . . 16
β’
(((((((((((((((π β§
π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β§ π β π) β§ πΆ = (((pInvGβπΊ)βπ)βπ¦)) β§ π§ β π) β§ (π¦ β (ππΌπ§) β§ (π¦ β π§) = (π¦ β π))) β§ π β π) β§ (π¦ β (ππΌπ) β§ (π¦ β π) = (π¦ β π))) β§ π β π) β§ (π¦ β ((((pInvGβπΊ)βπ§)βπ)πΌπ) β§ (π¦ β π) = (π¦ β πΆ))) β§ (π₯ β π β§ π = (((pInvGβπΊ)βπ₯)βπΆ))) β Β¬ πΆ β π΄) |
62 | | nelne2 3040 |
. . . . . . . . . . . . . . . 16
β’ ((π¦ β π΄ β§ Β¬ πΆ β π΄) β π¦ β πΆ) |
63 | 57, 61, 62 | syl2anc 584 |
. . . . . . . . . . . . . . 15
β’
(((((((((((((((π β§
π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β§ π β π) β§ πΆ = (((pInvGβπΊ)βπ)βπ¦)) β§ π§ β π) β§ (π¦ β (ππΌπ§) β§ (π¦ β π§) = (π¦ β π))) β§ π β π) β§ (π¦ β (ππΌπ) β§ (π¦ β π) = (π¦ β π))) β§ π β π) β§ (π¦ β ((((pInvGβπΊ)βπ§)βπ)πΌπ) β§ (π¦ β π) = (π¦ β πΆ))) β§ (π₯ β π β§ π = (((pInvGβπΊ)βπ₯)βπΆ))) β π¦ β πΆ) |
64 | 63 | necomd 2996 |
. . . . . . . . . . . . . 14
β’
(((((((((((((((π β§
π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β§ π β π) β§ πΆ = (((pInvGβπΊ)βπ)βπ¦)) β§ π§ β π) β§ (π¦ β (ππΌπ§) β§ (π¦ β π§) = (π¦ β π))) β§ π β π) β§ (π¦ β (ππΌπ) β§ (π¦ β π) = (π¦ β π))) β§ π β π) β§ (π¦ β ((((pInvGβπΊ)βπ§)βπ)πΌπ) β§ (π¦ β π) = (π¦ β πΆ))) β§ (π₯ β π β§ π = (((pInvGβπΊ)βπ₯)βπΆ))) β πΆ β π¦) |
65 | 40, 64 | eqnetrrd 3009 |
. . . . . . . . . . . . 13
β’
(((((((((((((((π β§
π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β§ π β π) β§ πΆ = (((pInvGβπΊ)βπ)βπ¦)) β§ π§ β π) β§ (π¦ β (ππΌπ§) β§ (π¦ β π§) = (π¦ β π))) β§ π β π) β§ (π¦ β (ππΌπ) β§ (π¦ β π) = (π¦ β π))) β§ π β π) β§ (π¦ β ((((pInvGβπΊ)βπ§)βπ)πΌπ) β§ (π¦ β π) = (π¦ β πΆ))) β§ (π₯ β π β§ π = (((pInvGβπΊ)βπ₯)βπΆ))) β (((pInvGβπΊ)βπ)βπ¦) β π¦) |
66 | | eqid 2732 |
. . . . . . . . . . . . . . 15
β’
((pInvGβπΊ)βπ) = ((pInvGβπΊ)βπ) |
67 | 1, 2, 3, 4, 5, 27,
34, 66, 28 | mirinv 27906 |
. . . . . . . . . . . . . 14
β’
(((((((((((((((π β§
π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β§ π β π) β§ πΆ = (((pInvGβπΊ)βπ)βπ¦)) β§ π§ β π) β§ (π¦ β (ππΌπ§) β§ (π¦ β π§) = (π¦ β π))) β§ π β π) β§ (π¦ β (ππΌπ) β§ (π¦ β π) = (π¦ β π))) β§ π β π) β§ (π¦ β ((((pInvGβπΊ)βπ§)βπ)πΌπ) β§ (π¦ β π) = (π¦ β πΆ))) β§ (π₯ β π β§ π = (((pInvGβπΊ)βπ₯)βπΆ))) β ((((pInvGβπΊ)βπ)βπ¦) = π¦ β π = π¦)) |
68 | 67 | necon3bid 2985 |
. . . . . . . . . . . . 13
β’
(((((((((((((((π β§
π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β§ π β π) β§ πΆ = (((pInvGβπΊ)βπ)βπ¦)) β§ π§ β π) β§ (π¦ β (ππΌπ§) β§ (π¦ β π§) = (π¦ β π))) β§ π β π) β§ (π¦ β (ππΌπ) β§ (π¦ β π) = (π¦ β π))) β§ π β π) β§ (π¦ β ((((pInvGβπΊ)βπ§)βπ)πΌπ) β§ (π¦ β π) = (π¦ β πΆ))) β§ (π₯ β π β§ π = (((pInvGβπΊ)βπ₯)βπΆ))) β ((((pInvGβπΊ)βπ)βπ¦) β π¦ β π β π¦)) |
69 | 65, 68 | mpbid 231 |
. . . . . . . . . . . 12
β’
(((((((((((((((π β§
π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β§ π β π) β§ πΆ = (((pInvGβπΊ)βπ)βπ¦)) β§ π§ β π) β§ (π¦ β (ππΌπ§) β§ (π¦ β π§) = (π¦ β π))) β§ π β π) β§ (π¦ β (ππΌπ) β§ (π¦ β π) = (π¦ β π))) β§ π β π) β§ (π¦ β ((((pInvGβπΊ)βπ§)βπ)πΌπ) β§ (π¦ β π) = (π¦ β πΆ))) β§ (π₯ β π β§ π = (((pInvGβπΊ)βπ₯)βπΆ))) β π β π¦) |
70 | 69 | necomd 2996 |
. . . . . . . . . . 11
β’
(((((((((((((((π β§
π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β§ π β π) β§ πΆ = (((pInvGβπΊ)βπ)βπ¦)) β§ π§ β π) β§ (π¦ β (ππΌπ§) β§ (π¦ β π§) = (π¦ β π))) β§ π β π) β§ (π¦ β (ππΌπ) β§ (π¦ β π) = (π¦ β π))) β§ π β π) β§ (π¦ β ((((pInvGβπΊ)βπ§)βπ)πΌπ) β§ (π¦ β π) = (π¦ β πΆ))) β§ (π₯ β π β§ π = (((pInvGβπΊ)βπ₯)βπΆ))) β π¦ β π) |
71 | 1, 2, 3, 27, 28, 34, 28, 30, 38, 70 | tgcgrneq 27723 |
. . . . . . . . . 10
β’
(((((((((((((((π β§
π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β§ π β π) β§ πΆ = (((pInvGβπΊ)βπ)βπ¦)) β§ π§ β π) β§ (π¦ β (ππΌπ§) β§ (π¦ β π§) = (π¦ β π))) β§ π β π) β§ (π¦ β (ππΌπ) β§ (π¦ β π) = (π¦ β π))) β§ π β π) β§ (π¦ β ((((pInvGβπΊ)βπ§)βπ)πΌπ) β§ (π¦ β π) = (π¦ β πΆ))) β§ (π₯ β π β§ π = (((pInvGβπΊ)βπ₯)βπΆ))) β π¦ β π§) |
72 | 71 | necomd 2996 |
. . . . . . . . . . 11
β’
(((((((((((((((π β§
π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β§ π β π) β§ πΆ = (((pInvGβπΊ)βπ)βπ¦)) β§ π§ β π) β§ (π¦ β (ππΌπ§) β§ (π¦ β π§) = (π¦ β π))) β§ π β π) β§ (π¦ β (ππΌπ) β§ (π¦ β π) = (π¦ β π))) β§ π β π) β§ (π¦ β ((((pInvGβπΊ)βπ§)βπ)πΌπ) β§ (π¦ β π) = (π¦ β πΆ))) β§ (π₯ β π β§ π = (((pInvGβπΊ)βπ₯)βπΆ))) β π§ β π¦) |
73 | | eqid 2732 |
. . . . . . . . . . . 12
β’
((pInvGβπΊ)βπ§) = ((pInvGβπΊ)βπ§) |
74 | | simp-4r 782 |
. . . . . . . . . . . . 13
β’
((((((((((((((π β§
π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β§ π β π) β§ πΆ = (((pInvGβπΊ)βπ)βπ¦)) β§ π§ β π) β§ (π¦ β (ππΌπ§) β§ (π¦ β π§) = (π¦ β π))) β§ π β π) β§ (π¦ β (ππΌπ) β§ (π¦ β π) = (π¦ β π))) β§ π β π) β§ (π¦ β ((((pInvGβπΊ)βπ§)βπ)πΌπ) β§ (π¦ β π) = (π¦ β πΆ))) β π β π) |
75 | 74 | adantr 481 |
. . . . . . . . . . . 12
β’
(((((((((((((((π β§
π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β§ π β π) β§ πΆ = (((pInvGβπΊ)βπ)βπ¦)) β§ π§ β π) β§ (π¦ β (ππΌπ§) β§ (π¦ β π§) = (π¦ β π))) β§ π β π) β§ (π¦ β (ππΌπ) β§ (π¦ β π) = (π¦ β π))) β§ π β π) β§ (π¦ β ((((pInvGβπΊ)βπ§)βπ)πΌπ) β§ (π¦ β π) = (π¦ β πΆ))) β§ (π₯ β π β§ π = (((pInvGβπΊ)βπ₯)βπΆ))) β π β π) |
76 | | simp-4r 782 |
. . . . . . . . . . . . . 14
β’
((((((((((((π β§
π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β§ π β π) β§ πΆ = (((pInvGβπΊ)βπ)βπ¦)) β§ π§ β π) β§ (π¦ β (ππΌπ§) β§ (π¦ β π§) = (π¦ β π))) β§ π β π) β§ (π¦ β (ππΌπ) β§ (π¦ β π) = (π¦ β π))) β π§ β π) |
77 | | simplr 767 |
. . . . . . . . . . . . . 14
β’
((((((((((((π β§
π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β§ π β π) β§ πΆ = (((pInvGβπΊ)βπ)βπ¦)) β§ π§ β π) β§ (π¦ β (ππΌπ§) β§ (π¦ β π§) = (π¦ β π))) β§ π β π) β§ (π¦ β (ππΌπ) β§ (π¦ β π) = (π¦ β π))) β π β π) |
78 | 1, 2, 3, 4, 5, 11,
76, 73, 77 | mircl 27901 |
. . . . . . . . . . . . 13
β’
((((((((((((π β§
π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β§ π β π) β§ πΆ = (((pInvGβπΊ)βπ)βπ¦)) β§ π§ β π) β§ (π¦ β (ππΌπ§) β§ (π¦ β π§) = (π¦ β π))) β§ π β π) β§ (π¦ β (ππΌπ) β§ (π¦ β π) = (π¦ β π))) β (((pInvGβπΊ)βπ§)βπ) β π) |
79 | 78 | ad3antrrr 728 |
. . . . . . . . . . . 12
β’
(((((((((((((((π β§
π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β§ π β π) β§ πΆ = (((pInvGβπΊ)βπ)βπ¦)) β§ π§ β π) β§ (π¦ β (ππΌπ§) β§ (π¦ β π§) = (π¦ β π))) β§ π β π) β§ (π¦ β (ππΌπ) β§ (π¦ β π) = (π¦ β π))) β§ π β π) β§ (π¦ β ((((pInvGβπΊ)βπ§)βπ)πΌπ) β§ (π¦ β π) = (π¦ β πΆ))) β§ (π₯ β π β§ π = (((pInvGβπΊ)βπ₯)βπΆ))) β (((pInvGβπΊ)βπ§)βπ) β π) |
80 | 18 | adantr 481 |
. . . . . . . . . . . 12
β’
(((((((((((((((π β§
π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β§ π β π) β§ πΆ = (((pInvGβπΊ)βπ)βπ¦)) β§ π§ β π) β§ (π¦ β (ππΌπ§) β§ (π¦ β π§) = (π¦ β π))) β§ π β π) β§ (π¦ β (ππΌπ) β§ (π¦ β π) = (π¦ β π))) β§ π β π) β§ (π¦ β ((((pInvGβπΊ)βπ§)βπ)πΌπ) β§ (π¦ β π) = (π¦ β πΆ))) β§ (π₯ β π β§ π = (((pInvGβπΊ)βπ₯)βπΆ))) β πΆ β π) |
81 | | simpllr 774 |
. . . . . . . . . . . 12
β’
(((((((((((((((π β§
π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β§ π β π) β§ πΆ = (((pInvGβπΊ)βπ)βπ¦)) β§ π§ β π) β§ (π¦ β (ππΌπ§) β§ (π¦ β π§) = (π¦ β π))) β§ π β π) β§ (π¦ β (ππΌπ) β§ (π¦ β π) = (π¦ β π))) β§ π β π) β§ (π¦ β ((((pInvGβπΊ)βπ§)βπ)πΌπ) β§ (π¦ β π) = (π¦ β πΆ))) β§ (π₯ β π β§ π = (((pInvGβπΊ)βπ₯)βπΆ))) β π β π) |
82 | 1, 2, 3, 4, 5, 27,
34, 66, 28 | mirbtwn 27898 |
. . . . . . . . . . . . . . 15
β’
(((((((((((((((π β§
π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β§ π β π) β§ πΆ = (((pInvGβπΊ)βπ)βπ¦)) β§ π§ β π) β§ (π¦ β (ππΌπ§) β§ (π¦ β π§) = (π¦ β π))) β§ π β π) β§ (π¦ β (ππΌπ) β§ (π¦ β π) = (π¦ β π))) β§ π β π) β§ (π¦ β ((((pInvGβπΊ)βπ§)βπ)πΌπ) β§ (π¦ β π) = (π¦ β πΆ))) β§ (π₯ β π β§ π = (((pInvGβπΊ)βπ₯)βπΆ))) β π β ((((pInvGβπΊ)βπ)βπ¦)πΌπ¦)) |
83 | 40 | oveq1d 7420 |
. . . . . . . . . . . . . . 15
β’
(((((((((((((((π β§
π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β§ π β π) β§ πΆ = (((pInvGβπΊ)βπ)βπ¦)) β§ π§ β π) β§ (π¦ β (ππΌπ§) β§ (π¦ β π§) = (π¦ β π))) β§ π β π) β§ (π¦ β (ππΌπ) β§ (π¦ β π) = (π¦ β π))) β§ π β π) β§ (π¦ β ((((pInvGβπΊ)βπ§)βπ)πΌπ) β§ (π¦ β π) = (π¦ β πΆ))) β§ (π₯ β π β§ π = (((pInvGβπΊ)βπ₯)βπΆ))) β (πΆπΌπ¦) = ((((pInvGβπΊ)βπ)βπ¦)πΌπ¦)) |
84 | 82, 83 | eleqtrrd 2836 |
. . . . . . . . . . . . . 14
β’
(((((((((((((((π β§
π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β§ π β π) β§ πΆ = (((pInvGβπΊ)βπ)βπ¦)) β§ π§ β π) β§ (π¦ β (ππΌπ§) β§ (π¦ β π§) = (π¦ β π))) β§ π β π) β§ (π¦ β (ππΌπ) β§ (π¦ β π) = (π¦ β π))) β§ π β π) β§ (π¦ β ((((pInvGβπΊ)βπ§)βπ)πΌπ) β§ (π¦ β π) = (π¦ β πΆ))) β§ (π₯ β π β§ π = (((pInvGβπΊ)βπ₯)βπΆ))) β π β (πΆπΌπ¦)) |
85 | | simpllr 774 |
. . . . . . . . . . . . . . . 16
β’
((((((((((((((π β§
π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β§ π β π) β§ πΆ = (((pInvGβπΊ)βπ)βπ¦)) β§ π§ β π) β§ (π¦ β (ππΌπ§) β§ (π¦ β π§) = (π¦ β π))) β§ π β π) β§ (π¦ β (ππΌπ) β§ (π¦ β π) = (π¦ β π))) β§ π β π) β§ (π¦ β ((((pInvGβπΊ)βπ§)βπ)πΌπ) β§ (π¦ β π) = (π¦ β πΆ))) β (π¦ β (ππΌπ) β§ (π¦ β π) = (π¦ β π))) |
86 | 85 | simpld 495 |
. . . . . . . . . . . . . . 15
β’
((((((((((((((π β§
π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β§ π β π) β§ πΆ = (((pInvGβπΊ)βπ)βπ¦)) β§ π§ β π) β§ (π¦ β (ππΌπ§) β§ (π¦ β π§) = (π¦ β π))) β§ π β π) β§ (π¦ β (ππΌπ) β§ (π¦ β π) = (π¦ β π))) β§ π β π) β§ (π¦ β ((((pInvGβπΊ)βπ§)βπ)πΌπ) β§ (π¦ β π) = (π¦ β πΆ))) β π¦ β (ππΌπ)) |
87 | 86 | adantr 481 |
. . . . . . . . . . . . . 14
β’
(((((((((((((((π β§
π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β§ π β π) β§ πΆ = (((pInvGβπΊ)βπ)βπ¦)) β§ π§ β π) β§ (π¦ β (ππΌπ§) β§ (π¦ β π§) = (π¦ β π))) β§ π β π) β§ (π¦ β (ππΌπ) β§ (π¦ β π) = (π¦ β π))) β§ π β π) β§ (π¦ β ((((pInvGβπΊ)βπ§)βπ)πΌπ) β§ (π¦ β π) = (π¦ β πΆ))) β§ (π₯ β π β§ π = (((pInvGβπΊ)βπ₯)βπΆ))) β π¦ β (ππΌπ)) |
88 | 1, 2, 3, 27, 80, 34, 28, 75, 69, 84, 87 | tgbtwnouttr2 27735 |
. . . . . . . . . . . . 13
β’
(((((((((((((((π β§
π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β§ π β π) β§ πΆ = (((pInvGβπΊ)βπ)βπ¦)) β§ π§ β π) β§ (π¦ β (ππΌπ§) β§ (π¦ β π§) = (π¦ β π))) β§ π β π) β§ (π¦ β (ππΌπ) β§ (π¦ β π) = (π¦ β π))) β§ π β π) β§ (π¦ β ((((pInvGβπΊ)βπ§)βπ)πΌπ) β§ (π¦ β π) = (π¦ β πΆ))) β§ (π₯ β π β§ π = (((pInvGβπΊ)βπ₯)βπΆ))) β π¦ β (πΆπΌπ)) |
89 | 1, 2, 3, 27, 80, 28, 75, 88 | tgbtwncom 27728 |
. . . . . . . . . . . 12
β’
(((((((((((((((π β§
π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β§ π β π) β§ πΆ = (((pInvGβπΊ)βπ)βπ¦)) β§ π§ β π) β§ (π¦ β (ππΌπ§) β§ (π¦ β π§) = (π¦ β π))) β§ π β π) β§ (π¦ β (ππΌπ) β§ (π¦ β π) = (π¦ β π))) β§ π β π) β§ (π¦ β ((((pInvGβπΊ)βπ§)βπ)πΌπ) β§ (π¦ β π) = (π¦ β πΆ))) β§ (π₯ β π β§ π = (((pInvGβπΊ)βπ₯)βπΆ))) β π¦ β (ππΌπΆ)) |
90 | | simplrl 775 |
. . . . . . . . . . . 12
β’
(((((((((((((((π β§
π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β§ π β π) β§ πΆ = (((pInvGβπΊ)βπ)βπ¦)) β§ π§ β π) β§ (π¦ β (ππΌπ§) β§ (π¦ β π§) = (π¦ β π))) β§ π β π) β§ (π¦ β (ππΌπ) β§ (π¦ β π) = (π¦ β π))) β§ π β π) β§ (π¦ β ((((pInvGβπΊ)βπ§)βπ)πΌπ) β§ (π¦ β π) = (π¦ β πΆ))) β§ (π₯ β π β§ π = (((pInvGβπΊ)βπ₯)βπΆ))) β π¦ β ((((pInvGβπΊ)βπ§)βπ)πΌπ)) |
91 | | eqid 2732 |
. . . . . . . . . . . . . . . 16
β’
(cgrGβπΊ) =
(cgrGβπΊ) |
92 | 51 | simprd 496 |
. . . . . . . . . . . . . . . . . 18
β’
((((((((((((((π β§
π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β§ π β π) β§ πΆ = (((pInvGβπΊ)βπ)βπ¦)) β§ π§ β π) β§ (π¦ β (ππΌπ§) β§ (π¦ β π§) = (π¦ β π))) β§ π β π) β§ (π¦ β (ππΌπ) β§ (π¦ β π) = (π¦ β π))) β§ π β π) β§ (π¦ β ((((pInvGβπΊ)βπ§)βπ)πΌπ) β§ (π¦ β π) = (π¦ β πΆ))) β (π β π¦) = (π β πΆ)) |
93 | 39 | oveq2d 7421 |
. . . . . . . . . . . . . . . . . 18
β’
((((((((((((((π β§
π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β§ π β π) β§ πΆ = (((pInvGβπΊ)βπ)βπ¦)) β§ π§ β π) β§ (π¦ β (ππΌπ§) β§ (π¦ β π§) = (π¦ β π))) β§ π β π) β§ (π¦ β (ππΌπ) β§ (π¦ β π) = (π¦ β π))) β§ π β π) β§ (π¦ β ((((pInvGβπΊ)βπ§)βπ)πΌπ) β§ (π¦ β π) = (π¦ β πΆ))) β (π β πΆ) = (π β (((pInvGβπΊ)βπ)βπ¦))) |
94 | 92, 93 | eqtrd 2772 |
. . . . . . . . . . . . . . . . 17
β’
((((((((((((((π β§
π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β§ π β π) β§ πΆ = (((pInvGβπΊ)βπ)βπ¦)) β§ π§ β π) β§ (π¦ β (ππΌπ§) β§ (π¦ β π§) = (π¦ β π))) β§ π β π) β§ (π¦ β (ππΌπ) β§ (π¦ β π) = (π¦ β π))) β§ π β π) β§ (π¦ β ((((pInvGβπΊ)βπ§)βπ)πΌπ) β§ (π¦ β π) = (π¦ β πΆ))) β (π β π¦) = (π β (((pInvGβπΊ)βπ)βπ¦))) |
95 | 1, 2, 3, 4, 5, 12,
45, 33, 23 | israg 27937 |
. . . . . . . . . . . . . . . . 17
β’
((((((((((((((π β§
π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β§ π β π) β§ πΆ = (((pInvGβπΊ)βπ)βπ¦)) β§ π§ β π) β§ (π¦ β (ππΌπ§) β§ (π¦ β π§) = (π¦ β π))) β§ π β π) β§ (π¦ β (ππΌπ) β§ (π¦ β π) = (π¦ β π))) β§ π β π) β§ (π¦ β ((((pInvGβπΊ)βπ§)βπ)πΌπ) β§ (π¦ β π) = (π¦ β πΆ))) β (β¨βπππ¦ββ© β (βGβπΊ) β (π β π¦) = (π β (((pInvGβπΊ)βπ)βπ¦)))) |
96 | 94, 95 | mpbird 256 |
. . . . . . . . . . . . . . . 16
β’
((((((((((((((π β§
π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β§ π β π) β§ πΆ = (((pInvGβπΊ)βπ)βπ¦)) β§ π§ β π) β§ (π¦ β (ππΌπ§) β§ (π¦ β π§) = (π¦ β π))) β§ π β π) β§ (π¦ β (ππΌπ) β§ (π¦ β π) = (π¦ β π))) β§ π β π) β§ (π¦ β ((((pInvGβπΊ)βπ§)βπ)πΌπ) β§ (π¦ β π) = (π¦ β πΆ))) β β¨βπππ¦ββ© β (βGβπΊ)) |
97 | 85 | simprd 496 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
((((((((((((((π β§
π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β§ π β π) β§ πΆ = (((pInvGβπΊ)βπ)βπ¦)) β§ π§ β π) β§ (π¦ β (ππΌπ§) β§ (π¦ β π§) = (π¦ β π))) β§ π β π) β§ (π¦ β (ππΌπ) β§ (π¦ β π) = (π¦ β π))) β§ π β π) β§ (π¦ β ((((pInvGβπΊ)βπ§)βπ)πΌπ) β§ (π¦ β π) = (π¦ β πΆ))) β (π¦ β π) = (π¦ β π)) |
98 | 1, 2, 3, 12, 45, 23, 45, 18, 92 | tgcgrcomlr 27720 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
((((((((((((((π β§
π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β§ π β π) β§ πΆ = (((pInvGβπΊ)βπ)βπ¦)) β§ π§ β π) β§ (π¦ β (ππΌπ§) β§ (π¦ β π§) = (π¦ β π))) β§ π β π) β§ (π¦ β (ππΌπ) β§ (π¦ β π) = (π¦ β π))) β§ π β π) β§ (π¦ β ((((pInvGβπΊ)βπ§)βπ)πΌπ) β§ (π¦ β π) = (π¦ β πΆ))) β (π¦ β π) = (πΆ β π)) |
99 | 97, 98 | eqtr2d 2773 |
. . . . . . . . . . . . . . . . . . . . 21
β’
((((((((((((((π β§
π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β§ π β π) β§ πΆ = (((pInvGβπΊ)βπ)βπ¦)) β§ π§ β π) β§ (π¦ β (ππΌπ§) β§ (π¦ β π§) = (π¦ β π))) β§ π β π) β§ (π¦ β (ππΌπ) β§ (π¦ β π) = (π¦ β π))) β§ π β π) β§ (π¦ β ((((pInvGβπΊ)βπ§)βπ)πΌπ) β§ (π¦ β π) = (π¦ β πΆ))) β (πΆ β π) = (π¦ β π)) |
100 | 1, 3, 4, 12, 45, 47, 49 | tglinerflx1 27873 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
((((((((((((((π β§
π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β§ π β π) β§ πΆ = (((pInvGβπΊ)βπ)βπ¦)) β§ π§ β π) β§ (π¦ β (ππΌπ§) β§ (π¦ β π§) = (π¦ β π))) β§ π β π) β§ (π¦ β (ππΌπ) β§ (π¦ β π) = (π¦ β π))) β§ π β π) β§ (π¦ β ((((pInvGβπΊ)βπ§)βπ)πΌπ) β§ (π¦ β π) = (π¦ β πΆ))) β π β (ππΏπ)) |
101 | 100, 55 | eleqtrrd 2836 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
((((((((((((((π β§
π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β§ π β π) β§ πΆ = (((pInvGβπΊ)βπ)βπ¦)) β§ π§ β π) β§ (π¦ β (ππΌπ§) β§ (π¦ β π§) = (π¦ β π))) β§ π β π) β§ (π¦ β (ππΌπ) β§ (π¦ β π) = (π¦ β π))) β§ π β π) β§ (π¦ β ((((pInvGβπΊ)βπ§)βπ)πΌπ) β§ (π¦ β π) = (π¦ β πΆ))) β π β π΄) |
102 | | nelne2 3040 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β π΄ β§ Β¬ πΆ β π΄) β π β πΆ) |
103 | 101, 60, 102 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
((((((((((((((π β§
π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β§ π β π) β§ πΆ = (((pInvGβπΊ)βπ)βπ¦)) β§ π§ β π) β§ (π¦ β (ππΌπ§) β§ (π¦ β π§) = (π¦ β π))) β§ π β π) β§ (π¦ β (ππΌπ) β§ (π¦ β π) = (π¦ β π))) β§ π β π) β§ (π¦ β ((((pInvGβπΊ)βπ§)βπ)πΌπ) β§ (π¦ β π) = (π¦ β πΆ))) β π β πΆ) |
104 | 103 | necomd 2996 |
. . . . . . . . . . . . . . . . . . . . 21
β’
((((((((((((((π β§
π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β§ π β π) β§ πΆ = (((pInvGβπΊ)βπ)βπ¦)) β§ π§ β π) β§ (π¦ β (ππΌπ§) β§ (π¦ β π§) = (π¦ β π))) β§ π β π) β§ (π¦ β (ππΌπ) β§ (π¦ β π) = (π¦ β π))) β§ π β π) β§ (π¦ β ((((pInvGβπΊ)βπ§)βπ)πΌπ) β§ (π¦ β π) = (π¦ β πΆ))) β πΆ β π) |
105 | 1, 2, 3, 12, 18, 45, 23, 74, 99, 104 | tgcgrneq 27723 |
. . . . . . . . . . . . . . . . . . . 20
β’
((((((((((((((π β§
π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β§ π β π) β§ πΆ = (((pInvGβπΊ)βπ)βπ¦)) β§ π§ β π) β§ (π¦ β (ππΌπ§) β§ (π¦ β π§) = (π¦ β π))) β§ π β π) β§ (π¦ β (ππΌπ) β§ (π¦ β π) = (π¦ β π))) β§ π β π) β§ (π¦ β ((((pInvGβπΊ)βπ§)βπ)πΌπ) β§ (π¦ β π) = (π¦ β πΆ))) β π¦ β π) |
106 | 105 | necomd 2996 |
. . . . . . . . . . . . . . . . . . 19
β’
((((((((((((((π β§
π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β§ π β π) β§ πΆ = (((pInvGβπΊ)βπ)βπ¦)) β§ π§ β π) β§ (π¦ β (ππΌπ§) β§ (π¦ β π§) = (π¦ β π))) β§ π β π) β§ (π¦ β (ππΌπ) β§ (π¦ β π) = (π¦ β π))) β§ π β π) β§ (π¦ β ((((pInvGβπΊ)βπ§)βπ)πΌπ) β§ (π¦ β π) = (π¦ β πΆ))) β π β π¦) |
107 | 1, 2, 3, 12, 33, 23, 74, 86 | tgbtwncom 27728 |
. . . . . . . . . . . . . . . . . . 19
β’
((((((((((((((π β§
π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β§ π β π) β§ πΆ = (((pInvGβπΊ)βπ)βπ¦)) β§ π§ β π) β§ (π¦ β (ππΌπ§) β§ (π¦ β π§) = (π¦ β π))) β§ π β π) β§ (π¦ β (ππΌπ) β§ (π¦ β π) = (π¦ β π))) β§ π β π) β§ (π¦ β ((((pInvGβπΊ)βπ§)βπ)πΌπ) β§ (π¦ β π) = (π¦ β πΆ))) β π¦ β (ππΌπ)) |
108 | 35 | simpld 495 |
. . . . . . . . . . . . . . . . . . 19
β’
((((((((((((((π β§
π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β§ π β π) β§ πΆ = (((pInvGβπΊ)βπ)βπ¦)) β§ π§ β π) β§ (π¦ β (ππΌπ§) β§ (π¦ β π§) = (π¦ β π))) β§ π β π) β§ (π¦ β (ππΌπ) β§ (π¦ β π) = (π¦ β π))) β§ π β π) β§ (π¦ β ((((pInvGβπΊ)βπ§)βπ)πΌπ) β§ (π¦ β π) = (π¦ β πΆ))) β π¦ β (ππΌπ§)) |
109 | 1, 2, 3, 12, 23, 74, 23, 45, 97 | tgcgrcomlr 27720 |
. . . . . . . . . . . . . . . . . . 19
β’
((((((((((((((π β§
π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β§ π β π) β§ πΆ = (((pInvGβπΊ)βπ)βπ¦)) β§ π§ β π) β§ (π¦ β (ππΌπ§) β§ (π¦ β π§) = (π¦ β π))) β§ π β π) β§ (π¦ β (ππΌπ) β§ (π¦ β π) = (π¦ β π))) β§ π β π) β§ (π¦ β ((((pInvGβπΊ)βπ§)βπ)πΌπ) β§ (π¦ β π) = (π¦ β πΆ))) β (π β π¦) = (π β π¦)) |
110 | 1, 2, 3, 12, 74, 45 | axtgcgrrflx 27702 |
. . . . . . . . . . . . . . . . . . 19
β’
((((((((((((((π β§
π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β§ π β π) β§ πΆ = (((pInvGβπΊ)βπ)βπ¦)) β§ π§ β π) β§ (π¦ β (ππΌπ§) β§ (π¦ β π§) = (π¦ β π))) β§ π β π) β§ (π¦ β (ππΌπ) β§ (π¦ β π) = (π¦ β π))) β§ π β π) β§ (π¦ β ((((pInvGβπΊ)βπ§)βπ)πΌπ) β§ (π¦ β π) = (π¦ β πΆ))) β (π β π) = (π β π)) |
111 | 97 | eqcomd 2738 |
. . . . . . . . . . . . . . . . . . 19
β’
((((((((((((((π β§
π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β§ π β π) β§ πΆ = (((pInvGβπΊ)βπ)βπ¦)) β§ π§ β π) β§ (π¦ β (ππΌπ§) β§ (π¦ β π§) = (π¦ β π))) β§ π β π) β§ (π¦ β (ππΌπ) β§ (π¦ β π) = (π¦ β π))) β§ π β π) β§ (π¦ β ((((pInvGβπΊ)βπ§)βπ)πΌπ) β§ (π¦ β π) = (π¦ β πΆ))) β (π¦ β π) = (π¦ β π)) |
112 | 1, 2, 3, 12, 74, 23, 33, 45, 23, 29, 45, 74, 106, 107, 108, 109, 37, 110, 111 | axtg5seg 27705 |
. . . . . . . . . . . . . . . . . 18
β’
((((((((((((((π β§
π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β§ π β π) β§ πΆ = (((pInvGβπΊ)βπ)βπ¦)) β§ π§ β π) β§ (π¦ β (ππΌπ§) β§ (π¦ β π§) = (π¦ β π))) β§ π β π) β§ (π¦ β (ππΌπ) β§ (π¦ β π) = (π¦ β π))) β§ π β π) β§ (π¦ β ((((pInvGβπΊ)βπ§)βπ)πΌπ) β§ (π¦ β π) = (π¦ β πΆ))) β (π β π) = (π§ β π)) |
113 | 1, 2, 3, 12, 33, 45, 29, 74, 112 | tgcgrcomlr 27720 |
. . . . . . . . . . . . . . . . 17
β’
((((((((((((((π β§
π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β§ π β π) β§ πΆ = (((pInvGβπΊ)βπ)βπ¦)) β§ π§ β π) β§ (π¦ β (ππΌπ§) β§ (π¦ β π§) = (π¦ β π))) β§ π β π) β§ (π¦ β (ππΌπ) β§ (π¦ β π) = (π¦ β π))) β§ π β π) β§ (π¦ β ((((pInvGβπΊ)βπ§)βπ)πΌπ) β§ (π¦ β π) = (π¦ β πΆ))) β (π β π) = (π β π§)) |
114 | 1, 2, 3, 12, 23, 33, 23, 29, 37 | tgcgrcomlr 27720 |
. . . . . . . . . . . . . . . . 17
β’
((((((((((((((π β§
π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β§ π β π) β§ πΆ = (((pInvGβπΊ)βπ)βπ¦)) β§ π§ β π) β§ (π¦ β (ππΌπ§) β§ (π¦ β π§) = (π¦ β π))) β§ π β π) β§ (π¦ β (ππΌπ) β§ (π¦ β π) = (π¦ β π))) β§ π β π) β§ (π¦ β ((((pInvGβπΊ)βπ§)βπ)πΌπ) β§ (π¦ β π) = (π¦ β πΆ))) β (π β π¦) = (π§ β π¦)) |
115 | 1, 2, 91, 12, 45, 33, 23, 74, 29, 23, 113, 114, 111 | trgcgr 27756 |
. . . . . . . . . . . . . . . 16
β’
((((((((((((((π β§
π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β§ π β π) β§ πΆ = (((pInvGβπΊ)βπ)βπ¦)) β§ π§ β π) β§ (π¦ β (ππΌπ§) β§ (π¦ β π§) = (π¦ β π))) β§ π β π) β§ (π¦ β (ππΌπ) β§ (π¦ β π) = (π¦ β π))) β§ π β π) β§ (π¦ β ((((pInvGβπΊ)βπ§)βπ)πΌπ) β§ (π¦ β π) = (π¦ β πΆ))) β β¨βπππ¦ββ©(cgrGβπΊ)β¨βππ§π¦ββ©) |
116 | 1, 2, 3, 4, 5, 12,
45, 33, 23, 91, 74, 29, 23, 96, 115 | ragcgr 27947 |
. . . . . . . . . . . . . . 15
β’
((((((((((((((π β§
π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β§ π β π) β§ πΆ = (((pInvGβπΊ)βπ)βπ¦)) β§ π§ β π) β§ (π¦ β (ππΌπ§) β§ (π¦ β π§) = (π¦ β π))) β§ π β π) β§ (π¦ β (ππΌπ) β§ (π¦ β π) = (π¦ β π))) β§ π β π) β§ (π¦ β ((((pInvGβπΊ)βπ§)βπ)πΌπ) β§ (π¦ β π) = (π¦ β πΆ))) β β¨βππ§π¦ββ© β (βGβπΊ)) |
117 | 1, 2, 3, 4, 5, 12,
74, 29, 23, 116 | ragcom 27938 |
. . . . . . . . . . . . . 14
β’
((((((((((((((π β§
π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β§ π β π) β§ πΆ = (((pInvGβπΊ)βπ)βπ¦)) β§ π§ β π) β§ (π¦ β (ππΌπ§) β§ (π¦ β π§) = (π¦ β π))) β§ π β π) β§ (π¦ β (ππΌπ) β§ (π¦ β π) = (π¦ β π))) β§ π β π) β§ (π¦ β ((((pInvGβπΊ)βπ§)βπ)πΌπ) β§ (π¦ β π) = (π¦ β πΆ))) β β¨βπ¦π§πββ© β (βGβπΊ)) |
118 | 1, 2, 3, 4, 5, 12,
23, 29, 74 | israg 27937 |
. . . . . . . . . . . . . 14
β’
((((((((((((((π β§
π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β§ π β π) β§ πΆ = (((pInvGβπΊ)βπ)βπ¦)) β§ π§ β π) β§ (π¦ β (ππΌπ§) β§ (π¦ β π§) = (π¦ β π))) β§ π β π) β§ (π¦ β (ππΌπ) β§ (π¦ β π) = (π¦ β π))) β§ π β π) β§ (π¦ β ((((pInvGβπΊ)βπ§)βπ)πΌπ) β§ (π¦ β π) = (π¦ β πΆ))) β (β¨βπ¦π§πββ© β (βGβπΊ) β (π¦ β π) = (π¦ β (((pInvGβπΊ)βπ§)βπ)))) |
119 | 117, 118 | mpbid 231 |
. . . . . . . . . . . . 13
β’
((((((((((((((π β§
π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β§ π β π) β§ πΆ = (((pInvGβπΊ)βπ)βπ¦)) β§ π§ β π) β§ (π¦ β (ππΌπ§) β§ (π¦ β π§) = (π¦ β π))) β§ π β π) β§ (π¦ β (ππΌπ) β§ (π¦ β π) = (π¦ β π))) β§ π β π) β§ (π¦ β ((((pInvGβπΊ)βπ§)βπ)πΌπ) β§ (π¦ β π) = (π¦ β πΆ))) β (π¦ β π) = (π¦ β (((pInvGβπΊ)βπ§)βπ))) |
120 | 119 | adantr 481 |
. . . . . . . . . . . 12
β’
(((((((((((((((π β§
π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β§ π β π) β§ πΆ = (((pInvGβπΊ)βπ)βπ¦)) β§ π§ β π) β§ (π¦ β (ππΌπ§) β§ (π¦ β π§) = (π¦ β π))) β§ π β π) β§ (π¦ β (ππΌπ) β§ (π¦ β π) = (π¦ β π))) β§ π β π) β§ (π¦ β ((((pInvGβπΊ)βπ§)βπ)πΌπ) β§ (π¦ β π) = (π¦ β πΆ))) β§ (π₯ β π β§ π = (((pInvGβπΊ)βπ₯)βπΆ))) β (π¦ β π) = (π¦ β (((pInvGβπΊ)βπ§)βπ))) |
121 | 25 | adantr 481 |
. . . . . . . . . . . 12
β’
(((((((((((((((π β§
π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β§ π β π) β§ πΆ = (((pInvGβπΊ)βπ)βπ¦)) β§ π§ β π) β§ (π¦ β (ππΌπ§) β§ (π¦ β π§) = (π¦ β π))) β§ π β π) β§ (π¦ β (ππΌπ) β§ (π¦ β π) = (π¦ β π))) β§ π β π) β§ (π¦ β ((((pInvGβπΊ)βπ§)βπ)πΌπ) β§ (π¦ β π) = (π¦ β πΆ))) β§ (π₯ β π β§ π = (((pInvGβπΊ)βπ₯)βπΆ))) β (π¦ β πΆ) = (π¦ β π)) |
122 | | eqidd 2733 |
. . . . . . . . . . . 12
β’
(((((((((((((((π β§
π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β§ π β π) β§ πΆ = (((pInvGβπΊ)βπ)βπ¦)) β§ π§ β π) β§ (π¦ β (ππΌπ§) β§ (π¦ β π§) = (π¦ β π))) β§ π β π) β§ (π¦ β (ππΌπ) β§ (π¦ β π) = (π¦ β π))) β§ π β π) β§ (π¦ β ((((pInvGβπΊ)βπ§)βπ)πΌπ) β§ (π¦ β π) = (π¦ β πΆ))) β§ (π₯ β π β§ π = (((pInvGβπΊ)βπ₯)βπΆ))) β (((pInvGβπΊ)βπ§)βπ) = (((pInvGβπΊ)βπ§)βπ)) |
123 | | simprr 771 |
. . . . . . . . . . . 12
β’
(((((((((((((((π β§
π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β§ π β π) β§ πΆ = (((pInvGβπΊ)βπ)βπ¦)) β§ π§ β π) β§ (π¦ β (ππΌπ§) β§ (π¦ β π§) = (π¦ β π))) β§ π β π) β§ (π¦ β (ππΌπ) β§ (π¦ β π) = (π¦ β π))) β§ π β π) β§ (π¦ β ((((pInvGβπΊ)βπ§)βπ)πΌπ) β§ (π¦ β π) = (π¦ β πΆ))) β§ (π₯ β π β§ π = (((pInvGβπΊ)βπ₯)βπΆ))) β π = (((pInvGβπΊ)βπ₯)βπΆ)) |
124 | 1, 2, 3, 4, 5, 27,
73, 13, 75, 79, 28, 80, 81, 30, 31, 89, 90, 120, 121, 122, 123 | krippen 27931 |
. . . . . . . . . . 11
β’
(((((((((((((((π β§
π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β§ π β π) β§ πΆ = (((pInvGβπΊ)βπ)βπ¦)) β§ π§ β π) β§ (π¦ β (ππΌπ§) β§ (π¦ β π§) = (π¦ β π))) β§ π β π) β§ (π¦ β (ππΌπ) β§ (π¦ β π) = (π¦ β π))) β§ π β π) β§ (π¦ β ((((pInvGβπΊ)βπ§)βπ)πΌπ) β§ (π¦ β π) = (π¦ β πΆ))) β§ (π₯ β π β§ π = (((pInvGβπΊ)βπ₯)βπΆ))) β π¦ β (π§πΌπ₯)) |
125 | 1, 3, 4, 27, 30, 28, 31, 72, 124 | btwnlng3 27861 |
. . . . . . . . . 10
β’
(((((((((((((((π β§
π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β§ π β π) β§ πΆ = (((pInvGβπΊ)βπ)βπ¦)) β§ π§ β π) β§ (π¦ β (ππΌπ§) β§ (π¦ β π§) = (π¦ β π))) β§ π β π) β§ (π¦ β (ππΌπ) β§ (π¦ β π) = (π¦ β π))) β§ π β π) β§ (π¦ β ((((pInvGβπΊ)βπ§)βπ)πΌπ) β§ (π¦ β π) = (π¦ β πΆ))) β§ (π₯ β π β§ π = (((pInvGβπΊ)βπ₯)βπΆ))) β π₯ β (π§πΏπ¦)) |
126 | 1, 3, 4, 27, 28, 30, 31, 71, 125 | lncom 27862 |
. . . . . . . . 9
β’
(((((((((((((((π β§
π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β§ π β π) β§ πΆ = (((pInvGβπΊ)βπ)βπ¦)) β§ π§ β π) β§ (π¦ β (ππΌπ§) β§ (π¦ β π§) = (π¦ β π))) β§ π β π) β§ (π¦ β (ππΌπ) β§ (π¦ β π) = (π¦ β π))) β§ π β π) β§ (π¦ β ((((pInvGβπΊ)βπ§)βπ)πΌπ) β§ (π¦ β π) = (π¦ β πΆ))) β§ (π₯ β π β§ π = (((pInvGβπΊ)βπ₯)βπΆ))) β π₯ β (π¦πΏπ§)) |
127 | | isperp.a |
. . . . . . . . . . . 12
β’ (π β π΄ β ran πΏ) |
128 | 127 | ad5antr 732 |
. . . . . . . . . . 11
β’
((((((π β§ π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β π΄ β ran πΏ) |
129 | 128 | ad9antr 740 |
. . . . . . . . . 10
β’
(((((((((((((((π β§
π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β§ π β π) β§ πΆ = (((pInvGβπΊ)βπ)βπ¦)) β§ π§ β π) β§ (π¦ β (ππΌπ§) β§ (π¦ β π§) = (π¦ β π))) β§ π β π) β§ (π¦ β (ππΌπ) β§ (π¦ β π) = (π¦ β π))) β§ π β π) β§ (π¦ β ((((pInvGβπΊ)βπ§)βπ)πΌπ) β§ (π¦ β π) = (π¦ β πΆ))) β§ (π₯ β π β§ π = (((pInvGβπΊ)βπ₯)βπΆ))) β π΄ β ran πΏ) |
130 | 45 | adantr 481 |
. . . . . . . . . . . 12
β’
(((((((((((((((π β§
π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β§ π β π) β§ πΆ = (((pInvGβπΊ)βπ)βπ¦)) β§ π§ β π) β§ (π¦ β (ππΌπ§) β§ (π¦ β π§) = (π¦ β π))) β§ π β π) β§ (π¦ β (ππΌπ) β§ (π¦ β π) = (π¦ β π))) β§ π β π) β§ (π¦ β ((((pInvGβπΊ)βπ§)βπ)πΌπ) β§ (π¦ β π) = (π¦ β πΆ))) β§ (π₯ β π β§ π = (((pInvGβπΊ)βπ₯)βπΆ))) β π β π) |
131 | 92 | adantr 481 |
. . . . . . . . . . . . . 14
β’
(((((((((((((((π β§
π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β§ π β π) β§ πΆ = (((pInvGβπΊ)βπ)βπ¦)) β§ π§ β π) β§ (π¦ β (ππΌπ§) β§ (π¦ β π§) = (π¦ β π))) β§ π β π) β§ (π¦ β (ππΌπ) β§ (π¦ β π) = (π¦ β π))) β§ π β π) β§ (π¦ β ((((pInvGβπΊ)βπ§)βπ)πΌπ) β§ (π¦ β π) = (π¦ β πΆ))) β§ (π₯ β π β§ π = (((pInvGβπΊ)βπ₯)βπΆ))) β (π β π¦) = (π β πΆ)) |
132 | 131 | eqcomd 2738 |
. . . . . . . . . . . . 13
β’
(((((((((((((((π β§
π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β§ π β π) β§ πΆ = (((pInvGβπΊ)βπ)βπ¦)) β§ π§ β π) β§ (π¦ β (ππΌπ§) β§ (π¦ β π§) = (π¦ β π))) β§ π β π) β§ (π¦ β (ππΌπ) β§ (π¦ β π) = (π¦ β π))) β§ π β π) β§ (π¦ β ((((pInvGβπΊ)βπ§)βπ)πΌπ) β§ (π¦ β π) = (π¦ β πΆ))) β§ (π₯ β π β§ π = (((pInvGβπΊ)βπ₯)βπΆ))) β (π β πΆ) = (π β π¦)) |
133 | 103 | adantr 481 |
. . . . . . . . . . . . 13
β’
(((((((((((((((π β§
π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β§ π β π) β§ πΆ = (((pInvGβπΊ)βπ)βπ¦)) β§ π§ β π) β§ (π¦ β (ππΌπ§) β§ (π¦ β π§) = (π¦ β π))) β§ π β π) β§ (π¦ β (ππΌπ) β§ (π¦ β π) = (π¦ β π))) β§ π β π) β§ (π¦ β ((((pInvGβπΊ)βπ§)βπ)πΌπ) β§ (π¦ β π) = (π¦ β πΆ))) β§ (π₯ β π β§ π = (((pInvGβπΊ)βπ₯)βπΆ))) β π β πΆ) |
134 | 1, 2, 3, 27, 130, 80, 130, 28, 132, 133 | tgcgrneq 27723 |
. . . . . . . . . . . 12
β’
(((((((((((((((π β§
π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β§ π β π) β§ πΆ = (((pInvGβπΊ)βπ)βπ¦)) β§ π§ β π) β§ (π¦ β (ππΌπ§) β§ (π¦ β π§) = (π¦ β π))) β§ π β π) β§ (π¦ β (ππΌπ) β§ (π¦ β π) = (π¦ β π))) β§ π β π) β§ (π¦ β ((((pInvGβπΊ)βπ§)βπ)πΌπ) β§ (π¦ β π) = (π¦ β πΆ))) β§ (π₯ β π β§ π = (((pInvGβπΊ)βπ₯)βπΆ))) β π β π¦) |
135 | 108 | adantr 481 |
. . . . . . . . . . . 12
β’
(((((((((((((((π β§
π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β§ π β π) β§ πΆ = (((pInvGβπΊ)βπ)βπ¦)) β§ π§ β π) β§ (π¦ β (ππΌπ§) β§ (π¦ β π§) = (π¦ β π))) β§ π β π) β§ (π¦ β (ππΌπ) β§ (π¦ β π) = (π¦ β π))) β§ π β π) β§ (π¦ β ((((pInvGβπΊ)βπ§)βπ)πΌπ) β§ (π¦ β π) = (π¦ β πΆ))) β§ (π₯ β π β§ π = (((pInvGβπΊ)βπ₯)βπΆ))) β π¦ β (ππΌπ§)) |
136 | 1, 3, 4, 27, 130, 28, 30, 134, 135 | btwnlng3 27861 |
. . . . . . . . . . 11
β’
(((((((((((((((π β§
π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β§ π β π) β§ πΆ = (((pInvGβπΊ)βπ)βπ¦)) β§ π§ β π) β§ (π¦ β (ππΌπ§) β§ (π¦ β π§) = (π¦ β π))) β§ π β π) β§ (π¦ β (ππΌπ) β§ (π¦ β π) = (π¦ β π))) β§ π β π) β§ (π¦ β ((((pInvGβπΊ)βπ§)βπ)πΌπ) β§ (π¦ β π) = (π¦ β πΆ))) β§ (π₯ β π β§ π = (((pInvGβπΊ)βπ₯)βπΆ))) β π§ β (ππΏπ¦)) |
137 | 101 | adantr 481 |
. . . . . . . . . . . 12
β’
(((((((((((((((π β§
π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β§ π β π) β§ πΆ = (((pInvGβπΊ)βπ)βπ¦)) β§ π§ β π) β§ (π¦ β (ππΌπ§) β§ (π¦ β π§) = (π¦ β π))) β§ π β π) β§ (π¦ β (ππΌπ) β§ (π¦ β π) = (π¦ β π))) β§ π β π) β§ (π¦ β ((((pInvGβπΊ)βπ§)βπ)πΌπ) β§ (π¦ β π) = (π¦ β πΆ))) β§ (π₯ β π β§ π = (((pInvGβπΊ)βπ₯)βπΆ))) β π β π΄) |
138 | 1, 3, 4, 27, 130, 28, 134, 134, 129, 137, 57 | tglinethru 27876 |
. . . . . . . . . . 11
β’
(((((((((((((((π β§
π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β§ π β π) β§ πΆ = (((pInvGβπΊ)βπ)βπ¦)) β§ π§ β π) β§ (π¦ β (ππΌπ§) β§ (π¦ β π§) = (π¦ β π))) β§ π β π) β§ (π¦ β (ππΌπ) β§ (π¦ β π) = (π¦ β π))) β§ π β π) β§ (π¦ β ((((pInvGβπΊ)βπ§)βπ)πΌπ) β§ (π¦ β π) = (π¦ β πΆ))) β§ (π₯ β π β§ π = (((pInvGβπΊ)βπ₯)βπΆ))) β π΄ = (ππΏπ¦)) |
139 | 136, 138 | eleqtrrd 2836 |
. . . . . . . . . 10
β’
(((((((((((((((π β§
π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β§ π β π) β§ πΆ = (((pInvGβπΊ)βπ)βπ¦)) β§ π§ β π) β§ (π¦ β (ππΌπ§) β§ (π¦ β π§) = (π¦ β π))) β§ π β π) β§ (π¦ β (ππΌπ) β§ (π¦ β π) = (π¦ β π))) β§ π β π) β§ (π¦ β ((((pInvGβπΊ)βπ§)βπ)πΌπ) β§ (π¦ β π) = (π¦ β πΆ))) β§ (π₯ β π β§ π = (((pInvGβπΊ)βπ₯)βπΆ))) β π§ β π΄) |
140 | 1, 3, 4, 27, 28, 30, 71, 71, 129, 57, 139 | tglinethru 27876 |
. . . . . . . . 9
β’
(((((((((((((((π β§
π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β§ π β π) β§ πΆ = (((pInvGβπΊ)βπ)βπ¦)) β§ π§ β π) β§ (π¦ β (ππΌπ§) β§ (π¦ β π§) = (π¦ β π))) β§ π β π) β§ (π¦ β (ππΌπ) β§ (π¦ β π) = (π¦ β π))) β§ π β π) β§ (π¦ β ((((pInvGβπΊ)βπ§)βπ)πΌπ) β§ (π¦ β π) = (π¦ β πΆ))) β§ (π₯ β π β§ π = (((pInvGβπΊ)βπ₯)βπΆ))) β π΄ = (π¦πΏπ§)) |
141 | 126, 140 | eleqtrrd 2836 |
. . . . . . . 8
β’
(((((((((((((((π β§
π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β§ π β π) β§ πΆ = (((pInvGβπΊ)βπ)βπ¦)) β§ π§ β π) β§ (π¦ β (ππΌπ§) β§ (π¦ β π§) = (π¦ β π))) β§ π β π) β§ (π¦ β (ππΌπ) β§ (π¦ β π) = (π¦ β π))) β§ π β π) β§ (π¦ β ((((pInvGβπΊ)βπ§)βπ)πΌπ) β§ (π¦ β π) = (π¦ β πΆ))) β§ (π₯ β π β§ π = (((pInvGβπΊ)βπ₯)βπΆ))) β π₯ β π΄) |
142 | | nelne2 3040 |
. . . . . . . . . . . 12
β’ ((π₯ β π΄ β§ Β¬ πΆ β π΄) β π₯ β πΆ) |
143 | 141, 61, 142 | syl2anc 584 |
. . . . . . . . . . 11
β’
(((((((((((((((π β§
π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β§ π β π) β§ πΆ = (((pInvGβπΊ)βπ)βπ¦)) β§ π§ β π) β§ (π¦ β (ππΌπ§) β§ (π¦ β π§) = (π¦ β π))) β§ π β π) β§ (π¦ β (ππΌπ) β§ (π¦ β π) = (π¦ β π))) β§ π β π) β§ (π¦ β ((((pInvGβπΊ)βπ§)βπ)πΌπ) β§ (π¦ β π) = (π¦ β πΆ))) β§ (π₯ β π β§ π = (((pInvGβπΊ)βπ₯)βπΆ))) β π₯ β πΆ) |
144 | 143 | necomd 2996 |
. . . . . . . . . 10
β’
(((((((((((((((π β§
π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β§ π β π) β§ πΆ = (((pInvGβπΊ)βπ)βπ¦)) β§ π§ β π) β§ (π¦ β (ππΌπ§) β§ (π¦ β π§) = (π¦ β π))) β§ π β π) β§ (π¦ β (ππΌπ) β§ (π¦ β π) = (π¦ β π))) β§ π β π) β§ (π¦ β ((((pInvGβπΊ)βπ§)βπ)πΌπ) β§ (π¦ β π) = (π¦ β πΆ))) β§ (π₯ β π β§ π = (((pInvGβπΊ)βπ₯)βπΆ))) β πΆ β π₯) |
145 | 1, 3, 4, 27, 80, 31, 144 | tgelrnln 27870 |
. . . . . . . . 9
β’
(((((((((((((((π β§
π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β§ π β π) β§ πΆ = (((pInvGβπΊ)βπ)βπ¦)) β§ π§ β π) β§ (π¦ β (ππΌπ§) β§ (π¦ β π§) = (π¦ β π))) β§ π β π) β§ (π¦ β (ππΌπ) β§ (π¦ β π) = (π¦ β π))) β§ π β π) β§ (π¦ β ((((pInvGβπΊ)βπ§)βπ)πΌπ) β§ (π¦ β π) = (π¦ β πΆ))) β§ (π₯ β π β§ π = (((pInvGβπΊ)βπ₯)βπΆ))) β (πΆπΏπ₯) β ran πΏ) |
146 | 1, 3, 4, 27, 80, 31, 144 | tglinerflx2 27874 |
. . . . . . . . . 10
β’
(((((((((((((((π β§
π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β§ π β π) β§ πΆ = (((pInvGβπΊ)βπ)βπ¦)) β§ π§ β π) β§ (π¦ β (ππΌπ§) β§ (π¦ β π§) = (π¦ β π))) β§ π β π) β§ (π¦ β (ππΌπ) β§ (π¦ β π) = (π¦ β π))) β§ π β π) β§ (π¦ β ((((pInvGβπΊ)βπ§)βπ)πΌπ) β§ (π¦ β π) = (π¦ β πΆ))) β§ (π₯ β π β§ π = (((pInvGβπΊ)βπ₯)βπΆ))) β π₯ β (πΆπΏπ₯)) |
147 | 146, 141 | elind 4193 |
. . . . . . . . 9
β’
(((((((((((((((π β§
π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β§ π β π) β§ πΆ = (((pInvGβπΊ)βπ)βπ¦)) β§ π§ β π) β§ (π¦ β (ππΌπ§) β§ (π¦ β π§) = (π¦ β π))) β§ π β π) β§ (π¦ β (ππΌπ) β§ (π¦ β π) = (π¦ β π))) β§ π β π) β§ (π¦ β ((((pInvGβπΊ)βπ§)βπ)πΌπ) β§ (π¦ β π) = (π¦ β πΆ))) β§ (π₯ β π β§ π = (((pInvGβπΊ)βπ₯)βπΆ))) β π₯ β ((πΆπΏπ₯) β© π΄)) |
148 | 1, 3, 4, 27, 80, 31, 144 | tglinerflx1 27873 |
. . . . . . . . 9
β’
(((((((((((((((π β§
π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β§ π β π) β§ πΆ = (((pInvGβπΊ)βπ)βπ¦)) β§ π§ β π) β§ (π¦ β (ππΌπ§) β§ (π¦ β π§) = (π¦ β π))) β§ π β π) β§ (π¦ β (ππΌπ) β§ (π¦ β π) = (π¦ β π))) β§ π β π) β§ (π¦ β ((((pInvGβπΊ)βπ§)βπ)πΌπ) β§ (π¦ β π) = (π¦ β πΆ))) β§ (π₯ β π β§ π = (((pInvGβπΊ)βπ₯)βπΆ))) β πΆ β (πΆπΏπ₯)) |
149 | 27 | adantr 481 |
. . . . . . . . . . . 12
β’
((((((((((((((((π
β§ π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β§ π β π) β§ πΆ = (((pInvGβπΊ)βπ)βπ¦)) β§ π§ β π) β§ (π¦ β (ππΌπ§) β§ (π¦ β π§) = (π¦ β π))) β§ π β π) β§ (π¦ β (ππΌπ) β§ (π¦ β π) = (π¦ β π))) β§ π β π) β§ (π¦ β ((((pInvGβπΊ)βπ§)βπ)πΌπ) β§ (π¦ β π) = (π¦ β πΆ))) β§ (π₯ β π β§ π = (((pInvGβπΊ)βπ₯)βπΆ))) β§ π¦ = π₯) β πΊ β TarskiG) |
150 | 130 | adantr 481 |
. . . . . . . . . . . 12
β’
((((((((((((((((π
β§ π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β§ π β π) β§ πΆ = (((pInvGβπΊ)βπ)βπ¦)) β§ π§ β π) β§ (π¦ β (ππΌπ§) β§ (π¦ β π§) = (π¦ β π))) β§ π β π) β§ (π¦ β (ππΌπ) β§ (π¦ β π) = (π¦ β π))) β§ π β π) β§ (π¦ β ((((pInvGβπΊ)βπ§)βπ)πΌπ) β§ (π¦ β π) = (π¦ β πΆ))) β§ (π₯ β π β§ π = (((pInvGβπΊ)βπ₯)βπΆ))) β§ π¦ = π₯) β π β π) |
151 | 28 | adantr 481 |
. . . . . . . . . . . 12
β’
((((((((((((((((π
β§ π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β§ π β π) β§ πΆ = (((pInvGβπΊ)βπ)βπ¦)) β§ π§ β π) β§ (π¦ β (ππΌπ§) β§ (π¦ β π§) = (π¦ β π))) β§ π β π) β§ (π¦ β (ππΌπ) β§ (π¦ β π) = (π¦ β π))) β§ π β π) β§ (π¦ β ((((pInvGβπΊ)βπ§)βπ)πΌπ) β§ (π¦ β π) = (π¦ β πΆ))) β§ (π₯ β π β§ π = (((pInvGβπΊ)βπ₯)βπΆ))) β§ π¦ = π₯) β π¦ β π) |
152 | 34 | adantr 481 |
. . . . . . . . . . . 12
β’
((((((((((((((((π
β§ π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β§ π β π) β§ πΆ = (((pInvGβπΊ)βπ)βπ¦)) β§ π§ β π) β§ (π¦ β (ππΌπ§) β§ (π¦ β π§) = (π¦ β π))) β§ π β π) β§ (π¦ β (ππΌπ) β§ (π¦ β π) = (π¦ β π))) β§ π β π) β§ (π¦ β ((((pInvGβπΊ)βπ§)βπ)πΌπ) β§ (π¦ β π) = (π¦ β πΆ))) β§ (π₯ β π β§ π = (((pInvGβπΊ)βπ₯)βπΆ))) β§ π¦ = π₯) β π β π) |
153 | 80 | adantr 481 |
. . . . . . . . . . . . . 14
β’
((((((((((((((((π
β§ π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β§ π β π) β§ πΆ = (((pInvGβπΊ)βπ)βπ¦)) β§ π§ β π) β§ (π¦ β (ππΌπ§) β§ (π¦ β π§) = (π¦ β π))) β§ π β π) β§ (π¦ β (ππΌπ) β§ (π¦ β π) = (π¦ β π))) β§ π β π) β§ (π¦ β ((((pInvGβπΊ)βπ§)βπ)πΌπ) β§ (π¦ β π) = (π¦ β πΆ))) β§ (π₯ β π β§ π = (((pInvGβπΊ)βπ₯)βπΆ))) β§ π¦ = π₯) β πΆ β π) |
154 | | eqidd 2733 |
. . . . . . . . . . . . . . . 16
β’
((((((((((((((((π
β§ π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β§ π β π) β§ πΆ = (((pInvGβπΊ)βπ)βπ¦)) β§ π§ β π) β§ (π¦ β (ππΌπ§) β§ (π¦ β π§) = (π¦ β π))) β§ π β π) β§ (π¦ β (ππΌπ) β§ (π¦ β π) = (π¦ β π))) β§ π β π) β§ (π¦ β ((((pInvGβπΊ)βπ§)βπ)πΌπ) β§ (π¦ β π) = (π¦ β πΆ))) β§ (π₯ β π β§ π = (((pInvGβπΊ)βπ₯)βπΆ))) β§ π¦ = π₯) β πΆ = πΆ) |
155 | | simpr 485 |
. . . . . . . . . . . . . . . 16
β’
((((((((((((((((π
β§ π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β§ π β π) β§ πΆ = (((pInvGβπΊ)βπ)βπ¦)) β§ π§ β π) β§ (π¦ β (ππΌπ§) β§ (π¦ β π§) = (π¦ β π))) β§ π β π) β§ (π¦ β (ππΌπ) β§ (π¦ β π) = (π¦ β π))) β§ π β π) β§ (π¦ β ((((pInvGβπΊ)βπ§)βπ)πΌπ) β§ (π¦ β π) = (π¦ β πΆ))) β§ (π₯ β π β§ π = (((pInvGβπΊ)βπ₯)βπΆ))) β§ π¦ = π₯) β π¦ = π₯) |
156 | | eqidd 2733 |
. . . . . . . . . . . . . . . 16
β’
((((((((((((((((π
β§ π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β§ π β π) β§ πΆ = (((pInvGβπΊ)βπ)βπ¦)) β§ π§ β π) β§ (π¦ β (ππΌπ§) β§ (π¦ β π§) = (π¦ β π))) β§ π β π) β§ (π¦ β (ππΌπ) β§ (π¦ β π) = (π¦ β π))) β§ π β π) β§ (π¦ β ((((pInvGβπΊ)βπ§)βπ)πΌπ) β§ (π¦ β π) = (π¦ β πΆ))) β§ (π₯ β π β§ π = (((pInvGβπΊ)βπ₯)βπΆ))) β§ π¦ = π₯) β π = π) |
157 | 154, 155,
156 | s3eqd 14811 |
. . . . . . . . . . . . . . 15
β’
((((((((((((((((π
β§ π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β§ π β π) β§ πΆ = (((pInvGβπΊ)βπ)βπ¦)) β§ π§ β π) β§ (π¦ β (ππΌπ§) β§ (π¦ β π§) = (π¦ β π))) β§ π β π) β§ (π¦ β (ππΌπ) β§ (π¦ β π) = (π¦ β π))) β§ π β π) β§ (π¦ β ((((pInvGβπΊ)βπ§)βπ)πΌπ) β§ (π¦ β π) = (π¦ β πΆ))) β§ (π₯ β π β§ π = (((pInvGβπΊ)βπ₯)βπΆ))) β§ π¦ = π₯) β β¨βπΆπ¦πββ© = β¨βπΆπ₯πββ©) |
158 | 31 | adantr 481 |
. . . . . . . . . . . . . . . 16
β’
((((((((((((((((π
β§ π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β§ π β π) β§ πΆ = (((pInvGβπΊ)βπ)βπ¦)) β§ π§ β π) β§ (π¦ β (ππΌπ§) β§ (π¦ β π§) = (π¦ β π))) β§ π β π) β§ (π¦ β (ππΌπ) β§ (π¦ β π) = (π¦ β π))) β§ π β π) β§ (π¦ β ((((pInvGβπΊ)βπ§)βπ)πΌπ) β§ (π¦ β π) = (π¦ β πΆ))) β§ (π₯ β π β§ π = (((pInvGβπΊ)βπ₯)βπΆ))) β§ π¦ = π₯) β π₯ β π) |
159 | 30 | adantr 481 |
. . . . . . . . . . . . . . . . 17
β’
((((((((((((((((π
β§ π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β§ π β π) β§ πΆ = (((pInvGβπΊ)βπ)βπ¦)) β§ π§ β π) β§ (π¦ β (ππΌπ§) β§ (π¦ β π§) = (π¦ β π))) β§ π β π) β§ (π¦ β (ππΌπ) β§ (π¦ β π) = (π¦ β π))) β§ π β π) β§ (π¦ β ((((pInvGβπΊ)βπ§)βπ)πΌπ) β§ (π¦ β π) = (π¦ β πΆ))) β§ (π₯ β π β§ π = (((pInvGβπΊ)βπ₯)βπΆ))) β§ π¦ = π₯) β π§ β π) |
160 | 106 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
(((((((((((((((π β§
π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β§ π β π) β§ πΆ = (((pInvGβπΊ)βπ)βπ¦)) β§ π§ β π) β§ (π¦ β (ππΌπ§) β§ (π¦ β π§) = (π¦ β π))) β§ π β π) β§ (π¦ β (ππΌπ) β§ (π¦ β π) = (π¦ β π))) β§ π β π) β§ (π¦ β ((((pInvGβπΊ)βπ§)βπ)πΌπ) β§ (π¦ β π) = (π¦ β πΆ))) β§ (π₯ β π β§ π = (((pInvGβπΊ)βπ₯)βπΆ))) β π β π¦) |
161 | 1, 2, 3, 27, 28, 75, 28, 79, 120 | tgcgrcomlr 27720 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
(((((((((((((((π β§
π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β§ π β π) β§ πΆ = (((pInvGβπΊ)βπ)βπ¦)) β§ π§ β π) β§ (π¦ β (ππΌπ§) β§ (π¦ β π§) = (π¦ β π))) β§ π β π) β§ (π¦ β (ππΌπ) β§ (π¦ β π) = (π¦ β π))) β§ π β π) β§ (π¦ β ((((pInvGβπΊ)βπ§)βπ)πΌπ) β§ (π¦ β π) = (π¦ β πΆ))) β§ (π₯ β π β§ π = (((pInvGβπΊ)βπ₯)βπΆ))) β (π β π¦) = ((((pInvGβπΊ)βπ§)βπ) β π¦)) |
162 | 1, 2, 3, 4, 5, 27,
30, 73, 75 | mircgr 27897 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
(((((((((((((((π β§
π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β§ π β π) β§ πΆ = (((pInvGβπΊ)βπ)βπ¦)) β§ π§ β π) β§ (π¦ β (ππΌπ§) β§ (π¦ β π§) = (π¦ β π))) β§ π β π) β§ (π¦ β (ππΌπ) β§ (π¦ β π) = (π¦ β π))) β§ π β π) β§ (π¦ β ((((pInvGβπΊ)βπ§)βπ)πΌπ) β§ (π¦ β π) = (π¦ β πΆ))) β§ (π₯ β π β§ π = (((pInvGβπΊ)βπ₯)βπΆ))) β (π§ β (((pInvGβπΊ)βπ§)βπ)) = (π§ β π)) |
163 | 162 | eqcomd 2738 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
(((((((((((((((π β§
π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β§ π β π) β§ πΆ = (((pInvGβπΊ)βπ)βπ¦)) β§ π§ β π) β§ (π¦ β (ππΌπ§) β§ (π¦ β π§) = (π¦ β π))) β§ π β π) β§ (π¦ β (ππΌπ) β§ (π¦ β π) = (π¦ β π))) β§ π β π) β§ (π¦ β ((((pInvGβπΊ)βπ§)βπ)πΌπ) β§ (π¦ β π) = (π¦ β πΆ))) β§ (π₯ β π β§ π = (((pInvGβπΊ)βπ₯)βπΆ))) β (π§ β π) = (π§ β (((pInvGβπΊ)βπ§)βπ))) |
164 | 1, 2, 3, 27, 30, 75, 30, 79, 163 | tgcgrcomlr 27720 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
(((((((((((((((π β§
π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β§ π β π) β§ πΆ = (((pInvGβπΊ)βπ)βπ¦)) β§ π§ β π) β§ (π¦ β (ππΌπ§) β§ (π¦ β π§) = (π¦ β π))) β§ π β π) β§ (π¦ β (ππΌπ) β§ (π¦ β π) = (π¦ β π))) β§ π β π) β§ (π¦ β ((((pInvGβπΊ)βπ§)βπ)πΌπ) β§ (π¦ β π) = (π¦ β πΆ))) β§ (π₯ β π β§ π = (((pInvGβπΊ)βπ₯)βπΆ))) β (π β π§) = ((((pInvGβπΊ)βπ§)βπ) β π§)) |
165 | | eqidd 2733 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
(((((((((((((((π β§
π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β§ π β π) β§ πΆ = (((pInvGβπΊ)βπ)βπ¦)) β§ π§ β π) β§ (π¦ β (ππΌπ§) β§ (π¦ β π§) = (π¦ β π))) β§ π β π) β§ (π¦ β (ππΌπ) β§ (π¦ β π) = (π¦ β π))) β§ π β π) β§ (π¦ β ((((pInvGβπΊ)βπ§)βπ)πΌπ) β§ (π¦ β π) = (π¦ β πΆ))) β§ (π₯ β π β§ π = (((pInvGβπΊ)βπ₯)βπΆ))) β (π¦ β π§) = (π¦ β π§)) |
166 | 1, 2, 3, 27, 75, 28, 80, 79, 28, 81, 30, 30, 160, 89, 90, 161, 121, 164, 165 | axtg5seg 27705 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(((((((((((((((π β§
π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β§ π β π) β§ πΆ = (((pInvGβπΊ)βπ)βπ¦)) β§ π§ β π) β§ (π¦ β (ππΌπ§) β§ (π¦ β π§) = (π¦ β π))) β§ π β π) β§ (π¦ β (ππΌπ) β§ (π¦ β π) = (π¦ β π))) β§ π β π) β§ (π¦ β ((((pInvGβπΊ)βπ§)βπ)πΌπ) β§ (π¦ β π) = (π¦ β πΆ))) β§ (π₯ β π β§ π = (((pInvGβπΊ)βπ₯)βπΆ))) β (πΆ β π§) = (π β π§)) |
167 | 1, 2, 3, 27, 80, 30, 81, 30, 166 | tgcgrcomlr 27720 |
. . . . . . . . . . . . . . . . . . . 20
β’
(((((((((((((((π β§
π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β§ π β π) β§ πΆ = (((pInvGβπΊ)βπ)βπ¦)) β§ π§ β π) β§ (π¦ β (ππΌπ§) β§ (π¦ β π§) = (π¦ β π))) β§ π β π) β§ (π¦ β (ππΌπ) β§ (π¦ β π) = (π¦ β π))) β§ π β π) β§ (π¦ β ((((pInvGβπΊ)βπ§)βπ)πΌπ) β§ (π¦ β π) = (π¦ β πΆ))) β§ (π₯ β π β§ π = (((pInvGβπΊ)βπ₯)βπΆ))) β (π§ β πΆ) = (π§ β π)) |
168 | 123 | oveq2d 7421 |
. . . . . . . . . . . . . . . . . . . 20
β’
(((((((((((((((π β§
π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β§ π β π) β§ πΆ = (((pInvGβπΊ)βπ)βπ¦)) β§ π§ β π) β§ (π¦ β (ππΌπ§) β§ (π¦ β π§) = (π¦ β π))) β§ π β π) β§ (π¦ β (ππΌπ) β§ (π¦ β π) = (π¦ β π))) β§ π β π) β§ (π¦ β ((((pInvGβπΊ)βπ§)βπ)πΌπ) β§ (π¦ β π) = (π¦ β πΆ))) β§ (π₯ β π β§ π = (((pInvGβπΊ)βπ₯)βπΆ))) β (π§ β π) = (π§ β (((pInvGβπΊ)βπ₯)βπΆ))) |
169 | 167, 168 | eqtrd 2772 |
. . . . . . . . . . . . . . . . . . 19
β’
(((((((((((((((π β§
π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β§ π β π) β§ πΆ = (((pInvGβπΊ)βπ)βπ¦)) β§ π§ β π) β§ (π¦ β (ππΌπ§) β§ (π¦ β π§) = (π¦ β π))) β§ π β π) β§ (π¦ β (ππΌπ) β§ (π¦ β π) = (π¦ β π))) β§ π β π) β§ (π¦ β ((((pInvGβπΊ)βπ§)βπ)πΌπ) β§ (π¦ β π) = (π¦ β πΆ))) β§ (π₯ β π β§ π = (((pInvGβπΊ)βπ₯)βπΆ))) β (π§ β πΆ) = (π§ β (((pInvGβπΊ)βπ₯)βπΆ))) |
170 | 1, 2, 3, 4, 5, 27,
30, 31, 80 | israg 27937 |
. . . . . . . . . . . . . . . . . . 19
β’
(((((((((((((((π β§
π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β§ π β π) β§ πΆ = (((pInvGβπΊ)βπ)βπ¦)) β§ π§ β π) β§ (π¦ β (ππΌπ§) β§ (π¦ β π§) = (π¦ β π))) β§ π β π) β§ (π¦ β (ππΌπ) β§ (π¦ β π) = (π¦ β π))) β§ π β π) β§ (π¦ β ((((pInvGβπΊ)βπ§)βπ)πΌπ) β§ (π¦ β π) = (π¦ β πΆ))) β§ (π₯ β π β§ π = (((pInvGβπΊ)βπ₯)βπΆ))) β (β¨βπ§π₯πΆββ© β (βGβπΊ) β (π§ β πΆ) = (π§ β (((pInvGβπΊ)βπ₯)βπΆ)))) |
171 | 169, 170 | mpbird 256 |
. . . . . . . . . . . . . . . . . 18
β’
(((((((((((((((π β§
π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β§ π β π) β§ πΆ = (((pInvGβπΊ)βπ)βπ¦)) β§ π§ β π) β§ (π¦ β (ππΌπ§) β§ (π¦ β π§) = (π¦ β π))) β§ π β π) β§ (π¦ β (ππΌπ) β§ (π¦ β π) = (π¦ β π))) β§ π β π) β§ (π¦ β ((((pInvGβπΊ)βπ§)βπ)πΌπ) β§ (π¦ β π) = (π¦ β πΆ))) β§ (π₯ β π β§ π = (((pInvGβπΊ)βπ₯)βπΆ))) β β¨βπ§π₯πΆββ© β (βGβπΊ)) |
172 | 171 | adantr 481 |
. . . . . . . . . . . . . . . . 17
β’
((((((((((((((((π
β§ π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β§ π β π) β§ πΆ = (((pInvGβπΊ)βπ)βπ¦)) β§ π§ β π) β§ (π¦ β (ππΌπ§) β§ (π¦ β π§) = (π¦ β π))) β§ π β π) β§ (π¦ β (ππΌπ) β§ (π¦ β π) = (π¦ β π))) β§ π β π) β§ (π¦ β ((((pInvGβπΊ)βπ§)βπ)πΌπ) β§ (π¦ β π) = (π¦ β πΆ))) β§ (π₯ β π β§ π = (((pInvGβπΊ)βπ₯)βπΆ))) β§ π¦ = π₯) β β¨βπ§π₯πΆββ© β (βGβπΊ)) |
173 | 72 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
β’
((((((((((((((((π
β§ π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β§ π β π) β§ πΆ = (((pInvGβπΊ)βπ)βπ¦)) β§ π§ β π) β§ (π¦ β (ππΌπ§) β§ (π¦ β π§) = (π¦ β π))) β§ π β π) β§ (π¦ β (ππΌπ) β§ (π¦ β π) = (π¦ β π))) β§ π β π) β§ (π¦ β ((((pInvGβπΊ)βπ§)βπ)πΌπ) β§ (π¦ β π) = (π¦ β πΆ))) β§ (π₯ β π β§ π = (((pInvGβπΊ)βπ₯)βπΆ))) β§ π¦ = π₯) β π§ β π¦) |
174 | 173, 155 | neeqtrd 3010 |
. . . . . . . . . . . . . . . . 17
β’
((((((((((((((((π
β§ π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β§ π β π) β§ πΆ = (((pInvGβπΊ)βπ)βπ¦)) β§ π§ β π) β§ (π¦ β (ππΌπ§) β§ (π¦ β π§) = (π¦ β π))) β§ π β π) β§ (π¦ β (ππΌπ) β§ (π¦ β π) = (π¦ β π))) β§ π β π) β§ (π¦ β ((((pInvGβπΊ)βπ§)βπ)πΌπ) β§ (π¦ β π) = (π¦ β πΆ))) β§ (π₯ β π β§ π = (((pInvGβπΊ)βπ₯)βπΆ))) β§ π¦ = π₯) β π§ β π₯) |
175 | 132 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
((((((((((((((((π
β§ π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β§ π β π) β§ πΆ = (((pInvGβπΊ)βπ)βπ¦)) β§ π§ β π) β§ (π¦ β (ππΌπ§) β§ (π¦ β π§) = (π¦ β π))) β§ π β π) β§ (π¦ β (ππΌπ) β§ (π¦ β π) = (π¦ β π))) β§ π β π) β§ (π¦ β ((((pInvGβπΊ)βπ§)βπ)πΌπ) β§ (π¦ β π) = (π¦ β πΆ))) β§ (π₯ β π β§ π = (((pInvGβπΊ)βπ₯)βπΆ))) β§ π¦ = π₯) β (π β πΆ) = (π β π¦)) |
176 | 133 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
((((((((((((((((π
β§ π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β§ π β π) β§ πΆ = (((pInvGβπΊ)βπ)βπ¦)) β§ π§ β π) β§ (π¦ β (ππΌπ§) β§ (π¦ β π§) = (π¦ β π))) β§ π β π) β§ (π¦ β (ππΌπ) β§ (π¦ β π) = (π¦ β π))) β§ π β π) β§ (π¦ β ((((pInvGβπΊ)βπ§)βπ)πΌπ) β§ (π¦ β π) = (π¦ β πΆ))) β§ (π₯ β π β§ π = (((pInvGβπΊ)βπ₯)βπΆ))) β§ π¦ = π₯) β π β πΆ) |
177 | 1, 2, 3, 149, 150, 153, 150, 151, 175, 176 | tgcgrneq 27723 |
. . . . . . . . . . . . . . . . . . . . 21
β’
((((((((((((((((π
β§ π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β§ π β π) β§ πΆ = (((pInvGβπΊ)βπ)βπ¦)) β§ π§ β π) β§ (π¦ β (ππΌπ§) β§ (π¦ β π§) = (π¦ β π))) β§ π β π) β§ (π¦ β (ππΌπ) β§ (π¦ β π) = (π¦ β π))) β§ π β π) β§ (π¦ β ((((pInvGβπΊ)βπ§)βπ)πΌπ) β§ (π¦ β π) = (π¦ β πΆ))) β§ (π₯ β π β§ π = (((pInvGβπΊ)βπ₯)βπΆ))) β§ π¦ = π₯) β π β π¦) |
178 | 177 | necomd 2996 |
. . . . . . . . . . . . . . . . . . . 20
β’
((((((((((((((((π
β§ π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β§ π β π) β§ πΆ = (((pInvGβπΊ)βπ)βπ¦)) β§ π§ β π) β§ (π¦ β (ππΌπ§) β§ (π¦ β π§) = (π¦ β π))) β§ π β π) β§ (π¦ β (ππΌπ) β§ (π¦ β π) = (π¦ β π))) β§ π β π) β§ (π¦ β ((((pInvGβπΊ)βπ§)βπ)πΌπ) β§ (π¦ β π) = (π¦ β πΆ))) β§ (π₯ β π β§ π = (((pInvGβπΊ)βπ₯)βπΆ))) β§ π¦ = π₯) β π¦ β π) |
179 | 136 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
β’
((((((((((((((((π
β§ π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β§ π β π) β§ πΆ = (((pInvGβπΊ)βπ)βπ¦)) β§ π§ β π) β§ (π¦ β (ππΌπ§) β§ (π¦ β π§) = (π¦ β π))) β§ π β π) β§ (π¦ β (ππΌπ) β§ (π¦ β π) = (π¦ β π))) β§ π β π) β§ (π¦ β ((((pInvGβπΊ)βπ§)βπ)πΌπ) β§ (π¦ β π) = (π¦ β πΆ))) β§ (π₯ β π β§ π = (((pInvGβπΊ)βπ₯)βπΆ))) β§ π¦ = π₯) β π§ β (ππΏπ¦)) |
180 | 1, 3, 4, 149, 151, 150, 159, 178, 179 | lncom 27862 |
. . . . . . . . . . . . . . . . . . 19
β’
((((((((((((((((π
β§ π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β§ π β π) β§ πΆ = (((pInvGβπΊ)βπ)βπ¦)) β§ π§ β π) β§ (π¦ β (ππΌπ§) β§ (π¦ β π§) = (π¦ β π))) β§ π β π) β§ (π¦ β (ππΌπ) β§ (π¦ β π) = (π¦ β π))) β§ π β π) β§ (π¦ β ((((pInvGβπΊ)βπ§)βπ)πΌπ) β§ (π¦ β π) = (π¦ β πΆ))) β§ (π₯ β π β§ π = (((pInvGβπΊ)βπ₯)βπΆ))) β§ π¦ = π₯) β π§ β (π¦πΏπ)) |
181 | 155 | oveq1d 7420 |
. . . . . . . . . . . . . . . . . . 19
β’
((((((((((((((((π
β§ π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β§ π β π) β§ πΆ = (((pInvGβπΊ)βπ)βπ¦)) β§ π§ β π) β§ (π¦ β (ππΌπ§) β§ (π¦ β π§) = (π¦ β π))) β§ π β π) β§ (π¦ β (ππΌπ) β§ (π¦ β π) = (π¦ β π))) β§ π β π) β§ (π¦ β ((((pInvGβπΊ)βπ§)βπ)πΌπ) β§ (π¦ β π) = (π¦ β πΆ))) β§ (π₯ β π β§ π = (((pInvGβπΊ)βπ₯)βπΆ))) β§ π¦ = π₯) β (π¦πΏπ) = (π₯πΏπ)) |
182 | 180, 181 | eleqtrd 2835 |
. . . . . . . . . . . . . . . . . 18
β’
((((((((((((((((π
β§ π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β§ π β π) β§ πΆ = (((pInvGβπΊ)βπ)βπ¦)) β§ π§ β π) β§ (π¦ β (ππΌπ§) β§ (π¦ β π§) = (π¦ β π))) β§ π β π) β§ (π¦ β (ππΌπ) β§ (π¦ β π) = (π¦ β π))) β§ π β π) β§ (π¦ β ((((pInvGβπΊ)βπ§)βπ)πΌπ) β§ (π¦ β π) = (π¦ β πΆ))) β§ (π₯ β π β§ π = (((pInvGβπΊ)βπ₯)βπΆ))) β§ π¦ = π₯) β π§ β (π₯πΏπ)) |
183 | 182 | orcd 871 |
. . . . . . . . . . . . . . . . 17
β’
((((((((((((((((π
β§ π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β§ π β π) β§ πΆ = (((pInvGβπΊ)βπ)βπ¦)) β§ π§ β π) β§ (π¦ β (ππΌπ§) β§ (π¦ β π§) = (π¦ β π))) β§ π β π) β§ (π¦ β (ππΌπ) β§ (π¦ β π) = (π¦ β π))) β§ π β π) β§ (π¦ β ((((pInvGβπΊ)βπ§)βπ)πΌπ) β§ (π¦ β π) = (π¦ β πΆ))) β§ (π₯ β π β§ π = (((pInvGβπΊ)βπ₯)βπΆ))) β§ π¦ = π₯) β (π§ β (π₯πΏπ) β¨ π₯ = π)) |
184 | 1, 2, 3, 4, 5, 149, 159, 158, 153, 150, 172, 174, 183 | ragcol 27939 |
. . . . . . . . . . . . . . . 16
β’
((((((((((((((((π
β§ π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β§ π β π) β§ πΆ = (((pInvGβπΊ)βπ)βπ¦)) β§ π§ β π) β§ (π¦ β (ππΌπ§) β§ (π¦ β π§) = (π¦ β π))) β§ π β π) β§ (π¦ β (ππΌπ) β§ (π¦ β π) = (π¦ β π))) β§ π β π) β§ (π¦ β ((((pInvGβπΊ)βπ§)βπ)πΌπ) β§ (π¦ β π) = (π¦ β πΆ))) β§ (π₯ β π β§ π = (((pInvGβπΊ)βπ₯)βπΆ))) β§ π¦ = π₯) β β¨βππ₯πΆββ© β (βGβπΊ)) |
185 | 1, 2, 3, 4, 5, 149, 150, 158, 153, 184 | ragcom 27938 |
. . . . . . . . . . . . . . 15
β’
((((((((((((((((π
β§ π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β§ π β π) β§ πΆ = (((pInvGβπΊ)βπ)βπ¦)) β§ π§ β π) β§ (π¦ β (ππΌπ§) β§ (π¦ β π§) = (π¦ β π))) β§ π β π) β§ (π¦ β (ππΌπ) β§ (π¦ β π) = (π¦ β π))) β§ π β π) β§ (π¦ β ((((pInvGβπΊ)βπ§)βπ)πΌπ) β§ (π¦ β π) = (π¦ β πΆ))) β§ (π₯ β π β§ π = (((pInvGβπΊ)βπ₯)βπΆ))) β§ π¦ = π₯) β β¨βπΆπ₯πββ© β (βGβπΊ)) |
186 | 157, 185 | eqeltrd 2833 |
. . . . . . . . . . . . . 14
β’
((((((((((((((((π
β§ π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β§ π β π) β§ πΆ = (((pInvGβπΊ)βπ)βπ¦)) β§ π§ β π) β§ (π¦ β (ππΌπ§) β§ (π¦ β π§) = (π¦ β π))) β§ π β π) β§ (π¦ β (ππΌπ) β§ (π¦ β π) = (π¦ β π))) β§ π β π) β§ (π¦ β ((((pInvGβπΊ)βπ§)βπ)πΌπ) β§ (π¦ β π) = (π¦ β πΆ))) β§ (π₯ β π β§ π = (((pInvGβπΊ)βπ₯)βπΆ))) β§ π¦ = π₯) β β¨βπΆπ¦πββ© β (βGβπΊ)) |
187 | 64 | adantr 481 |
. . . . . . . . . . . . . 14
β’
((((((((((((((((π
β§ π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β§ π β π) β§ πΆ = (((pInvGβπΊ)βπ)βπ¦)) β§ π§ β π) β§ (π¦ β (ππΌπ§) β§ (π¦ β π§) = (π¦ β π))) β§ π β π) β§ (π¦ β (ππΌπ) β§ (π¦ β π) = (π¦ β π))) β§ π β π) β§ (π¦ β ((((pInvGβπΊ)βπ§)βπ)πΌπ) β§ (π¦ β π) = (π¦ β πΆ))) β§ (π₯ β π β§ π = (((pInvGβπΊ)βπ₯)βπΆ))) β§ π¦ = π₯) β πΆ β π¦) |
188 | 1, 2, 3, 27, 80, 34, 28, 84 | tgbtwncom 27728 |
. . . . . . . . . . . . . . . 16
β’
(((((((((((((((π β§
π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β§ π β π) β§ πΆ = (((pInvGβπΊ)βπ)βπ¦)) β§ π§ β π) β§ (π¦ β (ππΌπ§) β§ (π¦ β π§) = (π¦ β π))) β§ π β π) β§ (π¦ β (ππΌπ) β§ (π¦ β π) = (π¦ β π))) β§ π β π) β§ (π¦ β ((((pInvGβπΊ)βπ§)βπ)πΌπ) β§ (π¦ β π) = (π¦ β πΆ))) β§ (π₯ β π β§ π = (((pInvGβπΊ)βπ₯)βπΆ))) β π β (π¦πΌπΆ)) |
189 | 1, 4, 3, 27, 28, 34, 80, 188 | btwncolg3 27797 |
. . . . . . . . . . . . . . 15
β’
(((((((((((((((π β§
π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β§ π β π) β§ πΆ = (((pInvGβπΊ)βπ)βπ¦)) β§ π§ β π) β§ (π¦ β (ππΌπ§) β§ (π¦ β π§) = (π¦ β π))) β§ π β π) β§ (π¦ β (ππΌπ) β§ (π¦ β π) = (π¦ β π))) β§ π β π) β§ (π¦ β ((((pInvGβπΊ)βπ§)βπ)πΌπ) β§ (π¦ β π) = (π¦ β πΆ))) β§ (π₯ β π β§ π = (((pInvGβπΊ)βπ₯)βπΆ))) β (πΆ β (π¦πΏπ) β¨ π¦ = π)) |
190 | 189 | adantr 481 |
. . . . . . . . . . . . . 14
β’
((((((((((((((((π
β§ π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β§ π β π) β§ πΆ = (((pInvGβπΊ)βπ)βπ¦)) β§ π§ β π) β§ (π¦ β (ππΌπ§) β§ (π¦ β π§) = (π¦ β π))) β§ π β π) β§ (π¦ β (ππΌπ) β§ (π¦ β π) = (π¦ β π))) β§ π β π) β§ (π¦ β ((((pInvGβπΊ)βπ§)βπ)πΌπ) β§ (π¦ β π) = (π¦ β πΆ))) β§ (π₯ β π β§ π = (((pInvGβπΊ)βπ₯)βπΆ))) β§ π¦ = π₯) β (πΆ β (π¦πΏπ) β¨ π¦ = π)) |
191 | 1, 2, 3, 4, 5, 149, 153, 151, 150, 152, 186, 187, 190 | ragcol 27939 |
. . . . . . . . . . . . 13
β’
((((((((((((((((π
β§ π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β§ π β π) β§ πΆ = (((pInvGβπΊ)βπ)βπ¦)) β§ π§ β π) β§ (π¦ β (ππΌπ§) β§ (π¦ β π§) = (π¦ β π))) β§ π β π) β§ (π¦ β (ππΌπ) β§ (π¦ β π) = (π¦ β π))) β§ π β π) β§ (π¦ β ((((pInvGβπΊ)βπ§)βπ)πΌπ) β§ (π¦ β π) = (π¦ β πΆ))) β§ (π₯ β π β§ π = (((pInvGβπΊ)βπ₯)βπΆ))) β§ π¦ = π₯) β β¨βππ¦πββ© β (βGβπΊ)) |
192 | 1, 2, 3, 4, 5, 149, 152, 151, 150, 191 | ragcom 27938 |
. . . . . . . . . . . 12
β’
((((((((((((((((π
β§ π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β§ π β π) β§ πΆ = (((pInvGβπΊ)βπ)βπ¦)) β§ π§ β π) β§ (π¦ β (ππΌπ§) β§ (π¦ β π§) = (π¦ β π))) β§ π β π) β§ (π¦ β (ππΌπ) β§ (π¦ β π) = (π¦ β π))) β§ π β π) β§ (π¦ β ((((pInvGβπΊ)βπ§)βπ)πΌπ) β§ (π¦ β π) = (π¦ β πΆ))) β§ (π₯ β π β§ π = (((pInvGβπΊ)βπ₯)βπΆ))) β§ π¦ = π₯) β β¨βππ¦πββ© β (βGβπΊ)) |
193 | 96 | ad2antrr 724 |
. . . . . . . . . . . 12
β’
((((((((((((((((π
β§ π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β§ π β π) β§ πΆ = (((pInvGβπΊ)βπ)βπ¦)) β§ π§ β π) β§ (π¦ β (ππΌπ§) β§ (π¦ β π§) = (π¦ β π))) β§ π β π) β§ (π¦ β (ππΌπ) β§ (π¦ β π) = (π¦ β π))) β§ π β π) β§ (π¦ β ((((pInvGβπΊ)βπ§)βπ)πΌπ) β§ (π¦ β π) = (π¦ β πΆ))) β§ (π₯ β π β§ π = (((pInvGβπΊ)βπ₯)βπΆ))) β§ π¦ = π₯) β β¨βπππ¦ββ© β (βGβπΊ)) |
194 | 1, 2, 3, 4, 5, 149, 150, 151, 152, 192, 193 | ragflat 27944 |
. . . . . . . . . . 11
β’
((((((((((((((((π
β§ π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β§ π β π) β§ πΆ = (((pInvGβπΊ)βπ)βπ¦)) β§ π§ β π) β§ (π¦ β (ππΌπ§) β§ (π¦ β π§) = (π¦ β π))) β§ π β π) β§ (π¦ β (ππΌπ) β§ (π¦ β π) = (π¦ β π))) β§ π β π) β§ (π¦ β ((((pInvGβπΊ)βπ§)βπ)πΌπ) β§ (π¦ β π) = (π¦ β πΆ))) β§ (π₯ β π β§ π = (((pInvGβπΊ)βπ₯)βπΆ))) β§ π¦ = π₯) β π¦ = π) |
195 | 70 | adantr 481 |
. . . . . . . . . . . 12
β’
((((((((((((((((π
β§ π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β§ π β π) β§ πΆ = (((pInvGβπΊ)βπ)βπ¦)) β§ π§ β π) β§ (π¦ β (ππΌπ§) β§ (π¦ β π§) = (π¦ β π))) β§ π β π) β§ (π¦ β (ππΌπ) β§ (π¦ β π) = (π¦ β π))) β§ π β π) β§ (π¦ β ((((pInvGβπΊ)βπ§)βπ)πΌπ) β§ (π¦ β π) = (π¦ β πΆ))) β§ (π₯ β π β§ π = (((pInvGβπΊ)βπ₯)βπΆ))) β§ π¦ = π₯) β π¦ β π) |
196 | 195 | neneqd 2945 |
. . . . . . . . . . 11
β’
((((((((((((((((π
β§ π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β§ π β π) β§ πΆ = (((pInvGβπΊ)βπ)βπ¦)) β§ π§ β π) β§ (π¦ β (ππΌπ§) β§ (π¦ β π§) = (π¦ β π))) β§ π β π) β§ (π¦ β (ππΌπ) β§ (π¦ β π) = (π¦ β π))) β§ π β π) β§ (π¦ β ((((pInvGβπΊ)βπ§)βπ)πΌπ) β§ (π¦ β π) = (π¦ β πΆ))) β§ (π₯ β π β§ π = (((pInvGβπΊ)βπ₯)βπΆ))) β§ π¦ = π₯) β Β¬ π¦ = π) |
197 | 194, 196 | pm2.65da 815 |
. . . . . . . . . 10
β’
(((((((((((((((π β§
π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β§ π β π) β§ πΆ = (((pInvGβπΊ)βπ)βπ¦)) β§ π§ β π) β§ (π¦ β (ππΌπ§) β§ (π¦ β π§) = (π¦ β π))) β§ π β π) β§ (π¦ β (ππΌπ) β§ (π¦ β π) = (π¦ β π))) β§ π β π) β§ (π¦ β ((((pInvGβπΊ)βπ§)βπ)πΌπ) β§ (π¦ β π) = (π¦ β πΆ))) β§ (π₯ β π β§ π = (((pInvGβπΊ)βπ₯)βπΆ))) β Β¬ π¦ = π₯) |
198 | 197 | neqned 2947 |
. . . . . . . . 9
β’
(((((((((((((((π β§
π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β§ π β π) β§ πΆ = (((pInvGβπΊ)βπ)βπ¦)) β§ π§ β π) β§ (π¦ β (ππΌπ§) β§ (π¦ β π§) = (π¦ β π))) β§ π β π) β§ (π¦ β (ππΌπ) β§ (π¦ β π) = (π¦ β π))) β§ π β π) β§ (π¦ β ((((pInvGβπΊ)βπ§)βπ)πΌπ) β§ (π¦ β π) = (π¦ β πΆ))) β§ (π₯ β π β§ π = (((pInvGβπΊ)βπ₯)βπΆ))) β π¦ β π₯) |
199 | 123 | oveq2d 7421 |
. . . . . . . . . . . 12
β’
(((((((((((((((π β§
π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β§ π β π) β§ πΆ = (((pInvGβπΊ)βπ)βπ¦)) β§ π§ β π) β§ (π¦ β (ππΌπ§) β§ (π¦ β π§) = (π¦ β π))) β§ π β π) β§ (π¦ β (ππΌπ) β§ (π¦ β π) = (π¦ β π))) β§ π β π) β§ (π¦ β ((((pInvGβπΊ)βπ§)βπ)πΌπ) β§ (π¦ β π) = (π¦ β πΆ))) β§ (π₯ β π β§ π = (((pInvGβπΊ)βπ₯)βπΆ))) β (π¦ β π) = (π¦ β (((pInvGβπΊ)βπ₯)βπΆ))) |
200 | 121, 199 | eqtrd 2772 |
. . . . . . . . . . 11
β’
(((((((((((((((π β§
π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β§ π β π) β§ πΆ = (((pInvGβπΊ)βπ)βπ¦)) β§ π§ β π) β§ (π¦ β (ππΌπ§) β§ (π¦ β π§) = (π¦ β π))) β§ π β π) β§ (π¦ β (ππΌπ) β§ (π¦ β π) = (π¦ β π))) β§ π β π) β§ (π¦ β ((((pInvGβπΊ)βπ§)βπ)πΌπ) β§ (π¦ β π) = (π¦ β πΆ))) β§ (π₯ β π β§ π = (((pInvGβπΊ)βπ₯)βπΆ))) β (π¦ β πΆ) = (π¦ β (((pInvGβπΊ)βπ₯)βπΆ))) |
201 | 1, 2, 3, 4, 5, 27,
28, 31, 80 | israg 27937 |
. . . . . . . . . . 11
β’
(((((((((((((((π β§
π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β§ π β π) β§ πΆ = (((pInvGβπΊ)βπ)βπ¦)) β§ π§ β π) β§ (π¦ β (ππΌπ§) β§ (π¦ β π§) = (π¦ β π))) β§ π β π) β§ (π¦ β (ππΌπ) β§ (π¦ β π) = (π¦ β π))) β§ π β π) β§ (π¦ β ((((pInvGβπΊ)βπ§)βπ)πΌπ) β§ (π¦ β π) = (π¦ β πΆ))) β§ (π₯ β π β§ π = (((pInvGβπΊ)βπ₯)βπΆ))) β (β¨βπ¦π₯πΆββ© β (βGβπΊ) β (π¦ β πΆ) = (π¦ β (((pInvGβπΊ)βπ₯)βπΆ)))) |
202 | 200, 201 | mpbird 256 |
. . . . . . . . . 10
β’
(((((((((((((((π β§
π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β§ π β π) β§ πΆ = (((pInvGβπΊ)βπ)βπ¦)) β§ π§ β π) β§ (π¦ β (ππΌπ§) β§ (π¦ β π§) = (π¦ β π))) β§ π β π) β§ (π¦ β (ππΌπ) β§ (π¦ β π) = (π¦ β π))) β§ π β π) β§ (π¦ β ((((pInvGβπΊ)βπ§)βπ)πΌπ) β§ (π¦ β π) = (π¦ β πΆ))) β§ (π₯ β π β§ π = (((pInvGβπΊ)βπ₯)βπΆ))) β β¨βπ¦π₯πΆββ© β (βGβπΊ)) |
203 | 1, 2, 3, 4, 5, 27,
28, 31, 80, 202 | ragcom 27938 |
. . . . . . . . 9
β’
(((((((((((((((π β§
π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β§ π β π) β§ πΆ = (((pInvGβπΊ)βπ)βπ¦)) β§ π§ β π) β§ (π¦ β (ππΌπ§) β§ (π¦ β π§) = (π¦ β π))) β§ π β π) β§ (π¦ β (ππΌπ) β§ (π¦ β π) = (π¦ β π))) β§ π β π) β§ (π¦ β ((((pInvGβπΊ)βπ§)βπ)πΌπ) β§ (π¦ β π) = (π¦ β πΆ))) β§ (π₯ β π β§ π = (((pInvGβπΊ)βπ₯)βπΆ))) β β¨βπΆπ₯π¦ββ© β (βGβπΊ)) |
204 | 1, 2, 3, 4, 27, 145, 129, 147, 148, 57, 144, 198, 203 | ragperp 27957 |
. . . . . . . 8
β’
(((((((((((((((π β§
π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β§ π β π) β§ πΆ = (((pInvGβπΊ)βπ)βπ¦)) β§ π§ β π) β§ (π¦ β (ππΌπ§) β§ (π¦ β π§) = (π¦ β π))) β§ π β π) β§ (π¦ β (ππΌπ) β§ (π¦ β π) = (π¦ β π))) β§ π β π) β§ (π¦ β ((((pInvGβπΊ)βπ§)βπ)πΌπ) β§ (π¦ β π) = (π¦ β πΆ))) β§ (π₯ β π β§ π = (((pInvGβπΊ)βπ₯)βπΆ))) β (πΆπΏπ₯)(βGβπΊ)π΄) |
205 | 26, 141, 204 | reximssdv 3172 |
. . . . . . 7
β’
((((((((((((((π β§
π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β§ π β π) β§ πΆ = (((pInvGβπΊ)βπ)βπ¦)) β§ π§ β π) β§ (π¦ β (ππΌπ§) β§ (π¦ β π§) = (π¦ β π))) β§ π β π) β§ (π¦ β (ππΌπ) β§ (π¦ β π) = (π¦ β π))) β§ π β π) β§ (π¦ β ((((pInvGβπΊ)βπ§)βπ)πΌπ) β§ (π¦ β π) = (π¦ β πΆ))) β βπ₯ β π΄ (πΆπΏπ₯)(βGβπΊ)π΄) |
206 | 1, 2, 3, 11, 78, 22, 22, 17 | axtgsegcon 27704 |
. . . . . . 7
β’
((((((((((((π β§
π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β§ π β π) β§ πΆ = (((pInvGβπΊ)βπ)βπ¦)) β§ π§ β π) β§ (π¦ β (ππΌπ§) β§ (π¦ β π§) = (π¦ β π))) β§ π β π) β§ (π¦ β (ππΌπ) β§ (π¦ β π) = (π¦ β π))) β βπ β π (π¦ β ((((pInvGβπΊ)βπ§)βπ)πΌπ) β§ (π¦ β π) = (π¦ β πΆ))) |
207 | 205, 206 | r19.29a 3162 |
. . . . . 6
β’
((((((((((((π β§
π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β§ π β π) β§ πΆ = (((pInvGβπΊ)βπ)βπ¦)) β§ π§ β π) β§ (π¦ β (ππΌπ§) β§ (π¦ β π§) = (π¦ β π))) β§ π β π) β§ (π¦ β (ππΌπ) β§ (π¦ β π) = (π¦ β π))) β βπ₯ β π΄ (πΆπΏπ₯)(βGβπΊ)π΄) |
208 | 1, 2, 3, 10, 32, 21, 21, 44 | axtgsegcon 27704 |
. . . . . 6
β’
((((((((((π β§
π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β§ π β π) β§ πΆ = (((pInvGβπΊ)βπ)βπ¦)) β§ π§ β π) β§ (π¦ β (ππΌπ§) β§ (π¦ β π§) = (π¦ β π))) β βπ β π (π¦ β (ππΌπ) β§ (π¦ β π) = (π¦ β π))) |
209 | 207, 208 | r19.29a 3162 |
. . . . 5
β’
((((((((((π β§
π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β§ π β π) β§ πΆ = (((pInvGβπΊ)βπ)βπ¦)) β§ π§ β π) β§ (π¦ β (ππΌπ§) β§ (π¦ β π§) = (π¦ β π))) β βπ₯ β π΄ (πΆπΏπ₯)(βGβπΊ)π΄) |
210 | | simplr 767 |
. . . . . 6
β’
((((((((π β§ π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β§ π β π) β§ πΆ = (((pInvGβπΊ)βπ)βπ¦)) β π β π) |
211 | 1, 2, 3, 9, 43, 20, 20, 210 | axtgsegcon 27704 |
. . . . 5
β’
((((((((π β§ π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β§ π β π) β§ πΆ = (((pInvGβπΊ)βπ)βπ¦)) β βπ§ β π (π¦ β (ππΌπ§) β§ (π¦ β π§) = (π¦ β π))) |
212 | 209, 211 | r19.29a 3162 |
. . . 4
β’
((((((((π β§ π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β§ π β π) β§ πΆ = (((pInvGβπΊ)βπ)βπ¦)) β βπ₯ β π΄ (πΆπΏπ₯)(βGβπΊ)π΄) |
213 | | simplr 767 |
. . . . 5
β’
((((((π β§ π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β π¦ β π) |
214 | | simprr 771 |
. . . . 5
β’
((((((π β§ π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β (π β π¦) = (π β πΆ)) |
215 | 1, 2, 3, 4, 5, 8, 66, 213, 16, 42, 214 | midexlem 27932 |
. . . 4
β’
((((((π β§ π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β βπ β π πΆ = (((pInvGβπΊ)βπ)βπ¦)) |
216 | 212, 215 | r19.29a 3162 |
. . 3
β’
((((((π β§ π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β§ π¦ β π) β§ (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) β βπ₯ β π΄ (πΆπΏπ₯)(βGβπΊ)π΄) |
217 | 1, 2, 3, 7, 46, 41, 41, 15 | axtgsegcon 27704 |
. . 3
β’ ((((π β§ π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β βπ¦ β π (π β (ππΌπ¦) β§ (π β π¦) = (π β πΆ))) |
218 | 216, 217 | r19.29a 3162 |
. 2
β’ ((((π β§ π β π) β§ π β π) β§ (π΄ = (ππΏπ) β§ π β π)) β βπ₯ β π΄ (πΆπΏπ₯)(βGβπΊ)π΄) |
219 | 1, 3, 4, 6, 127 | tgisline 27867 |
. 2
β’ (π β βπ β π βπ β π (π΄ = (ππΏπ) β§ π β π)) |
220 | 218, 219 | r19.29vva 3213 |
1
β’ (π β βπ₯ β π΄ (πΆπΏπ₯)(βGβπΊ)π΄) |