brcgr - Metamath Proof Explorer

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

Theorem brcgr 24986

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 4681	. . 3
2		opex 4681	. . 3
3		eleq1 2528	. . . . . 6
4	3	anbi1d 716	. . . . 5 $/\$ $/\$
5		fveq2 5892	. . . . . . . . . 10
6	5	fveq1d 5894	. . . . . . . . 9
7		fveq2 5892	. . . . . . . . . 10
8	7	fveq1d 5894	. . . . . . . . 9
9	6, 8	oveq12d 6338	. . . . . . . 8
10	9	oveq1d 6335	. . . . . . 7
11	10	sumeq2sdv 13825	. . . . . 6
12	11	eqeq1d 2464	. . . . 5
13	4, 12	anbi12d 722	. . . 4 $/\$ $/\$ $/\$ $/\$
14	13	rexbidv 2913	. . 3 $/\$ $/\$ $/\$ $/\$
15		eleq1 2528	. . . . . 6
16	15	anbi2d 715	. . . . 5 $/\$ $/\$
17		fveq2 5892	. . . . . . . . . 10
18	17	fveq1d 5894	. . . . . . . . 9
19		fveq2 5892	. . . . . . . . . 10
20	19	fveq1d 5894	. . . . . . . . 9
21	18, 20	oveq12d 6338	. . . . . . . 8
22	21	oveq1d 6335	. . . . . . 7
23	22	sumeq2sdv 13825	. . . . . 6
24	23	eqeq2d 2472	. . . . 5
25	16, 24	anbi12d 722	. . . 4 $/\$ $/\$ $/\$ $/\$
26	25	rexbidv 2913	. . 3 $/\$ $/\$ $/\$ $/\$
27		df-cgr 24979	. . 3 Cgr $/\$ $/\$
28	1, 2, 14, 26, 27	brab 4741	. 2 Cgr $/\$ $/\$
29		opelxp2 4890	. . . . . . . . . . 11
30	29	ad2antll 740	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$
31		simplrr 776	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$
32		eedimeq 24984	. . . . . . . . . 10 $/\$
33	30, 31, 32	syl2anc 671	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$
34	33	adantlr 726	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
35		oveq2 6328	. . . . . . . . . 10
36	35	sumeq1d 13822	. . . . . . . . 9
37	35	sumeq1d 13822	. . . . . . . . 9
38	36, 37	eqeq12d 2477	. . . . . . . 8
39	34, 38	syl 17	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
40		op1stg 6837	. . . . . . . . . . . . 13 $/\$
41	40	fveq1d 5894	. . . . . . . . . . . 12 $/\$
42		op2ndg 6838	. . . . . . . . . . . . 13 $/\$
43	42	fveq1d 5894	. . . . . . . . . . . 12 $/\$
44	41, 43	oveq12d 6338	. . . . . . . . . . 11 $/\$
45	44	oveq1d 6335	. . . . . . . . . 10 $/\$
46	45	sumeq2sdv 13825	. . . . . . . . 9 $/\$
47		op1stg 6837	. . . . . . . . . . . . 13 $/\$
48	47	fveq1d 5894	. . . . . . . . . . . 12 $/\$
49		op2ndg 6838	. . . . . . . . . . . . 13 $/\$
50	49	fveq1d 5894	. . . . . . . . . . . 12 $/\$
51	48, 50	oveq12d 6338	. . . . . . . . . . 11 $/\$
52	51	oveq1d 6335	. . . . . . . . . 10 $/\$
53	52	sumeq2sdv 13825	. . . . . . . . 9 $/\$
54	46, 53	eqeqan12d 2478	. . . . . . . 8 $/\$ $/\$ $/\$
55	54	ad2antrr 737	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
56	39, 55	bitrd 261	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
57	56	biimpd 212	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
58	57	expimpd 612	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
59	58	rexlimdva 2891	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$
60		eleenn 24982	. . . . 5
61	60	ad2antll 740	. . . 4 $/\$ $/\$ $/\$
62		opelxpi 4888	. . . . . . . . 9 $/\$
63		opelxpi 4888	. . . . . . . . 9 $/\$
64	62, 63	anim12i 574	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
65	64	adantr 471	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$
66	54	biimpar 492	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
67	65, 66	jca 539	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
68		fveq2 5892	. . . . . . . . . . 11
69	68	sqxpeqd 4882	. . . . . . . . . 10
70	69	eleq2d 2525	. . . . . . . . 9
71	69	eleq2d 2525	. . . . . . . . 9
72	70, 71	anbi12d 722	. . . . . . . 8 $/\$ $/\$
73	72, 38	anbi12d 722	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
74	73	rspcev 3162	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$
75	67, 74	sylan2 481	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
76	75	exp32 614	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$
77	61, 76	mpcom 37	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$
78	59, 77	impbid 195	. 2 $/\$ $/\$ $/\$ $/\$ $/\$
79	28, 78	syl5bb 265	1 $/\$ $/\$ $/\$ Cgr

