Step | Hyp | Ref
| Expression |
1 | | trgcopy.p |
. 2
β’ π = (BaseβπΊ) |
2 | | trgcopy.m |
. 2
β’ β =
(distβπΊ) |
3 | | trgcopy.i |
. 2
β’ πΌ = (ItvβπΊ) |
4 | | trgcopy.g |
. 2
β’ (π β πΊ β TarskiG) |
5 | | trgcopy.l |
. . 3
β’ πΏ = (LineGβπΊ) |
6 | | trgcopy.b |
. . 3
β’ (π β π΅ β π) |
7 | | trgcopy.c |
. . 3
β’ (π β πΆ β π) |
8 | | trgcopy.a |
. . 3
β’ (π β π΄ β π) |
9 | | trgcopy.1 |
. . 3
β’ (π β Β¬ (π΄ β (π΅πΏπΆ) β¨ π΅ = πΆ)) |
10 | 1, 5, 3, 4, 6, 7, 8, 9 | ncoltgdim2 27805 |
. 2
β’ (π β πΊDimTarskiGβ₯2) |
11 | | eqid 2732 |
. 2
β’
((lInvGβπΊ)β(π·πΏπΈ)) = ((lInvGβπΊ)β(π·πΏπΈ)) |
12 | | trgcopy.d |
. . 3
β’ (π β π· β π) |
13 | | trgcopy.e |
. . 3
β’ (π β πΈ β π) |
14 | | trgcopy.f |
. . . 4
β’ (π β πΉ β π) |
15 | | trgcopy.2 |
. . . 4
β’ (π β Β¬ (π· β (πΈπΏπΉ) β¨ πΈ = πΉ)) |
16 | 1, 3, 5, 4, 12, 13, 14, 15 | ncolne1 27865 |
. . 3
β’ (π β π· β πΈ) |
17 | 1, 3, 5, 4, 12, 13, 16 | tgelrnln 27870 |
. 2
β’ (π β (π·πΏπΈ) β ran πΏ) |
18 | | trgcopyeulem.x |
. 2
β’ (π β π β π) |
19 | | trgcopyeulem.y |
. 2
β’ (π β π β π) |
20 | | eqid 2732 |
. . . . . . . . 9
β’
(pInvGβπΊ) =
(pInvGβπΊ) |
21 | 4 | ad2antrr 724 |
. . . . . . . . 9
β’ (((π β§ π‘ β (π·πΏπΈ)) β§ π‘ β (ππΌ(((lInvGβπΊ)β(π·πΏπΈ))βπ))) β πΊ β TarskiG) |
22 | 17 | ad2antrr 724 |
. . . . . . . . . 10
β’ (((π β§ π‘ β (π·πΏπΈ)) β§ π‘ β (ππΌ(((lInvGβπΊ)β(π·πΏπΈ))βπ))) β (π·πΏπΈ) β ran πΏ) |
23 | | simplr 767 |
. . . . . . . . . 10
β’ (((π β§ π‘ β (π·πΏπΈ)) β§ π‘ β (ππΌ(((lInvGβπΊ)β(π·πΏπΈ))βπ))) β π‘ β (π·πΏπΈ)) |
24 | 1, 5, 3, 21, 22, 23 | tglnpt 27789 |
. . . . . . . . 9
β’ (((π β§ π‘ β (π·πΏπΈ)) β§ π‘ β (ππΌ(((lInvGβπΊ)β(π·πΏπΈ))βπ))) β π‘ β π) |
25 | | eqid 2732 |
. . . . . . . . 9
β’
((pInvGβπΊ)βπ‘) = ((pInvGβπΊ)βπ‘) |
26 | 1, 2, 3, 4, 10, 11, 5, 17, 19 | lmicl 28026 |
. . . . . . . . . 10
β’ (π β (((lInvGβπΊ)β(π·πΏπΈ))βπ) β π) |
27 | 26 | ad2antrr 724 |
. . . . . . . . 9
β’ (((π β§ π‘ β (π·πΏπΈ)) β§ π‘ β (ππΌ(((lInvGβπΊ)β(π·πΏπΈ))βπ))) β (((lInvGβπΊ)β(π·πΏπΈ))βπ) β π) |
28 | 18 | ad2antrr 724 |
. . . . . . . . . . 11
β’ (((π β§ π‘ β (π·πΏπΈ)) β§ π‘ β (ππΌ(((lInvGβπΊ)β(π·πΏπΈ))βπ))) β π β π) |
29 | 12 | ad2antrr 724 |
. . . . . . . . . . . 12
β’ (((π β§ π‘ β (π·πΏπΈ)) β§ π‘ β (ππΌ(((lInvGβπΊ)β(π·πΏπΈ))βπ))) β π· β π) |
30 | 13 | ad2antrr 724 |
. . . . . . . . . . . 12
β’ (((π β§ π‘ β (π·πΏπΈ)) β§ π‘ β (ππΌ(((lInvGβπΊ)β(π·πΏπΈ))βπ))) β πΈ β π) |
31 | | eqid 2732 |
. . . . . . . . . . . 12
β’
(cgrGβπΊ) =
(cgrGβπΊ) |
32 | 16 | ad2antrr 724 |
. . . . . . . . . . . 12
β’ (((π β§ π‘ β (π·πΏπΈ)) β§ π‘ β (ππΌ(((lInvGβπΊ)β(π·πΏπΈ))βπ))) β π· β πΈ) |
33 | 32 | necomd 2996 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π‘ β (π·πΏπΈ)) β§ π‘ β (ππΌ(((lInvGβπΊ)β(π·πΏπΈ))βπ))) β πΈ β π·) |
34 | 1, 3, 5, 21, 30, 29, 24, 33, 23 | lncom 27862 |
. . . . . . . . . . . . . 14
β’ (((π β§ π‘ β (π·πΏπΈ)) β§ π‘ β (ππΌ(((lInvGβπΊ)β(π·πΏπΈ))βπ))) β π‘ β (πΈπΏπ·)) |
35 | 34 | orcd 871 |
. . . . . . . . . . . . 13
β’ (((π β§ π‘ β (π·πΏπΈ)) β§ π‘ β (ππΌ(((lInvGβπΊ)β(π·πΏπΈ))βπ))) β (π‘ β (πΈπΏπ·) β¨ πΈ = π·)) |
36 | 1, 5, 3, 21, 30, 29, 24, 35 | colrot1 27799 |
. . . . . . . . . . . 12
β’ (((π β§ π‘ β (π·πΏπΈ)) β§ π‘ β (ππΌ(((lInvGβπΊ)β(π·πΏπΈ))βπ))) β (πΈ β (π·πΏπ‘) β¨ π· = π‘)) |
37 | | trgcopyeulem.1 |
. . . . . . . . . . . . . . . . 17
β’ (π β β¨βπ΄π΅πΆββ©(cgrGβπΊ)β¨βπ·πΈπββ©) |
38 | 1, 2, 3, 31, 4, 8,
6, 7, 12, 13, 18, 37 | cgr3simp3 27762 |
. . . . . . . . . . . . . . . 16
β’ (π β (πΆ β π΄) = (π β π·)) |
39 | 1, 2, 3, 4, 7, 8, 18, 12, 38 | tgcgrcomlr 27720 |
. . . . . . . . . . . . . . 15
β’ (π β (π΄ β πΆ) = (π· β π)) |
40 | | trgcopyeulem.2 |
. . . . . . . . . . . . . . . . 17
β’ (π β β¨βπ΄π΅πΆββ©(cgrGβπΊ)β¨βπ·πΈπββ©) |
41 | 1, 2, 3, 31, 4, 8,
6, 7, 12, 13, 19, 40 | cgr3simp3 27762 |
. . . . . . . . . . . . . . . 16
β’ (π β (πΆ β π΄) = (π β π·)) |
42 | 1, 2, 3, 4, 7, 8, 19, 12, 41 | tgcgrcomlr 27720 |
. . . . . . . . . . . . . . 15
β’ (π β (π΄ β πΆ) = (π· β π)) |
43 | 39, 42 | eqtr3d 2774 |
. . . . . . . . . . . . . 14
β’ (π β (π· β π) = (π· β π)) |
44 | 1, 2, 3, 4, 10, 11, 5, 17, 12, 19 | lmiiso 28037 |
. . . . . . . . . . . . . 14
β’ (π β ((((lInvGβπΊ)β(π·πΏπΈ))βπ·) β (((lInvGβπΊ)β(π·πΏπΈ))βπ)) = (π· β π)) |
45 | 1, 3, 5, 4, 12, 13, 16 | tglinerflx1 27873 |
. . . . . . . . . . . . . . . 16
β’ (π β π· β (π·πΏπΈ)) |
46 | 1, 2, 3, 4, 10, 11, 5, 17, 12, 45 | lmicinv 28033 |
. . . . . . . . . . . . . . 15
β’ (π β (((lInvGβπΊ)β(π·πΏπΈ))βπ·) = π·) |
47 | 46 | oveq1d 7420 |
. . . . . . . . . . . . . 14
β’ (π β ((((lInvGβπΊ)β(π·πΏπΈ))βπ·) β (((lInvGβπΊ)β(π·πΏπΈ))βπ)) = (π· β (((lInvGβπΊ)β(π·πΏπΈ))βπ))) |
48 | 43, 44, 47 | 3eqtr2d 2778 |
. . . . . . . . . . . . 13
β’ (π β (π· β π) = (π· β (((lInvGβπΊ)β(π·πΏπΈ))βπ))) |
49 | 48 | ad2antrr 724 |
. . . . . . . . . . . 12
β’ (((π β§ π‘ β (π·πΏπΈ)) β§ π‘ β (ππΌ(((lInvGβπΊ)β(π·πΏπΈ))βπ))) β (π· β π) = (π· β (((lInvGβπΊ)β(π·πΏπΈ))βπ))) |
50 | 1, 2, 3, 31, 4, 8,
6, 7, 12, 13, 18, 37 | cgr3simp2 27761 |
. . . . . . . . . . . . . . 15
β’ (π β (π΅ β πΆ) = (πΈ β π)) |
51 | 1, 2, 3, 31, 4, 8,
6, 7, 12, 13, 19, 40 | cgr3simp2 27761 |
. . . . . . . . . . . . . . 15
β’ (π β (π΅ β πΆ) = (πΈ β π)) |
52 | 50, 51 | eqtr3d 2774 |
. . . . . . . . . . . . . 14
β’ (π β (πΈ β π) = (πΈ β π)) |
53 | 1, 2, 3, 4, 10, 11, 5, 17, 13, 19 | lmiiso 28037 |
. . . . . . . . . . . . . 14
β’ (π β ((((lInvGβπΊ)β(π·πΏπΈ))βπΈ) β (((lInvGβπΊ)β(π·πΏπΈ))βπ)) = (πΈ β π)) |
54 | 1, 3, 5, 4, 12, 13, 16 | tglinerflx2 27874 |
. . . . . . . . . . . . . . . 16
β’ (π β πΈ β (π·πΏπΈ)) |
55 | 1, 2, 3, 4, 10, 11, 5, 17, 13, 54 | lmicinv 28033 |
. . . . . . . . . . . . . . 15
β’ (π β (((lInvGβπΊ)β(π·πΏπΈ))βπΈ) = πΈ) |
56 | 55 | oveq1d 7420 |
. . . . . . . . . . . . . 14
β’ (π β ((((lInvGβπΊ)β(π·πΏπΈ))βπΈ) β (((lInvGβπΊ)β(π·πΏπΈ))βπ)) = (πΈ β (((lInvGβπΊ)β(π·πΏπΈ))βπ))) |
57 | 52, 53, 56 | 3eqtr2d 2778 |
. . . . . . . . . . . . 13
β’ (π β (πΈ β π) = (πΈ β (((lInvGβπΊ)β(π·πΏπΈ))βπ))) |
58 | 57 | ad2antrr 724 |
. . . . . . . . . . . 12
β’ (((π β§ π‘ β (π·πΏπΈ)) β§ π‘ β (ππΌ(((lInvGβπΊ)β(π·πΏπΈ))βπ))) β (πΈ β π) = (πΈ β (((lInvGβπΊ)β(π·πΏπΈ))βπ))) |
59 | 1, 5, 3, 21, 29, 30, 24, 31, 28, 27, 2, 32, 36, 49, 58 | lncgr 27809 |
. . . . . . . . . . 11
β’ (((π β§ π‘ β (π·πΏπΈ)) β§ π‘ β (ππΌ(((lInvGβπΊ)β(π·πΏπΈ))βπ))) β (π‘ β π) = (π‘ β (((lInvGβπΊ)β(π·πΏπΈ))βπ))) |
60 | | simpr 485 |
. . . . . . . . . . 11
β’ (((π β§ π‘ β (π·πΏπΈ)) β§ π‘ β (ππΌ(((lInvGβπΊ)β(π·πΏπΈ))βπ))) β π‘ β (ππΌ(((lInvGβπΊ)β(π·πΏπΈ))βπ))) |
61 | 1, 2, 3, 5, 20, 21, 24, 25, 27, 28, 59, 60 | ismir 27899 |
. . . . . . . . . 10
β’ (((π β§ π‘ β (π·πΏπΈ)) β§ π‘ β (ππΌ(((lInvGβπΊ)β(π·πΏπΈ))βπ))) β π = (((pInvGβπΊ)βπ‘)β(((lInvGβπΊ)β(π·πΏπΈ))βπ))) |
62 | 61 | eqcomd 2738 |
. . . . . . . . 9
β’ (((π β§ π‘ β (π·πΏπΈ)) β§ π‘ β (ππΌ(((lInvGβπΊ)β(π·πΏπΈ))βπ))) β (((pInvGβπΊ)βπ‘)β(((lInvGβπΊ)β(π·πΏπΈ))βπ)) = π) |
63 | 1, 2, 3, 5, 20, 21, 24, 25, 27, 62 | mircom 27903 |
. . . . . . . 8
β’ (((π β§ π‘ β (π·πΏπΈ)) β§ π‘ β (ππΌ(((lInvGβπΊ)β(π·πΏπΈ))βπ))) β (((pInvGβπΊ)βπ‘)βπ) = (((lInvGβπΊ)β(π·πΏπΈ))βπ)) |
64 | 63 | eqcomd 2738 |
. . . . . . 7
β’ (((π β§ π‘ β (π·πΏπΈ)) β§ π‘ β (ππΌ(((lInvGβπΊ)β(π·πΏπΈ))βπ))) β (((lInvGβπΊ)β(π·πΏπΈ))βπ) = (((pInvGβπΊ)βπ‘)βπ)) |
65 | 10 | ad2antrr 724 |
. . . . . . . 8
β’ (((π β§ π‘ β (π·πΏπΈ)) β§ π‘ β (ππΌ(((lInvGβπΊ)β(π·πΏπΈ))βπ))) β πΊDimTarskiGβ₯2) |
66 | 1, 2, 3, 21, 65, 28, 27, 20, 24 | ismidb 28018 |
. . . . . . 7
β’ (((π β§ π‘ β (π·πΏπΈ)) β§ π‘ β (ππΌ(((lInvGβπΊ)β(π·πΏπΈ))βπ))) β ((((lInvGβπΊ)β(π·πΏπΈ))βπ) = (((pInvGβπΊ)βπ‘)βπ) β (π(midGβπΊ)(((lInvGβπΊ)β(π·πΏπΈ))βπ)) = π‘)) |
67 | 64, 66 | mpbid 231 |
. . . . . 6
β’ (((π β§ π‘ β (π·πΏπΈ)) β§ π‘ β (ππΌ(((lInvGβπΊ)β(π·πΏπΈ))βπ))) β (π(midGβπΊ)(((lInvGβπΊ)β(π·πΏπΈ))βπ)) = π‘) |
68 | 67, 23 | eqeltrd 2833 |
. . . . 5
β’ (((π β§ π‘ β (π·πΏπΈ)) β§ π‘ β (ππΌ(((lInvGβπΊ)β(π·πΏπΈ))βπ))) β (π(midGβπΊ)(((lInvGβπΊ)β(π·πΏπΈ))βπ)) β (π·πΏπΈ)) |
69 | | trgcopyeulem.o |
. . . . . . . . 9
β’ π = {β¨π, πβ© β£ ((π β (π β (π·πΏπΈ)) β§ π β (π β (π·πΏπΈ))) β§ βπ‘ β (π·πΏπΈ)π‘ β (ππΌπ))} |
70 | | trgcopyeulem.4 |
. . . . . . . . 9
β’ (π β π((hpGβπΊ)β(π·πΏπΈ))πΉ) |
71 | | trgcopyeulem.3 |
. . . . . . . . . 10
β’ (π β π((hpGβπΊ)β(π·πΏπΈ))πΉ) |
72 | 1, 3, 5, 4, 17, 18, 69, 14, 71 | hpgcom 28007 |
. . . . . . . . 9
β’ (π β πΉ((hpGβπΊ)β(π·πΏπΈ))π) |
73 | 1, 3, 5, 4, 17, 19, 69, 14, 70, 18, 72 | hpgtr 28008 |
. . . . . . . 8
β’ (π β π((hpGβπΊ)β(π·πΏπΈ))π) |
74 | 1, 3, 5, 69, 4, 17, 19, 14, 70 | hpgne1 28001 |
. . . . . . . . . 10
β’ (π β Β¬ π β (π·πΏπΈ)) |
75 | 1, 2, 3, 5, 4, 10,
17, 69, 11, 19, 74 | lmiopp 28042 |
. . . . . . . . 9
β’ (π β ππ(((lInvGβπΊ)β(π·πΏπΈ))βπ)) |
76 | 1, 3, 5, 69, 4, 17, 19, 18, 26, 75 | lnopp2hpgb 28003 |
. . . . . . . 8
β’ (π β (ππ(((lInvGβπΊ)β(π·πΏπΈ))βπ) β π((hpGβπΊ)β(π·πΏπΈ))π)) |
77 | 73, 76 | mpbird 256 |
. . . . . . 7
β’ (π β ππ(((lInvGβπΊ)β(π·πΏπΈ))βπ)) |
78 | 1, 2, 3, 69, 18, 26 | islnopp 27979 |
. . . . . . 7
β’ (π β (ππ(((lInvGβπΊ)β(π·πΏπΈ))βπ) β ((Β¬ π β (π·πΏπΈ) β§ Β¬ (((lInvGβπΊ)β(π·πΏπΈ))βπ) β (π·πΏπΈ)) β§ βπ‘ β (π·πΏπΈ)π‘ β (ππΌ(((lInvGβπΊ)β(π·πΏπΈ))βπ))))) |
79 | 77, 78 | mpbid 231 |
. . . . . 6
β’ (π β ((Β¬ π β (π·πΏπΈ) β§ Β¬ (((lInvGβπΊ)β(π·πΏπΈ))βπ) β (π·πΏπΈ)) β§ βπ‘ β (π·πΏπΈ)π‘ β (ππΌ(((lInvGβπΊ)β(π·πΏπΈ))βπ)))) |
80 | 79 | simprd 496 |
. . . . 5
β’ (π β βπ‘ β (π·πΏπΈ)π‘ β (ππΌ(((lInvGβπΊ)β(π·πΏπΈ))βπ))) |
81 | 68, 80 | r19.29a 3162 |
. . . 4
β’ (π β (π(midGβπΊ)(((lInvGβπΊ)β(π·πΏπΈ))βπ)) β (π·πΏπΈ)) |
82 | 21 | adantr 481 |
. . . . . . . 8
β’ ((((π β§ π‘ β (π·πΏπΈ)) β§ π‘ β (ππΌ(((lInvGβπΊ)β(π·πΏπΈ))βπ))) β§ πΈ β π‘) β πΊ β TarskiG) |
83 | 22 | adantr 481 |
. . . . . . . 8
β’ ((((π β§ π‘ β (π·πΏπΈ)) β§ π‘ β (ππΌ(((lInvGβπΊ)β(π·πΏπΈ))βπ))) β§ πΈ β π‘) β (π·πΏπΈ) β ran πΏ) |
84 | 1, 2, 3, 69, 5, 17, 4, 18, 26, 77 | oppne3 27983 |
. . . . . . . . . . 11
β’ (π β π β (((lInvGβπΊ)β(π·πΏπΈ))βπ)) |
85 | 1, 3, 5, 4, 18, 26, 84 | tgelrnln 27870 |
. . . . . . . . . 10
β’ (π β (ππΏ(((lInvGβπΊ)β(π·πΏπΈ))βπ)) β ran πΏ) |
86 | 85 | ad2antrr 724 |
. . . . . . . . 9
β’ (((π β§ π‘ β (π·πΏπΈ)) β§ π‘ β (ππΌ(((lInvGβπΊ)β(π·πΏπΈ))βπ))) β (ππΏ(((lInvGβπΊ)β(π·πΏπΈ))βπ)) β ran πΏ) |
87 | 86 | adantr 481 |
. . . . . . . 8
β’ ((((π β§ π‘ β (π·πΏπΈ)) β§ π‘ β (ππΌ(((lInvGβπΊ)β(π·πΏπΈ))βπ))) β§ πΈ β π‘) β (ππΏ(((lInvGβπΊ)β(π·πΏπΈ))βπ)) β ran πΏ) |
88 | 84 | ad2antrr 724 |
. . . . . . . . . . 11
β’ (((π β§ π‘ β (π·πΏπΈ)) β§ π‘ β (ππΌ(((lInvGβπΊ)β(π·πΏπΈ))βπ))) β π β (((lInvGβπΊ)β(π·πΏπΈ))βπ)) |
89 | 1, 3, 5, 21, 28, 27, 24, 88, 60 | btwnlng1 27859 |
. . . . . . . . . 10
β’ (((π β§ π‘ β (π·πΏπΈ)) β§ π‘ β (ππΌ(((lInvGβπΊ)β(π·πΏπΈ))βπ))) β π‘ β (ππΏ(((lInvGβπΊ)β(π·πΏπΈ))βπ))) |
90 | 23, 89 | elind 4193 |
. . . . . . . . 9
β’ (((π β§ π‘ β (π·πΏπΈ)) β§ π‘ β (ππΌ(((lInvGβπΊ)β(π·πΏπΈ))βπ))) β π‘ β ((π·πΏπΈ) β© (ππΏ(((lInvGβπΊ)β(π·πΏπΈ))βπ)))) |
91 | 90 | adantr 481 |
. . . . . . . 8
β’ ((((π β§ π‘ β (π·πΏπΈ)) β§ π‘ β (ππΌ(((lInvGβπΊ)β(π·πΏπΈ))βπ))) β§ πΈ β π‘) β π‘ β ((π·πΏπΈ) β© (ππΏ(((lInvGβπΊ)β(π·πΏπΈ))βπ)))) |
92 | 54 | ad3antrrr 728 |
. . . . . . . 8
β’ ((((π β§ π‘ β (π·πΏπΈ)) β§ π‘ β (ππΌ(((lInvGβπΊ)β(π·πΏπΈ))βπ))) β§ πΈ β π‘) β πΈ β (π·πΏπΈ)) |
93 | 1, 3, 5, 4, 18, 26, 84 | tglinerflx1 27873 |
. . . . . . . . 9
β’ (π β π β (ππΏ(((lInvGβπΊ)β(π·πΏπΈ))βπ))) |
94 | 93 | ad3antrrr 728 |
. . . . . . . 8
β’ ((((π β§ π‘ β (π·πΏπΈ)) β§ π‘ β (ππΌ(((lInvGβπΊ)β(π·πΏπΈ))βπ))) β§ πΈ β π‘) β π β (ππΏ(((lInvGβπΊ)β(π·πΏπΈ))βπ))) |
95 | | simpr 485 |
. . . . . . . 8
β’ ((((π β§ π‘ β (π·πΏπΈ)) β§ π‘ β (ππΌ(((lInvGβπΊ)β(π·πΏπΈ))βπ))) β§ πΈ β π‘) β πΈ β π‘) |
96 | 79 | simplld 766 |
. . . . . . . . . . . 12
β’ (π β Β¬ π β (π·πΏπΈ)) |
97 | 96 | ad2antrr 724 |
. . . . . . . . . . 11
β’ (((π β§ π‘ β (π·πΏπΈ)) β§ π‘ β (ππΌ(((lInvGβπΊ)β(π·πΏπΈ))βπ))) β Β¬ π β (π·πΏπΈ)) |
98 | | nelne2 3040 |
. . . . . . . . . . 11
β’ ((π‘ β (π·πΏπΈ) β§ Β¬ π β (π·πΏπΈ)) β π‘ β π) |
99 | 23, 97, 98 | syl2anc 584 |
. . . . . . . . . 10
β’ (((π β§ π‘ β (π·πΏπΈ)) β§ π‘ β (ππΌ(((lInvGβπΊ)β(π·πΏπΈ))βπ))) β π‘ β π) |
100 | 99 | necomd 2996 |
. . . . . . . . 9
β’ (((π β§ π‘ β (π·πΏπΈ)) β§ π‘ β (ππΌ(((lInvGβπΊ)β(π·πΏπΈ))βπ))) β π β π‘) |
101 | 100 | adantr 481 |
. . . . . . . 8
β’ ((((π β§ π‘ β (π·πΏπΈ)) β§ π‘ β (ππΌ(((lInvGβπΊ)β(π·πΏπΈ))βπ))) β§ πΈ β π‘) β π β π‘) |
102 | 64 | oveq2d 7421 |
. . . . . . . . . . 11
β’ (((π β§ π‘ β (π·πΏπΈ)) β§ π‘ β (ππΌ(((lInvGβπΊ)β(π·πΏπΈ))βπ))) β (πΈ β (((lInvGβπΊ)β(π·πΏπΈ))βπ)) = (πΈ β (((pInvGβπΊ)βπ‘)βπ))) |
103 | 58, 102 | eqtrd 2772 |
. . . . . . . . . 10
β’ (((π β§ π‘ β (π·πΏπΈ)) β§ π‘ β (ππΌ(((lInvGβπΊ)β(π·πΏπΈ))βπ))) β (πΈ β π) = (πΈ β (((pInvGβπΊ)βπ‘)βπ))) |
104 | 103 | adantr 481 |
. . . . . . . . 9
β’ ((((π β§ π‘ β (π·πΏπΈ)) β§ π‘ β (ππΌ(((lInvGβπΊ)β(π·πΏπΈ))βπ))) β§ πΈ β π‘) β (πΈ β π) = (πΈ β (((pInvGβπΊ)βπ‘)βπ))) |
105 | 30 | adantr 481 |
. . . . . . . . . 10
β’ ((((π β§ π‘ β (π·πΏπΈ)) β§ π‘ β (ππΌ(((lInvGβπΊ)β(π·πΏπΈ))βπ))) β§ πΈ β π‘) β πΈ β π) |
106 | 24 | adantr 481 |
. . . . . . . . . 10
β’ ((((π β§ π‘ β (π·πΏπΈ)) β§ π‘ β (ππΌ(((lInvGβπΊ)β(π·πΏπΈ))βπ))) β§ πΈ β π‘) β π‘ β π) |
107 | 28 | adantr 481 |
. . . . . . . . . 10
β’ ((((π β§ π‘ β (π·πΏπΈ)) β§ π‘ β (ππΌ(((lInvGβπΊ)β(π·πΏπΈ))βπ))) β§ πΈ β π‘) β π β π) |
108 | 1, 2, 3, 5, 20, 82, 105, 106, 107 | israg 27937 |
. . . . . . . . 9
β’ ((((π β§ π‘ β (π·πΏπΈ)) β§ π‘ β (ππΌ(((lInvGβπΊ)β(π·πΏπΈ))βπ))) β§ πΈ β π‘) β (β¨βπΈπ‘πββ© β (βGβπΊ) β (πΈ β π) = (πΈ β (((pInvGβπΊ)βπ‘)βπ)))) |
109 | 104, 108 | mpbird 256 |
. . . . . . . 8
β’ ((((π β§ π‘ β (π·πΏπΈ)) β§ π‘ β (ππΌ(((lInvGβπΊ)β(π·πΏπΈ))βπ))) β§ πΈ β π‘) β β¨βπΈπ‘πββ© β (βGβπΊ)) |
110 | 1, 2, 3, 5, 82, 83, 87, 91, 92, 94, 95, 101, 109 | ragperp 27957 |
. . . . . . 7
β’ ((((π β§ π‘ β (π·πΏπΈ)) β§ π‘ β (ππΌ(((lInvGβπΊ)β(π·πΏπΈ))βπ))) β§ πΈ β π‘) β (π·πΏπΈ)(βGβπΊ)(ππΏ(((lInvGβπΊ)β(π·πΏπΈ))βπ))) |
111 | 21 | adantr 481 |
. . . . . . . 8
β’ ((((π β§ π‘ β (π·πΏπΈ)) β§ π‘ β (ππΌ(((lInvGβπΊ)β(π·πΏπΈ))βπ))) β§ π· β π‘) β πΊ β TarskiG) |
112 | 22 | adantr 481 |
. . . . . . . 8
β’ ((((π β§ π‘ β (π·πΏπΈ)) β§ π‘ β (ππΌ(((lInvGβπΊ)β(π·πΏπΈ))βπ))) β§ π· β π‘) β (π·πΏπΈ) β ran πΏ) |
113 | 86 | adantr 481 |
. . . . . . . 8
β’ ((((π β§ π‘ β (π·πΏπΈ)) β§ π‘ β (ππΌ(((lInvGβπΊ)β(π·πΏπΈ))βπ))) β§ π· β π‘) β (ππΏ(((lInvGβπΊ)β(π·πΏπΈ))βπ)) β ran πΏ) |
114 | 90 | adantr 481 |
. . . . . . . 8
β’ ((((π β§ π‘ β (π·πΏπΈ)) β§ π‘ β (ππΌ(((lInvGβπΊ)β(π·πΏπΈ))βπ))) β§ π· β π‘) β π‘ β ((π·πΏπΈ) β© (ππΏ(((lInvGβπΊ)β(π·πΏπΈ))βπ)))) |
115 | 45 | ad3antrrr 728 |
. . . . . . . 8
β’ ((((π β§ π‘ β (π·πΏπΈ)) β§ π‘ β (ππΌ(((lInvGβπΊ)β(π·πΏπΈ))βπ))) β§ π· β π‘) β π· β (π·πΏπΈ)) |
116 | 93 | ad3antrrr 728 |
. . . . . . . 8
β’ ((((π β§ π‘ β (π·πΏπΈ)) β§ π‘ β (ππΌ(((lInvGβπΊ)β(π·πΏπΈ))βπ))) β§ π· β π‘) β π β (ππΏ(((lInvGβπΊ)β(π·πΏπΈ))βπ))) |
117 | | simpr 485 |
. . . . . . . 8
β’ ((((π β§ π‘ β (π·πΏπΈ)) β§ π‘ β (ππΌ(((lInvGβπΊ)β(π·πΏπΈ))βπ))) β§ π· β π‘) β π· β π‘) |
118 | 100 | adantr 481 |
. . . . . . . 8
β’ ((((π β§ π‘ β (π·πΏπΈ)) β§ π‘ β (ππΌ(((lInvGβπΊ)β(π·πΏπΈ))βπ))) β§ π· β π‘) β π β π‘) |
119 | 64 | oveq2d 7421 |
. . . . . . . . . . 11
β’ (((π β§ π‘ β (π·πΏπΈ)) β§ π‘ β (ππΌ(((lInvGβπΊ)β(π·πΏπΈ))βπ))) β (π· β (((lInvGβπΊ)β(π·πΏπΈ))βπ)) = (π· β (((pInvGβπΊ)βπ‘)βπ))) |
120 | 49, 119 | eqtrd 2772 |
. . . . . . . . . 10
β’ (((π β§ π‘ β (π·πΏπΈ)) β§ π‘ β (ππΌ(((lInvGβπΊ)β(π·πΏπΈ))βπ))) β (π· β π) = (π· β (((pInvGβπΊ)βπ‘)βπ))) |
121 | 120 | adantr 481 |
. . . . . . . . 9
β’ ((((π β§ π‘ β (π·πΏπΈ)) β§ π‘ β (ππΌ(((lInvGβπΊ)β(π·πΏπΈ))βπ))) β§ π· β π‘) β (π· β π) = (π· β (((pInvGβπΊ)βπ‘)βπ))) |
122 | 29 | adantr 481 |
. . . . . . . . . 10
β’ ((((π β§ π‘ β (π·πΏπΈ)) β§ π‘ β (ππΌ(((lInvGβπΊ)β(π·πΏπΈ))βπ))) β§ π· β π‘) β π· β π) |
123 | 24 | adantr 481 |
. . . . . . . . . 10
β’ ((((π β§ π‘ β (π·πΏπΈ)) β§ π‘ β (ππΌ(((lInvGβπΊ)β(π·πΏπΈ))βπ))) β§ π· β π‘) β π‘ β π) |
124 | 28 | adantr 481 |
. . . . . . . . . 10
β’ ((((π β§ π‘ β (π·πΏπΈ)) β§ π‘ β (ππΌ(((lInvGβπΊ)β(π·πΏπΈ))βπ))) β§ π· β π‘) β π β π) |
125 | 1, 2, 3, 5, 20, 111, 122, 123, 124 | israg 27937 |
. . . . . . . . 9
β’ ((((π β§ π‘ β (π·πΏπΈ)) β§ π‘ β (ππΌ(((lInvGβπΊ)β(π·πΏπΈ))βπ))) β§ π· β π‘) β (β¨βπ·π‘πββ© β (βGβπΊ) β (π· β π) = (π· β (((pInvGβπΊ)βπ‘)βπ)))) |
126 | 121, 125 | mpbird 256 |
. . . . . . . 8
β’ ((((π β§ π‘ β (π·πΏπΈ)) β§ π‘ β (ππΌ(((lInvGβπΊ)β(π·πΏπΈ))βπ))) β§ π· β π‘) β β¨βπ·π‘πββ© β (βGβπΊ)) |
127 | 1, 2, 3, 5, 111, 112, 113, 114, 115, 116, 117, 118, 126 | ragperp 27957 |
. . . . . . 7
β’ ((((π β§ π‘ β (π·πΏπΈ)) β§ π‘ β (ππΌ(((lInvGβπΊ)β(π·πΏπΈ))βπ))) β§ π· β π‘) β (π·πΏπΈ)(βGβπΊ)(ππΏ(((lInvGβπΊ)β(π·πΏπΈ))βπ))) |
128 | | neneor 3042 |
. . . . . . . 8
β’ (πΈ β π· β (πΈ β π‘ β¨ π· β π‘)) |
129 | 33, 128 | syl 17 |
. . . . . . 7
β’ (((π β§ π‘ β (π·πΏπΈ)) β§ π‘ β (ππΌ(((lInvGβπΊ)β(π·πΏπΈ))βπ))) β (πΈ β π‘ β¨ π· β π‘)) |
130 | 110, 127,
129 | mpjaodan 957 |
. . . . . 6
β’ (((π β§ π‘ β (π·πΏπΈ)) β§ π‘ β (ππΌ(((lInvGβπΊ)β(π·πΏπΈ))βπ))) β (π·πΏπΈ)(βGβπΊ)(ππΏ(((lInvGβπΊ)β(π·πΏπΈ))βπ))) |
131 | 130 | orcd 871 |
. . . . 5
β’ (((π β§ π‘ β (π·πΏπΈ)) β§ π‘ β (ππΌ(((lInvGβπΊ)β(π·πΏπΈ))βπ))) β ((π·πΏπΈ)(βGβπΊ)(ππΏ(((lInvGβπΊ)β(π·πΏπΈ))βπ)) β¨ π = (((lInvGβπΊ)β(π·πΏπΈ))βπ))) |
132 | 131, 80 | r19.29a 3162 |
. . . 4
β’ (π β ((π·πΏπΈ)(βGβπΊ)(ππΏ(((lInvGβπΊ)β(π·πΏπΈ))βπ)) β¨ π = (((lInvGβπΊ)β(π·πΏπΈ))βπ))) |
133 | 1, 2, 3, 4, 10, 11, 5, 17, 18, 26 | islmib 28027 |
. . . 4
β’ (π β ((((lInvGβπΊ)β(π·πΏπΈ))βπ) = (((lInvGβπΊ)β(π·πΏπΈ))βπ) β ((π(midGβπΊ)(((lInvGβπΊ)β(π·πΏπΈ))βπ)) β (π·πΏπΈ) β§ ((π·πΏπΈ)(βGβπΊ)(ππΏ(((lInvGβπΊ)β(π·πΏπΈ))βπ)) β¨ π = (((lInvGβπΊ)β(π·πΏπΈ))βπ))))) |
134 | 81, 132, 133 | mpbir2and 711 |
. . 3
β’ (π β (((lInvGβπΊ)β(π·πΏπΈ))βπ) = (((lInvGβπΊ)β(π·πΏπΈ))βπ)) |
135 | 134 | eqcomd 2738 |
. 2
β’ (π β (((lInvGβπΊ)β(π·πΏπΈ))βπ) = (((lInvGβπΊ)β(π·πΏπΈ))βπ)) |
136 | 1, 2, 3, 4, 10, 11, 5, 17, 18, 19, 135 | lmieq 28031 |
1
β’ (π β π = π) |