Metamath Proof Explorer

Theorem inagcgratrgw

Description: inagcgratrgmain with the existential introduced at its own witness Q . Split out so that the substitution instance is built once, at the top level, rather than under the existential eliminations that produce S , T and Q . (Contributed by JAG, 12-Aug-2026)

Ref Expression
Hypotheses inagcgratrgmain.p 
|- P = ( Base ` G )
inagcgratrgmain.i 
|- I = ( Itv ` G )
inagcgratrgmain.k 
|- K = ( hlG ` G )
inagcgratrgmain.g 
|- ( ph -> G e. TarskiG )
inagcgratrgmain.d 
|- ( ph -> D e. P )
inagcgratrgmain.e 
|- ( ph -> E e. P )
inagcgratrgmain.w 
|- ( ph -> W e. P )
inagcgratrgmain.x 
|- ( ph -> X e. P )
inagcgratrgmain.y 
|- ( ph -> Y e. P )
inagcgratrgmain.z 
|- ( ph -> Z e. P )
inagcgratrgmain.j 
|- ( ph -> J e. P )
inagcgratrgmain.s 
|- ( ph -> S e. P )
inagcgratrgmain.t 
|- ( ph -> T e. P )
inagcgratrgmain.q 
|- ( ph -> Q e. P )
inagcgratrgmain.de 
|- ( ph -> D =/= E )
inagcgratrgmain.jw 
|- ( ph -> J ( K ` E ) W )
inagcgratrgmain.sx 
|- ( ph -> S ( K ` Y ) X )
inagcgratrgmain.tz 
|- ( ph -> T ( K ` Y ) Z )
inagcgratrgmain.q1 
|- ( ph -> Q e. ( S I T ) )
inagcgratrgmain.sub 
|- ( ph -> <" D E J "> ( cgrG ` G ) <" S Y Q "> )
Assertion inagcgratrgw 
|- ( ph -> E. v e. P ( v ( inA ` G ) <" X Y Z "> /\ <" D E W "> ( cgrA ` G ) <" X Y v "> ) )

Proof

Step Hyp Ref Expression
1 inagcgratrgmain.p 
 |-  P = ( Base ` G )
2 inagcgratrgmain.i 
 |-  I = ( Itv ` G )
3 inagcgratrgmain.k 
 |-  K = ( hlG ` G )
4 inagcgratrgmain.g 
 |-  ( ph -> G e. TarskiG )
5 inagcgratrgmain.d 
 |-  ( ph -> D e. P )
6 inagcgratrgmain.e 
 |-  ( ph -> E e. P )
7 inagcgratrgmain.w 
 |-  ( ph -> W e. P )
8 inagcgratrgmain.x 
 |-  ( ph -> X e. P )
9 inagcgratrgmain.y 
 |-  ( ph -> Y e. P )
10 inagcgratrgmain.z 
 |-  ( ph -> Z e. P )
11 inagcgratrgmain.j 
 |-  ( ph -> J e. P )
12 inagcgratrgmain.s 
 |-  ( ph -> S e. P )
13 inagcgratrgmain.t 
 |-  ( ph -> T e. P )
14 inagcgratrgmain.q 
 |-  ( ph -> Q e. P )
15 inagcgratrgmain.de 
 |-  ( ph -> D =/= E )
16 inagcgratrgmain.jw 
 |-  ( ph -> J ( K ` E ) W )
17 inagcgratrgmain.sx 
 |-  ( ph -> S ( K ` Y ) X )
18 inagcgratrgmain.tz 
 |-  ( ph -> T ( K ` Y ) Z )
19 inagcgratrgmain.q1 
 |-  ( ph -> Q e. ( S I T ) )
20 inagcgratrgmain.sub 
 |-  ( ph -> <" D E J "> ( cgrG ` G ) <" S Y Q "> )
21 simpr 
 |-  ( ( ph /\ v = Q ) -> v = Q )
22 21 breq1d 
 |-  ( ( ph /\ v = Q ) -> ( v ( inA ` G ) <" X Y Z "> <-> Q ( inA ` G ) <" X Y Z "> ) )
23 eqidd 
 |-  ( ( ph /\ v = Q ) -> X = X )
24 eqidd 
 |-  ( ( ph /\ v = Q ) -> Y = Y )
25 23 24 21 s3eqd 
 |-  ( ( ph /\ v = Q ) -> <" X Y v "> = <" X Y Q "> )
26 25 breq2d 
 |-  ( ( ph /\ v = Q ) -> ( <" D E W "> ( cgrA ` G ) <" X Y v "> <-> <" D E W "> ( cgrA ` G ) <" X Y Q "> ) )
27 22 26 anbi12d 
 |-  ( ( ph /\ v = Q ) -> ( ( v ( inA ` G ) <" X Y Z "> /\ <" D E W "> ( cgrA ` G ) <" X Y v "> ) <-> ( Q ( inA ` G ) <" X Y Z "> /\ <" D E W "> ( cgrA ` G ) <" X Y Q "> ) ) )
28 eqid 
 |-  ( dist ` G ) = ( dist ` G )
29 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 28 inagcgratrgmain 
 |-  ( ph -> ( Q ( inA ` G ) <" X Y Z "> /\ <" D E W "> ( cgrA ` G ) <" X Y Q "> ) )
30 14 27 29 rspcedvd 
 |-  ( ph -> E. v e. P ( v ( inA ` G ) <" X Y Z "> /\ <" D E W "> ( cgrA ` G ) <" X Y v "> ) )