mulgdirlem - Intuitionistic Logic Explorer

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

Theorem mulgdirlem 13705

Description: Lemma for mulgdir 13706. (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 13561	. . . . 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 13704	. . . . 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 13692	. . . . . . . . . 10 $/\$ $/\$
18	12, 14, 15, 17	syl3anc 1271	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
19	18	oveq1d 6022	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
20	6, 7	mulgcl 13691	. . . . . . . . . 10 $/\$ $/\$
21	12, 14, 15, 20	syl3anc 1271	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
22		eqid 2229	. . . . . . . . . 10
23	6, 8, 22, 16	grplinv 13598	. . . . . . . . 9 $/\$
24	12, 21, 23	syl2anc 411	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
25	19, 24	eqtrd 2262	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
26	25	oveq2d 6023	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
27		simpl3 1026	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
28		nn0z 9477	. . . . . . . . 9
29	27, 28	syl 14	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
30	6, 7	mulgcl 13691	. . . . . . . 8 $/\$ $/\$
31	12, 29, 15, 30	syl3anc 1271	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
32	6, 8, 22	grprid 13580	. . . . . . 7 $/\$
33	12, 31, 32	syl2anc 411	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
34	26, 33	eqtrd 2262	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
35		nn0z 9477	. . . . . . . . 9
36	35	ad2antll 491	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
37	6, 7	mulgcl 13691	. . . . . . . 8 $/\$ $/\$
38	12, 36, 15, 37	syl3anc 1271	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
39	6, 8	grpass 13557	. . . . . . 7 $/\$ $/\$ $/\$
40	12, 31, 38, 21, 39	syl13anc 1273	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
41	12	grpmndd 13561	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
42		simprr 531	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
43	6, 7, 8	mulgnn0dir 13704	. . . . . . . . 9 $/\$ $/\$ $/\$
44	41, 27, 42, 15, 43	syl13anc 1273	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
45		simp21 1054	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
46	45	zcnd 9581	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
47	13	zcnd 9581	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
48	46, 47	addcld 8177	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
49	48	adantr 276	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
50	47	adantr 276	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
51	49, 50	negsubd 8474	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
52	46	adantr 276	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
53	52, 50	pncand 8469	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
54	51, 53	eqtrd 2262	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
55	54	oveq1d 6022	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
56	44, 55	eqtr3d 2264	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
57	56	oveq1d 6022	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
58	40, 57	eqtr3d 2264	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
59	34, 58	eqtr3d 2264	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
60	59	anassrs 400	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
61		elznn0 9472	. . . . . 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 13691	. . . . 5 $/\$ $/\$
70	66, 67, 68, 69	syl3anc 1271	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$
71	67	znegcld 9582	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$
72	6, 7	mulgcl 13691	. . . . 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 13557	. . . 4 $/\$ $/\$ $/\$
78	66, 70, 73, 76, 77	syl13anc 1273	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$
79	6, 7, 16	mulgneg 13692	. . . . . . . 8 $/\$ $/\$
80	66, 67, 68, 79	syl3anc 1271	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$
81	80	oveq2d 6023	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$
82	6, 8, 22, 16	grprinv 13599	. . . . . . 7 $/\$
83	66, 70, 82	syl2anc 411	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$
84	81, 83	eqtrd 2262	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$
85	84	oveq1d 6022	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$
86	6, 8, 22	grplid 13579	. . . . 5 $/\$
87	66, 76, 86	syl2anc 411	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$
88	85, 87	eqtrd 2262	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$
89	66	grpmndd 13561	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$
90		simpr 110	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$
91		simpl3 1026	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$
92	6, 7, 8	mulgnn0dir 13704	. . . . . 6 $/\$ $/\$ $/\$
93	89, 90, 91, 68, 92	syl13anc 1273	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$
94	46	adantr 276	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$
95	94	negcld 8455	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$
96	48	adantr 276	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$
97	95, 96	addcomd 8308	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$
98	96, 94	negsubd 8474	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$
99	47	adantr 276	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$
100	94, 99	pncan2d 8470	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$
101	97, 98, 100	3eqtrd 2266	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$
102	101	oveq1d 6022	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$
103	93, 102	eqtr3d 2264	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$
104	103	oveq2d 6023	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$
105	78, 88, 104	3eqtr3d 2270	. 2 $/\$ $/\$ $/\$ $/\$ $/\$
106		elznn0 9472	. . . 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 5318 (class class class)co 6007

cc 8008

cr 8009

caddc 8013

cmin 8328

cneg 8329

cn0 9380

cz 9457

cbs 13047

cplusg 13125

c0g 13304

cmnd 13464

cgrp 13548

cminusg 13549 ._gcmg 13671

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 4199 ax-sep 4202 ax-nul 4210 ax-pow 4258 ax-pr 4293 ax-un 4524 ax-setind 4629 ax-iinf 4680 ax-cnex 8101 ax-resscn 8102 ax-1cn 8103 ax-1re 8104 ax-icn 8105 ax-addcl 8106 ax-addrcl 8107 ax-mulcl 8108 ax-addcom 8110 ax-addass 8112 ax-distr 8114 ax-i2m1 8115 ax-0lt1 8116 ax-0id 8118 ax-rnegex 8119 ax-cnre 8121 ax-pre-ltirr 8122 ax-pre-ltwlin 8123 ax-pre-lttrn 8124 ax-pre-ltadd 8126

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 3889 df-int 3924 df-iun 3967 df-br 4084 df-opab 4146 df-mpt 4147 df-tr 4183 df-id 4384 df-iord 4457 df-on 4459 df-ilim 4460 df-suc 4462 df-iom 4683 df-xp 4725 df-rel 4726 df-cnv 4727 df-co 4728 df-dm 4729 df-rn 4730 df-res 4731 df-ima 4732 df-iota 5278 df-fun 5320 df-fn 5321 df-f 5322 df-f1 5323 df-fo 5324 df-f1o 5325 df-fv 5326 df-riota 5960 df-ov 6010 df-oprab 6011 df-mpo 6012 df-1st 6292 df-2nd 6293 df-recs 6457 df-frec 6543 df-pnf 8194 df-mnf 8195 df-xr 8196 df-ltxr 8197 df-le 8198 df-sub 8330 df-neg 8331 df-inn 9122 df-2 9180 df-n0 9381 df-z 9458 df-uz 9734 df-fz 10217 df-seqfrec 10682 df-ndx 13050 df-slot 13051 df-base 13053 df-plusg 13138 df-0g 13306 df-mgm 13404 df-sgrp 13450 df-mnd 13465 df-grp 13551 df-minusg 13552 df-mulg 13672

This theorem is referenced by: mulgdir 13706

W3C validator