Colors of variables: wff setvar class

Syntax hints:

wi 4

wb 189 $/\$ wa 375

wceq 1455

wcel 1898

wrex 2750

cop 3986 class class class wbr 4418

cxp 4854

cfv 5605 (class class class)co 6320

c1st 6823

c2nd 6824

c1 9571

cmin 9891

cn 10642

c2 10692

cfz 11819

cexp 12310

csu 13807

cee 24974 Cgrccgr 24976

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1680 ax-4 1693 ax-5 1769 ax-6 1816 ax-7 1862 ax-8 1900 ax-9 1907 ax-10 1926 ax-11 1931 ax-12 1944 ax-13 2102 ax-ext 2442 ax-sep 4541 ax-nul 4550 ax-pow 4598 ax-pr 4656 ax-un 6615 ax-cnex 9626 ax-resscn 9627 ax-1cn 9628 ax-icn 9629 ax-addcl 9630 ax-addrcl 9631 ax-mulcl 9632 ax-mulrcl 9633 ax-mulcom 9634 ax-addass 9635 ax-mulass 9636 ax-distr 9637 ax-i2m1 9638 ax-1ne0 9639 ax-1rid 9640 ax-rnegex 9641 ax-rrecex 9642 ax-cnre 9643 ax-pre-lttri 9644 ax-pre-lttrn 9645 ax-pre-ltadd 9646 ax-pre-mulgt0 9647

This theorem depends on definitions: df-bi 190 df-or 376 df-an 377 df-3or 992 df-3an 993 df-tru 1458 df-fal 1461 df-ex 1675 df-nf 1679 df-sb 1809 df-eu 2314 df-mo 2315 df-clab 2449 df-cleq 2455 df-clel 2458 df-nfc 2592 df-ne 2635 df-nel 2636 df-ral 2754 df-rex 2755 df-reu 2756 df-rab 2758 df-v 3059 df-sbc 3280 df-csb 3376 df-dif 3419 df-un 3421 df-in 3423 df-ss 3430 df-pss 3432 df-nul 3744 df-if 3894 df-pw 3965 df-sn 3981 df-pr 3983 df-tp 3985 df-op 3987 df-uni 4213 df-iun 4294 df-br 4419 df-opab 4478 df-mpt 4479 df-tr 4514 df-eprel 4767 df-id 4771 df-po 4777 df-so 4778 df-fr 4815 df-we 4817 df-xp 4862 df-rel 4863 df-cnv 4864 df-co 4865 df-dm 4866 df-rn 4867 df-res 4868 df-ima 4869 df-pred 5403 df-ord 5449 df-on 5450 df-lim 5451 df-suc 5452 df-iota 5569 df-fun 5607 df-fn 5608 df-f 5609 df-f1 5610 df-fo 5611 df-f1o 5612 df-fv 5613 df-riota 6282 df-ov 6323 df-oprab 6324 df-mpt2 6325 df-om 6725 df-1st 6825 df-2nd 6826 df-wrecs 7059 df-recs 7121 df-rdg 7159 df-er 7394 df-map 7505 df-en 7601 df-dom 7602 df-sdom 7603 df-pnf 9708 df-mnf 9709 df-xr 9710 df-ltxr 9711 df-le 9712 df-sub 9893 df-neg 9894 df-nn 10643 df-n0 10904 df-z 10972 df-uz 11194 df-fz 11820 df-seq 12252 df-sum 13808 df-ee 24977 df-cgr 24979

This theorem is referenced by: axcgrrflx 25000 axcgrtr 25001 axcgrid 25002 axsegcon 25013 ax5seglem3 25017 ax5seglem6 25020 ax5seg 25024 axlowdimlem17 25044 ecgrtg 25069

W3C validator