brcgr - Metamath Proof Explorer

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

Theorem brcgr 24068

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 4697	. . 3
2		opex 4697	. . 3
3		eleq1 2513	. . . . . 6
4	3	anbi1d 704	. . . . 5 $/\$ $/\$
5		fveq2 5852	. . . . . . . . . 10
6	5	fveq1d 5854	. . . . . . . . 9
7		fveq2 5852	. . . . . . . . . 10
8	7	fveq1d 5854	. . . . . . . . 9
9	6, 8	oveq12d 6295	. . . . . . . 8
10	9	oveq1d 6292	. . . . . . 7
11	10	sumeq2sdv 13500	. . . . . 6
12	11	eqeq1d 2443	. . . . 5
13	4, 12	anbi12d 710	. . . 4 $/\$ $/\$ $/\$ $/\$
14	13	rexbidv 2952	. . 3 $/\$ $/\$ $/\$ $/\$
15		eleq1 2513	. . . . . 6
16	15	anbi2d 703	. . . . 5 $/\$ $/\$
17		fveq2 5852	. . . . . . . . . 10
18	17	fveq1d 5854	. . . . . . . . 9
19		fveq2 5852	. . . . . . . . . 10
20	19	fveq1d 5854	. . . . . . . . 9
21	18, 20	oveq12d 6295	. . . . . . . 8
22	21	oveq1d 6292	. . . . . . 7
23	22	sumeq2sdv 13500	. . . . . 6
24	23	eqeq2d 2455	. . . . 5
25	16, 24	anbi12d 710	. . . 4 $/\$ $/\$ $/\$ $/\$
26	25	rexbidv 2952	. . 3 $/\$ $/\$ $/\$ $/\$
27		df-cgr 24061	. . 3 Cgr $/\$ $/\$
28	1, 2, 14, 26, 27	brab 4756	. 2 Cgr $/\$ $/\$
29		opelxp2 5019	. . . . . . . . . . 11
30	29	ad2antll 728	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$
31		simplrr 760	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$
32		eedimeq 24066	. . . . . . . . . 10 $/\$
33	30, 31, 32	syl2anc 661	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$
34	33	adantlr 714	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
35		oveq2 6285	. . . . . . . . . 10
36	35	sumeq1d 13497	. . . . . . . . 9
37	35	sumeq1d 13497	. . . . . . . . 9
38	36, 37	eqeq12d 2463	. . . . . . . 8
39	34, 38	syl 16	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
40		op1stg 6793	. . . . . . . . . . . . 13 $/\$
41	40	fveq1d 5854	. . . . . . . . . . . 12 $/\$
42		op2ndg 6794	. . . . . . . . . . . . 13 $/\$
43	42	fveq1d 5854	. . . . . . . . . . . 12 $/\$
44	41, 43	oveq12d 6295	. . . . . . . . . . 11 $/\$
45	44	oveq1d 6292	. . . . . . . . . 10 $/\$
46	45	sumeq2sdv 13500	. . . . . . . . 9 $/\$
47		op1stg 6793	. . . . . . . . . . . . 13 $/\$
48	47	fveq1d 5854	. . . . . . . . . . . 12 $/\$
49		op2ndg 6794	. . . . . . . . . . . . 13 $/\$
50	49	fveq1d 5854	. . . . . . . . . . . 12 $/\$
51	48, 50	oveq12d 6295	. . . . . . . . . . 11 $/\$
52	51	oveq1d 6292	. . . . . . . . . 10 $/\$
53	52	sumeq2sdv 13500	. . . . . . . . 9 $/\$
54	46, 53	eqeqan12d 2464	. . . . . . . 8 $/\$ $/\$ $/\$
55	54	ad2antrr 725	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
56	39, 55	bitrd 253	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
57	56	biimpd 207	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
58	57	expimpd 603	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
59	58	rexlimdva 2933	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$
60		eleenn 24064	. . . . 5
61	60	ad2antll 728	. . . 4 $/\$ $/\$ $/\$
62		opelxpi 5017	. . . . . . . . 9 $/\$
63		opelxpi 5017	. . . . . . . . 9 $/\$
64	62, 63	anim12i 566	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
65	64	adantr 465	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$
66	54	biimpar 485	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
67	65, 66	jca 532	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
68		fveq2 5852	. . . . . . . . . . 11
69	68	sqxpeqd 5011	. . . . . . . . . 10
70	69	eleq2d 2511	. . . . . . . . 9
71	69	eleq2d 2511	. . . . . . . . 9
72	70, 71	anbi12d 710	. . . . . . . 8 $/\$ $/\$
73	72, 38	anbi12d 710	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
74	73	rspcev 3194	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$
75	67, 74	sylan2 474	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
76	75	exp32 605	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$
77	61, 76	mpcom 36	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$
78	59, 77	impbid 191	. 2 $/\$ $/\$ $/\$ $/\$ $/\$
79	28, 78	syl5bb 257	1 $/\$ $/\$ $/\$ Cgr

