brcgr - Metamath Proof Explorer

	Metamath Proof Explorer	< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > brcgr		Structured version Unicode version

Theorem brcgr 24817

Description: The binary relationship form of the congruence predicate. The statement

Cgr

should be read informally as "the

dimensional point

is as far from

is from

, or "the line segment

is congruent to the line segment

. This particular definition is encapsulated by Tarski's axioms later on. (Contributed by Scott Fenton, 3-Jun-2013.)

**Assertion**
Ref	Expression
brcgr	$/\$ $/\$ $/\$ Cgr

Distinct variable groups:

Proof of Theorem brcgr Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		opex 4677	. . 3
2		opex 4677	. . 3
3		eleq1 2492	. . . . . 6
4	3	anbi1d 709	. . . . 5 $/\$ $/\$
5		fveq2 5872	. . . . . . . . . 10
6	5	fveq1d 5874	. . . . . . . . 9
7		fveq2 5872	. . . . . . . . . 10
8	7	fveq1d 5874	. . . . . . . . 9
9	6, 8	oveq12d 6314	. . . . . . . 8
10	9	oveq1d 6311	. . . . . . 7
11	10	sumeq2sdv 13737	. . . . . 6
12	11	eqeq1d 2422	. . . . 5
13	4, 12	anbi12d 715	. . . 4 $/\$ $/\$ $/\$ $/\$
14	13	rexbidv 2937	. . 3 $/\$ $/\$ $/\$ $/\$
15		eleq1 2492	. . . . . 6
16	15	anbi2d 708	. . . . 5 $/\$ $/\$
17		fveq2 5872	. . . . . . . . . 10
18	17	fveq1d 5874	. . . . . . . . 9
19		fveq2 5872	. . . . . . . . . 10
20	19	fveq1d 5874	. . . . . . . . 9
21	18, 20	oveq12d 6314	. . . . . . . 8
22	21	oveq1d 6311	. . . . . . 7
23	22	sumeq2sdv 13737	. . . . . 6
24	23	eqeq2d 2434	. . . . 5
25	16, 24	anbi12d 715	. . . 4 $/\$ $/\$ $/\$ $/\$
26	25	rexbidv 2937	. . 3 $/\$ $/\$ $/\$ $/\$
27		df-cgr 24810	. . 3 Cgr $/\$ $/\$
28	1, 2, 14, 26, 27	brab 4735	. 2 Cgr $/\$ $/\$
29		opelxp2 4879	. . . . . . . . . . 11
30	29	ad2antll 733	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$
31		simplrr 769	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$
32		eedimeq 24815	. . . . . . . . . 10 $/\$
33	30, 31, 32	syl2anc 665	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$
34	33	adantlr 719	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
35		oveq2 6304	. . . . . . . . . 10
36	35	sumeq1d 13734	. . . . . . . . 9
37	35	sumeq1d 13734	. . . . . . . . 9
38	36, 37	eqeq12d 2442	. . . . . . . 8
39	34, 38	syl 17	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
40		op1stg 6810	. . . . . . . . . . . . 13 $/\$
41	40	fveq1d 5874	. . . . . . . . . . . 12 $/\$
42		op2ndg 6811	. . . . . . . . . . . . 13 $/\$
43	42	fveq1d 5874	. . . . . . . . . . . 12 $/\$
44	41, 43	oveq12d 6314	. . . . . . . . . . 11 $/\$
45	44	oveq1d 6311	. . . . . . . . . 10 $/\$
46	45	sumeq2sdv 13737	. . . . . . . . 9 $/\$
47		op1stg 6810	. . . . . . . . . . . . 13 $/\$
48	47	fveq1d 5874	. . . . . . . . . . . 12 $/\$
49		op2ndg 6811	. . . . . . . . . . . . 13 $/\$
50	49	fveq1d 5874	. . . . . . . . . . . 12 $/\$
51	48, 50	oveq12d 6314	. . . . . . . . . . 11 $/\$
52	51	oveq1d 6311	. . . . . . . . . 10 $/\$
53	52	sumeq2sdv 13737	. . . . . . . . 9 $/\$
54	46, 53	eqeqan12d 2443	. . . . . . . 8 $/\$ $/\$ $/\$
55	54	ad2antrr 730	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
56	39, 55	bitrd 256	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
57	56	biimpd 210	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
58	57	expimpd 606	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
59	58	rexlimdva 2915	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$
60		eleenn 24813	. . . . 5
61	60	ad2antll 733	. . . 4 $/\$ $/\$ $/\$
62		opelxpi 4877	. . . . . . . . 9 $/\$
63		opelxpi 4877	. . . . . . . . 9 $/\$
64	62, 63	anim12i 568	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
65	64	adantr 466	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$
66	54	biimpar 487	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
67	65, 66	jca 534	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
68		fveq2 5872	. . . . . . . . . . 11
69	68	sqxpeqd 4871	. . . . . . . . . 10
70	69	eleq2d 2490	. . . . . . . . 9
71	69	eleq2d 2490	. . . . . . . . 9
72	70, 71	anbi12d 715	. . . . . . . 8 $/\$ $/\$
73	72, 38	anbi12d 715	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
74	73	rspcev 3179	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$
75	67, 74	sylan2 476	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
76	75	exp32 608	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$
77	61, 76	mpcom 37	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$
78	59, 77	impbid 193	. 2 $/\$ $/\$ $/\$ $/\$ $/\$
79	28, 78	syl5bb 260	1 $/\$ $/\$ $/\$ Cgr

