Metamath Proof Explorer


Theorem colperpexlem3

Description: Lemma for colperpex . Case 1 of theorem 8.21 of Schwabhauser p. 63. (Contributed by Thierry Arnoux, 20-Nov-2019)

Ref Expression
Hypotheses colperpex.p P=BaseG
colperpex.d -˙=distG
colperpex.i I=ItvG
colperpex.l L=Line𝒢G
colperpex.g φG𝒢Tarski
colperpex.1 φAP
colperpex.2 φBP
colperpex.3 φCP
colperpex.4 φAB
colperpexlem3.1 φ¬CALB
Assertion colperpexlem3 φpPALp𝒢GALBtPtALBA=BtCIp

Proof

Step Hyp Ref Expression
1 colperpex.p P=BaseG
2 colperpex.d -˙=distG
3 colperpex.i I=ItvG
4 colperpex.l L=Line𝒢G
5 colperpex.g φG𝒢Tarski
6 colperpex.1 φAP
7 colperpex.2 φBP
8 colperpex.3 φCP
9 colperpex.4 φAB
10 colperpexlem3.1 φ¬CALB
11 eqid pInv𝒢G=pInv𝒢G
12 5 ad2antrr φxALBCLx𝒢GALBG𝒢Tarski
13 eqid pInv𝒢Gp=pInv𝒢Gp
14 1 3 4 5 6 7 9 tgelrnln φALBranL
15 14 ad2antrr φxALBCLx𝒢GALBALBranL
16 simplr φxALBCLx𝒢GALBxALB
17 1 4 3 12 15 16 tglnpt φxALBCLx𝒢GALBxP
18 eqid pInv𝒢Gx=pInv𝒢Gx
19 8 ad2antrr φxALBCLx𝒢GALBCP
20 1 2 3 4 11 12 17 18 19 mircl φxALBCLx𝒢GALBpInv𝒢GxCP
21 6 ad2antrr φxALBCLx𝒢GALBAP
22 eqid pInv𝒢GA=pInv𝒢GA
23 1 2 3 4 11 12 21 22 19 mircl φxALBCLx𝒢GALBpInv𝒢GACP
24 1 2 3 4 11 12 21 22 19 mircgr φxALBCLx𝒢GALBA-˙pInv𝒢GAC=A-˙C
25 7 ad2antrr φxALBCLx𝒢GALBBP
26 10 ad2antrr φxALBCLx𝒢GALB¬CALB
27 nelne2 xALB¬CALBxC
28 16 26 27 syl2anc φxALBCLx𝒢GALBxC
29 1 3 4 12 17 19 28 tgelrnln φxALBCLx𝒢GALBxLCranL
30 1 3 4 12 17 19 28 tglinecom φxALBCLx𝒢GALBxLC=CLx
31 simpr φxALBCLx𝒢GALBCLx𝒢GALB
32 30 31 eqbrtrd φxALBCLx𝒢GALBxLC𝒢GALB
33 1 2 3 4 12 29 15 32 perpcom φxALBCLx𝒢GALBALB𝒢GxLC
34 1 2 3 4 12 21 25 16 19 33 perprag φxALBCLx𝒢GALB⟨“AxC”⟩𝒢G
35 1 2 3 4 11 12 21 17 19 israg φxALBCLx𝒢GALB⟨“AxC”⟩𝒢GA-˙C=A-˙pInv𝒢GxC
36 34 35 mpbid φxALBCLx𝒢GALBA-˙C=A-˙pInv𝒢GxC
37 24 36 eqtr2d φxALBCLx𝒢GALBA-˙pInv𝒢GxC=A-˙pInv𝒢GAC
38 1 2 3 4 11 12 13 20 23 21 37 midexlem φxALBCLx𝒢GALBpPpInv𝒢GAC=pInv𝒢GppInv𝒢GxC
39 12 ad2antrr φxALBCLx𝒢GALBpPpInv𝒢GAC=pInv𝒢GppInv𝒢GxCG𝒢Tarski
40 23 ad2antrr φxALBCLx𝒢GALBpPpInv𝒢GAC=pInv𝒢GppInv𝒢GxCpInv𝒢GACP
41 21 ad2antrr φxALBCLx𝒢GALBpPpInv𝒢GAC=pInv𝒢GppInv𝒢GxCAP
42 19 ad2antrr φxALBCLx𝒢GALBpPpInv𝒢GAC=pInv𝒢GppInv𝒢GxCCP
43 20 ad2antrr φxALBCLx𝒢GALBpPpInv𝒢GAC=pInv𝒢GppInv𝒢GxCpInv𝒢GxCP
44 17 ad2antrr φxALBCLx𝒢GALBpPpInv𝒢GAC=pInv𝒢GppInv𝒢GxCxP
45 simplr φxALBCLx𝒢GALBpPpInv𝒢GAC=pInv𝒢GppInv𝒢GxCpP
46 1 2 3 4 11 39 41 22 42 mirbtwn φxALBCLx𝒢GALBpPpInv𝒢GAC=pInv𝒢GppInv𝒢GxCApInv𝒢GACIC
47 1 2 3 4 11 39 44 18 42 mirbtwn φxALBCLx𝒢GALBpPpInv𝒢GAC=pInv𝒢GppInv𝒢GxCxpInv𝒢GxCIC
48 1 2 3 4 11 39 45 13 43 mirbtwn φxALBCLx𝒢GALBpPpInv𝒢GAC=pInv𝒢GppInv𝒢GxCppInv𝒢GppInv𝒢GxCIpInv𝒢GxC
49 simpr φxALBCLx𝒢GALBpPpInv𝒢GAC=pInv𝒢GppInv𝒢GxCpInv𝒢GAC=pInv𝒢GppInv𝒢GxC
50 49 eqcomd φxALBCLx𝒢GALBpPpInv𝒢GAC=pInv𝒢GppInv𝒢GxCpInv𝒢GppInv𝒢GxC=pInv𝒢GAC
51 50 oveq1d φxALBCLx𝒢GALBpPpInv𝒢GAC=pInv𝒢GppInv𝒢GxCpInv𝒢GppInv𝒢GxCIpInv𝒢GxC=pInv𝒢GACIpInv𝒢GxC
52 48 51 eleqtrd φxALBCLx𝒢GALBpPpInv𝒢GAC=pInv𝒢GppInv𝒢GxCppInv𝒢GACIpInv𝒢GxC
53 1 2 3 39 40 41 42 43 44 45 46 47 52 tgtrisegint φxALBCLx𝒢GALBpPpInv𝒢GAC=pInv𝒢GppInv𝒢GxCtPtpICtAIx
54 39 ad3antrrr φxALBCLx𝒢GALBpPpInv𝒢GAC=pInv𝒢GppInv𝒢GxCtPtpICtAIxx=AG𝒢Tarski
55 41 ad3antrrr φxALBCLx𝒢GALBpPpInv𝒢GAC=pInv𝒢GppInv𝒢GxCtPtpICtAIxx=AAP
56 simpllr φxALBCLx𝒢GALBpPpInv𝒢GAC=pInv𝒢GppInv𝒢GxCtPtpICtAIxx=AtP
57 simplrr φxALBCLx𝒢GALBpPpInv𝒢GAC=pInv𝒢GppInv𝒢GxCtPtpICtAIxx=AtAIx
58 simpr φxALBCLx𝒢GALBpPpInv𝒢GAC=pInv𝒢GppInv𝒢GxCtPtpICtAIxx=Ax=A
59 58 oveq2d φxALBCLx𝒢GALBpPpInv𝒢GAC=pInv𝒢GppInv𝒢GxCtPtpICtAIxx=AAIx=AIA
60 57 59 eleqtrd φxALBCLx𝒢GALBpPpInv𝒢GAC=pInv𝒢GppInv𝒢GxCtPtpICtAIxx=AtAIA
61 1 2 3 54 55 56 60 axtgbtwnid φxALBCLx𝒢GALBpPpInv𝒢GAC=pInv𝒢GppInv𝒢GxCtPtpICtAIxx=AA=t
62 61 eqcomd φxALBCLx𝒢GALBpPpInv𝒢GAC=pInv𝒢GppInv𝒢GxCtPtpICtAIxx=At=A
63 62 oveq1d φxALBCLx𝒢GALBpPpInv𝒢GAC=pInv𝒢GppInv𝒢GxCtPtpICtAIxx=AtLp=ALp
64 50 ad3antrrr φxALBCLx𝒢GALBpPpInv𝒢GAC=pInv𝒢GppInv𝒢GxCtPtpICtAIxx=ApInv𝒢GppInv𝒢GxC=pInv𝒢GAC
65 58 fveq2d φxALBCLx𝒢GALBpPpInv𝒢GAC=pInv𝒢GppInv𝒢GxCtPtpICtAIxx=ApInv𝒢Gx=pInv𝒢GA
66 65 fveq1d φxALBCLx𝒢GALBpPpInv𝒢GAC=pInv𝒢GppInv𝒢GxCtPtpICtAIxx=ApInv𝒢GxC=pInv𝒢GAC
67 64 66 eqtr4d φxALBCLx𝒢GALBpPpInv𝒢GAC=pInv𝒢GppInv𝒢GxCtPtpICtAIxx=ApInv𝒢GppInv𝒢GxC=pInv𝒢GxC
68 45 ad3antrrr φxALBCLx𝒢GALBpPpInv𝒢GAC=pInv𝒢GppInv𝒢GxCtPtpICtAIxx=ApP
69 43 ad3antrrr φxALBCLx𝒢GALBpPpInv𝒢GAC=pInv𝒢GppInv𝒢GxCtPtpICtAIxx=ApInv𝒢GxCP
70 1 2 3 4 11 54 68 13 69 mirinv φxALBCLx𝒢GALBpPpInv𝒢GAC=pInv𝒢GppInv𝒢GxCtPtpICtAIxx=ApInv𝒢GppInv𝒢GxC=pInv𝒢GxCp=pInv𝒢GxC
71 67 70 mpbid φxALBCLx𝒢GALBpPpInv𝒢GAC=pInv𝒢GppInv𝒢GxCtPtpICtAIxx=Ap=pInv𝒢GxC
72 44 ad3antrrr φxALBCLx𝒢GALBpPpInv𝒢GAC=pInv𝒢GppInv𝒢GxCtPtpICtAIxx=AxP
73 58 oveq1d φxALBCLx𝒢GALBpPpInv𝒢GAC=pInv𝒢GppInv𝒢GxCtPtpICtAIxx=AxIx=AIx
74 57 73 eleqtrrd φxALBCLx𝒢GALBpPpInv𝒢GAC=pInv𝒢GppInv𝒢GxCtPtpICtAIxx=AtxIx
75 1 2 3 54 72 56 74 axtgbtwnid φxALBCLx𝒢GALBpPpInv𝒢GAC=pInv𝒢GppInv𝒢GxCtPtpICtAIxx=Ax=t
76 75 eqcomd φxALBCLx𝒢GALBpPpInv𝒢GAC=pInv𝒢GppInv𝒢GxCtPtpICtAIxx=At=x
77 71 76 oveq12d φxALBCLx𝒢GALBpPpInv𝒢GAC=pInv𝒢GppInv𝒢GxCtPtpICtAIxx=ApLt=pInv𝒢GxCLx
78 34 ad2antrr φxALBCLx𝒢GALBpPpInv𝒢GAC=pInv𝒢GppInv𝒢GxC⟨“AxC”⟩𝒢G
79 1 2 3 4 11 39 45 13 43 50 mircom φxALBCLx𝒢GALBpPpInv𝒢GAC=pInv𝒢GppInv𝒢GxCpInv𝒢GppInv𝒢GAC=pInv𝒢GxC
80 28 ad2antrr φxALBCLx𝒢GALBpPpInv𝒢GAC=pInv𝒢GppInv𝒢GxCxC
81 1 2 3 4 39 11 22 18 13 41 44 42 45 78 79 80 colperpexlem2 φxALBCLx𝒢GALBpPpInv𝒢GAC=pInv𝒢GppInv𝒢GxCAp
82 81 ad3antrrr φxALBCLx𝒢GALBpPpInv𝒢GAC=pInv𝒢GppInv𝒢GxCtPtpICtAIxx=AAp
83 62 82 eqnetrd φxALBCLx𝒢GALBpPpInv𝒢GAC=pInv𝒢GppInv𝒢GxCtPtpICtAIxx=Atp
84 1 3 4 54 56 68 83 tglinecom φxALBCLx𝒢GALBpPpInv𝒢GAC=pInv𝒢GppInv𝒢GxCtPtpICtAIxx=AtLp=pLt
85 42 ad3antrrr φxALBCLx𝒢GALBpPpInv𝒢GAC=pInv𝒢GppInv𝒢GxCtPtpICtAIxx=ACP
86 80 ad3antrrr φxALBCLx𝒢GALBpPpInv𝒢GAC=pInv𝒢GppInv𝒢GxCtPtpICtAIxx=AxC
87 54 adantr φxALBCLx𝒢GALBpPpInv𝒢GAC=pInv𝒢GppInv𝒢GxCtPtpICtAIxx=ApInv𝒢GxC=xG𝒢Tarski
88 72 adantr φxALBCLx𝒢GALBpPpInv𝒢GAC=pInv𝒢GppInv𝒢GxCtPtpICtAIxx=ApInv𝒢GxC=xxP
89 85 adantr φxALBCLx𝒢GALBpPpInv𝒢GAC=pInv𝒢GppInv𝒢GxCtPtpICtAIxx=ApInv𝒢GxC=xCP
90 1 2 3 4 11 87 88 18 mircinv φxALBCLx𝒢GALBpPpInv𝒢GAC=pInv𝒢GppInv𝒢GxCtPtpICtAIxx=ApInv𝒢GxC=xpInv𝒢Gxx=x
91 simpr φxALBCLx𝒢GALBpPpInv𝒢GAC=pInv𝒢GppInv𝒢GxCtPtpICtAIxx=ApInv𝒢GxC=xpInv𝒢GxC=x
92 90 91 eqtr4d φxALBCLx𝒢GALBpPpInv𝒢GAC=pInv𝒢GppInv𝒢GxCtPtpICtAIxx=ApInv𝒢GxC=xpInv𝒢Gxx=pInv𝒢GxC
93 1 2 3 4 11 87 88 18 88 89 92 mireq φxALBCLx𝒢GALBpPpInv𝒢GAC=pInv𝒢GppInv𝒢GxCtPtpICtAIxx=ApInv𝒢GxC=xx=C
94 86 adantr φxALBCLx𝒢GALBpPpInv𝒢GAC=pInv𝒢GppInv𝒢GxCtPtpICtAIxx=ApInv𝒢GxC=xxC
95 94 neneqd φxALBCLx𝒢GALBpPpInv𝒢GAC=pInv𝒢GppInv𝒢GxCtPtpICtAIxx=ApInv𝒢GxC=x¬x=C
96 93 95 pm2.65da φxALBCLx𝒢GALBpPpInv𝒢GAC=pInv𝒢GppInv𝒢GxCtPtpICtAIxx=A¬pInv𝒢GxC=x
97 96 neqned φxALBCLx𝒢GALBpPpInv𝒢GAC=pInv𝒢GppInv𝒢GxCtPtpICtAIxx=ApInv𝒢GxCx
98 47 ad3antrrr φxALBCLx𝒢GALBpPpInv𝒢GAC=pInv𝒢GppInv𝒢GxCtPtpICtAIxx=AxpInv𝒢GxCIC
99 1 3 4 54 72 85 69 86 98 btwnlng2 φxALBCLx𝒢GALBpPpInv𝒢GAC=pInv𝒢GppInv𝒢GxCtPtpICtAIxx=ApInv𝒢GxCxLC
100 1 3 4 54 72 85 86 69 97 99 tglineelsb2 φxALBCLx𝒢GALBpPpInv𝒢GAC=pInv𝒢GppInv𝒢GxCtPtpICtAIxx=AxLC=xLpInv𝒢GxC
101 28 necomd φxALBCLx𝒢GALBCx
102 101 ad5antr φxALBCLx𝒢GALBpPpInv𝒢GAC=pInv𝒢GppInv𝒢GxCtPtpICtAIxx=ACx
103 1 3 4 54 85 72 102 tglinecom φxALBCLx𝒢GALBpPpInv𝒢GAC=pInv𝒢GppInv𝒢GxCtPtpICtAIxx=ACLx=xLC
104 1 3 4 54 69 72 97 tglinecom φxALBCLx𝒢GALBpPpInv𝒢GAC=pInv𝒢GppInv𝒢GxCtPtpICtAIxx=ApInv𝒢GxCLx=xLpInv𝒢GxC
105 100 103 104 3eqtr4d φxALBCLx𝒢GALBpPpInv𝒢GAC=pInv𝒢GppInv𝒢GxCtPtpICtAIxx=ACLx=pInv𝒢GxCLx
106 77 84 105 3eqtr4d φxALBCLx𝒢GALBpPpInv𝒢GAC=pInv𝒢GppInv𝒢GxCtPtpICtAIxx=AtLp=CLx
107 63 106 eqtr3d φxALBCLx𝒢GALBpPpInv𝒢GAC=pInv𝒢GppInv𝒢GxCtPtpICtAIxx=AALp=CLx
108 31 ad5antr φxALBCLx𝒢GALBpPpInv𝒢GAC=pInv𝒢GppInv𝒢GxCtPtpICtAIxx=ACLx𝒢GALB
109 107 108 eqbrtrd φxALBCLx𝒢GALBpPpInv𝒢GAC=pInv𝒢GppInv𝒢GxCtPtpICtAIxx=AALp𝒢GALB
110 39 ad3antrrr φxALBCLx𝒢GALBpPpInv𝒢GAC=pInv𝒢GppInv𝒢GxCtPtpICtAIxxAG𝒢Tarski
111 41 ad3antrrr φxALBCLx𝒢GALBpPpInv𝒢GAC=pInv𝒢GppInv𝒢GxCtPtpICtAIxxAAP
112 45 ad3antrrr φxALBCLx𝒢GALBpPpInv𝒢GAC=pInv𝒢GppInv𝒢GxCtPtpICtAIxxApP
113 81 ad3antrrr φxALBCLx𝒢GALBpPpInv𝒢GAC=pInv𝒢GppInv𝒢GxCtPtpICtAIxxAAp
114 1 3 4 110 111 112 113 tgelrnln φxALBCLx𝒢GALBpPpInv𝒢GAC=pInv𝒢GppInv𝒢GxCtPtpICtAIxxAALpranL
115 15 ad5antr φxALBCLx𝒢GALBpPpInv𝒢GAC=pInv𝒢GppInv𝒢GxCtPtpICtAIxxAALBranL
116 1 3 4 110 111 112 113 tglinerflx1 φxALBCLx𝒢GALBpPpInv𝒢GAC=pInv𝒢GppInv𝒢GxCtPtpICtAIxxAAALp
117 9 ad2antrr φxALBCLx𝒢GALBAB
118 1 3 4 12 21 25 117 tglinerflx1 φxALBCLx𝒢GALBAALB
119 118 ad5antr φxALBCLx𝒢GALBpPpInv𝒢GAC=pInv𝒢GppInv𝒢GxCtPtpICtAIxxAAALB
120 116 119 elind φxALBCLx𝒢GALBpPpInv𝒢GAC=pInv𝒢GppInv𝒢GxCtPtpICtAIxxAAALpALB
121 1 3 4 110 111 112 113 tglinerflx2 φxALBCLx𝒢GALBpPpInv𝒢GAC=pInv𝒢GppInv𝒢GxCtPtpICtAIxxApALp
122 16 ad5antr φxALBCLx𝒢GALBpPpInv𝒢GAC=pInv𝒢GppInv𝒢GxCtPtpICtAIxxAxALB
123 113 necomd φxALBCLx𝒢GALBpPpInv𝒢GAC=pInv𝒢GppInv𝒢GxCtPtpICtAIxxApA
124 simpr φxALBCLx𝒢GALBpPpInv𝒢GAC=pInv𝒢GppInv𝒢GxCtPtpICtAIxxAxA
125 44 ad3antrrr φxALBCLx𝒢GALBpPpInv𝒢GAC=pInv𝒢GppInv𝒢GxCtPtpICtAIxxAxP
126 1 2 3 4 39 11 22 18 13 41 44 42 45 78 79 colperpexlem1 φxALBCLx𝒢GALBpPpInv𝒢GAC=pInv𝒢GppInv𝒢GxC⟨“xAp”⟩𝒢G
127 126 ad3antrrr φxALBCLx𝒢GALBpPpInv𝒢GAC=pInv𝒢GppInv𝒢GxCtPtpICtAIxxA⟨“xAp”⟩𝒢G
128 1 2 3 4 11 110 125 111 112 127 ragcom φxALBCLx𝒢GALBpPpInv𝒢GAC=pInv𝒢GppInv𝒢GxCtPtpICtAIxxA⟨“pAx”⟩𝒢G
129 1 2 3 4 110 114 115 120 121 122 123 124 128 ragperp φxALBCLx𝒢GALBpPpInv𝒢GAC=pInv𝒢GppInv𝒢GxCtPtpICtAIxxAALp𝒢GALB
130 109 129 pm2.61dane φxALBCLx𝒢GALBpPpInv𝒢GAC=pInv𝒢GppInv𝒢GxCtPtpICtAIxALp𝒢GALB
131 118 ad5antr φxALBCLx𝒢GALBpPpInv𝒢GAC=pInv𝒢GppInv𝒢GxCtPtpICtAIxx=AAALB
132 62 131 eqeltrd φxALBCLx𝒢GALBpPpInv𝒢GAC=pInv𝒢GppInv𝒢GxCtPtpICtAIxx=AtALB
133 132 orcd φxALBCLx𝒢GALBpPpInv𝒢GAC=pInv𝒢GppInv𝒢GxCtPtpICtAIxx=AtALBA=B
134 25 ad5antr φxALBCLx𝒢GALBpPpInv𝒢GAC=pInv𝒢GppInv𝒢GxCtPtpICtAIxxABP
135 117 ad5antr φxALBCLx𝒢GALBpPpInv𝒢GAC=pInv𝒢GppInv𝒢GxCtPtpICtAIxxAAB
136 simpllr φxALBCLx𝒢GALBpPpInv𝒢GAC=pInv𝒢GppInv𝒢GxCtPtpICtAIxxAtP
137 124 necomd φxALBCLx𝒢GALBpPpInv𝒢GAC=pInv𝒢GppInv𝒢GxCtPtpICtAIxxAAx
138 simplrr φxALBCLx𝒢GALBpPpInv𝒢GAC=pInv𝒢GppInv𝒢GxCtPtpICtAIxxAtAIx
139 1 3 4 110 111 125 136 137 138 btwnlng1 φxALBCLx𝒢GALBpPpInv𝒢GAC=pInv𝒢GppInv𝒢GxCtPtpICtAIxxAtALx
140 1 3 4 110 111 134 135 125 124 122 136 139 tglineeltr φxALBCLx𝒢GALBpPpInv𝒢GAC=pInv𝒢GppInv𝒢GxCtPtpICtAIxxAtALB
141 140 orcd φxALBCLx𝒢GALBpPpInv𝒢GAC=pInv𝒢GppInv𝒢GxCtPtpICtAIxxAtALBA=B
142 133 141 pm2.61dane φxALBCLx𝒢GALBpPpInv𝒢GAC=pInv𝒢GppInv𝒢GxCtPtpICtAIxtALBA=B
143 39 ad2antrr φxALBCLx𝒢GALBpPpInv𝒢GAC=pInv𝒢GppInv𝒢GxCtPtpICtAIxG𝒢Tarski
144 45 ad2antrr φxALBCLx𝒢GALBpPpInv𝒢GAC=pInv𝒢GppInv𝒢GxCtPtpICtAIxpP
145 simplr φxALBCLx𝒢GALBpPpInv𝒢GAC=pInv𝒢GppInv𝒢GxCtPtpICtAIxtP
146 42 ad2antrr φxALBCLx𝒢GALBpPpInv𝒢GAC=pInv𝒢GppInv𝒢GxCtPtpICtAIxCP
147 simprl φxALBCLx𝒢GALBpPpInv𝒢GAC=pInv𝒢GppInv𝒢GxCtPtpICtAIxtpIC
148 1 2 3 143 144 145 146 147 tgbtwncom φxALBCLx𝒢GALBpPpInv𝒢GAC=pInv𝒢GppInv𝒢GxCtPtpICtAIxtCIp
149 130 142 148 jca32 φxALBCLx𝒢GALBpPpInv𝒢GAC=pInv𝒢GppInv𝒢GxCtPtpICtAIxALp𝒢GALBtALBA=BtCIp
150 149 ex φxALBCLx𝒢GALBpPpInv𝒢GAC=pInv𝒢GppInv𝒢GxCtPtpICtAIxALp𝒢GALBtALBA=BtCIp
151 150 reximdva φxALBCLx𝒢GALBpPpInv𝒢GAC=pInv𝒢GppInv𝒢GxCtPtpICtAIxtPALp𝒢GALBtALBA=BtCIp
152 53 151 mpd φxALBCLx𝒢GALBpPpInv𝒢GAC=pInv𝒢GppInv𝒢GxCtPALp𝒢GALBtALBA=BtCIp
153 r19.42v tPALp𝒢GALBtALBA=BtCIpALp𝒢GALBtPtALBA=BtCIp
154 152 153 sylib φxALBCLx𝒢GALBpPpInv𝒢GAC=pInv𝒢GppInv𝒢GxCALp𝒢GALBtPtALBA=BtCIp
155 154 ex φxALBCLx𝒢GALBpPpInv𝒢GAC=pInv𝒢GppInv𝒢GxCALp𝒢GALBtPtALBA=BtCIp
156 155 reximdva φxALBCLx𝒢GALBpPpInv𝒢GAC=pInv𝒢GppInv𝒢GxCpPALp𝒢GALBtPtALBA=BtCIp
157 38 156 mpd φxALBCLx𝒢GALBpPALp𝒢GALBtPtALBA=BtCIp
158 1 2 3 4 5 14 8 10 footex φxALBCLx𝒢GALB
159 157 158 r19.29a φpPALp𝒢GALBtPtALBA=BtCIp