Metamath Proof Explorer


Theorem exidreslem

Description: Lemma for exidres and exidresid . (Contributed by Jeff Madsen, 8-Jun-2010) (Revised by Mario Carneiro, 23-Dec-2013)

Ref Expression
Hypotheses exidres.1 X = ran G
exidres.2 U = GId G
exidres.3 H = G Y × Y
Assertion exidreslem G Magma ExId Y X U Y U dom dom H x dom dom H U H x = x x H U = x

Proof

Step Hyp Ref Expression
1 exidres.1 X = ran G
2 exidres.2 U = GId G
3 exidres.3 H = G Y × Y
4 3 dmeqi dom H = dom G Y × Y
5 xpss12 Y X Y X Y × Y X × X
6 5 anidms Y X Y × Y X × X
7 1 opidon2OLD G Magma ExId G : X × X onto X
8 fof G : X × X onto X G : X × X X
9 fdm G : X × X X dom G = X × X
10 7 8 9 3syl G Magma ExId dom G = X × X
11 10 sseq2d G Magma ExId Y × Y dom G Y × Y X × X
12 6 11 syl5ibr G Magma ExId Y X Y × Y dom G
13 12 imp G Magma ExId Y X Y × Y dom G
14 ssdmres Y × Y dom G dom G Y × Y = Y × Y
15 13 14 sylib G Magma ExId Y X dom G Y × Y = Y × Y
16 4 15 syl5eq G Magma ExId Y X dom H = Y × Y
17 16 dmeqd G Magma ExId Y X dom dom H = dom Y × Y
18 dmxpid dom Y × Y = Y
19 17 18 syl6eq G Magma ExId Y X dom dom H = Y
20 19 eleq2d G Magma ExId Y X U dom dom H U Y
21 20 biimp3ar G Magma ExId Y X U Y U dom dom H
22 ssel2 Y X x Y x X
23 1 2 cmpidelt G Magma ExId x X U G x = x x G U = x
24 22 23 sylan2 G Magma ExId Y X x Y U G x = x x G U = x
25 24 anassrs G Magma ExId Y X x Y U G x = x x G U = x
26 25 adantrl G Magma ExId Y X U Y x Y U G x = x x G U = x
27 3 oveqi U H x = U G Y × Y x
28 ovres U Y x Y U G Y × Y x = U G x
29 27 28 syl5eq U Y x Y U H x = U G x
30 29 eqeq1d U Y x Y U H x = x U G x = x
31 3 oveqi x H U = x G Y × Y U
32 ovres x Y U Y x G Y × Y U = x G U
33 31 32 syl5eq x Y U Y x H U = x G U
34 33 ancoms U Y x Y x H U = x G U
35 34 eqeq1d U Y x Y x H U = x x G U = x
36 30 35 anbi12d U Y x Y U H x = x x H U = x U G x = x x G U = x
37 36 adantl G Magma ExId Y X U Y x Y U H x = x x H U = x U G x = x x G U = x
38 26 37 mpbird G Magma ExId Y X U Y x Y U H x = x x H U = x
39 38 anassrs G Magma ExId Y X U Y x Y U H x = x x H U = x
40 39 ralrimiva G Magma ExId Y X U Y x Y U H x = x x H U = x
41 40 3impa G Magma ExId Y X U Y x Y U H x = x x H U = x
42 13 3adant3 G Magma ExId Y X U Y Y × Y dom G
43 42 14 sylib G Magma ExId Y X U Y dom G Y × Y = Y × Y
44 4 43 syl5eq G Magma ExId Y X U Y dom H = Y × Y
45 44 dmeqd G Magma ExId Y X U Y dom dom H = dom Y × Y
46 45 18 syl6eq G Magma ExId Y X U Y dom dom H = Y
47 46 raleqdv G Magma ExId Y X U Y x dom dom H U H x = x x H U = x x Y U H x = x x H U = x
48 41 47 mpbird G Magma ExId Y X U Y x dom dom H U H x = x x H U = x
49 21 48 jca G Magma ExId Y X U Y U dom dom H x dom dom H U H x = x x H U = x