Metamath Proof Explorer


Theorem isomuspgrlem1

Description: Lemma 1 for isomuspgr . (Contributed by AV, 29-Nov-2022)

Ref Expression
Hypotheses isomushgr.v V = Vtx A
isomushgr.w W = Vtx B
isomushgr.e E = Edg A
isomushgr.k K = Edg B
Assertion isomuspgrlem1 A USHGraph B USHGraph f : V 1-1 onto W g : E 1-1 onto K e E f e = g e a V b V f a f b K a b E

Proof

Step Hyp Ref Expression
1 isomushgr.v V = Vtx A
2 isomushgr.w W = Vtx B
3 isomushgr.e E = Edg A
4 isomushgr.k K = Edg B
5 simpl g : E 1-1 onto K e E f e = g e g : E 1-1 onto K
6 5 ad2antlr A USHGraph B USHGraph f : V 1-1 onto W g : E 1-1 onto K e E f e = g e a V b V g : E 1-1 onto K
7 f1ocnvdm g : E 1-1 onto K f a f b K g -1 f a f b E
8 6 7 sylan A USHGraph B USHGraph f : V 1-1 onto W g : E 1-1 onto K e E f e = g e a V b V f a f b K g -1 f a f b E
9 uspgrupgr A USHGraph A UPGraph
10 9 adantr A USHGraph B USHGraph A UPGraph
11 10 ad4antr A USHGraph B USHGraph f : V 1-1 onto W g : E 1-1 onto K e E f e = g e a V b V f a f b K A UPGraph
12 1 3 upgredg A UPGraph g -1 f a f b E x V y V g -1 f a f b = x y
13 11 12 sylan A USHGraph B USHGraph f : V 1-1 onto W g : E 1-1 onto K e E f e = g e a V b V f a f b K g -1 f a f b E x V y V g -1 f a f b = x y
14 eleq1 g -1 f a f b = x y g -1 f a f b E x y E
15 14 biimpd g -1 f a f b = x y g -1 f a f b E x y E
16 15 com12 g -1 f a f b E g -1 f a f b = x y x y E
17 16 ad2antlr A USHGraph B USHGraph f : V 1-1 onto W g : E 1-1 onto K e E f e = g e a V b V f a f b K g -1 f a f b E x V y V g -1 f a f b = x y x y E
18 17 imp A USHGraph B USHGraph f : V 1-1 onto W g : E 1-1 onto K e E f e = g e a V b V f a f b K g -1 f a f b E x V y V g -1 f a f b = x y x y E
19 5 ad6antlr A USHGraph B USHGraph f : V 1-1 onto W g : E 1-1 onto K e E f e = g e a V b V f a f b K g -1 f a f b E x V y V x y E g : E 1-1 onto K
20 simpr A USHGraph B USHGraph f : V 1-1 onto W g : E 1-1 onto K e E f e = g e a V b V f a f b K g -1 f a f b E x V y V x y E x y E
21 simpr A USHGraph B USHGraph f : V 1-1 onto W g : E 1-1 onto K e E f e = g e a V b V f a f b K f a f b K
22 21 ad5ant12 A USHGraph B USHGraph f : V 1-1 onto W g : E 1-1 onto K e E f e = g e a V b V f a f b K g -1 f a f b E x V y V x y E f a f b K
23 19 20 22 3jca A USHGraph B USHGraph f : V 1-1 onto W g : E 1-1 onto K e E f e = g e a V b V f a f b K g -1 f a f b E x V y V x y E g : E 1-1 onto K x y E f a f b K
24 f1ocnvfvb g : E 1-1 onto K x y E f a f b K g x y = f a f b g -1 f a f b = x y
25 23 24 syl A USHGraph B USHGraph f : V 1-1 onto W g : E 1-1 onto K e E f e = g e a V b V f a f b K g -1 f a f b E x V y V x y E g x y = f a f b g -1 f a f b = x y
26 imaeq2 e = x y f e = f x y
27 fveq2 e = x y g e = g x y
28 26 27 eqeq12d e = x y f e = g e f x y = g x y
29 28 rspccv e E f e = g e x y E f x y = g x y
30 29 adantl g : E 1-1 onto K e E f e = g e x y E f x y = g x y
31 30 adantl A USHGraph B USHGraph f : V 1-1 onto W g : E 1-1 onto K e E f e = g e x y E f x y = g x y
32 31 ad4antr A USHGraph B USHGraph f : V 1-1 onto W g : E 1-1 onto K e E f e = g e a V b V f a f b K g -1 f a f b E x V y V x y E f x y = g x y
33 32 imp A USHGraph B USHGraph f : V 1-1 onto W g : E 1-1 onto K e E f e = g e a V b V f a f b K g -1 f a f b E x V y V x y E f x y = g x y
34 eqeq1 g x y = f x y g x y = f a f b f x y = f a f b
35 34 eqcoms f x y = g x y g x y = f a f b f x y = f a f b
36 35 adantl A USHGraph B USHGraph f : V 1-1 onto W g : E 1-1 onto K e E f e = g e a V b V f a f b K g -1 f a f b E x V y V x y E f x y = g x y g x y = f a f b f x y = f a f b
37 f1ofn f : V 1-1 onto W f Fn V
38 37 ad6antlr A USHGraph B USHGraph f : V 1-1 onto W g : E 1-1 onto K e E f e = g e a V b V f a f b K g -1 f a f b E x V y V f Fn V
39 simpl x V y V x V
40 39 adantl A USHGraph B USHGraph f : V 1-1 onto W g : E 1-1 onto K e E f e = g e a V b V f a f b K g -1 f a f b E x V y V x V
41 simpr x V y V y V
42 41 adantl A USHGraph B USHGraph f : V 1-1 onto W g : E 1-1 onto K e E f e = g e a V b V f a f b K g -1 f a f b E x V y V y V
43 38 40 42 3jca A USHGraph B USHGraph f : V 1-1 onto W g : E 1-1 onto K e E f e = g e a V b V f a f b K g -1 f a f b E x V y V f Fn V x V y V
44 43 adantr A USHGraph B USHGraph f : V 1-1 onto W g : E 1-1 onto K e E f e = g e a V b V f a f b K g -1 f a f b E x V y V x y E f Fn V x V y V
45 fnimapr f Fn V x V y V f x y = f x f y
46 44 45 syl A USHGraph B USHGraph f : V 1-1 onto W g : E 1-1 onto K e E f e = g e a V b V f a f b K g -1 f a f b E x V y V x y E f x y = f x f y
47 46 eqeq1d A USHGraph B USHGraph f : V 1-1 onto W g : E 1-1 onto K e E f e = g e a V b V f a f b K g -1 f a f b E x V y V x y E f x y = f a f b f x f y = f a f b
48 fvex f x V
49 fvex f y V
50 fvex f a V
51 fvex f b V
52 48 49 50 51 preq12b f x f y = f a f b f x = f a f y = f b f x = f b f y = f a
53 f1of1 f : V 1-1 onto W f : V 1-1 W
54 simpl a V b V a V
55 54 39 anim12ci a V b V x V y V x V a V
56 f1veqaeq f : V 1-1 W x V a V f x = f a x = a
57 53 55 56 syl2anr a V b V x V y V f : V 1-1 onto W f x = f a x = a
58 simpr a V b V b V
59 58 41 anim12ci a V b V x V y V y V b V
60 f1veqaeq f : V 1-1 W y V b V f y = f b y = b
61 53 59 60 syl2anr a V b V x V y V f : V 1-1 onto W f y = f b y = b
62 57 61 anim12d a V b V x V y V f : V 1-1 onto W f x = f a f y = f b x = a y = b
63 62 impcom f x = f a f y = f b a V b V x V y V f : V 1-1 onto W x = a y = b
64 63 orcd f x = f a f y = f b a V b V x V y V f : V 1-1 onto W x = a y = b x = b y = a
65 64 ex f x = f a f y = f b a V b V x V y V f : V 1-1 onto W x = a y = b x = b y = a
66 58 39 anim12ci a V b V x V y V x V b V
67 f1veqaeq f : V 1-1 W x V b V f x = f b x = b
68 53 66 67 syl2anr a V b V x V y V f : V 1-1 onto W f x = f b x = b
69 54 41 anim12ci a V b V x V y V y V a V
70 f1veqaeq f : V 1-1 W y V a V f y = f a y = a
71 53 69 70 syl2anr a V b V x V y V f : V 1-1 onto W f y = f a y = a
72 68 71 anim12d a V b V x V y V f : V 1-1 onto W f x = f b f y = f a x = b y = a
73 72 impcom f x = f b f y = f a a V b V x V y V f : V 1-1 onto W x = b y = a
74 73 olcd f x = f b f y = f a a V b V x V y V f : V 1-1 onto W x = a y = b x = b y = a
75 74 ex f x = f b f y = f a a V b V x V y V f : V 1-1 onto W x = a y = b x = b y = a
76 65 75 jaoi f x = f a f y = f b f x = f b f y = f a a V b V x V y V f : V 1-1 onto W x = a y = b x = b y = a
77 vex x V
78 vex y V
79 vex a V
80 vex b V
81 77 78 79 80 preq12b x y = a b x = a y = b x = b y = a
82 76 81 syl6ibr f x = f a f y = f b f x = f b f y = f a a V b V x V y V f : V 1-1 onto W x y = a b
83 52 82 sylbi f x f y = f a f b a V b V x V y V f : V 1-1 onto W x y = a b
84 83 com12 a V b V x V y V f : V 1-1 onto W f x f y = f a f b x y = a b
85 84 expcom f : V 1-1 onto W a V b V x V y V f x f y = f a f b x y = a b
86 85 expd f : V 1-1 onto W a V b V x V y V f x f y = f a f b x y = a b
87 86 ad2antlr A USHGraph B USHGraph f : V 1-1 onto W g : E 1-1 onto K e E f e = g e a V b V x V y V f x f y = f a f b x y = a b
88 87 imp A USHGraph B USHGraph f : V 1-1 onto W g : E 1-1 onto K e E f e = g e a V b V x V y V f x f y = f a f b x y = a b
89 88 adantr A USHGraph B USHGraph f : V 1-1 onto W g : E 1-1 onto K e E f e = g e a V b V f a f b K x V y V f x f y = f a f b x y = a b
90 89 adantr A USHGraph B USHGraph f : V 1-1 onto W g : E 1-1 onto K e E f e = g e a V b V f a f b K g -1 f a f b E x V y V f x f y = f a f b x y = a b
91 90 imp31 A USHGraph B USHGraph f : V 1-1 onto W g : E 1-1 onto K e E f e = g e a V b V f a f b K g -1 f a f b E x V y V f x f y = f a f b x y = a b
92 91 eleq1d A USHGraph B USHGraph f : V 1-1 onto W g : E 1-1 onto K e E f e = g e a V b V f a f b K g -1 f a f b E x V y V f x f y = f a f b x y E a b E
93 92 biimpd A USHGraph B USHGraph f : V 1-1 onto W g : E 1-1 onto K e E f e = g e a V b V f a f b K g -1 f a f b E x V y V f x f y = f a f b x y E a b E
94 93 impancom A USHGraph B USHGraph f : V 1-1 onto W g : E 1-1 onto K e E f e = g e a V b V f a f b K g -1 f a f b E x V y V x y E f x f y = f a f b a b E
95 47 94 sylbid A USHGraph B USHGraph f : V 1-1 onto W g : E 1-1 onto K e E f e = g e a V b V f a f b K g -1 f a f b E x V y V x y E f x y = f a f b a b E
96 95 adantr A USHGraph B USHGraph f : V 1-1 onto W g : E 1-1 onto K e E f e = g e a V b V f a f b K g -1 f a f b E x V y V x y E f x y = g x y f x y = f a f b a b E
97 36 96 sylbid A USHGraph B USHGraph f : V 1-1 onto W g : E 1-1 onto K e E f e = g e a V b V f a f b K g -1 f a f b E x V y V x y E f x y = g x y g x y = f a f b a b E
98 33 97 mpdan A USHGraph B USHGraph f : V 1-1 onto W g : E 1-1 onto K e E f e = g e a V b V f a f b K g -1 f a f b E x V y V x y E g x y = f a f b a b E
99 25 98 sylbird A USHGraph B USHGraph f : V 1-1 onto W g : E 1-1 onto K e E f e = g e a V b V f a f b K g -1 f a f b E x V y V x y E g -1 f a f b = x y a b E
100 99 impancom A USHGraph B USHGraph f : V 1-1 onto W g : E 1-1 onto K e E f e = g e a V b V f a f b K g -1 f a f b E x V y V g -1 f a f b = x y x y E a b E
101 18 100 mpd A USHGraph B USHGraph f : V 1-1 onto W g : E 1-1 onto K e E f e = g e a V b V f a f b K g -1 f a f b E x V y V g -1 f a f b = x y a b E
102 101 ex A USHGraph B USHGraph f : V 1-1 onto W g : E 1-1 onto K e E f e = g e a V b V f a f b K g -1 f a f b E x V y V g -1 f a f b = x y a b E
103 102 rexlimdvva A USHGraph B USHGraph f : V 1-1 onto W g : E 1-1 onto K e E f e = g e a V b V f a f b K g -1 f a f b E x V y V g -1 f a f b = x y a b E
104 13 103 mpd A USHGraph B USHGraph f : V 1-1 onto W g : E 1-1 onto K e E f e = g e a V b V f a f b K g -1 f a f b E a b E
105 8 104 mpdan A USHGraph B USHGraph f : V 1-1 onto W g : E 1-1 onto K e E f e = g e a V b V f a f b K a b E
106 105 ex A USHGraph B USHGraph f : V 1-1 onto W g : E 1-1 onto K e E f e = g e a V b V f a f b K a b E