brcgr - Metamath Proof Explorer

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

Theorem brcgr 23145

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 4555	. . 3
2		opex 4555	. . 3
3		eleq1 2502	. . . . . 6
4	3	anbi1d 704	. . . . 5 $/\$ $/\$
5		fveq2 5690	. . . . . . . . . 10
6	5	fveq1d 5692	. . . . . . . . 9
7		fveq2 5690	. . . . . . . . . 10
8	7	fveq1d 5692	. . . . . . . . 9
9	6, 8	oveq12d 6108	. . . . . . . 8
10	9	oveq1d 6105	. . . . . . 7
11	10	sumeq2sdv 13180	. . . . . 6
12	11	eqeq1d 2450	. . . . 5
13	4, 12	anbi12d 710	. . . 4 $/\$ $/\$ $/\$ $/\$
14	13	rexbidv 2735	. . 3 $/\$ $/\$ $/\$ $/\$
15		eleq1 2502	. . . . . 6
16	15	anbi2d 703	. . . . 5 $/\$ $/\$
17		fveq2 5690	. . . . . . . . . 10
18	17	fveq1d 5692	. . . . . . . . 9
19		fveq2 5690	. . . . . . . . . 10
20	19	fveq1d 5692	. . . . . . . . 9
21	18, 20	oveq12d 6108	. . . . . . . 8
22	21	oveq1d 6105	. . . . . . 7
23	22	sumeq2sdv 13180	. . . . . 6
24	23	eqeq2d 2453	. . . . 5
25	16, 24	anbi12d 710	. . . 4 $/\$ $/\$ $/\$ $/\$
26	25	rexbidv 2735	. . 3 $/\$ $/\$ $/\$ $/\$
27		df-cgr 23138	. . 3 Cgr $/\$ $/\$
28	1, 2, 14, 26, 27	brab 4610	. 2 Cgr $/\$ $/\$
29		opelxp2 4872	. . . . . . . . . . 11
30	29	ad2antll 728	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$
31		simplrr 760	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$
32		eedimeq 23143	. . . . . . . . . 10 $/\$
33	30, 31, 32	syl2anc 661	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$
34	33	adantlr 714	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
35		oveq2 6098	. . . . . . . . . 10
36	35	sumeq1d 13177	. . . . . . . . 9
37	35	sumeq1d 13177	. . . . . . . . 9
38	36, 37	eqeq12d 2456	. . . . . . . 8
39	34, 38	syl 16	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
40		op1stg 6588	. . . . . . . . . . . . 13 $/\$
41	40	fveq1d 5692	. . . . . . . . . . . 12 $/\$
42		op2ndg 6589	. . . . . . . . . . . . 13 $/\$
43	42	fveq1d 5692	. . . . . . . . . . . 12 $/\$
44	41, 43	oveq12d 6108	. . . . . . . . . . 11 $/\$
45	44	oveq1d 6105	. . . . . . . . . 10 $/\$
46	45	sumeq2sdv 13180	. . . . . . . . 9 $/\$
47		op1stg 6588	. . . . . . . . . . . . 13 $/\$
48	47	fveq1d 5692	. . . . . . . . . . . 12 $/\$
49		op2ndg 6589	. . . . . . . . . . . . 13 $/\$
50	49	fveq1d 5692	. . . . . . . . . . . 12 $/\$
51	48, 50	oveq12d 6108	. . . . . . . . . . 11 $/\$
52	51	oveq1d 6105	. . . . . . . . . 10 $/\$
53	52	sumeq2sdv 13180	. . . . . . . . 9 $/\$
54	46, 53	eqeqan12d 2457	. . . . . . . 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 2840	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$
60		eleenn 23141	. . . . 5
61	60	ad2antll 728	. . . 4 $/\$ $/\$ $/\$
62		opelxpi 4870	. . . . . . . . 9 $/\$
63		opelxpi 4870	. . . . . . . . 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 5690	. . . . . . . . . . 11
69	68, 68	xpeq12d 4864	. . . . . . . . . 10
70	69	eleq2d 2509	. . . . . . . . 9
71	69	eleq2d 2509	. . . . . . . . 9
72	70, 71	anbi12d 710	. . . . . . . 8 $/\$ $/\$
73	72, 38	anbi12d 710	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
74	73	rspcev 3072	. . . . . 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 1369

