Metamath Proof Explorer

Theorem ghmqusnsglem1

Description: Lemma for ghmqusnsg . (Contributed by Thierry Arnoux, 13-May-2025)

Ref Expression
Hypotheses ghmqusnsg.0 ⊢ 0 ˙ = 0 H
ghmqusnsg.f ⊢ φ → F ∈ G GrpHom H
ghmqusnsg.k ⊢ K = F -1 0 ˙
ghmqusnsg.q ⊢ Q = G / 𝑠 G ~ QG N
ghmqusnsg.j ⊢ J = q ∈ Base Q ⟼ ⋃ F q
ghmqusnsg.n ⊢ φ → N ⊆ K
ghmqusnsg.1 ⊢ φ → N ∈ NrmSGrp ⁡ G
ghmqusnsglem1.x ⊢ φ → X ∈ Base G
Assertion ghmqusnsglem1 ⊢ φ → J ⁡ X G ~ QG N = F ⁡ X

Proof

Step Hyp Ref Expression
1 ghmqusnsg.0 ⊢ 0 ˙ = 0 H
2 ghmqusnsg.f ⊢ φ → F ∈ G GrpHom H
3 ghmqusnsg.k ⊢ K = F -1 0 ˙
4 ghmqusnsg.q ⊢ Q = G / 𝑠 G ~ QG N
5 ghmqusnsg.j ⊢ J = q ∈ Base Q ⟼ ⋃ F q
6 ghmqusnsg.n ⊢ φ → N ⊆ K
7 ghmqusnsg.1 ⊢ φ → N ∈ NrmSGrp ⁡ G
8 ghmqusnsglem1.x ⊢ φ → X ∈ Base G
9 imaeq2 ⊢ q = X G ~ QG N → F q = F X G ~ QG N
10 9 unieqd ⊢ q = X G ~ QG N → ⋃ F q = ⋃ F X G ~ QG N
11 ovex ⊢ G ~ QG N ∈ V
12 11 ecelqsi ⊢ X ∈ Base G → X G ~ QG N ∈ Base G / G ~ QG N
13 8 12 syl ⊢ φ → X G ~ QG N ∈ Base G / G ~ QG N
14 4 a1i ⊢ φ → Q = G / 𝑠 G ~ QG N
15 eqidd ⊢ φ → Base G = Base G
16 ovexd ⊢ φ → G ~ QG N ∈ V
17 ghmgrp1 ⊢ F ∈ G GrpHom H → G ∈ Grp
18 2 17 syl ⊢ φ → G ∈ Grp
19 14 15 16 18 qusbas ⊢ φ → Base G / G ~ QG N = Base Q
20 13 19 eleqtrd ⊢ φ → X G ~ QG N ∈ Base Q
21 2 imaexd ⊢ φ → F X G ~ QG N ∈ V
22 21 uniexd ⊢ φ → ⋃ F X G ~ QG N ∈ V
23 5 10 20 22 fvmptd3 ⊢ φ → J ⁡ X G ~ QG N = ⋃ F X G ~ QG N
24 eqid ⊢ Base G = Base G
25 eqid ⊢ Base H = Base H
26 24 25 ghmf ⊢ F ∈ G GrpHom H → F : Base G ⟶ Base H
27 2 26 syl ⊢ φ → F : Base G ⟶ Base H
28 27 ffnd ⊢ φ → F Fn Base G
29 nsgsubg ⊢ N ∈ NrmSGrp ⁡ G → N ∈ SubGrp ⁡ G
30 eqid ⊢ G ~ QG N = G ~ QG N
31 24 30 eqger ⊢ N ∈ SubGrp ⁡ G → G ~ QG N Er Base G
32 7 29 31 3syl ⊢ φ → G ~ QG N Er Base G
33 32 ecss ⊢ φ → X G ~ QG N ⊆ Base G
34 28 33 fvelimabd ⊢ φ → y ∈ F X G ~ QG N ↔ ∃ z ∈ X G ~ QG N F ⁡ z = y
35 simpr ⊢ φ ∧ z ∈ X G ~ QG N ∧ F ⁡ z = y → F ⁡ z = y
36 2 adantr ⊢ φ ∧ z ∈ X G ~ QG N → F ∈ G GrpHom H
37 eqid ⊢ inv g ⁡ G = inv g ⁡ G
38 36 17 syl ⊢ φ ∧ z ∈ X G ~ QG N → G ∈ Grp
39 8 adantr ⊢ φ ∧ z ∈ X G ~ QG N → X ∈ Base G
40 24 37 38 39 grpinvcld ⊢ φ ∧ z ∈ X G ~ QG N → inv g ⁡ G ⁡ X ∈ Base G
41 33 sselda ⊢ φ ∧ z ∈ X G ~ QG N → z ∈ Base G
42 eqid ⊢ + G = + G
43 eqid ⊢ + H = + H
44 24 42 43 ghmlin ⊢ F ∈ G GrpHom H ∧ inv g ⁡ G ⁡ X ∈ Base G ∧ z ∈ Base G → F ⁡ inv g ⁡ G ⁡ X + G z = F ⁡ inv g ⁡ G ⁡ X + H F ⁡ z
45 36 40 41 44 syl3anc ⊢ φ ∧ z ∈ X G ~ QG N → F ⁡ inv g ⁡ G ⁡ X + G z = F ⁡ inv g ⁡ G ⁡ X + H F ⁡ z
46 28 adantr ⊢ φ ∧ z ∈ X G ~ QG N → F Fn Base G
47 6 3 sseqtrdi ⊢ φ → N ⊆ F -1 0 ˙
48 47 adantr ⊢ φ ∧ z ∈ X G ~ QG N → N ⊆ F -1 0 ˙
49 24 subgss ⊢ N ∈ SubGrp ⁡ G → N ⊆ Base G
50 7 29 49 3syl ⊢ φ → N ⊆ Base G
51 50 adantr ⊢ φ ∧ z ∈ X G ~ QG N → N ⊆ Base G
52 vex ⊢ z ∈ V
53 elecg ⊢ z ∈ V ∧ X ∈ Base G → z ∈ X G ~ QG N ↔ X G ~ QG N z
54 52 53 mpan ⊢ X ∈ Base G → z ∈ X G ~ QG N ↔ X G ~ QG N z
55 54 biimpa ⊢ X ∈ Base G ∧ z ∈ X G ~ QG N → X G ~ QG N z
56 8 55 sylan ⊢ φ ∧ z ∈ X G ~ QG N → X G ~ QG N z
57 24 37 42 30 eqgval ⊢ G ∈ Grp ∧ N ⊆ Base G → X G ~ QG N z ↔ X ∈ Base G ∧ z ∈ Base G ∧ inv g ⁡ G ⁡ X + G z ∈ N
58 57 biimpa ⊢ G ∈ Grp ∧ N ⊆ Base G ∧ X G ~ QG N z → X ∈ Base G ∧ z ∈ Base G ∧ inv g ⁡ G ⁡ X + G z ∈ N
59 58 simp3d ⊢ G ∈ Grp ∧ N ⊆ Base G ∧ X G ~ QG N z → inv g ⁡ G ⁡ X + G z ∈ N
60 38 51 56 59 syl21anc ⊢ φ ∧ z ∈ X G ~ QG N → inv g ⁡ G ⁡ X + G z ∈ N
61 48 60 sseldd ⊢ φ ∧ z ∈ X G ~ QG N → inv g ⁡ G ⁡ X + G z ∈ F -1 0 ˙
62 fniniseg ⊢ F Fn Base G → inv g ⁡ G ⁡ X + G z ∈ F -1 0 ˙ ↔ inv g ⁡ G ⁡ X + G z ∈ Base G ∧ F ⁡ inv g ⁡ G ⁡ X + G z = 0 ˙
63 62 biimpa ⊢ F Fn Base G ∧ inv g ⁡ G ⁡ X + G z ∈ F -1 0 ˙ → inv g ⁡ G ⁡ X + G z ∈ Base G ∧ F ⁡ inv g ⁡ G ⁡ X + G z = 0 ˙
64 46 61 63 syl2anc ⊢ φ ∧ z ∈ X G ~ QG N → inv g ⁡ G ⁡ X + G z ∈ Base G ∧ F ⁡ inv g ⁡ G ⁡ X + G z = 0 ˙
65 64 simprd ⊢ φ ∧ z ∈ X G ~ QG N → F ⁡ inv g ⁡ G ⁡ X + G z = 0 ˙
66 45 65 eqtr3d ⊢ φ ∧ z ∈ X G ~ QG N → F ⁡ inv g ⁡ G ⁡ X + H F ⁡ z = 0 ˙
67 66 oveq2d ⊢ φ ∧ z ∈ X G ~ QG N → F ⁡ X + H F ⁡ inv g ⁡ G ⁡ X + H F ⁡ z = F ⁡ X + H 0 ˙
68 eqid ⊢ inv g ⁡ H = inv g ⁡ H
69 24 37 68 ghminv ⊢ F ∈ G GrpHom H ∧ X ∈ Base G → F ⁡ inv g ⁡ G ⁡ X = inv g ⁡ H ⁡ F ⁡ X
70 36 39 69 syl2anc ⊢ φ ∧ z ∈ X G ~ QG N → F ⁡ inv g ⁡ G ⁡ X = inv g ⁡ H ⁡ F ⁡ X
71 70 oveq1d ⊢ φ ∧ z ∈ X G ~ QG N → F ⁡ inv g ⁡ G ⁡ X + H F ⁡ z = inv g ⁡ H ⁡ F ⁡ X + H F ⁡ z
72 71 oveq2d ⊢ φ ∧ z ∈ X G ~ QG N → F ⁡ X + H F ⁡ inv g ⁡ G ⁡ X + H F ⁡ z = F ⁡ X + H inv g ⁡ H ⁡ F ⁡ X + H F ⁡ z
73 ghmgrp2 ⊢ F ∈ G GrpHom H → H ∈ Grp
74 36 73 syl ⊢ φ ∧ z ∈ X G ~ QG N → H ∈ Grp
75 36 26 syl ⊢ φ ∧ z ∈ X G ~ QG N → F : Base G ⟶ Base H
76 75 39 ffvelcdmd ⊢ φ ∧ z ∈ X G ~ QG N → F ⁡ X ∈ Base H
77 75 41 ffvelcdmd ⊢ φ ∧ z ∈ X G ~ QG N → F ⁡ z ∈ Base H
78 25 43 68 grpasscan1 ⊢ H ∈ Grp ∧ F ⁡ X ∈ Base H ∧ F ⁡ z ∈ Base H → F ⁡ X + H inv g ⁡ H ⁡ F ⁡ X + H F ⁡ z = F ⁡ z
79 74 76 77 78 syl3anc ⊢ φ ∧ z ∈ X G ~ QG N → F ⁡ X + H inv g ⁡ H ⁡ F ⁡ X + H F ⁡ z = F ⁡ z
80 72 79 eqtrd ⊢ φ ∧ z ∈ X G ~ QG N → F ⁡ X + H F ⁡ inv g ⁡ G ⁡ X + H F ⁡ z = F ⁡ z
81 25 43 1 74 76 grpridd ⊢ φ ∧ z ∈ X G ~ QG N → F ⁡ X + H 0 ˙ = F ⁡ X
82 67 80 81 3eqtr3d ⊢ φ ∧ z ∈ X G ~ QG N → F ⁡ z = F ⁡ X
83 82 adantr ⊢ φ ∧ z ∈ X G ~ QG N ∧ F ⁡ z = y → F ⁡ z = F ⁡ X
84 35 83 eqtr3d ⊢ φ ∧ z ∈ X G ~ QG N ∧ F ⁡ z = y → y = F ⁡ X
85 84 r19.29an ⊢ φ ∧ ∃ z ∈ X G ~ QG N F ⁡ z = y → y = F ⁡ X
86 fveqeq2 ⊢ z = X → F ⁡ z = y ↔ F ⁡ X = y
87 ecref ⊢ G ~ QG N Er Base G ∧ X ∈ Base G → X ∈ X G ~ QG N
88 32 8 87 syl2anc ⊢ φ → X ∈ X G ~ QG N
89 88 adantr ⊢ φ ∧ y = F ⁡ X → X ∈ X G ~ QG N
90 simpr ⊢ φ ∧ y = F ⁡ X → y = F ⁡ X
91 90 eqcomd ⊢ φ ∧ y = F ⁡ X → F ⁡ X = y
92 86 89 91 rspcedvdw ⊢ φ ∧ y = F ⁡ X → ∃ z ∈ X G ~ QG N F ⁡ z = y
93 85 92 impbida ⊢ φ → ∃ z ∈ X G ~ QG N F ⁡ z = y ↔ y = F ⁡ X
94 velsn ⊢ y ∈ F ⁡ X ↔ y = F ⁡ X
95 93 94 bitr4di ⊢ φ → ∃ z ∈ X G ~ QG N F ⁡ z = y ↔ y ∈ F ⁡ X
96 34 95 bitrd ⊢ φ → y ∈ F X G ~ QG N ↔ y ∈ F ⁡ X
97 96 eqrdv ⊢ φ → F X G ~ QG N = F ⁡ X
98 97 unieqd ⊢ φ → ⋃ F X G ~ QG N = ⋃ F ⁡ X
99 fvex ⊢ F ⁡ X ∈ V
100 99 unisn ⊢ ⋃ F ⁡ X = F ⁡ X
101 98 100 eqtrdi ⊢ φ → ⋃ F X G ~ QG N = F ⁡ X
102 23 101 eqtrd ⊢ φ → J ⁡ X G ~ QG N = F ⁡ X