Metamath Proof Explorer


Theorem mideulem

Description: Lemma for mideu . We can assume mideulem.9 "without loss of generality". (Contributed by Thierry Arnoux, 25-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
mideu.s S = pInv 𝒢 G
mideu.1 φ A P
mideu.2 φ B P
mideulem.1 φ A B
mideulem.2 φ Q P
mideulem.3 φ O P
mideulem.4 φ T P
mideulem.5 φ A L B 𝒢 G Q L B
mideulem.6 φ A L B 𝒢 G A L O
mideulem.7 φ T A L B
mideulem.8 φ T Q I O
mideulem.9 φ A - ˙ O 𝒢 G B - ˙ Q
Assertion mideulem φ x P B = S x A

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 mideu.s S = pInv 𝒢 G
7 mideu.1 φ A P
8 mideu.2 φ B P
9 mideulem.1 φ A B
10 mideulem.2 φ Q P
11 mideulem.3 φ O P
12 mideulem.4 φ T P
13 mideulem.5 φ A L B 𝒢 G Q L B
14 mideulem.6 φ A L B 𝒢 G A L O
15 mideulem.7 φ T A L B
16 mideulem.8 φ T Q I O
17 mideulem.9 φ A - ˙ O 𝒢 G B - ˙ Q
18 simprrl φ r P r B I Q A - ˙ O = B - ˙ r x P B = S x A O = S x r B = S x A
19 5 ad2antrr φ r P r B I Q A - ˙ O = B - ˙ r G 𝒢 Tarski
20 7 ad2antrr φ r P r B I Q A - ˙ O = B - ˙ r A P
21 8 ad2antrr φ r P r B I Q A - ˙ O = B - ˙ r B P
22 9 ad2antrr φ r P r B I Q A - ˙ O = B - ˙ r A B
23 10 ad2antrr φ r P r B I Q A - ˙ O = B - ˙ r Q P
24 11 ad2antrr φ r P r B I Q A - ˙ O = B - ˙ r O P
25 12 ad2antrr φ r P r B I Q A - ˙ O = B - ˙ r T P
26 13 ad2antrr φ r P r B I Q A - ˙ O = B - ˙ r A L B 𝒢 G Q L B
27 14 ad2antrr φ r P r B I Q A - ˙ O = B - ˙ r A L B 𝒢 G A L O
28 15 ad2antrr φ r P r B I Q A - ˙ O = B - ˙ r T A L B
29 16 ad2antrr φ r P r B I Q A - ˙ O = B - ˙ r T Q I O
30 simplr φ r P r B I Q A - ˙ O = B - ˙ r r P
31 simprl φ r P r B I Q A - ˙ O = B - ˙ r r B I Q
32 simprr φ r P r B I Q A - ˙ O = B - ˙ r A - ˙ O = B - ˙ r
33 1 2 3 4 19 6 20 21 22 23 24 25 26 27 28 29 30 31 32 opphllem φ r P r B I Q A - ˙ O = B - ˙ r x P B = S x A O = S x r
34 18 33 reximddv φ r P r B I Q A - ˙ O = B - ˙ r x P B = S x A
35 eqid 𝒢 G = 𝒢 G
36 1 2 3 35 5 7 11 8 10 legov φ A - ˙ O 𝒢 G B - ˙ Q r P r B I Q A - ˙ O = B - ˙ r
37 17 36 mpbid φ r P r B I Q A - ˙ O = B - ˙ r
38 34 37 r19.29a φ x P B = S x A