Colors of variables: wff setvar class

Syntax hints:

wi 4

wb 184 $/\$ wa 369

wceq 1381

wcel 1802

wrex 2792

cop 4016 class class class wbr 4433

cxp 4983

cfv 5574 (class class class)co 6277

c1st 6779

c2nd 6780

c1 9491

cmin 9805

cn 10537

c2 10586

cfz 11676

cexp 12140

csu 13482

cee 24056 Cgrccgr 24058

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1603 ax-4 1616 ax-5 1689 ax-6 1732 ax-7 1774 ax-8 1804 ax-9 1806 ax-10 1821 ax-11 1826 ax-12 1838 ax-13 1983 ax-ext 2419 ax-sep 4554 ax-nul 4562 ax-pow 4611 ax-pr 4672 ax-un 6573 ax-cnex 9546 ax-resscn 9547 ax-1cn 9548 ax-icn 9549 ax-addcl 9550 ax-addrcl 9551 ax-mulcl 9552 ax-mulrcl 9553 ax-mulcom 9554 ax-addass 9555 ax-mulass 9556 ax-distr 9557 ax-i2m1 9558 ax-1ne0 9559 ax-1rid 9560 ax-rnegex 9561 ax-rrecex 9562 ax-cnre 9563 ax-pre-lttri 9564 ax-pre-lttrn 9565 ax-pre-ltadd 9566 ax-pre-mulgt0 9567

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 973 df-3an 974 df-tru 1384 df-fal 1387 df-ex 1598 df-nf 1602 df-sb 1725 df-eu 2270 df-mo 2271 df-clab 2427 df-cleq 2433 df-clel 2436 df-nfc 2591 df-ne 2638 df-nel 2639 df-ral 2796 df-rex 2797 df-reu 2798 df-rab 2800 df-v 3095 df-sbc 3312 df-csb 3418 df-dif 3461 df-un 3463 df-in 3465 df-ss 3472 df-pss 3474 df-nul 3768 df-if 3923 df-pw 3995 df-sn 4011 df-pr 4013 df-tp 4015 df-op 4017 df-uni 4231 df-iun 4313 df-br 4434 df-opab 4492 df-mpt 4493 df-tr 4527 df-eprel 4777 df-id 4781 df-po 4786 df-so 4787 df-fr 4824 df-we 4826 df-ord 4867 df-on 4868 df-lim 4869 df-suc 4870 df-xp 4991 df-rel 4992 df-cnv 4993 df-co 4994 df-dm 4995 df-rn 4996 df-res 4997 df-ima 4998 df-iota 5537 df-fun 5576 df-fn 5577 df-f 5578 df-f1 5579 df-fo 5580 df-f1o 5581 df-fv 5582 df-riota 6238 df-ov 6280 df-oprab 6281 df-mpt2 6282 df-om 6682 df-1st 6781 df-2nd 6782 df-recs 7040 df-rdg 7074 df-er 7309 df-map 7420 df-en 7515 df-dom 7516 df-sdom 7517 df-pnf 9628 df-mnf 9629 df-xr 9630 df-ltxr 9631 df-le 9632 df-sub 9807 df-neg 9808 df-nn 10538 df-n0 10797 df-z 10866 df-uz 11086 df-fz 11677 df-seq 12082 df-sum 13483 df-ee 24059 df-cgr 24061

This theorem is referenced by: axcgrrflx 24082 axcgrtr 24083 axcgrid 24084 axsegcon 24095 ax5seglem3 24099 ax5seglem6 24102 ax5seg 24106 axlowdimlem17 24126 ecgrtg 24151

W3C validator