Metamath Proof Explorer

Theorem tgaas1h

Description: tgaas1 with the constructed point H still explicit: the case split on F = H . Equal, and the side equality is a substitution; distinct, and tgaasne closes the branch. BOTH branches are proved -- assuming F = H would be assuming the theorem. (Contributed by JAG , 12-Aug-2026)

Ref Expression
Hypotheses tgaascgra.p 
|- P = ( Base ` G )
tgaascgra.m 
|- .- = ( dist ` G )
tgaascgra.i 
|- I = ( Itv ` G )
tgaascgra.l 
|- L = ( LineG ` G )
tgaascgra.k 
|- K = ( hlG ` G )
tgaascgra.g 
|- ( ph -> G e. TarskiG )
tgaascgra.a 
|- ( ph -> A e. P )
tgaascgra.b 
|- ( ph -> B e. P )
tgaascgra.c 
|- ( ph -> C e. P )
tgaascgra.d 
|- ( ph -> D e. P )
tgaascgra.e 
|- ( ph -> E e. P )
tgaascgra.f 
|- ( ph -> F e. P )
tgaascgra.h 
|- ( ph -> H e. P )
tgaascgra.ncol 
|- ( ph -> -. ( C e. ( A L B ) \/ A = B ) )
tgaascgra.1 
|- ( ph -> ( A .- B ) = ( D .- E ) )
tgaascgra.2 
|- ( ph -> <" A B C "> ( cgrA ` G ) <" D E F "> )
tgaascgra.3 
|- ( ph -> <" B C A "> ( cgrA ` G ) <" E F D "> )
tgaascgra.4 
|- ( ph -> H ( K ` E ) F )
tgaascgra.5 
|- ( ph -> ( E .- H ) = ( B .- C ) )
Assertion tgaas1h 
|- ( ph -> ( B .- C ) = ( E .- F ) )

Proof

Step Hyp Ref Expression
1 tgaascgra.p 
 |-  P = ( Base ` G )
2 tgaascgra.m 
 |-  .- = ( dist ` G )
3 tgaascgra.i 
 |-  I = ( Itv ` G )
4 tgaascgra.l 
 |-  L = ( LineG ` G )
5 tgaascgra.k 
 |-  K = ( hlG ` G )
6 tgaascgra.g 
 |-  ( ph -> G e. TarskiG )
7 tgaascgra.a 
 |-  ( ph -> A e. P )
8 tgaascgra.b 
 |-  ( ph -> B e. P )
9 tgaascgra.c 
 |-  ( ph -> C e. P )
10 tgaascgra.d 
 |-  ( ph -> D e. P )
11 tgaascgra.e 
 |-  ( ph -> E e. P )
12 tgaascgra.f 
 |-  ( ph -> F e. P )
13 tgaascgra.h 
 |-  ( ph -> H e. P )
14 tgaascgra.ncol 
 |-  ( ph -> -. ( C e. ( A L B ) \/ A = B ) )
15 tgaascgra.1 
 |-  ( ph -> ( A .- B ) = ( D .- E ) )
16 tgaascgra.2 
 |-  ( ph -> <" A B C "> ( cgrA ` G ) <" D E F "> )
17 tgaascgra.3 
 |-  ( ph -> <" B C A "> ( cgrA ` G ) <" E F D "> )
18 tgaascgra.4 
 |-  ( ph -> H ( K ` E ) F )
19 tgaascgra.5 
 |-  ( ph -> ( E .- H ) = ( B .- C ) )
20 19 eqcomd 
 |-  ( ph -> ( B .- C ) = ( E .- H ) )
21 20 adantr 
 |-  ( ( ph /\ F = H ) -> ( B .- C ) = ( E .- H ) )
22 simpr 
 |-  ( ( ph /\ F = H ) -> F = H )
23 22 oveq2d 
 |-  ( ( ph /\ F = H ) -> ( E .- F ) = ( E .- H ) )
24 23 eqcomd 
 |-  ( ( ph /\ F = H ) -> ( E .- H ) = ( E .- F ) )
25 21 24 eqtrd 
 |-  ( ( ph /\ F = H ) -> ( B .- C ) = ( E .- F ) )
26 6 adantr 
 |-  ( ( ph /\ F =/= H ) -> G e. TarskiG )
27 10 adantr 
 |-  ( ( ph /\ F =/= H ) -> D e. P )
28 11 adantr 
 |-  ( ( ph /\ F =/= H ) -> E e. P )
29 12 adantr 
 |-  ( ( ph /\ F =/= H ) -> F e. P )
30 13 adantr 
 |-  ( ( ph /\ F =/= H ) -> H e. P )
31 1 3 2 6 7 8 9 10 11 12 16 4 14 cgrancol 
 |-  ( ph -> -. ( F e. ( D L E ) \/ D = E ) )
32 1 4 3 6 10 11 12 31 ncolrot1 
 |-  ( ph -> -. ( D e. ( E L F ) \/ E = F ) )
33 32 adantr 
 |-  ( ( ph /\ F =/= H ) -> -. ( D e. ( E L F ) \/ E = F ) )
34 18 adantr 
 |-  ( ( ph /\ F =/= H ) -> H ( K ` E ) F )
35 simpr 
 |-  ( ( ph /\ F =/= H ) -> F =/= H )
36 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 tgaascgra 
 |-  ( ph -> <" D F E "> ( cgrA ` G ) <" D H E "> )
37 36 adantr 
 |-  ( ( ph /\ F =/= H ) -> <" D F E "> ( cgrA ` G ) <" D H E "> )
38 1 2 3 4 5 26 27 28 29 30 33 34 35 37 tgaasne 
 |-  ( ( ph /\ F =/= H ) -> ( B .- C ) = ( E .- F ) )
39 25 38 pm2.61dane 
 |-  ( ph -> ( B .- C ) = ( E .- F ) )