Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  colperpexlem3 Structured version   Unicode version

Theorem colperpexlem3 23926
 Description: Lemma for colperpex 23927. Case 1 of theorem 8.21 of [Schwabhauser] p. 63. (Contributed by Thierry Arnoux, 20-Nov-2019.)
Hypotheses
Ref Expression
colperpex.p
colperpex.d
colperpex.i Itv
colperpex.l LineG
colperpex.g TarskiG
colperpex.1
colperpex.2
colperpex.3
colperpex.4
colperpexlem3.1
Assertion
Ref Expression
colperpexlem3 ⟂G
Distinct variable groups:   ,,   ,,   ,,   ,,   ,,   ,,   ,,   ,,   ,,

Proof of Theorem colperpexlem3
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 colperpex.p . . . 4
2 colperpex.d . . . 4
3 colperpex.i . . . 4 Itv
4 colperpex.l . . . 4 LineG
5 eqid 2467 . . . 4 pInvG pInvG
6 colperpex.g . . . . 5 TarskiG
76ad2antrr 725 . . . 4 ⟂G TarskiG
8 eqid 2467 . . . 4 pInvG pInvG
9 colperpex.1 . . . . . . . 8
10 colperpex.2 . . . . . . . 8
11 colperpex.4 . . . . . . . 8
121, 3, 4, 6, 9, 10, 11tgelrnln 23839 . . . . . . 7
1312ad2antrr 725 . . . . . 6 ⟂G
14 simplr 754 . . . . . 6 ⟂G
151, 4, 3, 7, 13, 14tglnpt 23779 . . . . 5 ⟂G
16 eqid 2467 . . . . 5 pInvG pInvG
17 colperpex.3 . . . . . 6
1817ad2antrr 725 . . . . 5 ⟂G
191, 2, 3, 4, 5, 7, 15, 16, 18mircl 23870 . . . 4 ⟂G pInvG
209ad2antrr 725 . . . . 5 ⟂G
21 eqid 2467 . . . . 5 pInvG pInvG
221, 2, 3, 4, 5, 7, 20, 21, 18mircl 23870 . . . 4 ⟂G pInvG
231, 2, 3, 4, 5, 7, 20, 21, 18mircgr 23866 . . . . 5 ⟂G pInvG
2410ad2antrr 725 . . . . . . 7 ⟂G
25 colperpexlem3.1 . . . . . . . . . . . 12
2625ad2antrr 725 . . . . . . . . . . 11 ⟂G
27 nelne2 2797 . . . . . . . . . . 11
2814, 26, 27syl2anc 661 . . . . . . . . . 10 ⟂G
291, 3, 4, 7, 15, 18, 28tglinecom 23844 . . . . . . . . 9 ⟂G
3028necomd 2738 . . . . . . . . . 10 ⟂G
311, 3, 4, 7, 18, 15, 30tgelrnln 23839 . . . . . . . . 9 ⟂G
3229, 31eqeltrd 2555 . . . . . . . 8 ⟂G
33 simpr 461 . . . . . . . . 9 ⟂G ⟂G
3429, 33eqbrtrd 4472 . . . . . . . 8 ⟂G ⟂G
351, 2, 3, 4, 7, 32, 13, 34perpcom 23913 . . . . . . 7 ⟂G ⟂G
361, 2, 3, 4, 7, 20, 24, 14, 18, 35perprag 23920 . . . . . 6 ⟂G ∟G
371, 2, 3, 4, 5, 7, 20, 15, 18israg 23897 . . . . . 6 ⟂G ∟G pInvG
3836, 37mpbid 210 . . . . 5 ⟂G pInvG
3923, 38eqtr2d 2509 . . . 4 ⟂G pInvG pInvG
401, 2, 3, 4, 5, 7, 8, 19, 22, 20, 39midexlem 23892 . . 3 ⟂G pInvG pInvGpInvG
417ad2antrr 725 . . . . . . . 8 ⟂G pInvG pInvGpInvG TarskiG
4222ad2antrr 725 . . . . . . . 8 ⟂G pInvG pInvGpInvG pInvG
4320ad2antrr 725 . . . . . . . 8 ⟂G pInvG pInvGpInvG
4418ad2antrr 725 . . . . . . . 8 ⟂G pInvG pInvGpInvG
4519ad2antrr 725 . . . . . . . 8 ⟂G pInvG pInvGpInvG pInvG
4615ad2antrr 725 . . . . . . . 8 ⟂G pInvG pInvGpInvG
47 simplr 754 . . . . . . . 8 ⟂G pInvG pInvGpInvG
481, 2, 3, 4, 5, 41, 43, 21, 44mirbtwn 23867 . . . . . . . 8 ⟂G pInvG pInvGpInvG pInvG
491, 2, 3, 4, 5, 41, 46, 16, 44mirbtwn 23867 . . . . . . . 8 ⟂G pInvG pInvGpInvG pInvG
501, 2, 3, 4, 5, 41, 47, 8, 45mirbtwn 23867 . . . . . . . . 9 ⟂G pInvG pInvGpInvG pInvGpInvGpInvG
51 simpr 461 . . . . . . . . . . 11 ⟂G pInvG pInvGpInvG pInvG pInvGpInvG
5251eqcomd 2475 . . . . . . . . . 10 ⟂G pInvG pInvGpInvG pInvGpInvG pInvG
5352oveq1d 6309 . . . . . . . . 9 ⟂G pInvG pInvGpInvG pInvGpInvGpInvG pInvGpInvG
5450, 53eleqtrd 2557 . . . . . . . 8 ⟂G pInvG pInvGpInvG pInvGpInvG
551, 2, 3, 41, 42, 43, 44, 45, 46, 47, 48, 49, 54tgtrisegint 23733 . . . . . . 7 ⟂G pInvG pInvGpInvG
5641ad3antrrr 729 . . . . . . . . . . . . . . . 16 ⟂G pInvG pInvGpInvG TarskiG
5743ad3antrrr 729 . . . . . . . . . . . . . . . 16 ⟂G pInvG pInvGpInvG
58 simpllr 758 . . . . . . . . . . . . . . . 16 ⟂G pInvG pInvGpInvG
59 simplrr 760 . . . . . . . . . . . . . . . . 17 ⟂G pInvG pInvGpInvG
60 simpr 461 . . . . . . . . . . . . . . . . . 18 ⟂G pInvG pInvGpInvG
6160oveq2d 6310 . . . . . . . . . . . . . . . . 17 ⟂G pInvG pInvGpInvG
6259, 61eleqtrd 2557 . . . . . . . . . . . . . . . 16 ⟂G pInvG pInvGpInvG
631, 2, 3, 56, 57, 58, 62axtgbtwnid 23706 . . . . . . . . . . . . . . 15 ⟂G pInvG pInvGpInvG
6463eqcomd 2475 . . . . . . . . . . . . . 14 ⟂G pInvG pInvGpInvG
6564oveq1d 6309 . . . . . . . . . . . . 13 ⟂G pInvG pInvGpInvG
6652ad3antrrr 729 . . . . . . . . . . . . . . . . 17 ⟂G pInvG pInvGpInvG pInvGpInvG pInvG
6760fveq2d 5875 . . . . . . . . . . . . . . . . . 18 ⟂G pInvG pInvGpInvG pInvG pInvG
6867fveq1d 5873 . . . . . . . . . . . . . . . . 17 ⟂G pInvG pInvGpInvG pInvG pInvG
6966, 68eqtr4d 2511 . . . . . . . . . . . . . . . 16 ⟂G pInvG pInvGpInvG pInvGpInvG pInvG
7047ad3antrrr 729 . . . . . . . . . . . . . . . . 17 ⟂G pInvG pInvGpInvG
7145ad3antrrr 729 . . . . . . . . . . . . . . . . 17 ⟂G pInvG pInvGpInvG pInvG
721, 2, 3, 4, 5, 56, 70, 8, 71mirinv 23875 . . . . . . . . . . . . . . . 16 ⟂G pInvG pInvGpInvG pInvGpInvG pInvG pInvG
7369, 72mpbid 210 . . . . . . . . . . . . . . 15 ⟂G pInvG pInvGpInvG pInvG
7446ad3antrrr 729 . . . . . . . . . . . . . . . . 17 ⟂G pInvG pInvGpInvG
7560oveq1d 6309 . . . . . . . . . . . . . . . . . 18 ⟂G pInvG pInvGpInvG
7659, 75eleqtrrd 2558 . . . . . . . . . . . . . . . . 17 ⟂G pInvG pInvGpInvG
771, 2, 3, 56, 74, 58, 76axtgbtwnid 23706 . . . . . . . . . . . . . . . 16 ⟂G pInvG pInvGpInvG
7877eqcomd 2475 . . . . . . . . . . . . . . 15 ⟂G pInvG pInvGpInvG
7973, 78oveq12d 6312 . . . . . . . . . . . . . 14 ⟂G pInvG pInvGpInvG pInvG
8036ad2antrr 725 . . . . . . . . . . . . . . . . . 18 ⟂G pInvG pInvGpInvG ∟G
811, 2, 3, 4, 5, 41, 47, 8, 45, 52mircom 23872 . . . . . . . . . . . . . . . . . 18 ⟂G pInvG pInvGpInvG pInvGpInvG pInvG
8228ad2antrr 725 . . . . . . . . . . . . . . . . . 18 ⟂G pInvG pInvGpInvG
831, 2, 3, 4, 41, 5, 21, 16, 8, 43, 46, 44, 47, 80, 81, 82colperpexlem2 23925 . . . . . . . . . . . . . . . . 17 ⟂G pInvG pInvGpInvG
8483ad3antrrr 729 . . . . . . . . . . . . . . . 16 ⟂G pInvG pInvGpInvG
8564, 84eqnetrd 2760 . . . . . . . . . . . . . . 15 ⟂G pInvG pInvGpInvG
861, 3, 4, 56, 58, 70, 85tglinecom 23844 . . . . . . . . . . . . . 14 ⟂G pInvG pInvGpInvG
8744ad3antrrr 729 . . . . . . . . . . . . . . . 16 ⟂G pInvG pInvGpInvG
8882ad3antrrr 729 . . . . . . . . . . . . . . . 16 ⟂G pInvG pInvGpInvG
8956adantr 465 . . . . . . . . . . . . . . . . . . 19 ⟂G pInvG pInvGpInvG pInvG TarskiG
9074adantr 465 . . . . . . . . . . . . . . . . . . 19 ⟂G pInvG pInvGpInvG pInvG
9187adantr 465 . . . . . . . . . . . . . . . . . . 19 ⟂G pInvG pInvGpInvG pInvG
921, 2, 3, 4, 5, 89, 90, 16mircinv 23876 . . . . . . . . . . . . . . . . . . . 20 ⟂G pInvG pInvGpInvG pInvG pInvG
93 simpr 461 . . . . . . . . . . . . . . . . . . . 20 ⟂G pInvG pInvGpInvG pInvG pInvG
9492, 93eqtr4d 2511 . . . . . . . . . . . . . . . . . . 19 ⟂G pInvG pInvGpInvG pInvG pInvG pInvG
951, 2, 3, 4, 5, 89, 90, 16, 90, 91, 94mireq 23874 . . . . . . . . . . . . . . . . . 18 ⟂G pInvG pInvGpInvG pInvG
9688adantr 465 . . . . . . . . . . . . . . . . . . 19 ⟂G pInvG pInvGpInvG pInvG
9796neneqd 2669 . . . . . . . . . . . . . . . . . 18 ⟂G pInvG pInvGpInvG pInvG
9895, 97pm2.65da 576 . . . . . . . . . . . . . . . . 17 ⟂G pInvG pInvGpInvG pInvG
9998neqned 2670 . . . . . . . . . . . . . . . 16 ⟂G pInvG pInvGpInvG pInvG
10049ad3antrrr 729 . . . . . . . . . . . . . . . . 17 ⟂G pInvG pInvGpInvG pInvG
1011, 3, 4, 56, 74, 87, 71, 88, 100btwnlng2 23829 . . . . . . . . . . . . . . . 16 ⟂G pInvG pInvGpInvG pInvG
1021, 3, 4, 56, 74, 87, 88, 71, 99, 101tglineelsb2 23841 . . . . . . . . . . . . . . 15 ⟂G pInvG pInvGpInvG pInvG
10330ad5antr 733 . . . . . . . . . . . . . . . 16 ⟂G pInvG pInvGpInvG
1041, 3, 4, 56, 87, 74, 103tglinecom 23844 . . . . . . . . . . . . . . 15 ⟂G pInvG pInvGpInvG
1051, 3, 4, 56, 71, 74, 99tglinecom 23844 . . . . . . . . . . . . . . 15 ⟂G pInvG pInvGpInvG pInvG pInvG
106102, 104, 1053eqtr4d 2518 . . . . . . . . . . . . . 14 ⟂G pInvG pInvGpInvG pInvG
10779, 86, 1063eqtr4d 2518 . . . . . . . . . . . . 13 ⟂G pInvG pInvGpInvG
10865, 107eqtr3d 2510 . . . . . . . . . . . 12 ⟂G pInvG pInvGpInvG
10933ad5antr 733 . . . . . . . . . . . 12 ⟂G pInvG pInvGpInvG ⟂G
110108, 109eqbrtrd 4472 . . . . . . . . . . 11 ⟂G pInvG pInvGpInvG ⟂G
11141ad3antrrr 729 . . . . . . . . . . . 12 ⟂G pInvG pInvGpInvG TarskiG
11243ad3antrrr 729 . . . . . . . . . . . . 13 ⟂G pInvG pInvGpInvG
11347ad3antrrr 729 . . . . . . . . . . . . 13 ⟂G pInvG pInvGpInvG
11483ad3antrrr 729 . . . . . . . . . . . . 13 ⟂G pInvG pInvGpInvG
1151, 3, 4, 111, 112, 113, 114tgelrnln 23839 . . . . . . . . . . . 12 ⟂G pInvG pInvGpInvG
11613ad5antr 733 . . . . . . . . . . . 12 ⟂G pInvG pInvGpInvG
1171, 3, 4, 111, 112, 113, 114tglinerflx1 23842 . . . . . . . . . . . . 13 ⟂G pInvG pInvGpInvG
11811ad2antrr 725 . . . . . . . . . . . . . . 15 ⟂G
1191, 3, 4, 7, 20, 24, 118tglinerflx1 23842 . . . . . . . . . . . . . 14 ⟂G
120119ad5antr 733 . . . . . . . . . . . . 13 ⟂G pInvG pInvGpInvG
121117, 120elind 3693 . . . . . . . . . . . 12 ⟂G pInvG pInvGpInvG
1221, 3, 4, 111, 112, 113, 114tglinerflx2 23843 . . . . . . . . . . . 12 ⟂G pInvG pInvGpInvG
12314ad5antr 733 . . . . . . . . . . . 12 ⟂G pInvG pInvGpInvG
124114necomd 2738 . . . . . . . . . . . 12 ⟂G pInvG pInvGpInvG
125 simpr 461 . . . . . . . . . . . 12 ⟂G pInvG pInvGpInvG
12646ad3antrrr 729 . . . . . . . . . . . . 13 ⟂G pInvG pInvGpInvG
1271, 2, 3, 4, 41, 5, 21, 16, 8, 43, 46, 44, 47, 80, 81colperpexlem1 23924 . . . . . . . . . . . . . 14 ⟂G pInvG pInvGpInvG ∟G
128127ad3antrrr 729 . . . . . . . . . . . . 13 ⟂G pInvG pInvGpInvG ∟G
1291, 2, 3, 4, 5, 111, 126, 112, 113, 128ragcom 23898 . . . . . . . . . . . 12 ⟂G pInvG pInvGpInvG ∟G
1301, 2, 3, 4, 111, 115, 116, 121, 122, 123, 124, 125, 129ragperp 23917 . . . . . . . . . . 11 ⟂G pInvG pInvGpInvG ⟂G
131110, 130pm2.61dane 2785 . . . . . . . . . 10 ⟂G pInvG pInvGpInvG ⟂G
132119ad5antr 733 . . . . . . . . . . . . 13 ⟂G pInvG pInvGpInvG
13364, 132eqeltrd 2555 . . . . . . . . . . . 12 ⟂G pInvG pInvGpInvG
134133orcd 392 . . . . . . . . . . 11 ⟂G pInvG pInvGpInvG
13524ad5antr 733 . . . . . . . . . . . . 13 ⟂G pInvG pInvGpInvG
136118ad5antr 733 . . . . . . . . . . . . 13 ⟂G pInvG pInvGpInvG
137 simpllr 758 . . . . . . . . . . . . 13 ⟂G pInvG pInvGpInvG
138125necomd 2738 . . . . . . . . . . . . . 14 ⟂G pInvG pInvGpInvG
139 simplrr 760 . . . . . . . . . . . . . 14 ⟂G pInvG pInvGpInvG
1401, 3, 4, 111, 112, 126, 137, 138, 139btwnlng1 23828 . . . . . . . . . . . . 13 ⟂G pInvG pInvGpInvG
1411, 3, 4, 111, 112, 135, 136, 126, 125, 123, 137, 140tglineeltr 23840 . . . . . . . . . . . 12 ⟂G pInvG pInvGpInvG
142141orcd 392 . . . . . . . . . . 11 ⟂G pInvG pInvGpInvG
143134, 142pm2.61dane 2785 . . . . . . . . . 10 ⟂G pInvG pInvGpInvG
14441ad2antrr 725 . . . . . . . . . . 11 ⟂G pInvG pInvGpInvG TarskiG
14547ad2antrr 725 . . . . . . . . . . 11 ⟂G pInvG pInvGpInvG
146 simplr 754 . . . . . . . . . . 11 ⟂G pInvG pInvGpInvG
14744ad2antrr 725 . . . . . . . . . . 11 ⟂G pInvG pInvGpInvG
148 simprl 755 . . . . . . . . . . 11 ⟂G pInvG pInvGpInvG
1491, 2, 3, 144, 145, 146, 147, 148tgbtwncom 23722 . . . . . . . . . 10 ⟂G pInvG pInvGpInvG
150131, 143, 149jca32 535 . . . . . . . . 9 ⟂G pInvG pInvGpInvG ⟂G
151150ex 434 . . . . . . . 8 ⟂G pInvG pInvGpInvG ⟂G
152151reximdva 2942 . . . . . . 7 ⟂G pInvG pInvGpInvG ⟂G
15355, 152mpd 15 . . . . . 6 ⟂G pInvG pInvGpInvG ⟂G
154 r19.42v 3021 . . . . . 6 ⟂G ⟂G
155153, 154sylib 196 . . . . 5 ⟂G pInvG pInvGpInvG ⟂G
156155ex 434 . . . 4 ⟂G pInvG pInvGpInvG ⟂G
157156reximdva 2942 . . 3 ⟂G pInvG pInvGpInvG ⟂G
15840, 157mpd 15 . 2 ⟂G ⟂G
1591, 2, 3, 4, 6, 12, 17, 25footex 23918 . 2 ⟂G
160158, 159r19.29a 3008 1 ⟂G
 Colors of variables: wff setvar class Syntax hints:   wn 3   wi 4   wo 368   wa 369   wceq 1379   wcel 1767   wne 2662  wrex 2818   class class class wbr 4452   crn 5005  cfv 5593  (class class class)co 6294  cs3 12782  cbs 14502  cds 14576  TarskiGcstrkg 23668  Itvcitv 23675  LineGclng 23676  pInvGcmir 23861  ∟Gcrag 23893  ⟂Gcperpg 23895 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-8 1769  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-rep 4563  ax-sep 4573  ax-nul 4581  ax-pow 4630  ax-pr 4691  ax-un 6586  ax-cnex 9558  ax-resscn 9559  ax-1cn 9560  ax-icn 9561  ax-addcl 9562  ax-addrcl 9563  ax-mulcl 9564  ax-mulrcl 9565  ax-mulcom 9566  ax-addass 9567  ax-mulass 9568  ax-distr 9569  ax-i2m1 9570  ax-1ne0 9571  ax-1rid 9572  ax-rnegex 9573  ax-rrecex 9574  ax-cnre 9575  ax-pre-lttri 9576  ax-pre-lttrn 9577  ax-pre-ltadd 9578  ax-pre-mulgt0 9579 This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-nel 2665  df-ral 2822  df-rex 2823  df-reu 2824  df-rmo 2825  df-rab 2826  df-v 3120  df-sbc 3337  df-csb 3441  df-dif 3484  df-un 3486  df-in 3488  df-ss 3495  df-pss 3497  df-nul 3791  df-if 3945  df-pw 4017  df-sn 4033  df-pr 4035  df-tp 4037  df-op 4039  df-uni 4251  df-int 4288  df-iun 4332  df-br 4453  df-opab 4511  df-mpt 4512  df-tr 4546  df-eprel 4796  df-id 4800  df-po 4805  df-so 4806  df-fr 4843  df-we 4845  df-ord 4886  df-on 4887  df-lim 4888  df-suc 4889  df-xp 5010  df-rel 5011  df-cnv 5012  df-co 5013  df-dm 5014  df-rn 5015  df-res 5016  df-ima 5017  df-iota 5556  df-fun 5595  df-fn 5596  df-f 5597  df-f1 5598  df-fo 5599  df-f1o 5600  df-fv 5601  df-riota 6255  df-ov 6297  df-oprab 6298  df-mpt2 6299  df-om 6695  df-1st 6794  df-2nd 6795  df-recs 7052  df-rdg 7086  df-1o 7140  df-oadd 7144  df-er 7321  df-map 7432  df-pm 7433  df-en 7527  df-dom 7528  df-sdom 7529  df-fin 7530  df-card 8330  df-cda 8558  df-pnf 9640  df-mnf 9641  df-xr 9642  df-ltxr 9643  df-le 9644  df-sub 9817  df-neg 9818  df-nn 10547  df-2 10604  df-3 10605  df-n0 10806  df-z 10875  df-uz 11093  df-fz 11683  df-fzo 11803  df-hash 12384  df-word 12518  df-concat 12520  df-s1 12521  df-s2 12788  df-s3 12789  df-trkgc 23687  df-trkgb 23688  df-trkgcb 23689  df-trkg 23693  df-cgrg 23746  df-leg 23812  df-mir 23862  df-rag 23894  df-perpg 23896 This theorem is referenced by:  colperpex  23927
 Copyright terms: Public domain W3C validator