Users' Mathboxes Mathbox for Scott Fenton < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  cgrtr Unicode version

Theorem cgrtr 23992
Description: Transitivity law for congruence. Theorem 2.3 of [Schwabhauser] p. 27. (Contributed by Scott Fenton, 24-Sep-2013.)
Assertion
Ref Expression
cgrtr  |-  ( ( N  e.  NN  /\  ( A  e.  ( EE `  N )  /\  B  e.  ( EE `  N )  /\  C  e.  ( EE `  N
) )  /\  ( D  e.  ( EE `  N )  /\  E  e.  ( EE `  N
)  /\  F  e.  ( EE `  N ) ) )  ->  (
( <. A ,  B >.Cgr
<. C ,  D >.  /\ 
<. C ,  D >.Cgr <. E ,  F >. )  ->  <. A ,  B >.Cgr
<. E ,  F >. ) )

Proof of Theorem cgrtr
StepHypRef Expression
1 simp1 960 . . 3  |-  ( ( N  e.  NN  /\  ( A  e.  ( EE `  N )  /\  B  e.  ( EE `  N )  /\  C  e.  ( EE `  N
) )  /\  ( D  e.  ( EE `  N )  /\  E  e.  ( EE `  N
)  /\  F  e.  ( EE `  N ) ) )  ->  N  e.  NN )
2 simp23 995 . . 3  |-  ( ( N  e.  NN  /\  ( A  e.  ( EE `  N )  /\  B  e.  ( EE `  N )  /\  C  e.  ( EE `  N
) )  /\  ( D  e.  ( EE `  N )  /\  E  e.  ( EE `  N
)  /\  F  e.  ( EE `  N ) ) )  ->  C  e.  ( EE `  N
) )
3 simp31 996 . . 3  |-  ( ( N  e.  NN  /\  ( A  e.  ( EE `  N )  /\  B  e.  ( EE `  N )  /\  C  e.  ( EE `  N
) )  /\  ( D  e.  ( EE `  N )  /\  E  e.  ( EE `  N
)  /\  F  e.  ( EE `  N ) ) )  ->  D  e.  ( EE `  N
) )
4 simp21 993 . . 3  |-  ( ( N  e.  NN  /\  ( A  e.  ( EE `  N )  /\  B  e.  ( EE `  N )  /\  C  e.  ( EE `  N
) )  /\  ( D  e.  ( EE `  N )  /\  E  e.  ( EE `  N
)  /\  F  e.  ( EE `  N ) ) )  ->  A  e.  ( EE `  N
) )
5 simp22 994 . . 3  |-  ( ( N  e.  NN  /\  ( A  e.  ( EE `  N )  /\  B  e.  ( EE `  N )  /\  C  e.  ( EE `  N
) )  /\  ( D  e.  ( EE `  N )  /\  E  e.  ( EE `  N
)  /\  F  e.  ( EE `  N ) ) )  ->  B  e.  ( EE `  N
) )
6 simp32 997 . . 3  |-  ( ( N  e.  NN  /\  ( A  e.  ( EE `  N )  /\  B  e.  ( EE `  N )  /\  C  e.  ( EE `  N
) )  /\  ( D  e.  ( EE `  N )  /\  E  e.  ( EE `  N
)  /\  F  e.  ( EE `  N ) ) )  ->  E  e.  ( EE `  N
) )
7 simp33 998 . . 3  |-  ( ( N  e.  NN  /\  ( A  e.  ( EE `  N )  /\  B  e.  ( EE `  N )  /\  C  e.  ( EE `  N
) )  /\  ( D  e.  ( EE `  N )  /\  E  e.  ( EE `  N
)  /\  F  e.  ( EE `  N ) ) )  ->  F  e.  ( EE `  N
) )
8 simprl 735 . . . 4  |-  ( ( ( N  e.  NN  /\  ( A  e.  ( EE `  N )  /\  B  e.  ( EE `  N )  /\  C  e.  ( EE `  N ) )  /\  ( D  e.  ( EE `  N )  /\  E  e.  ( EE `  N
)  /\  F  e.  ( EE `  N ) ) )  /\  ( <. A ,  B >.Cgr <. C ,  D >.  /\ 
<. C ,  D >.Cgr <. E ,  F >. ) )  ->  <. A ,  B >.Cgr <. C ,  D >. )
91, 4, 5, 2, 3, 8cgrcomand 23991 . . 3  |-  ( ( ( N  e.  NN  /\  ( A  e.  ( EE `  N )  /\  B  e.  ( EE `  N )  /\  C  e.  ( EE `  N ) )  /\  ( D  e.  ( EE `  N )  /\  E  e.  ( EE `  N
)  /\  F  e.  ( EE `  N ) ) )  /\  ( <. A ,  B >.Cgr <. C ,  D >.  /\ 
<. C ,  D >.Cgr <. E ,  F >. ) )  ->  <. C ,  D >.Cgr <. A ,  B >. )
10 simprr 736 . . 3  |-  ( ( ( N  e.  NN  /\  ( A  e.  ( EE `  N )  /\  B  e.  ( EE `  N )  /\  C  e.  ( EE `  N ) )  /\  ( D  e.  ( EE `  N )  /\  E  e.  ( EE `  N
)  /\  F  e.  ( EE `  N ) ) )  /\  ( <. A ,  B >.Cgr <. C ,  D >.  /\ 
<. C ,  D >.Cgr <. E ,  F >. ) )  ->  <. C ,  D >.Cgr <. E ,  F >. )
111, 2, 3, 4, 5, 6, 7, 9, 10cgrtr4and 23986 . 2  |-  ( ( ( N  e.  NN  /\  ( A  e.  ( EE `  N )  /\  B  e.  ( EE `  N )  /\  C  e.  ( EE `  N ) )  /\  ( D  e.  ( EE `  N )  /\  E  e.  ( EE `  N
)  /\  F  e.  ( EE `  N ) ) )  /\  ( <. A ,  B >.Cgr <. C ,  D >.  /\ 
<. C ,  D >.Cgr <. E ,  F >. ) )  ->  <. A ,  B >.Cgr <. E ,  F >. )
1211ex 425 1  |-  ( ( N  e.  NN  /\  ( A  e.  ( EE `  N )  /\  B  e.  ( EE `  N )  /\  C  e.  ( EE `  N
) )  /\  ( D  e.  ( EE `  N )  /\  E  e.  ( EE `  N
)  /\  F  e.  ( EE `  N ) ) )  ->  (
( <. A ,  B >.Cgr
<. C ,  D >.  /\ 
<. C ,  D >.Cgr <. E ,  F >. )  ->  <. A ,  B >.Cgr
<. E ,  F >. ) )
Colors of variables: wff set class
Syntax hints:    -> wi 6    /\ wa 360    /\ w3a 939    e. wcel 1621   <.cop 3618   class class class wbr 3998   ` cfv 5195   NNcn 9715   EEcee 23893  Cgrccgr 23895
This theorem is referenced by:  cgrtrand  23993
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-13 1625  ax-14 1626  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1927  ax-ext 2239  ax-sep 4116  ax-nul 4124  ax-pow 4161  ax-pr 4187  ax-un 4485  ax-cnex 8762  ax-resscn 8763  ax-1cn 8764  ax-icn 8765  ax-addcl 8766  ax-addrcl 8767  ax-mulcl 8768  ax-mulrcl 8769  ax-mulcom 8770  ax-addass 8771  ax-mulass 8772  ax-distr 8773  ax-i2m1 8774  ax-1ne0 8775  ax-1rid 8776  ax-rnegex 8777  ax-rrecex 8778  ax-cnre 8779  ax-pre-lttri 8780  ax-pre-lttrn 8781  ax-pre-ltadd 8782  ax-pre-mulgt0 8783
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3or 940  df-3an 941  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1884  df-eu 2122  df-mo 2123  df-clab 2245  df-cleq 2251  df-clel 2254  df-nfc 2383  df-ne 2423  df-nel 2424  df-ral 2523  df-rex 2524  df-reu 2525  df-rab 2527  df-v 2765  df-sbc 2967  df-csb 3057  df-dif 3130  df-un 3132  df-in 3134  df-ss 3141  df-pss 3143  df-nul 3431  df-if 3541  df-pw 3602  df-sn 3621  df-pr 3622  df-tp 3623  df-op 3624  df-uni 3803  df-iun 3882  df-br 3999  df-opab 4053  df-mpt 4054  df-tr 4089  df-eprel 4278  df-id 4282  df-po 4287  df-so 4288  df-fr 4325  df-we 4327  df-ord 4368  df-on 4369  df-lim 4370  df-suc 4371  df-om 4630  df-xp 4668  df-rel 4669  df-cnv 4670  df-co 4671  df-dm 4672  df-rn 4673  df-res 4674  df-ima 4675  df-fun 5197  df-fn 5198  df-f 5199  df-f1 5200  df-fo 5201  df-f1o 5202  df-fv 5203  df-ov 5796  df-oprab 5797  df-mpt2 5798  df-1st 6057  df-2nd 6058  df-iota 6226  df-riota 6273  df-recs 6357  df-rdg 6392  df-er 6629  df-map 6743  df-en 6833  df-dom 6834  df-sdom 6835  df-pnf 8838  df-mnf 8839  df-xr 8840  df-ltxr 8841  df-le 8842  df-sub 9008  df-neg 9009  df-nn 9716  df-2 9773  df-n0 9935  df-z 9994  df-uz 10200  df-fz 10751  df-seq 11015  df-exp 11073  df-sum 12126  df-ee 23896  df-cgr 23898
  Copyright terms: Public domain W3C validator