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

Theorem brcgr3 24669
Description: Binary relationship form of the three-place congruence predicate. (Contributed by Scott Fenton, 4-Oct-2013.)
Assertion
Ref Expression
brcgr3  |-  ( ( 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 ,  C >. >.Cgr3 <. D ,  <. E ,  F >. >.  <->  ( <. A ,  B >.Cgr <. D ,  E >.  /\  <. A ,  C >.Cgr <. D ,  F >.  /\  <. B ,  C >.Cgr
<. E ,  F >. ) ) )

Proof of Theorem brcgr3
Dummy variables  a 
b  c  d  e  f  n  p  q are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 opeq1 3796 . . . 4  |-  ( a  =  A  ->  <. a ,  b >.  =  <. A ,  b >. )
21breq1d 4033 . . 3  |-  ( a  =  A  ->  ( <. a ,  b >.Cgr <. d ,  e >.  <->  <. A ,  b >.Cgr <.
d ,  e >.
) )
3 opeq1 3796 . . . 4  |-  ( a  =  A  ->  <. a ,  c >.  =  <. A ,  c >. )
43breq1d 4033 . . 3  |-  ( a  =  A  ->  ( <. a ,  c >.Cgr <. d ,  f >.  <->  <. A ,  c >.Cgr <.
d ,  f >.
) )
52, 43anbi12d 1253 . 2  |-  ( a  =  A  ->  (
( <. a ,  b
>.Cgr <. d ,  e
>.  /\  <. a ,  c
>.Cgr <. d ,  f
>.  /\  <. b ,  c
>.Cgr <. e ,  f
>. )  <->  ( <. A , 
b >.Cgr <. d ,  e
>.  /\  <. A ,  c
>.Cgr <. d ,  f
>.  /\  <. b ,  c
>.Cgr <. e ,  f
>. ) ) )
6 opeq2 3797 . . . 4  |-  ( b  =  B  ->  <. A , 
b >.  =  <. A ,  B >. )
76breq1d 4033 . . 3  |-  ( b  =  B  ->  ( <. A ,  b >.Cgr <. d ,  e >.  <->  <. A ,  B >.Cgr <.
d ,  e >.
) )
8 opeq1 3796 . . . 4  |-  ( b  =  B  ->  <. b ,  c >.  =  <. B ,  c >. )
98breq1d 4033 . . 3  |-  ( b  =  B  ->  ( <. b ,  c >.Cgr <. e ,  f >.  <->  <. B ,  c >.Cgr <.
e ,  f >.
) )
107, 93anbi13d 1254 . 2  |-  ( b  =  B  ->  (
( <. A ,  b
>.Cgr <. d ,  e
>.  /\  <. A ,  c
>.Cgr <. d ,  f
>.  /\  <. b ,  c
>.Cgr <. e ,  f
>. )  <->  ( <. A ,  B >.Cgr <. d ,  e
>.  /\  <. A ,  c
>.Cgr <. d ,  f
>.  /\  <. B ,  c
>.Cgr <. e ,  f
>. ) ) )
11 opeq2 3797 . . . 4  |-  ( c  =  C  ->  <. A , 
c >.  =  <. A ,  C >. )
1211breq1d 4033 . . 3  |-  ( c  =  C  ->  ( <. A ,  c >.Cgr <. d ,  f >.  <->  <. A ,  C >.Cgr <.
d ,  f >.
) )
13 opeq2 3797 . . . 4  |-  ( c  =  C  ->  <. B , 
c >.  =  <. B ,  C >. )
1413breq1d 4033 . . 3  |-  ( c  =  C  ->  ( <. B ,  c >.Cgr <. e ,  f >.  <->  <. B ,  C >.Cgr <.
e ,  f >.
) )
1512, 143anbi23d 1255 . 2  |-  ( c  =  C  ->  (
( <. A ,  B >.Cgr
<. d ,  e >.  /\  <. A ,  c
>.Cgr <. d ,  f
>.  /\  <. B ,  c
>.Cgr <. e ,  f
>. )  <->  ( <. A ,  B >.Cgr <. d ,  e
>.  /\  <. A ,  C >.Cgr
<. d ,  f >.  /\  <. B ,  C >.Cgr
<. e ,  f >.
) ) )
16 opeq1 3796 . . . 4  |-  ( d  =  D  ->  <. d ,  e >.  =  <. D ,  e >. )
1716breq2d 4035 . . 3  |-  ( d  =  D  ->  ( <. A ,  B >.Cgr <.
d ,  e >.  <->  <. A ,  B >.Cgr <. D ,  e >. ) )
18 opeq1 3796 . . . 4  |-  ( d  =  D  ->  <. d ,  f >.  =  <. D ,  f >. )
1918breq2d 4035 . . 3  |-  ( d  =  D  ->  ( <. A ,  C >.Cgr <.
d ,  f >.  <->  <. A ,  C >.Cgr <. D ,  f >. ) )
2017, 193anbi12d 1253 . 2  |-  ( d  =  D  ->  (
( <. A ,  B >.Cgr
<. d ,  e >.  /\  <. A ,  C >.Cgr
<. d ,  f >.  /\  <. B ,  C >.Cgr
<. e ,  f >.
)  <->  ( <. A ,  B >.Cgr <. D ,  e
>.  /\  <. A ,  C >.Cgr
<. D ,  f >.  /\  <. B ,  C >.Cgr
<. e ,  f >.
) ) )
21 opeq2 3797 . . . 4  |-  ( e  =  E  ->  <. D , 
e >.  =  <. D ,  E >. )
2221breq2d 4035 . . 3  |-  ( e  =  E  ->  ( <. A ,  B >.Cgr <. D ,  e >.  <->  <. A ,  B >.Cgr <. D ,  E >. ) )
23 opeq1 3796 . . . 4  |-  ( e  =  E  ->  <. e ,  f >.  =  <. E ,  f >. )
2423breq2d 4035 . . 3  |-  ( e  =  E  ->  ( <. B ,  C >.Cgr <.
e ,  f >.  <->  <. B ,  C >.Cgr <. E ,  f >. ) )
2522, 243anbi13d 1254 . 2  |-  ( e  =  E  ->  (
( <. A ,  B >.Cgr
<. D ,  e >.  /\  <. A ,  C >.Cgr
<. D ,  f >.  /\  <. B ,  C >.Cgr
<. e ,  f >.
)  <->  ( <. A ,  B >.Cgr <. D ,  E >.  /\  <. A ,  C >.Cgr
<. D ,  f >.  /\  <. B ,  C >.Cgr
<. E ,  f >.
) ) )
26 opeq2 3797 . . . 4  |-  ( f  =  F  ->  <. D , 
f >.  =  <. D ,  F >. )
2726breq2d 4035 . . 3  |-  ( f  =  F  ->  ( <. A ,  C >.Cgr <. D ,  f >.  <->  <. A ,  C >.Cgr <. D ,  F >. ) )
28 opeq2 3797 . . . 4  |-  ( f  =  F  ->  <. E , 
f >.  =  <. E ,  F >. )
2928breq2d 4035 . . 3  |-  ( f  =  F  ->  ( <. B ,  C >.Cgr <. E ,  f >.  <->  <. B ,  C >.Cgr <. E ,  F >. ) )
3027, 293anbi23d 1255 . 2  |-  ( f  =  F  ->  (
( <. A ,  B >.Cgr
<. D ,  E >.  /\ 
<. A ,  C >.Cgr <. D ,  f >.  /\ 
<. B ,  C >.Cgr <. E ,  f >. )  <-> 
( <. A ,  B >.Cgr
<. D ,  E >.  /\ 
<. A ,  C >.Cgr <. D ,  F >.  /\ 
<. B ,  C >.Cgr <. E ,  F >. ) ) )
31 fveq2 5525 . 2  |-  ( n  =  N  ->  ( EE `  n )  =  ( EE `  N
) )
32 df-cgr3 24663 . 2  |- Cgr3  =  { <. p ,  q >.  |  E. n  e.  NN  E. a  e.  ( EE
`  n ) E. b  e.  ( EE
`  n ) E. c  e.  ( EE
`  n ) E. d  e.  ( EE
`  n ) E. e  e.  ( EE
`  n ) E. f  e.  ( EE
`  n ) ( p  =  <. a ,  <. b ,  c
>. >.  /\  q  =  <. d ,  <. e ,  f >. >.  /\  ( <. a ,  b >.Cgr <. d ,  e >.  /\  <. a ,  c
>.Cgr <. d ,  f
>.  /\  <. b ,  c
>.Cgr <. e ,  f
>. ) ) }
335, 10, 15, 20, 25, 30, 31, 32br6 24114 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 ,  C >. >.Cgr3 <. D ,  <. E ,  F >. >.  <->  ( <. A ,  B >.Cgr <. D ,  E >.  /\  <. A ,  C >.Cgr <. D ,  F >.  /\  <. B ,  C >.Cgr
<. E ,  F >. ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ w3a 934    = wceq 1623    e. wcel 1684   <.cop 3643   class class class wbr 4023   ` cfv 5255   NNcn 9746   EEcee 24516  Cgrccgr 24518  Cgr3ccgr3 24659
This theorem is referenced by:  cgr3permute3  24670  cgr3permute1  24671  cgr3tr4  24675  cgr3com  24676  cgr3rflx  24677  cgrxfr  24678  btwnxfr  24679  lineext  24699  brofs2  24700  brifs2  24701  endofsegid  24708  btwnconn1lem4  24713  btwnconn1lem8  24717  btwnconn1lem11  24720  brsegle2  24732  seglecgr12im  24733  segletr  24737
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-14 1688  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-sep 4141  ax-nul 4149  ax-pr 4214
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-eu 2147  df-mo 2148  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ne 2448  df-ral 2548  df-rex 2549  df-rab 2552  df-v 2790  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456  df-if 3566  df-sn 3646  df-pr 3647  df-op 3649  df-uni 3828  df-br 4024  df-opab 4078  df-iota 5219  df-fv 5263  df-cgr3 24663
  Copyright terms: Public domain W3C validator