Colors of variables: wff setvar class

Syntax hints:

wi 4

wb 187 $/\$ wa 370

wceq 1437

wcel 1867

wrex 2774

cop 3999 class class class wbr 4417

cxp 4843

cfv 5592 (class class class)co 6296

c1st 6796

c2nd 6797

c1 9529

cmin 9849

cn 10598

c2 10648

cfz 11771

cexp 12258

csu 13719

cee 24805 Cgrccgr 24807

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1665 ax-4 1678 ax-5 1748 ax-6 1794 ax-7 1838 ax-8 1869 ax-9 1871 ax-10 1886 ax-11 1891 ax-12 1904 ax-13 2052 ax-ext 2398 ax-sep 4539 ax-nul 4547 ax-pow 4594 ax-pr 4652 ax-un 6588 ax-cnex 9584 ax-resscn 9585 ax-1cn 9586 ax-icn 9587 ax-addcl 9588 ax-addrcl 9589 ax-mulcl 9590 ax-mulrcl 9591 ax-mulcom 9592 ax-addass 9593 ax-mulass 9594 ax-distr 9595 ax-i2m1 9596 ax-1ne0 9597 ax-1rid 9598 ax-rnegex 9599 ax-rrecex 9600 ax-cnre 9601 ax-pre-lttri 9602 ax-pre-lttrn 9603 ax-pre-ltadd 9604 ax-pre-mulgt0 9605

This theorem depends on definitions: df-bi 188 df-or 371 df-an 372 df-3or 983 df-3an 984 df-tru 1440 df-fal 1443 df-ex 1660 df-nf 1664 df-sb 1787 df-eu 2267 df-mo 2268 df-clab 2406 df-cleq 2412 df-clel 2415 df-nfc 2570 df-ne 2618 df-nel 2619 df-ral 2778 df-rex 2779 df-reu 2780 df-rab 2782 df-v 3080 df-sbc 3297 df-csb 3393 df-dif 3436 df-un 3438 df-in 3440 df-ss 3447 df-pss 3449 df-nul 3759 df-if 3907 df-pw 3978 df-sn 3994 df-pr 3996 df-tp 3998 df-op 4000 df-uni 4214 df-iun 4295 df-br 4418 df-opab 4476 df-mpt 4477 df-tr 4512 df-eprel 4756 df-id 4760 df-po 4766 df-so 4767 df-fr 4804 df-we 4806 df-xp 4851 df-rel 4852 df-cnv 4853 df-co 4854 df-dm 4855 df-rn 4856 df-res 4857 df-ima 4858 df-pred 5390 df-ord 5436 df-on 5437 df-lim 5438 df-suc 5439 df-iota 5556 df-fun 5594 df-fn 5595 df-f 5596 df-f1 5597 df-fo 5598 df-f1o 5599 df-fv 5600 df-riota 6258 df-ov 6299 df-oprab 6300 df-mpt2 6301 df-om 6698 df-1st 6798 df-2nd 6799 df-wrecs 7027 df-recs 7089 df-rdg 7127 df-er 7362 df-map 7473 df-en 7569 df-dom 7570 df-sdom 7571 df-pnf 9666 df-mnf 9667 df-xr 9668 df-ltxr 9669 df-le 9670 df-sub 9851 df-neg 9852 df-nn 10599 df-n0 10859 df-z 10927 df-uz 11149 df-fz 11772 df-seq 12200 df-sum 13720 df-ee 24808 df-cgr 24810

This theorem is referenced by: axcgrrflx 24831 axcgrtr 24832 axcgrid 24833 axsegcon 24844 ax5seglem3 24848 ax5seglem6 24851 ax5seg 24855 axlowdimlem17 24875 ecgrtg 24900

W3C validator