mulgdirlem - Intuitionistic Logic Explorer

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

Theorem mulgdirlem 12864

Description: Lemma for mulgdir 12865. (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 996	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
2	1	grpmndd 12742	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
3		simprl 527	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
4		simprr 528	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
5		simpl23 1073	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
6		mulgnndir.b	. . . . . 6
7		mulgnndir.t	. . . . . 6 ._g
8		mulgnndir.p	. . . . . 6
9	6, 7, 8	mulgnn0dir 12863	. . . . 5 $/\$ $/\$ $/\$
10	2, 3, 4, 5, 9	syl13anc 1236	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
11	10	anassrs 398	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
12		simpl1 996	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
13		simp22 1027	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
14	13	adantr 274	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
15		simpl23 1073	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
16		eqid 2171	. . . . . . . . . . 11
17	6, 7, 16	mulgneg 12852	. . . . . . . . . 10 $/\$ $/\$
18	12, 14, 15, 17	syl3anc 1234	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
19	18	oveq1d 5872	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
20	6, 7	mulgcl 12851	. . . . . . . . . 10 $/\$ $/\$
21	12, 14, 15, 20	syl3anc 1234	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
22		eqid 2171	. . . . . . . . . 10
23	6, 8, 22, 16	grplinv 12774	. . . . . . . . 9 $/\$
24	12, 21, 23	syl2anc 409	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
25	19, 24	eqtrd 2204	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
26	25	oveq2d 5873	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
27		simpl3 998	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
28		nn0z 9236	. . . . . . . . 9
29	27, 28	syl 14	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
30	6, 7	mulgcl 12851	. . . . . . . 8 $/\$ $/\$
31	12, 29, 15, 30	syl3anc 1234	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
32	6, 8, 22	grprid 12759	. . . . . . 7 $/\$
33	12, 31, 32	syl2anc 409	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
34	26, 33	eqtrd 2204	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
35		nn0z 9236	. . . . . . . . 9
36	35	ad2antll 489	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
37	6, 7	mulgcl 12851	. . . . . . . 8 $/\$ $/\$
38	12, 36, 15, 37	syl3anc 1234	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
39	6, 8	grpass 12739	. . . . . . 7 $/\$ $/\$ $/\$
40	12, 31, 38, 21, 39	syl13anc 1236	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
41	12	grpmndd 12742	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
42		simprr 528	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
43	6, 7, 8	mulgnn0dir 12863	. . . . . . . . 9 $/\$ $/\$ $/\$
44	41, 27, 42, 15, 43	syl13anc 1236	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
45		simp21 1026	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
46	45	zcnd 9339	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
47	13	zcnd 9339	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
48	46, 47	addcld 7943	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
49	48	adantr 274	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
50	47	adantr 274	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
51	49, 50	negsubd 8240	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
52	46	adantr 274	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
53	52, 50	pncand 8235	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
54	51, 53	eqtrd 2204	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
55	54	oveq1d 5872	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
56	44, 55	eqtr3d 2206	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
57	56	oveq1d 5872	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
58	40, 57	eqtr3d 2206	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
59	34, 58	eqtr3d 2206	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
60	59	anassrs 398	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
61		elznn0 9231	. . . . . 6 $/\$ $\/$
62	61	simprbi 273	. . . . 5 $\/$
63	13, 62	syl 14	. . . 4 $/\$ $/\$ $/\$ $/\$ $\/$
64	63	adantr 274	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $\/$
65	11, 60, 64	mpjaodan 794	. 2 $/\$ $/\$ $/\$ $/\$ $/\$
66		simpl1 996	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$
67	45	adantr 274	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$
68		simpl23 1073	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$
69	6, 7	mulgcl 12851	. . . . 5 $/\$ $/\$
70	66, 67, 68, 69	syl3anc 1234	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$
71	67	znegcld 9340	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$
72	6, 7	mulgcl 12851	. . . . 5 $/\$ $/\$
73	66, 71, 68, 72	syl3anc 1234	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$
74	28	3ad2ant3 1016	. . . . . 6 $/\$ $/\$ $/\$ $/\$
75	74	adantr 274	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$
76	66, 75, 68, 30	syl3anc 1234	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$
77	6, 8	grpass 12739	. . . 4 $/\$ $/\$ $/\$
78	66, 70, 73, 76, 77	syl13anc 1236	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$
79	6, 7, 16	mulgneg 12852	. . . . . . . 8 $/\$ $/\$
80	66, 67, 68, 79	syl3anc 1234	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$
81	80	oveq2d 5873	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$
82	6, 8, 22, 16	grprinv 12775	. . . . . . 7 $/\$
83	66, 70, 82	syl2anc 409	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$
84	81, 83	eqtrd 2204	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$
85	84	oveq1d 5872	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$
86	6, 8, 22	grplid 12758	. . . . 5 $/\$
87	66, 76, 86	syl2anc 409	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$
88	85, 87	eqtrd 2204	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$
89	66	grpmndd 12742	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$
90		simpr 109	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$
91		simpl3 998	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$
92	6, 7, 8	mulgnn0dir 12863	. . . . . 6 $/\$ $/\$ $/\$
93	89, 90, 91, 68, 92	syl13anc 1236	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$
94	46	adantr 274	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$
95	94	negcld 8221	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$
96	48	adantr 274	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$
97	95, 96	addcomd 8074	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$
98	96, 94	negsubd 8240	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$
99	47	adantr 274	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$
100	94, 99	pncan2d 8236	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$
101	97, 98, 100	3eqtrd 2208	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$
102	101	oveq1d 5872	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$
103	93, 102	eqtr3d 2206	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$
104	103	oveq2d 5873	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$
105	78, 88, 104	3eqtr3d 2212	. 2 $/\$ $/\$ $/\$ $/\$ $/\$
106		elznn0 9231	. . . 4 $/\$ $\/$
107	106	simprbi 273	. . 3 $\/$
108	45, 107	syl 14	. 2 $/\$ $/\$ $/\$ $/\$ $\/$
109	65, 105, 108	mpjaodan 794	1 $/\$ $/\$ $/\$ $/\$

Colors of variables: wff set class

Syntax hints:

wi 4 $/\$ wa 103 $\/$ wo 704 $/\$ w3a 974

wceq 1349

wcel 2142

cfv 5200 (class class class)co 5857

cc 7776

cr 7777

caddc 7781

cmin 8094

cneg 8095

cn0 9139

cz 9216

cbs 12420

cplusg 12484

c0g 12618

cmnd 12674

cgrp 12730

cminusg 12731 ._gcmg 12834

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-in1 610 ax-in2 611 ax-io 705 ax-5 1441 ax-7 1442 ax-gen 1443 ax-ie1 1487 ax-ie2 1488 ax-8 1498 ax-10 1499 ax-11 1500 ax-i12 1501 ax-bndl 1503 ax-4 1504 ax-17 1520 ax-i9 1524 ax-ial 1528 ax-i5r 1529 ax-13 2144 ax-14 2145 ax-ext 2153 ax-coll 4105 ax-sep 4108 ax-nul 4116 ax-pow 4161 ax-pr 4195 ax-un 4419 ax-setind 4522 ax-iinf 4573 ax-cnex 7869 ax-resscn 7870 ax-1cn 7871 ax-1re 7872 ax-icn 7873 ax-addcl 7874 ax-addrcl 7875 ax-mulcl 7876 ax-addcom 7878 ax-addass 7880 ax-distr 7882 ax-i2m1 7883 ax-0lt1 7884 ax-0id 7886 ax-rnegex 7887 ax-cnre 7889 ax-pre-ltirr 7890 ax-pre-ltwlin 7891 ax-pre-lttrn 7892 ax-pre-ltadd 7894

This theorem depends on definitions: df-bi 116 df-dc 831 df-3or 975 df-3an 976 df-tru 1352 df-fal 1355 df-nf 1455 df-sb 1757 df-eu 2023 df-mo 2024 df-clab 2158 df-cleq 2164 df-clel 2167 df-nfc 2302 df-ne 2342 df-nel 2437 df-ral 2454 df-rex 2455 df-reu 2456 df-rmo 2457 df-rab 2458 df-v 2733 df-sbc 2957 df-csb 3051 df-dif 3124 df-un 3126 df-in 3128 df-ss 3135 df-nul 3416 df-if 3528 df-pw 3569 df-sn 3590 df-pr 3591 df-op 3593 df-uni 3798 df-int 3833 df-iun 3876 df-br 3991 df-opab 4052 df-mpt 4053 df-tr 4089 df-id 4279 df-iord 4352 df-on 4354 df-ilim 4355 df-suc 4357 df-iom 4576 df-xp 4618 df-rel 4619 df-cnv 4620 df-co 4621 df-dm 4622 df-rn 4623 df-res 4624 df-ima 4625 df-iota 5162 df-fun 5202 df-fn 5203 df-f 5204 df-f1 5205 df-fo 5206 df-f1o 5207 df-fv 5208 df-riota 5813 df-ov 5860 df-oprab 5861 df-mpo 5862 df-1st 6123 df-2nd 6124 df-recs 6288 df-frec 6374 df-pnf 7960 df-mnf 7961 df-xr 7962 df-ltxr 7963 df-le 7964 df-sub 8096 df-neg 8097 df-inn 8883 df-2 8941 df-n0 9140 df-z 9217 df-uz 9492 df-fz 9970 df-seqfrec 10406 df-ndx 12423 df-slot 12424 df-base 12426 df-plusg 12497 df-0g 12620 df-mgm 12632 df-sgrp 12665 df-mnd 12675 df-grp 12733 df-minusg 12734 df-mulg 12835

This theorem is referenced by: mulgdir 12865

W3C validator