Metamath Proof Explorer

Theorem leawittrg

Description: Target-side leA witness transport: move a witness inside <" D E F "> across a congruent target angle <" X Y Z "> , carrying the angle <" H U J "> copied at that witness with it. (Contributed by JAG, 12-Aug-2026)

Ref Expression
Hypotheses leawittrg.p 
|- P = ( Base ` G )
leawittrg.i 
|- I = ( Itv ` G )
leawittrg.k 
|- K = ( hlG ` G )
leawittrg.g 
|- ( ph -> G e. TarskiG )
leawittrg.d 
|- ( ph -> D e. P )
leawittrg.e 
|- ( ph -> E e. P )
leawittrg.f 
|- ( ph -> F e. P )
leawittrg.x 
|- ( ph -> X e. P )
leawittrg.y 
|- ( ph -> Y e. P )
leawittrg.z 
|- ( ph -> Z e. P )
leawittrg.h 
|- ( ph -> H e. P )
leawittrg.u 
|- ( ph -> U e. P )
leawittrg.j 
|- ( ph -> J e. P )
leawittrg.w 
|- ( ph -> W e. P )
leawittrg.in 
|- ( ph -> W ( inA ` G ) <" D E F "> )
leawittrg.cga 
|- ( ph -> <" H U J "> ( cgrA ` G ) <" D E W "> )
leawittrg.cgb 
|- ( ph -> <" D E F "> ( cgrA ` G ) <" X Y Z "> )
Assertion leawittrg 
|- ( ph -> E. v e. P ( v ( inA ` G ) <" X Y Z "> /\ <" H U J "> ( cgrA ` G ) <" X Y v "> ) )

Proof

Step Hyp Ref Expression
1 leawittrg.p 
 |-  P = ( Base ` G )
2 leawittrg.i 
 |-  I = ( Itv ` G )
3 leawittrg.k 
 |-  K = ( hlG ` G )
4 leawittrg.g 
 |-  ( ph -> G e. TarskiG )
5 leawittrg.d 
 |-  ( ph -> D e. P )
6 leawittrg.e 
 |-  ( ph -> E e. P )
7 leawittrg.f 
 |-  ( ph -> F e. P )
8 leawittrg.x 
 |-  ( ph -> X e. P )
9 leawittrg.y 
 |-  ( ph -> Y e. P )
10 leawittrg.z 
 |-  ( ph -> Z e. P )
11 leawittrg.h 
 |-  ( ph -> H e. P )
12 leawittrg.u 
 |-  ( ph -> U e. P )
13 leawittrg.j 
 |-  ( ph -> J e. P )
14 leawittrg.w 
 |-  ( ph -> W e. P )
15 leawittrg.in 
 |-  ( ph -> W ( inA ` G ) <" D E F "> )
16 leawittrg.cga 
 |-  ( ph -> <" H U J "> ( cgrA ` G ) <" D E W "> )
17 leawittrg.cgb 
 |-  ( ph -> <" D E F "> ( cgrA ` G ) <" X Y Z "> )
18 simpr 
 |-  ( ( ( ph /\ v e. P ) /\ ( v ( inA ` G ) <" X Y Z "> /\ <" D E W "> ( cgrA ` G ) <" X Y v "> ) ) -> ( v ( inA ` G ) <" X Y Z "> /\ <" D E W "> ( cgrA ` G ) <" X Y v "> ) )
