mulgdirlem - Intuitionistic Logic Explorer

	Intuitionistic Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > mulgdirlem		Unicode version

Theorem mulgdirlem 13685

Description: Lemma for mulgdir 13686. (Contributed by Mario Carneiro, 13-Dec-2014.)

**Hypotheses**
Ref	Expression
mulgnndir.b
mulgnndir.t	._g
mulgnndir.p

**Assertion**
Ref	Expression
mulgdirlem	$/\$ $/\$ $/\$ $/\$

**Proof of Theorem mulgdirlem**
Step	Hyp	Ref	Expression
1		simpl1 1024	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
2	1	grpmndd 13541	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
3		simprl 529	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
4		simprr 531	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
5		simpl23 1101	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
6		mulgnndir.b	. . . . . 6
7		mulgnndir.t	. . . . . 6 ._g
8		mulgnndir.p	. . . . . 6
9	6, 7, 8	mulgnn0dir 13684	. . . . 5 $/\$ $/\$ $/\$
10	2, 3, 4, 5, 9	syl13anc 1273	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
11	10	anassrs 400	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
12		simpl1 1024	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
13		simp22 1055	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
14	13	adantr 276	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
15		simpl23 1101	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
16		eqid 2229	. . . . . . . . . . 11
17	6, 7, 16	mulgneg 13672	. . . . . . . . . 10 $/\$ $/\$
18	12, 14, 15, 17	syl3anc 1271	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
19	18	oveq1d 6015	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
20	6, 7	mulgcl 13671	. . . . . . . . . 10 $/\$ $/\$
21	12, 14, 15, 20	syl3anc 1271	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
22		eqid 2229	. . . . . . . . . 10
23	6, 8, 22, 16	grplinv 13578	. . . . . . . . 9 $/\$
24	12, 21, 23	syl2anc 411	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
25	19, 24	eqtrd 2262	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
26	25	oveq2d 6016	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
27		simpl3 1026	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
28		nn0z 9462	. . . . . . . . 9
29	27, 28	syl 14	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
30	6, 7	mulgcl 13671	. . . . . . . 8 $/\$ $/\$
31	12, 29, 15, 30	syl3anc 1271	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
32	6, 8, 22	grprid 13560	. . . . . . 7 $/\$
33	12, 31, 32	syl2anc 411	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
34	26, 33	eqtrd 2262	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
35		nn0z 9462	. . . . . . . . 9
36	35	ad2antll 491	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
37	6, 7	mulgcl 13671	. . . . . . . 8 $/\$ $/\$
38	12, 36, 15, 37	syl3anc 1271	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
39	6, 8	grpass 13537	. . . . . . 7 $/\$ $/\$ $/\$
40	12, 31, 38, 21, 39	syl13anc 1273	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
41	12	grpmndd 13541	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
42		simprr 531	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
43	6, 7, 8	mulgnn0dir 13684	. . . . . . . . 9 $/\$ $/\$ $/\$
44	41, 27, 42, 15, 43	syl13anc 1273	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
45		simp21 1054	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
46	45	zcnd 9566	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
47	13	zcnd 9566	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
48	46, 47	addcld 8162	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
49	48	adantr 276	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
50	47	adantr 276	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
51	49, 50	negsubd 8459	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
52	46	adantr 276	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
53	52, 50	pncand 8454	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
54	51, 53	eqtrd 2262	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
55	54	oveq1d 6015	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
56	44, 55	eqtr3d 2264	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
57	56	oveq1d 6015	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
58	40, 57	eqtr3d 2264	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
59	34, 58	eqtr3d 2264	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
60	59	anassrs 400	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
61		elznn0 9457	. . . . . 6 $/\$ $\/$
62	61	simprbi 275	. . . . 5 $\/$
63	13, 62	syl 14	. . . 4 $/\$ $/\$ $/\$ $/\$ $\/$
64	63	adantr 276	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $\/$
65	11, 60, 64	mpjaodan 803	. 2 $/\$ $/\$ $/\$ $/\$ $/\$
66		simpl1 1024	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$
67	45	adantr 276	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$
68		simpl23 1101	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$
69	6, 7	mulgcl 13671	. . . . 5 $/\$ $/\$
70	66, 67, 68, 69	syl3anc 1271	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$
71	67	znegcld 9567	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$
72	6, 7	mulgcl 13671	. . . . 5 $/\$ $/\$
73	66, 71, 68, 72	syl3anc 1271	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$
74	28	3ad2ant3 1044	. . . . . 6 $/\$ $/\$ $/\$ $/\$
75	74	adantr 276	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$
76	66, 75, 68, 30	syl3anc 1271	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$
77	6, 8	grpass 13537	. . . 4 $/\$ $/\$ $/\$
78	66, 70, 73, 76, 77	syl13anc 1273	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$
79	6, 7, 16	mulgneg 13672	. . . . . . . 8 $/\$ $/\$
80	66, 67, 68, 79	syl3anc 1271	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$
81	80	oveq2d 6016	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$
82	6, 8, 22, 16	grprinv 13579	. . . . . . 7 $/\$
83	66, 70, 82	syl2anc 411	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$
84	81, 83	eqtrd 2262	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$
85	84	oveq1d 6015	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$
86	6, 8, 22	grplid 13559	. . . . 5 $/\$
87	66, 76, 86	syl2anc 411	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$
88	85, 87	eqtrd 2262	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$
89	66	grpmndd 13541	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$
90		simpr 110	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$
91		simpl3 1026	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$
92	6, 7, 8	mulgnn0dir 13684	. . . . . 6 $/\$ $/\$ $/\$
93	89, 90, 91, 68, 92	syl13anc 1273	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$
94	46	adantr 276	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$
95	94	negcld 8440	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$
96	48	adantr 276	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$
97	95, 96	addcomd 8293	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$
98	96, 94	negsubd 8459	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$
99	47	adantr 276	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$
100	94, 99	pncan2d 8455	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$
101	97, 98, 100	3eqtrd 2266	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$
102	101	oveq1d 6015	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$
103	93, 102	eqtr3d 2264	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$
104	103	oveq2d 6016	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$
105	78, 88, 104	3eqtr3d 2270	. 2 $/\$ $/\$ $/\$ $/\$ $/\$
106		elznn0 9457	. . . 4 $/\$ $\/$
107	106	simprbi 275	. . 3 $\/$
108	45, 107	syl 14	. 2 $/\$ $/\$ $/\$ $/\$ $\/$
109	65, 105, 108	mpjaodan 803	1 $/\$ $/\$ $/\$ $/\$

