Theorem grpidinvlem3 9330

Description: Lemma for grpidinv 9332.

Hypotheses

Ref	Expression
grpfo.1	|- X = ran G
grpidinvlem3.2	|- (ph <-> A.x e. X (UGx) = x)
grpidinvlem3.3	|- (ps <-> A.x e. X E.z e. X (zGx) = U)

Assertion

Ref	Expression
grpidinvlem3	|- ((((G e. Grp /\ U e. X) /\ (ph /\ ps)) /\ A e. X) -> E.y e. X ((yGA) = U /\ (AGy) = U))

Distinct variable groups:   x,y,z,A   x,G,y,z   x,X,y,z   y,U,x,z   ph,y   ps,y

Proof of Theorem grpidinvlem3

Step	Hyp	Ref	Expression
1		opreq2 4890	. . . . . . . 8 |- (x = A -> (yGx) = (yGA))
2	1	eqeq1d 1892	. . . . . . 7 |- (x = A -> ((yGx) = U <-> (yGA) = U))
3	2	rexbidv 2124	. . . . . 6 |- (x = A -> (E.y e. X (yGx) = U <-> E.y e. X (yGA) = U))
4	3	rcla4cva 2379	. . . . 5 |- ((A.x e. X E.y e. X (yGx) = U /\ A e. X) -> E.y e. X (yGA) = U)
5		grpidinvlem3.3	. . . . . 6 |- (ps <-> A.x e. X E.z e. X (zGx) = U)
6		opreq1 4889	. . . . . . . . 9 |- (z = y -> (zGx) = (yGx))
7	6	eqeq1d 1892	. . . . . . . 8 |- (z = y -> ((zGx) = U <-> (yGx) = U))
8	7	cbvrexv 2281	. . . . . . 7 |- (E.z e. X (zGx) = U <-> E.y e. X (yGx) = U)
9	8	ralbii 2127	. . . . . 6 |- (A.x e. X E.z e. X (zGx) = U <-> A.x e. X E.y e. X (yGx) = U)
10	5, 9	bitri 190	. . . . 5 |- (ps <-> A.x e. X E.y e. X (yGx) = U)
11	4, 10	sylanb 498	. . . 4 |- ((ps /\ A e. X) -> E.y e. X (yGA) = U)
12	11	adantll 428	. . 3 |- (((ph /\ ps) /\ A e. X) -> E.y e. X (yGA) = U)
13	12	adantll 428	. 2 |- ((((G e. Grp /\ U e. X) /\ (ph /\ ps)) /\ A e. X) -> E.y e. X (yGA) = U)
14		grpfo.1	. . . . . . . . . . . 12 |- X = ran G
15	14	grpcl 9324	. . . . . . . . . . 11 |- ((G e. Grp /\ A e. X /\ y e. X) -> (AGy) e. X)
16	15	3expa 1067	. . . . . . . . . 10 |- (((G e. Grp /\ A e. X) /\ y e. X) -> (AGy) e. X)
17	16	adantllr 433	. . . . . . . . 9 |- ((((G e. Grp /\ U e. X) /\ A e. X) /\ y e. X) -> (AGy) e. X)
18	17	adantllr 433	. . . . . . . 8 |- (((((G e. Grp /\ U e. X) /\ (ph /\ ps)) /\ A e. X) /\ y e. X) -> (AGy) e. X)
19		grpidinvlem3.2	. . . . . . . . . . 11 |- (ph <-> A.x e. X (UGx) = x)
20	19	biimpi 168	. . . . . . . . . 10 |- (ph -> A.x e. X (UGx) = x)
21	20	ad2antrl 442	. . . . . . . . 9 |- (((G e. Grp /\ U e. X) /\ (ph /\ ps)) -> A.x e. X (UGx) = x)
22	21	ad2antrr 440	. . . . . . . 8 |- (((((G e. Grp /\ U e. X) /\ (ph /\ ps)) /\ A e. X) /\ y e. X) -> A.x e. X (UGx) = x)
23		opreq2 4890	. . . . . . . . . 10 |- (x = (AGy) -> (UGx) = (UG(AGy)))
24		id 73	. . . . . . . . . 10 |- (x = (AGy) -> x = (AGy))
25	23, 24	eqeq12d 1899	. . . . . . . . 9 |- (x = (AGy) -> ((UGx) = x <-> (UG(AGy)) = (AGy)))
26	25	rcla4va 2378	. . . . . . . 8 |- (((AGy) e. X /\ A.x e. X (UGx) = x) -> (UG(AGy)) = (AGy))
27	18, 22, 26	syl11anc 524	. . . . . . 7 |- (((((G e. Grp /\ U e. X) /\ (ph /\ ps)) /\ A e. X) /\ y e. X) -> (UG(AGy)) = (AGy))
28	27	adantr 425	. . . . . 6 |- ((((((G e. Grp /\ U e. X) /\ (ph /\ ps)) /\ A e. X) /\ y e. X) /\ (yGA) = U) -> (UG(AGy)) = (AGy))
29		pm3.22 486	. . . . . . . . . . . 12 |- (((y e. X /\ A e. X) /\ G e. Grp) -> (G e. Grp /\ (y e. X /\ A e. X)))
30	29	ancom31s 549	. . . . . . . . . . 11 |- (((G e. Grp /\ A e. X) /\ y e. X) -> (G e. Grp /\ (y e. X /\ A e. X)))
31	30	adantllr 433	. . . . . . . . . 10 |- ((((G e. Grp /\ U e. X) /\ A e. X) /\ y e. X) -> (G e. Grp /\ (y e. X /\ A e. X)))
32	31	adantllr 433	. . . . . . . . 9 |- (((((G e. Grp /\ U e. X) /\ (ph /\ ps)) /\ A e. X) /\ y e. X) -> (G e. Grp /\ (y e. X /\ A e. X)))
33	32	adantr 425	. . . . . . . 8 |- ((((((G e. Grp /\ U e. X) /\ (ph /\ ps)) /\ A e. X) /\ y e. X) /\ (yGA) = U) -> (G e. Grp /\ (y e. X /\ A e. X)))
34		opreq2 4890	. . . . . . . . . . . . . . 15 |- (x = y -> (UGx) = (UGy))
35		id 73	. . . . . . . . . . . . . . 15 |- (x = y -> x = y)
36	34, 35	eqeq12d 1899	. . . . . . . . . . . . . 14 |- (x = y -> ((UGx) = x <-> (UGy) = y))
37	36	rcla4cva 2379	. . . . . . . . . . . . 13 |- ((A.x e. X (UGx) = x /\ y e. X) -> (UGy) = y)
38	37, 19	sylanb 498	. . . . . . . . . . . 12 |- ((ph /\ y e. X) -> (UGy) = y)
39	38	adantlr 429	. . . . . . . . . . 11 |- (((ph /\ ps) /\ y e. X) -> (UGy) = y)
40	39	adantlr 429	. . . . . . . . . 10 |- ((((ph /\ ps) /\ A e. X) /\ y e. X) -> (UGy) = y)
41	40	adantlll 432	. . . . . . . . 9 |- (((((G e. Grp /\ U e. X) /\ (ph /\ ps)) /\ A e. X) /\ y e. X) -> (UGy) = y)
42	41	anim1i 361	. . . . . . . 8 |- ((((((G e. Grp /\ U e. X) /\ (ph /\ ps)) /\ A e. X) /\ y e. X) /\ (yGA) = U) -> ((UGy) = y /\ (yGA) = U))
43	14	grpidinvlem2 9329	. . . . . . . 8 |- (((G e. Grp /\ (y e. X /\ A e. X)) /\ ((UGy) = y /\ (yGA) = U)) -> ((AGy)G(AGy)) = (AGy))
44	33, 42, 43	syl11anc 524	. . . . . . 7 |- ((((((G e. Grp /\ U e. X) /\ (ph /\ ps)) /\ A e. X) /\ y e. X) /\ (yGA) = U) -> ((AGy)G(AGy)) = (AGy))
45	15	3expb 1068	. . . . . . . . . . . . . . 15 |- ((G e. Grp /\ (A e. X /\ y e. X)) -> (AGy) e. X)
46	45	ad2ant2rl 447	. . . . . . . . . . . . . 14 |- (((G e. Grp /\ U e. X) /\ (ph /\ (A e. X /\ y e. X))) -> (AGy) e. X)
47	14	grpidinvlem1 9328	. . . . . . . . . . . . . . . . . 18 |- (((G e. Grp /\ (w e. X /\ (AGy) e. X)) /\ ((wG(AGy)) = U /\ ((AGy)G(AGy)) = (AGy))) -> (UG(AGy)) = U)
48		anass 487	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (((G e. Grp /\ w e. X) /\ (AGy) e. X) <-> (G e. Grp /\ (w e. X /\ (AGy) e. X)))
49	48	biimpi 168	. . . . . . . . . . . . . . . . . . . . . . 23 |- (((G e. Grp /\ w e. X) /\ (AGy) e. X) -> (G e. Grp /\ (w e. X /\ (AGy) e. X)))
50	49	an1rs 547	. . . . . . . . . . . . . . . . . . . . . 22 |- (((G e. Grp /\ (AGy) e. X) /\ w e. X) -> (G e. Grp /\ (w e. X /\ (AGy) e. X)))
51	50	ex 402	. . . . . . . . . . . . . . . . . . . . 21 |- ((G e. Grp /\ (AGy) e. X) -> (w e. X -> (G e. Grp /\ (w e. X /\ (AGy) e. X))))
52	45, 51	syldan 516	. . . . . . . . . . . . . . . . . . . 20 |- ((G e. Grp /\ (A e. X /\ y e. X)) -> (w e. X -> (G e. Grp /\ (w e. X /\ (AGy) e. X))))
53	52	ad2ant2rl 447	. . . . . . . . . . . . . . . . . . 19 |- (((G e. Grp /\ U e. X) /\ (ph /\ (A e. X /\ y e. X))) -> (w e. X -> (G e. Grp /\ (w e. X /\ (AGy) e. X))))
54	53	imp 377	. . . . . . . . . . . . . . . . . 18 |- ((((G e. Grp /\ U e. X) /\ (ph /\ (A e. X /\ y e. X))) /\ w e. X) -> (G e. Grp /\ (w e. X /\ (AGy) e. X)))
55	47, 54	sylan 497	. . . . . . . . . . . . . . . . 17 |- (((((G e. Grp /\ U e. X) /\ (ph /\ (A e. X /\ y e. X))) /\ w e. X) /\ ((wG(AGy)) = U /\ ((AGy)G(AGy)) = (AGy))) -> (UG(AGy)) = U)
56	55	exp43 415	. . . . . . . . . . . . . . . 16 |- (((G e. Grp /\ U e. X) /\ (ph /\ (A e. X /\ y e. X))) -> (w e. X -> ((wG(AGy)) = U -> (((AGy)G(AGy)) = (AGy) -> (UG(AGy)) = U))))
57	56	r19.23adv 2215	. . . . . . . . . . . . . . 15 |- (((G e. Grp /\ U e. X) /\ (ph /\ (A e. X /\ y e. X))) -> (E.w e. X (wG(AGy)) = U -> (((AGy)G(AGy)) = (AGy) -> (UG(AGy)) = U)))
58		opreq2 4890	. . . . . . . . . . . . . . . . . . 19 |- (x = (AGy) -> (wGx) = (wG(AGy)))
59	58	eqeq1d 1892	. . . . . . . . . . . . . . . . . 18 |- (x = (AGy) -> ((wGx) = U <-> (wG(AGy)) = U))
60	59	rexbidv 2124	. . . . . . . . . . . . . . . . 17 |- (x = (AGy) -> (E.w e. X (wGx) = U <-> E.w e. X (wG(AGy)) = U))
61	60	rcla4va 2378	. . . . . . . . . . . . . . . 16 |- (((AGy) e. X /\ A.x e. X E.w e. X (wGx) = U) -> E.w e. X (wG(AGy)) = U)
62		opreq1 4889	. . . . . . . . . . . . . . . . . . . 20 |- (z = w -> (zGx) = (wGx))
63	62	eqeq1d 1892	. . . . . . . . . . . . . . . . . . 19 |- (z = w -> ((zGx) = U <-> (wGx) = U))
64	63	cbvrexv 2281	. . . . . . . . . . . . . . . . . 18 |- (E.z e. X (zGx) = U <-> E.w e. X (wGx) = U)
65	64	ralbii 2127	. . . . . . . . . . . . . . . . 17 |- (A.x e. X E.z e. X (zGx) = U <-> A.x e. X E.w e. X (wGx) = U)
66	5, 65	bitri 190	. . . . . . . . . . . . . . . 16 |- (ps <-> A.x e. X E.w e. X (wGx) = U)
67	61, 66	sylan2b 501	. . . . . . . . . . . . . . 15 |- (((AGy) e. X /\ ps) -> E.w e. X (wG(AGy)) = U)
68	57, 67	syl5 20	. . . . . . . . . . . . . 14 |- (((G e. Grp /\ U e. X) /\ (ph /\ (A e. X /\ y e. X))) -> (((AGy) e. X /\ ps) -> (((AGy)G(AGy)) = (AGy) -> (UG(AGy)) = U)))
69	46, 68	mpand 765	. . . . . . . . . . . . 13 |- (((G e. Grp /\ U e. X) /\ (ph /\ (A e. X /\ y e. X))) -> (ps -> (((AGy)G(AGy)) = (AGy) -> (UG(AGy)) = U)))
70	69	exp32 408	. . . . . . . . . . . 12 |- ((G e. Grp /\ U e. X) -> (ph -> ((A e. X /\ y e. X) -> (ps -> (((AGy)G(AGy)) = (AGy) -> (UG(AGy)) = U)))))
71	70	com34 40	. . . . . . . . . . 11 |- ((G e. Grp /\ U e. X) -> (ph -> (ps -> ((A e. X /\ y e. X) -> (((AGy)G(AGy)) = (AGy) -> (UG(AGy)) = U)))))
72	71	imp32 390	. . . . . . . . . 10 |- (((G e. Grp /\ U e. X) /\ (ph /\ ps)) -> ((A e. X /\ y e. X) -> (((AGy)G(AGy)) = (AGy) -> (UG(AGy)) = U)))
73	72	exp3a 405	. . . . . . . . 9 |- (((G e. Grp /\ U e. X) /\ (ph /\ ps)) -> (A e. X -> (y e. X -> (((AGy)G(AGy)) = (AGy) -> (UG(AGy)) = U))))
74	73	imp31 389	. . . . . . . 8 |- (((((G e. Grp /\ U e. X) /\ (ph /\ ps)) /\ A e. X) /\ y e. X) -> (((AGy)G(AGy)) = (AGy) -> (UG(AGy)) = U))
75	74	adantr 425	. . . . . . 7 |- ((((((G e. Grp /\ U e. X) /\ (ph /\ ps)) /\ A e. X) /\ y e. X) /\ (yGA) = U) -> (((AGy)G(AGy)) = (AGy) -> (UG(AGy)) = U))
76	44, 75	mpd 29	. . . . . 6 |- ((((((G e. Grp /\ U e. X) /\ (ph /\ ps)) /\ A e. X) /\ y e. X) /\ (yGA) = U) -> (UG(AGy)) = U)
77	28, 76	eqtr3d 1927	. . . . 5 |- ((((((G e. Grp /\ U e. X) /\ (ph /\ ps)) /\ A e. X) /\ y e. X) /\ (yGA) = U) -> (AGy) = U)
78	77	ex 402	. . . 4 |- (((((G e. Grp /\ U e. X) /\ (ph /\ ps)) /\ A e. X) /\ y e. X) -> ((yGA) = U -> (AGy) = U))
79	78	ancld 322	. . 3 |- (((((G e. Grp /\ U e. X) /\ (ph /\ ps)) /\ A e. X) /\ y e. X) -> ((yGA) = U -> ((yGA) = U /\ (AGy) = U)))
80	79	reximdva 2203	. 2 |- ((((G e. Grp /\ U e. X) /\ (ph /\ ps)) /\ A e. X) -> (E.y e. X (yGA) = U -> E.y e. X ((yGA) = U /\ (AGy) = U)))
81	13, 80	mpd 29	1 |- ((((G e. Grp /\ U e. X) /\ (ph /\ ps)) /\ A e. X) -> E.y e. X ((yGA) = U /\ (AGy) = U))

Syntax hints:   -> wi 3   <-> wb 163   /\ wa 240   = wceq 1298   e. wcel 1300  A.wral 2105  E.wrex 2106  ran crn 3987  (class class class)co 4884  Grpcgr 9311

This theorem is referenced by:  grpidinv 9332

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-13 1311  ax-14 1312  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865  ax-sep 3438  ax-nul 3445  ax-pow 3481  ax-pr 3524  ax-un 3790

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-3an 860  df-ex 1327  df-sb 1536  df-eu 1775  df-mo 1776  df-clab 1872  df-cleq 1877  df-clel 1880  df-ne 2019  df-ral 2109  df-rex 2110  df-v 2294  df-dif 2597  df-un 2600  df-in 2603  df-ss 2605  df-nul 2876  df-pw 3035  df-sn 3049  df-pr 3050  df-op 3053  df-uni 3178  df-br 3339  df-opab 3396  df-id 3586  df-xp 4000  df-rel 4001  df-cnv 4002  df-co 4003  df-dm 4004  df-rn 4005  df-res 4006  df-ima 4007  df-fun 4008  df-fn 4009  df-f 4010  df-fo 4012  df-fv 4014  df-opr 4886  df-grp 9316

Copyright terms: Public domain