mulgdirlem - Intuitionistic Logic Explorer

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

Theorem mulgdirlem 13407

Description: Lemma for mulgdir 13408. (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 1002	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
2	1	grpmndd 13263	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
3		simprl 529	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
4		simprr 531	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
5		simpl23 1079	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
6		mulgnndir.b	. . . . . 6
7		mulgnndir.t	. . . . . 6 ._g
8		mulgnndir.p	. . . . . 6
9	6, 7, 8	mulgnn0dir 13406	. . . . 5 $/\$ $/\$ $/\$
10	2, 3, 4, 5, 9	syl13anc 1251	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
11	10	anassrs 400	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
12		simpl1 1002	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
13		simp22 1033	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
14	13	adantr 276	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
15		simpl23 1079	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
16		eqid 2204	. . . . . . . . . . 11
17	6, 7, 16	mulgneg 13394	. . . . . . . . . 10 $/\$ $/\$
18	12, 14, 15, 17	syl3anc 1249	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
19	18	oveq1d 5949	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
20	6, 7	mulgcl 13393	. . . . . . . . . 10 $/\$ $/\$
21	12, 14, 15, 20	syl3anc 1249	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
22		eqid 2204	. . . . . . . . . 10
23	6, 8, 22, 16	grplinv 13300	. . . . . . . . 9 $/\$
24	12, 21, 23	syl2anc 411	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
25	19, 24	eqtrd 2237	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
26	25	oveq2d 5950	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
27		simpl3 1004	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
28		nn0z 9374	. . . . . . . . 9
29	27, 28	syl 14	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
30	6, 7	mulgcl 13393	. . . . . . . 8 $/\$ $/\$
31	12, 29, 15, 30	syl3anc 1249	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
32	6, 8, 22	grprid 13282	. . . . . . 7 $/\$
33	12, 31, 32	syl2anc 411	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
34	26, 33	eqtrd 2237	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
35		nn0z 9374	. . . . . . . . 9
36	35	ad2antll 491	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
37	6, 7	mulgcl 13393	. . . . . . . 8 $/\$ $/\$
38	12, 36, 15, 37	syl3anc 1249	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
39	6, 8	grpass 13259	. . . . . . 7 $/\$ $/\$ $/\$
40	12, 31, 38, 21, 39	syl13anc 1251	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
41	12	grpmndd 13263	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
42		simprr 531	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
43	6, 7, 8	mulgnn0dir 13406	. . . . . . . . 9 $/\$ $/\$ $/\$
44	41, 27, 42, 15, 43	syl13anc 1251	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
45		simp21 1032	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
46	45	zcnd 9478	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
47	13	zcnd 9478	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
48	46, 47	addcld 8074	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
49	48	adantr 276	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
50	47	adantr 276	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
51	49, 50	negsubd 8371	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
52	46	adantr 276	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
53	52, 50	pncand 8366	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
54	51, 53	eqtrd 2237	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
55	54	oveq1d 5949	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
56	44, 55	eqtr3d 2239	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
57	56	oveq1d 5949	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
58	40, 57	eqtr3d 2239	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
59	34, 58	eqtr3d 2239	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
60	59	anassrs 400	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
61		elznn0 9369	. . . . . 6 $/\$ $\/$
62	61	simprbi 275	. . . . 5 $\/$
63	13, 62	syl 14	. . . 4 $/\$ $/\$ $/\$ $/\$ $\/$
64	63	adantr 276	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $\/$
65	11, 60, 64	mpjaodan 799	. 2 $/\$ $/\$ $/\$ $/\$ $/\$
66		simpl1 1002	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$
67	45	adantr 276	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$
68		simpl23 1079	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$
69	6, 7	mulgcl 13393	. . . . 5 $/\$ $/\$
70	66, 67, 68, 69	syl3anc 1249	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$
71	67	znegcld 9479	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$
72	6, 7	mulgcl 13393	. . . . 5 $/\$ $/\$
73	66, 71, 68, 72	syl3anc 1249	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$
74	28	3ad2ant3 1022	. . . . . 6 $/\$ $/\$ $/\$ $/\$
75	74	adantr 276	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$
76	66, 75, 68, 30	syl3anc 1249	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$
77	6, 8	grpass 13259	. . . 4 $/\$ $/\$ $/\$
78	66, 70, 73, 76, 77	syl13anc 1251	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$
79	6, 7, 16	mulgneg 13394	. . . . . . . 8 $/\$ $/\$
80	66, 67, 68, 79	syl3anc 1249	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$
81	80	oveq2d 5950	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$
82	6, 8, 22, 16	grprinv 13301	. . . . . . 7 $/\$
83	66, 70, 82	syl2anc 411	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$
84	81, 83	eqtrd 2237	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$
85	84	oveq1d 5949	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$
86	6, 8, 22	grplid 13281	. . . . 5 $/\$
87	66, 76, 86	syl2anc 411	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$
88	85, 87	eqtrd 2237	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$
89	66	grpmndd 13263	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$
90		simpr 110	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$
91		simpl3 1004	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$
92	6, 7, 8	mulgnn0dir 13406	. . . . . 6 $/\$ $/\$ $/\$
93	89, 90, 91, 68, 92	syl13anc 1251	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$
94	46	adantr 276	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$
95	94	negcld 8352	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$
96	48	adantr 276	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$
97	95, 96	addcomd 8205	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$
98	96, 94	negsubd 8371	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$
99	47	adantr 276	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$
100	94, 99	pncan2d 8367	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$
101	97, 98, 100	3eqtrd 2241	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$
102	101	oveq1d 5949	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$
103	93, 102	eqtr3d 2239	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$
104	103	oveq2d 5950	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$
105	78, 88, 104	3eqtr3d 2245	. 2 $/\$ $/\$ $/\$ $/\$ $/\$
106		elznn0 9369	. . . 4 $/\$ $\/$
107	106	simprbi 275	. . 3 $\/$
108	45, 107	syl 14	. 2 $/\$ $/\$ $/\$ $/\$ $\/$
109	65, 105, 108	mpjaodan 799	1 $/\$ $/\$ $/\$ $/\$

Colors of variables: wff set class

Syntax hints:

wi 4 $/\$ wa 104 $\/$ wo 709 $/\$ w3a 980

wceq 1372

wcel 2175

cfv 5268 (class class class)co 5934

cc 7905

cr 7906

caddc 7910

cmin 8225

cneg 8226

cn0 9277

cz 9354

cbs 12751

cplusg 12828

c0g 13006

cmnd 13166

cgrp 13250

cminusg 13251 ._gcmg 13373

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 615 ax-in2 616 ax-io 710 ax-5 1469 ax-7 1470 ax-gen 1471 ax-ie1 1515 ax-ie2 1516 ax-8 1526 ax-10 1527 ax-11 1528 ax-i12 1529 ax-bndl 1531 ax-4 1532 ax-17 1548 ax-i9 1552 ax-ial 1556 ax-i5r 1557 ax-13 2177 ax-14 2178 ax-ext 2186 ax-coll 4158 ax-sep 4161 ax-nul 4169 ax-pow 4217 ax-pr 4252 ax-un 4478 ax-setind 4583 ax-iinf 4634 ax-cnex 7998 ax-resscn 7999 ax-1cn 8000 ax-1re 8001 ax-icn 8002 ax-addcl 8003 ax-addrcl 8004 ax-mulcl 8005 ax-addcom 8007 ax-addass 8009 ax-distr 8011 ax-i2m1 8012 ax-0lt1 8013 ax-0id 8015 ax-rnegex 8016 ax-cnre 8018 ax-pre-ltirr 8019 ax-pre-ltwlin 8020 ax-pre-lttrn 8021 ax-pre-ltadd 8023

This theorem depends on definitions: df-bi 117 df-dc 836 df-3or 981 df-3an 982 df-tru 1375 df-fal 1378 df-nf 1483 df-sb 1785 df-eu 2056 df-mo 2057 df-clab 2191 df-cleq 2197 df-clel 2200 df-nfc 2336 df-ne 2376 df-nel 2471 df-ral 2488 df-rex 2489 df-reu 2490 df-rmo 2491 df-rab 2492 df-v 2773 df-sbc 2998 df-csb 3093 df-dif 3167 df-un 3169 df-in 3171 df-ss 3178 df-nul 3460 df-if 3571 df-pw 3617 df-sn 3638 df-pr 3639 df-op 3641 df-uni 3850 df-int 3885 df-iun 3928 df-br 4044 df-opab 4105 df-mpt 4106 df-tr 4142 df-id 4338 df-iord 4411 df-on 4413 df-ilim 4414 df-suc 4416 df-iom 4637 df-xp 4679 df-rel 4680 df-cnv 4681 df-co 4682 df-dm 4683 df-rn 4684 df-res 4685 df-ima 4686 df-iota 5229 df-fun 5270 df-fn 5271 df-f 5272 df-f1 5273 df-fo 5274 df-f1o 5275 df-fv 5276 df-riota 5889 df-ov 5937 df-oprab 5938 df-mpo 5939 df-1st 6216 df-2nd 6217 df-recs 6381 df-frec 6467 df-pnf 8091 df-mnf 8092 df-xr 8093 df-ltxr 8094 df-le 8095 df-sub 8227 df-neg 8228 df-inn 9019 df-2 9077 df-n0 9278 df-z 9355 df-uz 9631 df-fz 10113 df-seqfrec 10574 df-ndx 12754 df-slot 12755 df-base 12757 df-plusg 12841 df-0g 13008 df-mgm 13106 df-sgrp 13152 df-mnd 13167 df-grp 13253 df-minusg 13254 df-mulg 13374

This theorem is referenced by: mulgdir 13408

W3C validator