Colors of variables: wff set class

Syntax hints:

wi 4 $/\$ wa 104 $\/$ wo 713 $/\$ w3a 1002

wceq 1395

wcel 2200

cfv 5317 (class class class)co 6000

cc 7993

cr 7994

caddc 7998

cmin 8313

cneg 8314

cn0 9365

cz 9442

cbs 13027

cplusg 13105

c0g 13284

cmnd 13444

cgrp 13528

cminusg 13529 ._gcmg 13651

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 617 ax-in2 618 ax-io 714 ax-5 1493 ax-7 1494 ax-gen 1495 ax-ie1 1539 ax-ie2 1540 ax-8 1550 ax-10 1551 ax-11 1552 ax-i12 1553 ax-bndl 1555 ax-4 1556 ax-17 1572 ax-i9 1576 ax-ial 1580 ax-i5r 1581 ax-13 2202 ax-14 2203 ax-ext 2211 ax-coll 4198 ax-sep 4201 ax-nul 4209 ax-pow 4257 ax-pr 4292 ax-un 4523 ax-setind 4628 ax-iinf 4679 ax-cnex 8086 ax-resscn 8087 ax-1cn 8088 ax-1re 8089 ax-icn 8090 ax-addcl 8091 ax-addrcl 8092 ax-mulcl 8093 ax-addcom 8095 ax-addass 8097 ax-distr 8099 ax-i2m1 8100 ax-0lt1 8101 ax-0id 8103 ax-rnegex 8104 ax-cnre 8106 ax-pre-ltirr 8107 ax-pre-ltwlin 8108 ax-pre-lttrn 8109 ax-pre-ltadd 8111

This theorem depends on definitions: df-bi 117 df-dc 840 df-3or 1003 df-3an 1004 df-tru 1398 df-fal 1401 df-nf 1507 df-sb 1809 df-eu 2080 df-mo 2081 df-clab 2216 df-cleq 2222 df-clel 2225 df-nfc 2361 df-ne 2401 df-nel 2496 df-ral 2513 df-rex 2514 df-reu 2515 df-rmo 2516 df-rab 2517 df-v 2801 df-sbc 3029 df-csb 3125 df-dif 3199 df-un 3201 df-in 3203 df-ss 3210 df-nul 3492 df-if 3603 df-pw 3651 df-sn 3672 df-pr 3673 df-op 3675 df-uni 3888 df-int 3923 df-iun 3966 df-br 4083 df-opab 4145 df-mpt 4146 df-tr 4182 df-id 4383 df-iord 4456 df-on 4458 df-ilim 4459 df-suc 4461 df-iom 4682 df-xp 4724 df-rel 4725 df-cnv 4726 df-co 4727 df-dm 4728 df-rn 4729 df-res 4730 df-ima 4731 df-iota 5277 df-fun 5319 df-fn 5320 df-f 5321 df-f1 5322 df-fo 5323 df-f1o 5324 df-fv 5325 df-riota 5953 df-ov 6003 df-oprab 6004 df-mpo 6005 df-1st 6284 df-2nd 6285 df-recs 6449 df-frec 6535 df-pnf 8179 df-mnf 8180 df-xr 8181 df-ltxr 8182 df-le 8183 df-sub 8315 df-neg 8316 df-inn 9107 df-2 9165 df-n0 9366 df-z 9443 df-uz 9719 df-fz 10201 df-seqfrec 10665 df-ndx 13030 df-slot 13031 df-base 13033 df-plusg 13118 df-0g 13286 df-mgm 13384 df-sgrp 13430 df-mnd 13445 df-grp 13531 df-minusg 13532 df-mulg 13652

This theorem is referenced by: mulgdir 13686

W3C validator