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 = Base G
colperpex.d - ˙ = dist G
colperpex.i I = Itv G
colperpex.l L = Line 𝒢 G
colperpex.g φ G 𝒢 Tarski
colperpex.1 φ A P
colperpex.2 φ B P
colperpex.3 φ C P
colperpex.4 φ A B
colperpexlem3.1 φ ¬ C A L B
Assertion colperpexlem3 φ p P A L p 𝒢 G A L B t P t A L B A = B t C I p

Proof

Step Hyp Ref Expression
1 colperpex.p P = Base G
2 colperpex.d - ˙ = dist G
3 colperpex.i I = Itv G
4 colperpex.l L = Line 𝒢 G
5 colperpex.g φ G 𝒢 Tarski
6 colperpex.1 φ A P
7 colperpex.2 φ B P
8 colperpex.3 φ C P
9 colperpex.4 φ A B
10 colperpexlem3.1 φ ¬ C A L B
11 eqid pInv 𝒢 G = pInv 𝒢 G
12 5 ad2antrr φ x A L B C L x 𝒢 G A L B G 𝒢 Tarski
13 eqid pInv 𝒢 G p = pInv 𝒢 G p
14 1 3 4 5 6 7 9 tgelrnln φ A L B ran L
15 14 ad2antrr φ x A L B C L x 𝒢 G A L B A L B ran L
16 simplr φ x A L B C L x 𝒢 G A L B x A L B
17 1 4 3 12 15 16 tglnpt φ x A L B C L x 𝒢 G A L B x P
18 eqid pInv 𝒢 G x = pInv 𝒢 G x
19 8 ad2antrr φ x A L B C L x 𝒢 G A L B C P
20 1 2 3 4 11 12 17 18 19 mircl φ x A L B C L x 𝒢 G A L B pInv 𝒢 G x C P
21 6 ad2antrr φ x A L B C L x 𝒢 G A L B A P
22 eqid pInv 𝒢 G A = pInv 𝒢 G A
23 1 2 3 4 11 12 21 22 19 mircl φ x A L B C L x 𝒢 G A L B pInv 𝒢 G A C P
24 1 2 3 4 11 12 21 22 19 mircgr φ x A L B C L x 𝒢 G A L B A - ˙ pInv 𝒢 G A C = A - ˙ C
25 7 ad2antrr φ x A L B C L x 𝒢 G A L B B P
26 10 ad2antrr φ x A L B C L x 𝒢 G A L B ¬ C A L B
27 nelne2 x A L B ¬ C A L B x C
28 16 26 27 syl2anc φ x A L B C L x 𝒢 G A L B x C
29 1 3 4 12 17 19 28 tgelrnln φ x A L B C L x 𝒢 G A L B x L C ran L
30 1 3 4 12 17 19 28 tglinecom φ x A L B C L x 𝒢 G A L B x L C = C L x
31 simpr φ x A L B C L x 𝒢 G A L B C L x 𝒢 G A L B
32 30 31 eqbrtrd φ x A L B C L x 𝒢 G A L B x L C 𝒢 G A L B
33 1 2 3 4 12 29 15 32 perpcom φ x A L B C L x 𝒢 G A L B A L B 𝒢 G x L C
34 1 2 3 4 12 21 25 16 19 33 perprag φ x A L B C L x 𝒢 G A L B ⟨“ AxC ”⟩ 𝒢 G
35 1 2 3 4 11 12 21 17 19 israg φ x A L B C L x 𝒢 G A L B ⟨“ AxC ”⟩ 𝒢 G A - ˙ C = A - ˙ pInv 𝒢 G x C
36 34 35 mpbid φ x A L B C L x 𝒢 G A L B A - ˙ C = A - ˙ pInv 𝒢 G x C
37 24 36 eqtr2d φ x A L B C L x 𝒢 G A L B A - ˙ pInv 𝒢 G x C = A - ˙ pInv 𝒢 G A C
38 1 2 3 4 11 12 13 20 23 21 37 midexlem φ x A L B C L x 𝒢 G A L B p P pInv 𝒢 G A C = pInv 𝒢 G p pInv 𝒢 G x C
39 12 ad2antrr φ x A L B C L x 𝒢 G A L B p P pInv 𝒢 G A C = pInv 𝒢 G p pInv 𝒢 G x C G 𝒢 Tarski
40 23 ad2antrr φ x A L B C L x 𝒢 G A L B p P pInv 𝒢 G A C = pInv 𝒢 G p pInv 𝒢 G x C pInv 𝒢 G A C P
41 21 ad2antrr φ x A L B C L x 𝒢 G A L B p P pInv 𝒢 G A C = pInv 𝒢 G p pInv 𝒢 G x C A P
42 19 ad2antrr φ x A L B C L x 𝒢 G A L B p P pInv 𝒢 G A C = pInv 𝒢 G p pInv 𝒢 G x C C P
43 20 ad2antrr φ x A L B C L x 𝒢 G A L B p P pInv 𝒢 G A C = pInv 𝒢 G p pInv 𝒢 G x C pInv 𝒢 G x C P
44 17 ad2antrr φ x A L B C L x 𝒢 G A L B p P pInv 𝒢 G A C = pInv 𝒢 G p pInv 𝒢 G x C x P
45 simplr φ x A L B C L x 𝒢 G A L B p P pInv 𝒢 G A C = pInv 𝒢 G p pInv 𝒢 G x C p P
46 1 2 3 4 11 39 41 22 42 mirbtwn φ x A L B C L x 𝒢 G A L B p P pInv 𝒢 G A C = pInv 𝒢 G p pInv 𝒢 G x C A pInv 𝒢 G A C I C
47 1 2 3 4 11 39 44 18 42 mirbtwn φ x A L B C L x 𝒢 G A L B p P pInv 𝒢 G A C = pInv 𝒢 G p pInv 𝒢 G x C x pInv 𝒢 G x C I C
48 1 2 3 4 11 39 45 13 43 mirbtwn φ x A L B C L x 𝒢 G A L B p P pInv 𝒢 G A C = pInv 𝒢 G p pInv 𝒢 G x C p pInv 𝒢 G p pInv 𝒢 G x C I pInv 𝒢 G x C
49 simpr φ x A L B C L x 𝒢 G A L B p P pInv 𝒢 G A C = pInv 𝒢 G p pInv 𝒢 G x C pInv 𝒢 G A C = pInv 𝒢 G p pInv 𝒢 G x C
50 49 eqcomd φ x A L B C L x 𝒢 G A L B p P pInv 𝒢 G A C = pInv 𝒢 G p pInv 𝒢 G x C pInv 𝒢 G p pInv 𝒢 G x C = pInv 𝒢 G A C
51 50 oveq1d φ x A L B C L x 𝒢 G A L B p P pInv 𝒢 G A C = pInv 𝒢 G p pInv 𝒢 G x C pInv 𝒢 G p pInv 𝒢 G x C I pInv 𝒢 G x C = pInv 𝒢 G A C I pInv 𝒢 G x C
52 48 51 eleqtrd φ x A L B C L x 𝒢 G A L B p P pInv 𝒢 G A C = pInv 𝒢 G p pInv 𝒢 G x C p pInv 𝒢 G A C I pInv 𝒢 G x C
53 1 2 3 39 40 41 42 43 44 45 46 47 52 tgtrisegint φ x A L B C L x 𝒢 G A L B p P pInv 𝒢 G A C = pInv 𝒢 G p pInv 𝒢 G x C t P t p I C t A I x
54 39 ad3antrrr φ x A L B C L x 𝒢 G A L B p P pInv 𝒢 G A C = pInv 𝒢 G p pInv 𝒢 G x C t P t p I C t A I x x = A G 𝒢 Tarski
55 41 ad3antrrr φ x A L B C L x 𝒢 G A L B p P pInv 𝒢 G A C = pInv 𝒢 G p pInv 𝒢 G x C t P t p I C t A I x x = A A P
56 simpllr φ x A L B C L x 𝒢 G A L B p P pInv 𝒢 G A C = pInv 𝒢 G p pInv 𝒢 G x C t P t p I C t A I x x = A t P
57 simplrr φ x A L B C L x 𝒢 G A L B p P pInv 𝒢 G A C = pInv 𝒢 G p pInv 𝒢 G x C t P t p I C t A I x x = A t A I x
58 simpr φ x A L B C L x 𝒢 G A L B p P pInv 𝒢 G A C = pInv 𝒢 G p pInv 𝒢 G x C t P t p I C t A I x x = A x = A
59 58 oveq2d φ x A L B C L x 𝒢 G A L B p P pInv 𝒢 G A C = pInv 𝒢 G p pInv 𝒢 G x C t P t p I C t A I x x = A A I x = A I A
60 57 59 eleqtrd φ x A L B C L x 𝒢 G A L B p P pInv 𝒢 G A C = pInv 𝒢 G p pInv 𝒢 G x C t P t p I C t A I x x = A t A I A
61 1 2 3 54 55 56 60 axtgbtwnid φ x A L B C L x 𝒢 G A L B p P pInv 𝒢 G A C = pInv 𝒢 G p pInv 𝒢 G x C t P t p I C t A I x x = A A = t
62 61 eqcomd φ x A L B C L x 𝒢 G A L B p P pInv 𝒢 G A C = pInv 𝒢 G p pInv 𝒢 G x C t P t p I C t A I x x = A t = A
63 62 oveq1d φ x A L B C L x 𝒢 G A L B p P pInv 𝒢 G A C = pInv 𝒢 G p pInv 𝒢 G x C t P t p I C t A I x x = A t L p = A L p
64 50 ad3antrrr φ x A L B C L x 𝒢 G A L B p P pInv 𝒢 G A C = pInv 𝒢 G p pInv 𝒢 G x C t P t p I C t A I x x = A pInv 𝒢 G p pInv 𝒢 G x C = pInv 𝒢 G A C
65 58 fveq2d φ x A L B C L x 𝒢 G A L B p P pInv 𝒢 G A C = pInv 𝒢 G p pInv 𝒢 G x C t P t p I C t A I x x = A pInv 𝒢 G x = pInv 𝒢 G A
66 65 fveq1d φ x A L B C L x 𝒢 G A L B p P pInv 𝒢 G A C = pInv 𝒢 G p pInv 𝒢 G x C t P t p I C t A I x x = A pInv 𝒢 G x C = pInv 𝒢 G A C
67 64 66 eqtr4d φ x A L B C L x 𝒢 G A L B p P pInv 𝒢 G A C = pInv 𝒢 G p pInv 𝒢 G x C t P t p I C t A I x x = A pInv 𝒢 G p pInv 𝒢 G x C = pInv 𝒢 G x C
68 45 ad3antrrr φ x A L B C L x 𝒢 G A L B p P pInv 𝒢 G A C = pInv 𝒢 G p pInv 𝒢 G x C t P t p I C t A I x x = A p P
69 43 ad3antrrr φ x A L B C L x 𝒢 G A L B p P pInv 𝒢 G A C = pInv 𝒢 G p pInv 𝒢 G x C t P t p I C t A I x x = A pInv 𝒢 G x C P
70 1 2 3 4 11 54 68 13 69 mirinv φ x A L B C L x 𝒢 G A L B p P pInv 𝒢 G A C = pInv 𝒢 G p pInv 𝒢 G x C t P t p I C t A I x x = A pInv 𝒢 G p pInv 𝒢 G x C = pInv 𝒢 G x C p = pInv 𝒢 G x C
71 67 70 mpbid φ x A L B C L x 𝒢 G A L B p P pInv 𝒢 G A C = pInv 𝒢 G p pInv 𝒢 G x C t P t p I C t A I x x = A p = pInv 𝒢 G x C
72 44 ad3antrrr φ x A L B C L x 𝒢 G A L B p P pInv 𝒢 G A C = pInv 𝒢 G p pInv 𝒢 G x C t P t p I C t A I x x = A x P
73 58 oveq1d φ x A L B C L x 𝒢 G A L B p P pInv 𝒢 G A C = pInv 𝒢 G p pInv 𝒢 G x C t P t p I C t A I x x = A x I x = A I x
74 57 73 eleqtrrd φ x A L B C L x 𝒢 G A L B p P pInv 𝒢 G A C = pInv 𝒢 G p pInv 𝒢 G x C t P t p I C t A I x x = A t x I x
75 1 2 3 54 72 56 74 axtgbtwnid φ x A L B C L x 𝒢 G A L B p P pInv 𝒢 G A C = pInv 𝒢 G p pInv 𝒢 G x C t P t p I C t A I x x = A x = t
76 75 eqcomd φ x A L B C L x 𝒢 G A L B p P pInv 𝒢 G A C = pInv 𝒢 G p pInv 𝒢 G x C t P t p I C t A I x x = A t = x
77 71 76 oveq12d φ x A L B C L x 𝒢 G A L B p P pInv 𝒢 G A C = pInv 𝒢 G p pInv 𝒢 G x C t P t p I C t A I x x = A p L t = pInv 𝒢 G x C L x
78 34 ad2antrr φ x A L B C L x 𝒢 G A L B p P pInv 𝒢 G A C = pInv 𝒢 G p pInv 𝒢 G x C ⟨“ AxC ”⟩ 𝒢 G
79 1 2 3 4 11 39 45 13 43 50 mircom φ x A L B C L x 𝒢 G A L B p P pInv 𝒢 G A C = pInv 𝒢 G p pInv 𝒢 G x C pInv 𝒢 G p pInv 𝒢 G A C = pInv 𝒢 G x C
80 28 ad2antrr φ x A L B C L x 𝒢 G A L B p P pInv 𝒢 G A C = pInv 𝒢 G p pInv 𝒢 G x C x C
81 1 2 3 4 39 11 22 18 13 41 44 42 45 78 79 80 colperpexlem2 φ x A L B C L x 𝒢 G A L B p P pInv 𝒢 G A C = pInv 𝒢 G p pInv 𝒢 G x C A p
82 81 ad3antrrr φ x A L B C L x 𝒢 G A L B p P pInv 𝒢 G A C = pInv 𝒢 G p pInv 𝒢 G x C t P t p I C t A I x x = A A p
83 62 82 eqnetrd φ x A L B C L x 𝒢 G A L B p P pInv 𝒢 G A C = pInv 𝒢 G p pInv 𝒢 G x C t P t p I C t A I x x = A t p
84 1 3 4 54 56 68 83 tglinecom φ x A L B C L x 𝒢 G A L B p P pInv 𝒢 G A C = pInv 𝒢 G p pInv 𝒢 G x C t P t p I C t A I x x = A t L p = p L t
85 42 ad3antrrr φ x A L B C L x 𝒢 G A L B p P pInv 𝒢 G A C = pInv 𝒢 G p pInv 𝒢 G x C t P t p I C t A I x x = A C P
86 80 ad3antrrr φ x A L B C L x 𝒢 G A L B p P pInv 𝒢 G A C = pInv 𝒢 G p pInv 𝒢 G x C t P t p I C t A I x x = A x C
87 54 adantr φ x A L B C L x 𝒢 G A L B p P pInv 𝒢 G A C = pInv 𝒢 G p pInv 𝒢 G x C t P t p I C t A I x x = A pInv 𝒢 G x C = x G 𝒢 Tarski
88 72 adantr φ x A L B C L x 𝒢 G A L B p P pInv 𝒢 G A C = pInv 𝒢 G p pInv 𝒢 G x C t P t p I C t A I x x = A pInv 𝒢 G x C = x x P
89 85 adantr φ x A L B C L x 𝒢 G A L B p P pInv 𝒢 G A C = pInv 𝒢 G p pInv 𝒢 G x C t P t p I C t A I x x = A pInv 𝒢 G x C = x C P
90 1 2 3 4 11 87 88 18 mircinv φ x A L B C L x 𝒢 G A L B p P pInv 𝒢 G A C = pInv 𝒢 G p pInv 𝒢 G x C t P t p I C t A I x x = A pInv 𝒢 G x C = x pInv 𝒢 G x x = x
91 simpr φ x A L B C L x 𝒢 G A L B p P pInv 𝒢 G A C = pInv 𝒢 G p pInv 𝒢 G x C t P t p I C t A I x x = A pInv 𝒢 G x C = x pInv 𝒢 G x C = x
92 90 91 eqtr4d φ x A L B C L x 𝒢 G A L B p P pInv 𝒢 G A C = pInv 𝒢 G p pInv 𝒢 G x C t P t p I C t A I x x = A pInv 𝒢 G x C = x pInv 𝒢 G x x = pInv 𝒢 G x C
93 1 2 3 4 11 87 88 18 88 89 92 mireq φ x A L B C L x 𝒢 G A L B p P pInv 𝒢 G A C = pInv 𝒢 G p pInv 𝒢 G x C t P t p I C t A I x x = A pInv 𝒢 G x C = x x = C
94 86 adantr φ x A L B C L x 𝒢 G A L B p P pInv 𝒢 G A C = pInv 𝒢 G p pInv 𝒢 G x C t P t p I C t A I x x = A pInv 𝒢 G x C = x x C
95 94 neneqd φ x A L B C L x 𝒢 G A L B p P pInv 𝒢 G A C = pInv 𝒢 G p pInv 𝒢 G x C t P t p I C t A I x x = A pInv 𝒢 G x C = x ¬ x = C
96 93 95 pm2.65da φ x A L B C L x 𝒢 G A L B p P pInv 𝒢 G A C = pInv 𝒢 G p pInv 𝒢 G x C t P t p I C t A I x x = A ¬ pInv 𝒢 G x C = x
97 96 neqned φ x A L B C L x 𝒢 G A L B p P pInv 𝒢 G A C = pInv 𝒢 G p pInv 𝒢 G x C t P t p I C t A I x x = A pInv 𝒢 G x C x
98 47 ad3antrrr φ x A L B C L x 𝒢 G A L B p P pInv 𝒢 G A C = pInv 𝒢 G p pInv 𝒢 G x C t P t p I C t A I x x = A x pInv 𝒢 G x C I C
99 1 3 4 54 72 85 69 86 98 btwnlng2 φ x A L B C L x 𝒢 G A L B p P pInv 𝒢 G A C = pInv 𝒢 G p pInv 𝒢 G x C t P t p I C t A I x x = A pInv 𝒢 G x C x L C
100 1 3 4 54 72 85 86 69 97 99 tglineelsb2 φ x A L B C L x 𝒢 G A L B p P pInv 𝒢 G A C = pInv 𝒢 G p pInv 𝒢 G x C t P t p I C t A I x x = A x L C = x L pInv 𝒢 G x C
101 28 necomd φ x A L B C L x 𝒢 G A L B C x
102 101 ad5antr φ x A L B C L x 𝒢 G A L B p P pInv 𝒢 G A C = pInv 𝒢 G p pInv 𝒢 G x C t P t p I C t A I x x = A C x
103 1 3 4 54 85 72 102 tglinecom φ x A L B C L x 𝒢 G A L B p P pInv 𝒢 G A C = pInv 𝒢 G p pInv 𝒢 G x C t P t p I C t A I x x = A C L x = x L C
104 1 3 4 54 69 72 97 tglinecom φ x A L B C L x 𝒢 G A L B p P pInv 𝒢 G A C = pInv 𝒢 G p pInv 𝒢 G x C t P t p I C t A I x x = A pInv 𝒢 G x C L x = x L pInv 𝒢 G x C
105 100 103 104 3eqtr4d φ x A L B C L x 𝒢 G A L B p P pInv 𝒢 G A C = pInv 𝒢 G p pInv 𝒢 G x C t P t p I C t A I x x = A C L x = pInv 𝒢 G x C L x
106 77 84 105 3eqtr4d φ x A L B C L x 𝒢 G A L B p P pInv 𝒢 G A C = pInv 𝒢 G p pInv 𝒢 G x C t P t p I C t A I x x = A t L p = C L x
107 63 106 eqtr3d φ x A L B C L x 𝒢 G A L B p P pInv 𝒢 G A C = pInv 𝒢 G p pInv 𝒢 G x C t P t p I C t A I x x = A A L p = C L x
108 31 ad5antr φ x A L B C L x 𝒢 G A L B p P pInv 𝒢 G A C = pInv 𝒢 G p pInv 𝒢 G x C t P t p I C t A I x x = A C L x 𝒢 G A L B
109 107 108 eqbrtrd φ x A L B C L x 𝒢 G A L B p P pInv 𝒢 G A C = pInv 𝒢 G p pInv 𝒢 G x C t P t p I C t A I x x = A A L p 𝒢 G A L B
110 39 ad3antrrr φ x A L B C L x 𝒢 G A L B p P pInv 𝒢 G A C = pInv 𝒢 G p pInv 𝒢 G x C t P t p I C t A I x x A G 𝒢 Tarski
111 41 ad3antrrr φ x A L B C L x 𝒢 G A L B p P pInv 𝒢 G A C = pInv 𝒢 G p pInv 𝒢 G x C t P t p I C t A I x x A A P
112 45 ad3antrrr φ x A L B C L x 𝒢 G A L B p P pInv 𝒢 G A C = pInv 𝒢 G p pInv 𝒢 G x C t P t p I C t A I x x A p P
113 81 ad3antrrr φ x A L B C L x 𝒢 G A L B p P pInv 𝒢 G A C = pInv 𝒢 G p pInv 𝒢 G x C t P t p I C t A I x x A A p
114 1 3 4 110 111 112 113 tgelrnln φ x A L B C L x 𝒢 G A L B p P pInv 𝒢 G A C = pInv 𝒢 G p pInv 𝒢 G x C t P t p I C t A I x x A A L p ran L
115 15 ad5antr φ x A L B C L x 𝒢 G A L B p P pInv 𝒢 G A C = pInv 𝒢 G p pInv 𝒢 G x C t P t p I C t A I x x A A L B ran L
116 1 3 4 110 111 112 113 tglinerflx1 φ x A L B C L x 𝒢 G A L B p P pInv 𝒢 G A C = pInv 𝒢 G p pInv 𝒢 G x C t P t p I C t A I x x A A A L p
117 9 ad2antrr φ x A L B C L x 𝒢 G A L B A B
118 1 3 4 12 21 25 117 tglinerflx1 φ x A L B C L x 𝒢 G A L B A A L B
119 118 ad5antr φ x A L B C L x 𝒢 G A L B p P pInv 𝒢 G A C = pInv 𝒢 G p pInv 𝒢 G x C t P t p I C t A I x x A A A L B
120 116 119 elind φ x A L B C L x 𝒢 G A L B p P pInv 𝒢 G A C = pInv 𝒢 G p pInv 𝒢 G x C t P t p I C t A I x x A A A L p A L B
121 1 3 4 110 111 112 113 tglinerflx2 φ x A L B C L x 𝒢 G A L B p P pInv 𝒢 G A C = pInv 𝒢 G p pInv 𝒢 G x C t P t p I C t A I x x A p A L p
122 16 ad5antr φ x A L B C L x 𝒢 G A L B p P pInv 𝒢 G A C = pInv 𝒢 G p pInv 𝒢 G x C t P t p I C t A I x x A x A L B
123 113 necomd φ x A L B C L x 𝒢 G A L B p P pInv 𝒢 G A C = pInv 𝒢 G p pInv 𝒢 G x C t P t p I C t A I x x A p A
124 simpr φ x A L B C L x 𝒢 G A L B p P pInv 𝒢 G A C = pInv 𝒢 G p pInv 𝒢 G x C t P t p I C t A I x x A x A
125 44 ad3antrrr φ x A L B C L x 𝒢 G A L B p P pInv 𝒢 G A C = pInv 𝒢 G p pInv 𝒢 G x C t P t p I C t A I x x A x P
126 1 2 3 4 39 11 22 18 13 41 44 42 45 78 79 colperpexlem1 φ x A L B C L x 𝒢 G A L B p P pInv 𝒢 G A C = pInv 𝒢 G p pInv 𝒢 G x C ⟨“ xAp ”⟩ 𝒢 G
127 126 ad3antrrr φ x A L B C L x 𝒢 G A L B p P pInv 𝒢 G A C = pInv 𝒢 G p pInv 𝒢 G x C t P t p I C t A I x x A ⟨“ xAp ”⟩ 𝒢 G
128 1 2 3 4 11 110 125 111 112 127 ragcom φ x A L B C L x 𝒢 G A L B p P pInv 𝒢 G A C = pInv 𝒢 G p pInv 𝒢 G x C t P t p I C t A I x x A ⟨“ pAx ”⟩ 𝒢 G
129 1 2 3 4 110 114 115 120 121 122 123 124 128 ragperp φ x A L B C L x 𝒢 G A L B p P pInv 𝒢 G A C = pInv 𝒢 G p pInv 𝒢 G x C t P t p I C t A I x x A A L p 𝒢 G A L B
130 109 129 pm2.61dane φ x A L B C L x 𝒢 G A L B p P pInv 𝒢 G A C = pInv 𝒢 G p pInv 𝒢 G x C t P t p I C t A I x A L p 𝒢 G A L B
131 118 ad5antr φ x A L B C L x 𝒢 G A L B p P pInv 𝒢 G A C = pInv 𝒢 G p pInv 𝒢 G x C t P t p I C t A I x x = A A A L B
132 62 131 eqeltrd φ x A L B C L x 𝒢 G A L B p P pInv 𝒢 G A C = pInv 𝒢 G p pInv 𝒢 G x C t P t p I C t A I x x = A t A L B
133 132 orcd φ x A L B C L x 𝒢 G A L B p P pInv 𝒢 G A C = pInv 𝒢 G p pInv 𝒢 G x C t P t p I C t A I x x = A t A L B A = B
134 25 ad5antr φ x A L B C L x 𝒢 G A L B p P pInv 𝒢 G A C = pInv 𝒢 G p pInv 𝒢 G x C t P t p I C t A I x x A B P
135 117 ad5antr φ x A L B C L x 𝒢 G A L B p P pInv 𝒢 G A C = pInv 𝒢 G p pInv 𝒢 G x C t P t p I C t A I x x A A B
136 simpllr φ x A L B C L x 𝒢 G A L B p P pInv 𝒢 G A C = pInv 𝒢 G p pInv 𝒢 G x C t P t p I C t A I x x A t P
137 124 necomd φ x A L B C L x 𝒢 G A L B p P pInv 𝒢 G A C = pInv 𝒢 G p pInv 𝒢 G x C t P t p I C t A I x x A A x
138 simplrr φ x A L B C L x 𝒢 G A L B p P pInv 𝒢 G A C = pInv 𝒢 G p pInv 𝒢 G x C t P t p I C t A I x x A t A I x
139 1 3 4 110 111 125 136 137 138 btwnlng1 φ x A L B C L x 𝒢 G A L B p P pInv 𝒢 G A C = pInv 𝒢 G p pInv 𝒢 G x C t P t p I C t A I x x A t A L x
140 1 3 4 110 111 134 135 125 124 122 136 139 tglineeltr φ x A L B C L x 𝒢 G A L B p P pInv 𝒢 G A C = pInv 𝒢 G p pInv 𝒢 G x C t P t p I C t A I x x A t A L B
141 140 orcd φ x A L B C L x 𝒢 G A L B p P pInv 𝒢 G A C = pInv 𝒢 G p pInv 𝒢 G x C t P t p I C t A I x x A t A L B A = B
142 133 141 pm2.61dane φ x A L B C L x 𝒢 G A L B p P pInv 𝒢 G A C = pInv 𝒢 G p pInv 𝒢 G x C t P t p I C t A I x t A L B A = B
143 39 ad2antrr φ x A L B C L x 𝒢 G A L B p P pInv 𝒢 G A C = pInv 𝒢 G p pInv 𝒢 G x C t P t p I C t A I x G 𝒢 Tarski
144 45 ad2antrr φ x A L B C L x 𝒢 G A L B p P pInv 𝒢 G A C = pInv 𝒢 G p pInv 𝒢 G x C t P t p I C t A I x p P
145 simplr φ x A L B C L x 𝒢 G A L B p P pInv 𝒢 G A C = pInv 𝒢 G p pInv 𝒢 G x C t P t p I C t A I x t P
146 42 ad2antrr φ x A L B C L x 𝒢 G A L B p P pInv 𝒢 G A C = pInv 𝒢 G p pInv 𝒢 G x C t P t p I C t A I x C P
147 simprl φ x A L B C L x 𝒢 G A L B p P pInv 𝒢 G A C = pInv 𝒢 G p pInv 𝒢 G x C t P t p I C t A I x t p I C
148 1 2 3 143 144 145 146 147 tgbtwncom φ x A L B C L x 𝒢 G A L B p P pInv 𝒢 G A C = pInv 𝒢 G p pInv 𝒢 G x C t P t p I C t A I x t C I p
149 130 142 148 jca32 φ x A L B C L x 𝒢 G A L B p P pInv 𝒢 G A C = pInv 𝒢 G p pInv 𝒢 G x C t P t p I C t A I x A L p 𝒢 G A L B t A L B A = B t C I p
150 149 ex φ x A L B C L x 𝒢 G A L B p P pInv 𝒢 G A C = pInv 𝒢 G p pInv 𝒢 G x C t P t p I C t A I x A L p 𝒢 G A L B t A L B A = B t C I p
151 150 reximdva φ x A L B C L x 𝒢 G A L B p P pInv 𝒢 G A C = pInv 𝒢 G p pInv 𝒢 G x C t P t p I C t A I x t P A L p 𝒢 G A L B t A L B A = B t C I p
152 53 151 mpd φ x A L B C L x 𝒢 G A L B p P pInv 𝒢 G A C = pInv 𝒢 G p pInv 𝒢 G x C t P A L p 𝒢 G A L B t A L B A = B t C I p
153 r19.42v t P A L p 𝒢 G A L B t A L B A = B t C I p A L p 𝒢 G A L B t P t A L B A = B t C I p
154 152 153 sylib φ x A L B C L x 𝒢 G A L B p P pInv 𝒢 G A C = pInv 𝒢 G p pInv 𝒢 G x C A L p 𝒢 G A L B t P t A L B A = B t C I p
155 154 ex φ x A L B C L x 𝒢 G A L B p P pInv 𝒢 G A C = pInv 𝒢 G p pInv 𝒢 G x C A L p 𝒢 G A L B t P t A L B A = B t C I p
156 155 reximdva φ x A L B C L x 𝒢 G A L B p P pInv 𝒢 G A C = pInv 𝒢 G p pInv 𝒢 G x C p P A L p 𝒢 G A L B t P t A L B A = B t C I p
157 38 156 mpd φ x A L B C L x 𝒢 G A L B p P A L p 𝒢 G A L B t P t A L B A = B t C I p
158 1 2 3 4 5 14 8 10 footex φ x A L B C L x 𝒢 G A L B
159 157 158 r19.29a φ p P A L p 𝒢 G A L B t P t A L B A = B t C I p