wcel 1756

wrex 2715

cop 3882 class class class wbr 4291

cxp 4837

cfv 5417 (class class class)co 6090

c1st 6574

c2nd 6575

c1 9282

cmin 9594

cn 10321

c2 10370

cfz 11436

cexp 11864

csu 13162

cee 23133 Cgrccgr 23135

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1591 ax-4 1602 ax-5 1670 ax-6 1708 ax-7 1728 ax-8 1758 ax-9 1760 ax-10 1775 ax-11 1780 ax-12 1792 ax-13 1943 ax-ext 2423 ax-sep 4412 ax-nul 4420 ax-pow 4469 ax-pr 4530 ax-un 6371 ax-cnex 9337 ax-resscn 9338 ax-1cn 9339 ax-icn 9340 ax-addcl 9341 ax-addrcl 9342 ax-mulcl 9343 ax-mulrcl 9344 ax-mulcom 9345 ax-addass 9346 ax-mulass 9347 ax-distr 9348 ax-i2m1 9349 ax-1ne0 9350 ax-1rid 9351 ax-rnegex 9352 ax-rrecex 9353 ax-cnre 9354 ax-pre-lttri 9355 ax-pre-lttrn 9356 ax-pre-ltadd 9357 ax-pre-mulgt0 9358

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 966 df-3an 967 df-tru 1372 df-fal 1375 df-ex 1587 df-nf 1590 df-sb 1701 df-eu 2257 df-mo 2258 df-clab 2429 df-cleq 2435 df-clel 2438 df-nfc 2567 df-ne 2607 df-nel 2608 df-ral 2719 df-rex 2720 df-reu 2721 df-rab 2723 df-v 2973 df-sbc 3186 df-csb 3288 df-dif 3330 df-un 3332 df-in 3334 df-ss 3341 df-pss 3343 df-nul 3637 df-if 3791 df-pw 3861 df-sn 3877 df-pr 3879 df-tp 3881 df-op 3883 df-uni 4091 df-iun 4172 df-br 4292 df-opab 4350 df-mpt 4351 df-tr 4385 df-eprel 4631 df-id 4635 df-po 4640 df-so 4641 df-fr 4678 df-we 4680 df-ord 4721 df-on 4722 df-lim 4723 df-suc 4724 df-xp 4845 df-rel 4846 df-cnv 4847 df-co 4848 df-dm 4849 df-rn 4850 df-res 4851 df-ima 4852 df-iota 5380 df-fun 5419 df-fn 5420 df-f 5421 df-f1 5422 df-fo 5423 df-f1o 5424 df-fv 5425 df-riota 6051 df-ov 6093 df-oprab 6094 df-mpt2 6095 df-om 6476 df-1st 6576 df-2nd 6577 df-recs 6831 df-rdg 6865 df-er 7100 df-map 7215 df-en 7310 df-dom 7311 df-sdom 7312 df-pnf 9419 df-mnf 9420 df-xr 9421 df-ltxr 9422 df-le 9423 df-sub 9596 df-neg 9597 df-nn 10322 df-n0 10579 df-z 10646 df-uz 10861 df-fz 11437 df-seq 11806 df-sum 13163 df-ee 23136 df-cgr 23138

This theorem is referenced by: axcgrrflx 23159 axcgrtr 23160 axcgrid 23161 axsegcon 23172 ax5seglem3 23176 ax5seglem6 23179 ax5seg 23183 axlowdimlem17 23203 ecgrtg 23228

W3C validator