19 18 simpld 
 |-  ( ( ( ph /\ v e. P ) /\ ( v ( inA ` G ) <" X Y Z "> /\ <" D E W "> ( cgrA ` G ) <" X Y v "> ) ) -> v ( inA ` G ) <" X Y Z "> )
20 4 adantr 
 |-  ( ( ph /\ v e. P ) -> G e. TarskiG )
21 20 adantr 
 |-  ( ( ( ph /\ v e. P ) /\ ( v ( inA ` G ) <" X Y Z "> /\ <" D E W "> ( cgrA ` G ) <" X Y v "> ) ) -> G e. TarskiG )
22 11 adantr 
 |-  ( ( ph /\ v e. P ) -> H e. P )
23 22 adantr 
 |-  ( ( ( ph /\ v e. P ) /\ ( v ( inA ` G ) <" X Y Z "> /\ <" D E W "> ( cgrA ` G ) <" X Y v "> ) ) -> H e. P )
24 12 adantr 
 |-  ( ( ph /\ v e. P ) -> U e. P )
25 24 adantr 
 |-  ( ( ( ph /\ v e. P ) /\ ( v ( inA ` G ) <" X Y Z "> /\ <" D E W "> ( cgrA ` G ) <" X Y v "> ) ) -> U e. P )
26 13 adantr 
 |-  ( ( ph /\ v e. P ) -> J e. P )
27 26 adantr 
 |-  ( ( ( ph /\ v e. P ) /\ ( v ( inA ` G ) <" X Y Z "> /\ <" D E W "> ( cgrA ` G ) <" X Y v "> ) ) -> J e. P )
28 5 adantr 
 |-  ( ( ph /\ v e. P ) -> D e. P )
29 28 adantr 
 |-  ( ( ( ph /\ v e. P ) /\ ( v ( inA ` G ) <" X Y Z "> /\ <" D E W "> ( cgrA ` G ) <" X Y v "> ) ) -> D e. P )
30 6 adantr 
 |-  ( ( ph /\ v e. P ) -> E e. P )
31 30 adantr 
 |-  ( ( ( ph /\ v e. P ) /\ ( v ( inA ` G ) <" X Y Z "> /\ <" D E W "> ( cgrA ` G ) <" X Y v "> ) ) -> E e. P )
32 14 adantr 
 |-  ( ( ph /\ v e. P ) -> W e. P )
33 32 adantr 
 |-  ( ( ( ph /\ v e. P ) /\ ( v ( inA ` G ) <" X Y Z "> /\ <" D E W "> ( cgrA ` G ) <" X Y v "> ) ) -> W e. P )
34 16 adantr 
 |-  ( ( ph /\ v e. P ) -> <" H U J "> ( cgrA ` G ) <" D E W "> )
35 34 adantr 
 |-  ( ( ( ph /\ v e. P ) /\ ( v ( inA ` G ) <" X Y Z "> /\ <" D E W "> ( cgrA ` G ) <" X Y v "> ) ) -> <" H U J "> ( cgrA ` G ) <" D E W "> )
36 8 adantr 
 |-  ( ( ph /\ v e. P ) -> X e. P )
37 36 adantr 
 |-  ( ( ( ph /\ v e. P ) /\ ( v ( inA ` G ) <" X Y Z "> /\ <" D E W "> ( cgrA ` G ) <" X Y v "> ) ) -> X e. P )
38 9 adantr 
 |-  ( ( ph /\ v e. P ) -> Y e. P )
39 38 adantr 
 |-  ( ( ( ph /\ v e. P ) /\ ( v ( inA ` G ) <" X Y Z "> /\ <" D E W "> ( cgrA ` G ) <" X Y v "> ) ) -> Y e. P )
40 simpl 
 |-  ( ( ( ph /\ v e. P ) /\ ( v ( inA ` G ) <" X Y Z "> /\ <" D E W "> ( cgrA ` G ) <" X Y v "> ) ) -> ( ph /\ v e. P ) )
41 40 simprd 
 |-  ( ( ( ph /\ v e. P ) /\ ( v ( inA ` G ) <" X Y Z "> /\ <" D E W "> ( cgrA ` G ) <" X Y v "> ) ) -> v e. P )
42 18 simprd 
 |-  ( ( ( ph /\ v e. P ) /\ ( v ( inA ` G ) <" X Y Z "> /\ <" D E W "> ( cgrA ` G ) <" X Y v "> ) ) -> <" D E W "> ( cgrA ` G ) <" X Y v "> )
43 1 2 21 3 23 25 27 29 31 33 35 37 39 41 42 cgratr 
 |-  ( ( ( ph /\ v e. P ) /\ ( v ( inA ` G ) <" X Y Z "> /\ <" D E W "> ( cgrA ` G ) <" X Y v "> ) ) -> <" H U J "> ( cgrA ` G ) <" X Y v "> )
44 19 43 jca 
 |-  ( ( ( ph /\ v e. P ) /\ ( v ( inA ` G ) <" X Y Z "> /\ <" D E W "> ( cgrA ` G ) <" X Y v "> ) ) -> ( v ( inA ` G ) <" X Y Z "> /\ <" H U J "> ( cgrA ` G ) <" X Y v "> ) )
45 1 2 3 4 5 6 7 8 9 10 14 15 17 cgrainag 
 |-  ( ph -> E. v e. P ( v ( inA ` G ) <" X Y Z "> /\ <" D E W "> ( cgrA ` G ) <" X Y v "> ) )
46 44 45 reximddv3 
 |-  ( ph -> E. v e. P ( v ( inA ` G ) <" X Y Z "> /\ <" H U J "> ( cgrA ` G ) <" X Y v "> ) )