dmncan1 - Mathbox for Jeff Madsen

	Mathbox for Jeff Madsen		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > dmncan1		Structured version Visualization version GIF version

Theorem dmncan1 37247

Description: Cancellation law for domains. (Contributed by Jeff Madsen, 6-Jan-2011.)

**Hypotheses**
Ref	Expression
dmncan.1	⊢ 𝐺 = (1^st ‘𝑅)
dmncan.2	⊢ 𝐻 = (2^nd ‘𝑅)
dmncan.3	⊢ 𝑋 = ran 𝐺
dmncan.4	⊢ 𝑍 = (GId‘𝐺)

**Assertion**
Ref	Expression
dmncan1	⊢ (((𝑅 ∈ Dmn ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) ∧ 𝐴 ≠ 𝑍) → ((𝐴𝐻𝐵) = (𝐴𝐻𝐶) → 𝐵 = 𝐶))

**Proof of Theorem dmncan1**
Step	Hyp	Ref	Expression
1		dmnrngo 37228	. . . . . 6 ⊢ (𝑅 ∈ Dmn → 𝑅 ∈ RingOps)
2		dmncan.1	. . . . . . 7 ⊢ 𝐺 = (1^st ‘𝑅)
3		dmncan.2	. . . . . . 7 ⊢ 𝐻 = (2^nd ‘𝑅)
4		dmncan.3	. . . . . . 7 ⊢ 𝑋 = ran 𝐺
5		eqid 2730	. . . . . . 7 ⊢ ( /_𝑔 ‘𝐺) = ( /_𝑔 ‘𝐺)
6	2, 3, 4, 5	rngosubdi 37116	. . . . . 6 ⊢ ((𝑅 ∈ RingOps ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → (𝐴𝐻(𝐵( /_𝑔 ‘𝐺)𝐶)) = ((𝐴𝐻𝐵)( /_𝑔 ‘𝐺)(𝐴𝐻𝐶)))
7	1, 6	sylan 578	. . . . 5 ⊢ ((𝑅 ∈ Dmn ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → (𝐴𝐻(𝐵( /_𝑔 ‘𝐺)𝐶)) = ((𝐴𝐻𝐵)( /_𝑔 ‘𝐺)(𝐴𝐻𝐶)))
8	7	adantr 479	. . . 4 ⊢ (((𝑅 ∈ Dmn ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) ∧ 𝐴 ≠ 𝑍) → (𝐴𝐻(𝐵( /_𝑔 ‘𝐺)𝐶)) = ((𝐴𝐻𝐵)( /_𝑔 ‘𝐺)(𝐴𝐻𝐶)))
9	8	eqeq1d 2732	. . 3 ⊢ (((𝑅 ∈ Dmn ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) ∧ 𝐴 ≠ 𝑍) → ((𝐴𝐻(𝐵( /_𝑔 ‘𝐺)𝐶)) = 𝑍 ↔ ((𝐴𝐻𝐵)( /_𝑔 ‘𝐺)(𝐴𝐻𝐶)) = 𝑍))
10	2	rngogrpo 37081	. . . . . . . . . . . 12 ⊢ (𝑅 ∈ RingOps → 𝐺 ∈ GrpOp)
11	1, 10	syl 17	. . . . . . . . . . 11 ⊢ (𝑅 ∈ Dmn → 𝐺 ∈ GrpOp)
12	4, 5	grpodivcl 30059	. . . . . . . . . . . 12 ⊢ ((𝐺 ∈ GrpOp ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋) → (𝐵( /_𝑔 ‘𝐺)𝐶) ∈ 𝑋)
13	12	3expb 1118	. . . . . . . . . . 11 ⊢ ((𝐺 ∈ GrpOp ∧ (𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → (𝐵( /_𝑔 ‘𝐺)𝐶) ∈ 𝑋)
14	11, 13	sylan 578	. . . . . . . . . 10 ⊢ ((𝑅 ∈ Dmn ∧ (𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → (𝐵( /_𝑔 ‘𝐺)𝐶) ∈ 𝑋)
15	14	adantlr 711	. . . . . . . . 9 ⊢ (((𝑅 ∈ Dmn ∧ 𝐴 ∈ 𝑋) ∧ (𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → (𝐵( /_𝑔 ‘𝐺)𝐶) ∈ 𝑋)
16		dmncan.4	. . . . . . . . . . . 12 ⊢ 𝑍 = (GId‘𝐺)
17	2, 3, 4, 16	dmnnzd 37246	. . . . . . . . . . 11 ⊢ ((𝑅 ∈ Dmn ∧ (𝐴 ∈ 𝑋 ∧ (𝐵( /_𝑔 ‘𝐺)𝐶) ∈ 𝑋 ∧ (𝐴𝐻(𝐵( /_𝑔 ‘𝐺)𝐶)) = 𝑍)) → (𝐴 = 𝑍 ∨ (𝐵( /_𝑔 ‘𝐺)𝐶) = 𝑍))
18	17	3exp2 1352	. . . . . . . . . 10 ⊢ (𝑅 ∈ Dmn → (𝐴 ∈ 𝑋 → ((𝐵( /_𝑔 ‘𝐺)𝐶) ∈ 𝑋 → ((𝐴𝐻(𝐵( /_𝑔 ‘𝐺)𝐶)) = 𝑍 → (𝐴 = 𝑍 ∨ (𝐵( /_𝑔 ‘𝐺)𝐶) = 𝑍)))))
19	18	imp31 416	. . . . . . . . 9 ⊢ (((𝑅 ∈ Dmn ∧ 𝐴 ∈ 𝑋) ∧ (𝐵( /_𝑔 ‘𝐺)𝐶) ∈ 𝑋) → ((𝐴𝐻(𝐵( /_𝑔 ‘𝐺)𝐶)) = 𝑍 → (𝐴 = 𝑍 ∨ (𝐵( /_𝑔 ‘𝐺)𝐶) = 𝑍)))
20	15, 19	syldan 589	. . . . . . . 8 ⊢ (((𝑅 ∈ Dmn ∧ 𝐴 ∈ 𝑋) ∧ (𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐴𝐻(𝐵( /_𝑔 ‘𝐺)𝐶)) = 𝑍 → (𝐴 = 𝑍 ∨ (𝐵( /_𝑔 ‘𝐺)𝐶) = 𝑍)))
21	20	exp43 435	. . . . . . 7 ⊢ (𝑅 ∈ Dmn → (𝐴 ∈ 𝑋 → (𝐵 ∈ 𝑋 → (𝐶 ∈ 𝑋 → ((𝐴𝐻(𝐵( /_𝑔 ‘𝐺)𝐶)) = 𝑍 → (𝐴 = 𝑍 ∨ (𝐵( /_𝑔 ‘𝐺)𝐶) = 𝑍))))))
22	21	3imp2 1347	. . . . . 6 ⊢ ((𝑅 ∈ Dmn ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐴𝐻(𝐵( /_𝑔 ‘𝐺)𝐶)) = 𝑍 → (𝐴 = 𝑍 ∨ (𝐵( /_𝑔 ‘𝐺)𝐶) = 𝑍)))
23		neor 3032	. . . . . 6 ⊢ ((𝐴 = 𝑍 ∨ (𝐵( /_𝑔 ‘𝐺)𝐶) = 𝑍) ↔ (𝐴 ≠ 𝑍 → (𝐵( /_𝑔 ‘𝐺)𝐶) = 𝑍))
24	22, 23	imbitrdi 250	. . . . 5 ⊢ ((𝑅 ∈ Dmn ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐴𝐻(𝐵( /_𝑔 ‘𝐺)𝐶)) = 𝑍 → (𝐴 ≠ 𝑍 → (𝐵( /_𝑔 ‘𝐺)𝐶) = 𝑍)))
25	24	com23 86	. . . 4 ⊢ ((𝑅 ∈ Dmn ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → (𝐴 ≠ 𝑍 → ((𝐴𝐻(𝐵( /_𝑔 ‘𝐺)𝐶)) = 𝑍 → (𝐵( /_𝑔 ‘𝐺)𝐶) = 𝑍)))
26	25	imp 405	. . 3 ⊢ (((𝑅 ∈ Dmn ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) ∧ 𝐴 ≠ 𝑍) → ((𝐴𝐻(𝐵( /_𝑔 ‘𝐺)𝐶)) = 𝑍 → (𝐵( /_𝑔 ‘𝐺)𝐶) = 𝑍))
27	9, 26	sylbird 259	. 2 ⊢ (((𝑅 ∈ Dmn ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) ∧ 𝐴 ≠ 𝑍) → (((𝐴𝐻𝐵)( /_𝑔 ‘𝐺)(𝐴𝐻𝐶)) = 𝑍 → (𝐵( /_𝑔 ‘𝐺)𝐶) = 𝑍))
28	11	adantr 479	. . . 4 ⊢ ((𝑅 ∈ Dmn ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → 𝐺 ∈ GrpOp)
29	2, 3, 4	rngocl 37072	. . . . . 6 ⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝐻𝐵) ∈ 𝑋)
30	29	3adant3r3 1182	. . . . 5 ⊢ ((𝑅 ∈ RingOps ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → (𝐴𝐻𝐵) ∈ 𝑋)
31	1, 30	sylan 578	. . . 4 ⊢ ((𝑅 ∈ Dmn ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → (𝐴𝐻𝐵) ∈ 𝑋)
32	2, 3, 4	rngocl 37072	. . . . . 6 ⊢ ((𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋) → (𝐴𝐻𝐶) ∈ 𝑋)
33	32	3adant3r2 1181	. . . . 5 ⊢ ((𝑅 ∈ RingOps ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → (𝐴𝐻𝐶) ∈ 𝑋)
34	1, 33	sylan 578	. . . 4 ⊢ ((𝑅 ∈ Dmn ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → (𝐴𝐻𝐶) ∈ 𝑋)
35	4, 16, 5	grpoeqdivid 37052	. . . 4 ⊢ ((𝐺 ∈ GrpOp ∧ (𝐴𝐻𝐵) ∈ 𝑋 ∧ (𝐴𝐻𝐶) ∈ 𝑋) → ((𝐴𝐻𝐵) = (𝐴𝐻𝐶) ↔ ((𝐴𝐻𝐵)( /_𝑔 ‘𝐺)(𝐴𝐻𝐶)) = 𝑍))
36	28, 31, 34, 35	syl3anc 1369	. . 3 ⊢ ((𝑅 ∈ Dmn ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐴𝐻𝐵) = (𝐴𝐻𝐶) ↔ ((𝐴𝐻𝐵)( /_𝑔 ‘𝐺)(𝐴𝐻𝐶)) = 𝑍))
37	36	adantr 479	. 2 ⊢ (((𝑅 ∈ Dmn ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) ∧ 𝐴 ≠ 𝑍) → ((𝐴𝐻𝐵) = (𝐴𝐻𝐶) ↔ ((𝐴𝐻𝐵)( /_𝑔 ‘𝐺)(𝐴𝐻𝐶)) = 𝑍))
38	4, 16, 5	grpoeqdivid 37052	. . . . . 6 ⊢ ((𝐺 ∈ GrpOp ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋) → (𝐵 = 𝐶 ↔ (𝐵( /_𝑔 ‘𝐺)𝐶) = 𝑍))
39	38	3expb 1118	. . . . 5 ⊢ ((𝐺 ∈ GrpOp ∧ (𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → (𝐵 = 𝐶 ↔ (𝐵( /_𝑔 ‘𝐺)𝐶) = 𝑍))
40	11, 39	sylan 578	. . . 4 ⊢ ((𝑅 ∈ Dmn ∧ (𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → (𝐵 = 𝐶 ↔ (𝐵( /_𝑔 ‘𝐺)𝐶) = 𝑍))
41	40	3adantr1 1167	. . 3 ⊢ ((𝑅 ∈ Dmn ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → (𝐵 = 𝐶 ↔ (𝐵( /_𝑔 ‘𝐺)𝐶) = 𝑍))
42	41	adantr 479	. 2 ⊢ (((𝑅 ∈ Dmn ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) ∧ 𝐴 ≠ 𝑍) → (𝐵 = 𝐶 ↔ (𝐵( /_𝑔 ‘𝐺)𝐶) = 𝑍))
43	27, 37, 42	3imtr4d 293	1 ⊢ (((𝑅 ∈ Dmn ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) ∧ 𝐴 ≠ 𝑍) → ((𝐴𝐻𝐵) = (𝐴𝐻𝐶) → 𝐵 = 𝐶))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 205 ∧ wa 394 ∨ wo 843 ∧ w3a 1085 = wceq 1539 ∈ wcel 2104 ≠ wne 2938 ran crn 5676 ‘cfv 6542 (class class class)co 7411 1^st c1st 7975 2^nd c2nd 7976 GrpOpcgr 30009 GIdcgi 30010 /_𝑔 cgs 30012 RingOpscrngo 37065 Dmncdmn 37218

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1911 ax-6 1969 ax-7 2009 ax-8 2106 ax-9 2114 ax-10 2135 ax-11 2152 ax-12 2169 ax-ext 2701 ax-rep 5284 ax-sep 5298 ax-nul 5305 ax-pow 5362 ax-pr 5426 ax-un 7727

This theorem depends on definitions: df-bi 206 df-an 395 df-or 844 df-3an 1087 df-tru 1542 df-fal 1552 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2532 df-eu 2561 df-clab 2708 df-cleq 2722 df-clel 2808 df-nfc 2883 df-ne 2939 df-ral 3060 df-rex 3069 df-rmo 3374 df-reu 3375 df-rab 3431 df-v 3474 df-sbc 3777 df-csb 3893 df-dif 3950 df-un 3952 df-in 3954 df-ss 3964 df-nul 4322 df-if 4528 df-pw 4603 df-sn 4628 df-pr 4630 df-op 4634 df-uni 4908 df-int 4950 df-iun 4998 df-br 5148 df-opab 5210 df-mpt 5231 df-id 5573 df-xp 5681 df-rel 5682 df-cnv 5683 df-co 5684 df-dm 5685 df-rn 5686 df-res 5687 df-ima 5688 df-suc 6369 df-iota 6494 df-fun 6544 df-fn 6545 df-f 6546 df-f1 6547 df-fo 6548 df-f1o 6549 df-fv 6550 df-riota 7367 df-ov 7414 df-oprab 7415 df-mpo 7416 df-1st 7977 df-2nd 7978 df-1o 8468 df-en 8942 df-grpo 30013 df-gid 30014 df-ginv 30015 df-gdiv 30016 df-ablo 30065 df-ass 37014 df-exid 37016 df-mgmOLD 37020 df-sgrOLD 37032 df-mndo 37038 df-rngo 37066 df-com2 37161 df-crngo 37165 df-idl 37181 df-pridl 37182 df-prrngo 37219 df-dmn 37220 df-igen 37231

This theorem is referenced by: dmncan2 37248

W3C validator