Theorem grpidinvlem3 8050

Description: Lemma for grpidinv 8052.

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 3969	. . . . . . . 8 |- (x = A -> (yGx) = (yGA))
2	1	eqeq1d 1483	. . . . . . 7 |- (x = A -> ((yGx) = U <-> (yGA) = U))
3	2	rexbidv 1664	. . . . . 6 |- (x = A -> (E.y e. X (yGx) = U <-> E.y e. X (yGA) = U))
4	3	rcla4cva 1876	. . . . 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 3968	. . . . . . . . 9 |- (z = y -> (zGx) = (yGx))
7	6	eqeq1d 1483	. . . . . . . 8 |- (z = y -> ((zGx) = U <-> (yGx) = U))
8	7	cbvrexv 1801	. . . . . . 7 |- (E.z e. X (zGx) = U <-> E.y e. X (yGx) = U)
9	8	ralbii 1667	. . . . . 6 |- (A.x e. X E.z e. X (zGx) = U <-> A.x e. X E.y e. X (yGx) = U)
10	5, 9	bitr 173	. . . . 5 |- (ps <-> A.x e. X E.y e. X (yGx) = U)
11	4, 10	sylanb 449	. . . 4 |- ((ps /\ A e. X) -> E.y e. X (yGA) = U)
12	11	adantll 392	. . 3 |- (((ph /\ ps) /\ A e. X) -> E.y e. X (yGA) = U)
13	12	adantll 392	. 2 |- ((((G e. Grp /\ U e. X) /\ (ph /\ ps)) /\ A e. X) -> E.y e. X (yGA) = U)
14		opreq2 3969	. . . . . . . . . 10 |- (x = (AGy) -> (UGx) = (UG(AGy)))
15		id 59	. . . . . . . . . 10 |- (x = (AGy) -> x = (AGy))
16	14, 15	eqeq12d 1489	. . . . . . . . 9 |- (x = (AGy) -> ((UGx) = x <-> (UG(AGy)) = (AGy)))
17	16	rcla4va 1875	. . . . . . . 8 |- (((AGy) e. X /\ A.x e. X (UGx) = x) -> (UG(AGy)) = (AGy))
18		grpfo.1	. . . . . . . . . . . 12 |- X = ran G
19	18	grpcl 8044	. . . . . . . . . . 11 |- ((G e. Grp /\ A e. X /\ y e. X) -> (AGy) e. X)
20	19	3expa 833	. . . . . . . . . 10 |- (((G e. Grp /\ A e. X) /\ y e. X) -> (AGy) e. X)
21	20	adantllr 397	. . . . . . . . 9 |- ((((G e. Grp /\ U e. X) /\ A e. X) /\ y e. X) -> (AGy) e. X)
22	21	adantllr 397	. . . . . . . 8 |- (((((G e. Grp /\ U e. X) /\ (ph /\ ps)) /\ A e. X) /\ y e. X) -> (AGy) e. X)
23		grpidinvlem3.2	. . . . . . . . . . 11 |- (ph <-> A.x e. X (UGx) = x)
24	23	biimp 151	. . . . . . . . . 10 |- (ph -> A.x e. X (UGx) = x)
25	24	ad2antrl 406	. . . . . . . . 9 |- (((G e. Grp /\ U e. X) /\ (ph /\ ps)) -> A.x e. X (UGx) = x)
26	25	ad2antrr 404	. . . . . . . 8 |- (((((G e. Grp /\ U e. X) /\ (ph /\ ps)) /\ A e. X) /\ y e. X) -> A.x e. X (UGx) = x)
27	17, 22, 26	sylanc 471	. . . . . . 7 |- (((((G e. Grp /\ U e. X) /\ (ph /\ ps)) /\ A e. X) /\ y e. X) -> (UG(AGy)) = (AGy))
28	27	adantr 389	. . . . . 6 |- ((((((G e. Grp /\ U e. X) /\ (ph /\ ps)) /\ A e. X) /\ y e. X) /\ (yGA) = U) -> (UG(AGy)) = (AGy))
29	18	grpidinvlem2 8049	. . . . . . . 8 |- (((G e. Grp /\ (y e. X /\ A e. X)) /\ ((UGy) = y /\ (yGA) = U)) -> ((AGy)G(AGy)) = (AGy))
30		pm3.22 438	. . . . . . . . . . . 12 |- (((y e. X /\ A e. X) /\ G e. Grp) -> (G e. Grp /\ (y e. X /\ A e. X)))
31	30	ancom31s 491	. . . . . . . . . . 11 |- (((G e. Grp /\ A e. X) /\ y e. X) -> (G e. Grp /\ (y e. X /\ A e. X)))
32	31	adantllr 397	. . . . . . . . . 10 |- ((((G e. Grp /\ U e. X) /\ A e. X) /\ y e. X) -> (G e. Grp /\ (y e. X /\ A e. X)))
33	32	adantllr 397	. . . . . . . . 9 |- (((((G e. Grp /\ U e. X) /\ (ph /\ ps)) /\ A e. X) /\ y e. X) -> (G e. Grp /\ (y e. X /\ A e. X)))
34	33	adantr 389	. . . . . . . 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)))
35		opreq2 3969	. . . . . . . . . . . . . . 15 |- (x = y -> (UGx) = (UGy))
36		id 59	. . . . . . . . . . . . . . 15 |- (x = y -> x = y)
37	35, 36	eqeq12d 1489	. . . . . . . . . . . . . 14 |- (x = y -> ((UGx) = x <-> (UGy) = y))
38	37	rcla4cva 1876	. . . . . . . . . . . . 13 |- ((A.x e. X (UGx) = x /\ y e. X) -> (UGy) = y)
39	38, 23	sylanb 449	. . . . . . . . . . . 12 |- ((ph /\ y e. X) -> (UGy) = y)
40	39	adantlr 393	. . . . . . . . . . 11 |- (((ph /\ ps) /\ y e. X) -> (UGy) = y)
41	40	adantlr 393	. . . . . . . . . 10 |- ((((ph /\ ps) /\ A e. X) /\ y e. X) -> (UGy) = y)
42	41	adantlll 396	. . . . . . . . 9 |- (((((G e. Grp /\ U e. X) /\ (ph /\ ps)) /\ A e. X) /\ y e. X) -> (UGy) = y)
43	42	anim1i 334	. . . . . . . 8 |- ((((((G e. Grp /\ U e. X) /\ (ph /\ ps)) /\ A e. X) /\ y e. X) /\ (yGA) = U) -> ((UGy) = y /\ (yGA) = U))
44	29, 34, 43	sylanc 471	. . . . . . 7 |- ((((((G e. Grp /\ U e. X) /\ (ph /\ ps)) /\ A e. X) /\ y e. X) /\ (yGA) = U) -> ((AGy)G(AGy)) = (AGy))
45	19	3expb 834	. . . . . . . . . . . . . . 15 |- ((G e. Grp /\ (A e. X /\ y e. X)) -> (AGy) e. X)
46	45	ad2ant2rl 411	. . . . . . . . . . . . . 14 |- (((G e. Grp /\ U e. X) /\ (ph /\ (A e. X /\ y e. X))) -> (AGy) e. X)
47	18	grpidinvlem1 8048	. . . . . . . . . . . . . . . . . 18 |- (((G e. Grp /\ (w e. X /\ (AGy) e. X)) /\ ((wG(AGy)) = U /\ ((AGy)G(AGy)) = (AGy))) -> (UG(AGy)) = U)
48		anass 439	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (((G e. Grp /\ w e. X) /\ (AGy) e. X) <-> (G e. Grp /\ (w e. X /\ (AGy) e. X)))
49	48	biimp 151	. . . . . . . . . . . . . . . . . . . . . . 23 |- (((G e. Grp /\ w e. X) /\ (AGy) e. X) -> (G e. Grp /\ (w e. X /\ (AGy) e. X)))
50	49	an1rs 489	. . . . . . . . . . . . . . . . . . . . . 22 |- (((G e. Grp /\ (AGy) e. X) /\ w e. X) -> (G e. Grp /\ (w e. X /\ (AGy) e. X)))
51	50	ex 373	. . . . . . . . . . . . . . . . . . . . 21 |- ((G e. Grp /\ (AGy) e. X) -> (w e. X -> (G e. Grp /\ (w e. X /\ (AGy) e. X))))
52	45, 51	syldan 467	. . . . . . . . . . . . . . . . . . . 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 411	. . . . . . . . . . . . . . . . . . 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 350	. . . . . . . . . . . . . . . . . 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 448	. . . . . . . . . . . . . . . . 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 384	. . . . . . . . . . . . . . . 16 |- (((G e. Grp /\ U e. X) /\ (ph /\ (A e. X /\ y e. X))) -> (w e. X -> ((wG(AGy)) = U -> (((AG