nsgqusf1olem1

	Ref	Expression
Hypotheses	nsgqusf1o.b	$⊢ B = {Base}_{G}$
	nsgqusf1o.s	$⊢ S = \{h \in SubGrp (G) \| N \subseteq h\}$
	nsgqusf1o.t	$⊢ T = SubGrp (Q)$
	nsgqusf1o.1	$⊢ \underset{˙}{\leq} = \leq_{toInc (S)}$
	nsgqusf1o.2	No typesetting found for \|- .c_ = ( le ` ( toInc ` T ) ) with typecode \|-
	nsgqusf1o.q	$⊢ Q = G /_{𝑠} (G ~_{QG} N)$
	nsgqusf1o.p	$⊢ \underset{˙}{\oplus} = LSSum (G)$
	nsgqusf1o.e	$⊢ E = (h \in S ⟼ ran (x \in h ⟼ \{x\} \underset{˙}{\oplus} N))$
	nsgqusf1o.f	$⊢ F = (f \in T ⟼ \{a \in B \| \{a\} \underset{˙}{\oplus} N \in f\})$
	nsgqusf1o.n	$⊢ φ \to N \in NrmSGrp (G)$
Assertion	nsgqusf1olem1	$⊢ ((φ \land h \in SubGrp (G)) \land N \subseteq h) \to ran (x \in h ⟼ \{x\} \underset{˙}{\oplus} N) \in T$

Proof

Step	Hyp	Ref	Expression
1		nsgqusf1o.b	$⊢ B = {Base}_{G}$
2		nsgqusf1o.s	$⊢ S = \{h \in SubGrp (G) \| N \subseteq h\}$
3		nsgqusf1o.t	$⊢ T = SubGrp (Q)$
4		nsgqusf1o.1	$⊢ \underset{˙}{\leq} = \leq_{toInc (S)}$
5		nsgqusf1o.2	Could not format .c_ = ( le ` ( toInc ` T ) ) : No typesetting found for \|- .c_ = ( le ` ( toInc ` T ) ) with typecode \|-
6		nsgqusf1o.q	$⊢ Q = G /_{𝑠} (G ~_{QG} N)$
7		nsgqusf1o.p	$⊢ \underset{˙}{\oplus} = LSSum (G)$
8		nsgqusf1o.e	$⊢ E = (h \in S ⟼ ran (x \in h ⟼ \{x\} \underset{˙}{\oplus} N))$
9		nsgqusf1o.f	$⊢ F = (f \in T ⟼ \{a \in B \| \{a\} \underset{˙}{\oplus} N \in f\})$
10		nsgqusf1o.n	$⊢ φ \to N \in NrmSGrp (G)$
11	6	qusgrp	$⊢ N \in NrmSGrp (G) \to Q \in Grp$
12	10 11	syl	$⊢ φ \to Q \in Grp$
13	12	ad2antrr	$⊢ ((φ \land h \in SubGrp (G)) \land N \subseteq h) \to Q \in Grp$
14	1	subgss	$⊢ h \in SubGrp (G) \to h \subseteq B$
15	14	ad2antlr	$⊢ ((φ \land h \in SubGrp (G)) \land N \subseteq h) \to h \subseteq B$
16	15	sselda	$⊢ (((φ \land h \in SubGrp (G)) \land N \subseteq h) \land x \in h) \to x \in B$
17		ovex	$⊢ G ~_{QG} N \in V$
18	17	ecelqsi	$⊢ x \in B \to [x] (G ~_{QG} N) \in (B / (G ~_{QG} N))$
19	16 18	syl	$⊢ (((φ \land h \in SubGrp (G)) \land N \subseteq h) \land x \in h) \to [x] (G ~_{QG} N) \in (B / (G ~_{QG} N))$
20		nsgsubg	$⊢ N \in NrmSGrp (G) \to N \in SubGrp (G)$
21	10 20	syl	$⊢ φ \to N \in SubGrp (G)$
22	21	ad3antrrr	$⊢ (((φ \land h \in SubGrp (G)) \land N \subseteq h) \land x \in h) \to N \in SubGrp (G)$
23	1 7 22 16	quslsm	$⊢ (((φ \land h \in SubGrp (G)) \land N \subseteq h) \land x \in h) \to [x] (G ~_{QG} N) = \{x\} \underset{˙}{\oplus} N$
24	6	a1i	$⊢ φ \to Q = G /_{𝑠} (G ~_{QG} N)$
25	1	a1i	$⊢ φ \to B = {Base}_{G}$
26		ovexd	$⊢ φ \to G ~_{QG} N \in V$
27		subgrcl	$⊢ N \in SubGrp (G) \to G \in Grp$
28	21 27	syl	$⊢ φ \to G \in Grp$
29	24 25 26 28	qusbas	$⊢ φ \to B / (G ~_{QG} N) = {Base}_{Q}$
30	29	ad3antrrr	$⊢ (((φ \land h \in SubGrp (G)) \land N \subseteq h) \land x \in h) \to B / (G ~_{QG} N) = {Base}_{Q}$
31	19 23 30	3eltr3d	$⊢ (((φ \land h \in SubGrp (G)) \land N \subseteq h) \land x \in h) \to \{x\} \underset{˙}{\oplus} N \in {Base}_{Q}$
32	31	ralrimiva	$⊢ ((φ \land h \in SubGrp (G)) \land N \subseteq h) \to \forall x \in h \{x\} \underset{˙}{\oplus} N \in {Base}_{Q}$
33		eqid	$⊢ (x \in h ⟼ \{x\} \underset{˙}{\oplus} N) = (x \in h ⟼ \{x\} \underset{˙}{\oplus} N)$
34	33	rnmptss	$⊢ \forall x \in h \{x\} \underset{˙}{\oplus} N \in {Base}_{Q} \to ran (x \in h ⟼ \{x\} \underset{˙}{\oplus} N) \subseteq {Base}_{Q}$
35	32 34	syl	$⊢ ((φ \land h \in SubGrp (G)) \land N \subseteq h) \to ran (x \in h ⟼ \{x\} \underset{˙}{\oplus} N) \subseteq {Base}_{Q}$
36		nfv	$⊢ Ⅎ x ((φ \land h \in SubGrp (G)) \land N \subseteq h)$
37		ovexd	$⊢ (((φ \land h \in SubGrp (G)) \land N \subseteq h) \land x \in h) \to \{x\} \underset{˙}{\oplus} N \in V$
38		eqid	$⊢ 0_{G} = 0_{G}$
39	38	subg0cl	$⊢ h \in SubGrp (G) \to 0_{G} \in h$
40	39	ne0d	$⊢ h \in SubGrp (G) \to h \neq \emptyset$
41	40	ad2antlr	$⊢ ((φ \land h \in SubGrp (G)) \land N \subseteq h) \to h \neq \emptyset$
42	36 37 33 41	rnmptn0	$⊢ ((φ \land h \in SubGrp (G)) \land N \subseteq h) \to ran (x \in h ⟼ \{x\} \underset{˙}{\oplus} N) \neq \emptyset$
43		nfmpt1	$⊢ \underline{Ⅎ} x (x \in h ⟼ \{x\} \underset{˙}{\oplus} N)$
44	43	nfrn	$⊢ \underline{Ⅎ} x ran (x \in h ⟼ \{x\} \underset{˙}{\oplus} N)$
45	44	nfel2	$⊢ Ⅎ x i \in ran (x \in h ⟼ \{x\} \underset{˙}{\oplus} N)$
46	36 45	nfan	$⊢ Ⅎ x (((φ \land h \in SubGrp (G)) \land N \subseteq h) \land i \in ran (x \in h ⟼ \{x\} \underset{˙}{\oplus} N))$
47	44	nfel2	$⊢ Ⅎ x i +_{Q} j \in ran (x \in h ⟼ \{x\} \underset{˙}{\oplus} N)$
48	44 47	nfralw	$⊢ Ⅎ x \forall j \in ran (x \in h ⟼ \{x\} \underset{˙}{\oplus} N) i +_{Q} j \in ran (x \in h ⟼ \{x\} \underset{˙}{\oplus} N)$
49	44	nfel2	$⊢ Ⅎ x {inv}_{g} (Q) (i) \in ran (x \in h ⟼ \{x\} \underset{˙}{\oplus} N)$
50	48 49	nfan	$⊢ Ⅎ x (\forall j \in ran (x \in h ⟼ \{x\} \underset{˙}{\oplus} N) i +_{Q} j \in ran (x \in h ⟼ \{x\} \underset{˙}{\oplus} N) \land {inv}_{g} (Q) (i) \in ran (x \in h ⟼ \{x\} \underset{˙}{\oplus} N))$
51		sneq	$⊢ x = z \to \{x\} = \{z\}$
52	51	oveq1d	$⊢ x = z \to \{x\} \underset{˙}{\oplus} N = \{z\} \underset{˙}{\oplus} N$
53	52	cbvmptv	$⊢ (x \in h ⟼ \{x\} \underset{˙}{\oplus} N) = (z \in h ⟼ \{z\} \underset{˙}{\oplus} N)$
54		simp-4r	$⊢ ((((φ \land h \in SubGrp (G)) \land N \subseteq h) \land x \in h) \land i = \{x\} \underset{˙}{\oplus} N) \to h \in SubGrp (G)$
55	54	ad2antrr	$⊢ ((((((φ \land h \in SubGrp (G)) \land N \subseteq h) \land x \in h) \land i = \{x\} \underset{˙}{\oplus} N) \land y \in h) \land j = \{y\} \underset{˙}{\oplus} N) \to h \in SubGrp (G)$
56		simp-4r	$⊢ ((((((φ \land h \in SubGrp (G)) \land N \subseteq h) \land x \in h) \land i = \{x\} \underset{˙}{\oplus} N) \land y \in h) \land j = \{y\} \underset{˙}{\oplus} N) \to x \in h$
57		simplr	$⊢ ((((((φ \land h \in SubGrp (G)) \land N \subseteq h) \land x \in h) \land i = \{x\} \underset{˙}{\oplus} N) \land y \in h) \land j = \{y\} \underset{˙}{\oplus} N) \to y \in h$
58		eqid	$⊢ +_{G} = +_{G}$
59	58	subgcl	$⊢ (h \in SubGrp (G) \land x \in h \land y \in h) \to x +_{G} y \in h$
60	55 56 57 59	syl3anc	$⊢ ((((((φ \land h \in SubGrp (G)) \land N \subseteq h) \land x \in h) \land i = \{x\} \underset{˙}{\oplus} N) \land y \in h) \land j = \{y\} \underset{˙}{\oplus} N) \to x +_{G} y \in h$
61		sneq	$⊢ z = x +_{G} y \to \{z\} = \{x +_{G} y\}$
62	61	oveq1d	$⊢ z = x +_{G} y \to \{z\} \underset{˙}{\oplus} N = \{x +_{G} y\} \underset{˙}{\oplus} N$
63	62	eqeq2d	$⊢ z = x +_{G} y \to (i +_{Q} j = \{z\} \underset{˙}{\oplus} N \leftrightarrow i +_{Q} j = \{x +_{G} y\} \underset{˙}{\oplus} N)$
64	63	adantl	$⊢ (((((((φ \land h \in SubGrp (G)) \land N \subseteq h) \land x \in h) \land i = \{x\} \underset{˙}{\oplus} N) \land y \in h) \land j = \{y\} \underset{˙}{\oplus} N) \land z = x +_{G} y) \to (i +_{Q} j = \{z\} \underset{˙}{\oplus} N \leftrightarrow i +_{Q} j = \{x +_{G} y\} \underset{˙}{\oplus} N)$
65		simpr	$⊢ ((((φ \land h \in SubGrp (G)) \land N \subseteq h) \land x \in h) \land i = \{x\} \underset{˙}{\oplus} N) \to i = \{x\} \underset{˙}{\oplus} N$
66	23	adantr	$⊢ ((((φ \land h \in SubGrp (G)) \land N \subseteq h) \land x \in h) \land i = \{x\} \underset{˙}{\oplus} N) \to [x] (G ~_{QG} N) = \{x\} \underset{˙}{\oplus} N$
67	65 66	eqtr4d	$⊢ ((((φ \land h \in SubGrp (G)) \land N \subseteq h) \land x \in h) \land i = \{x\} \underset{˙}{\oplus} N) \to i = [x] (G ~_{QG} N)$
68	67	ad2antrr	$⊢ ((((((φ \land h \in SubGrp (G)) \land N \subseteq h) \land x \in h) \land i = \{x\} \underset{˙}{\oplus} N) \land y \in h) \land j = \{y\} \underset{˙}{\oplus} N) \to i = [x] (G ~_{QG} N)$
69		simpr	$⊢ ((((((φ \land h \in SubGrp (G)) \land N \subseteq h) \land x \in h) \land i = \{x\} \underset{˙}{\oplus} N) \land y \in h) \land j = \{y\} \underset{˙}{\oplus} N) \to j = \{y\} \underset{˙}{\oplus} N$
70	10	ad4antr	$⊢ ((((φ \land h \in SubGrp (G)) \land N \subseteq h) \land x \in h) \land i = \{x\} \underset{˙}{\oplus} N) \to N \in NrmSGrp (G)$
71	70	ad2antrr	$⊢ ((((((φ \land h \in SubGrp (G)) \land N \subseteq h) \land x \in h) \land i = \{x\} \underset{˙}{\oplus} N) \land y \in h) \land j = \{y\} \underset{˙}{\oplus} N) \to N \in NrmSGrp (G)$
72	71 20	syl	$⊢ ((((((φ \land h \in SubGrp (G)) \land N \subseteq h) \land x \in h) \land i = \{x\} \underset{˙}{\oplus} N) \land y \in h) \land j = \{y\} \underset{˙}{\oplus} N) \to N \in SubGrp (G)$
73	55 14	syl	$⊢ ((((((φ \land h \in SubGrp (G)) \land N \subseteq h) \land x \in h) \land i = \{x\} \underset{˙}{\oplus} N) \land y \in h) \land j = \{y\} \underset{˙}{\oplus} N) \to h \subseteq B$
74	73 57	sseldd	$⊢ ((((((φ \land h \in SubGrp (G)) \land N \subseteq h) \land x \in h) \land i = \{x\} \underset{˙}{\oplus} N) \land y \in h) \land j = \{y\} \underset{˙}{\oplus} N) \to y \in B$
75	1 7 72 74	quslsm	$⊢ ((((((φ \land h \in SubGrp (G)) \land N \subseteq h) \land x \in h) \land i = \{x\} \underset{˙}{\oplus} N) \land y \in h) \land j = \{y\} \underset{˙}{\oplus} N) \to [y] (G ~_{QG} N) = \{y\} \underset{˙}{\oplus} N$
76	69 75	eqtr4d	$⊢ ((((((φ \land h \in SubGrp (G)) \land N \subseteq h) \land x \in h) \land i = \{x\} \underset{˙}{\oplus} N) \land y \in h) \land j = \{y\} \underset{˙}{\oplus} N) \to j = [y] (G ~_{QG} N)$
77	68 76	oveq12d	$⊢ ((((((φ \land h \in SubGrp (G)) \land N \subseteq h) \land x \in h) \land i = \{x\} \underset{˙}{\oplus} N) \land y \in h) \land j = \{y\} \underset{˙}{\oplus} N) \to i +_{Q} j = [x] (G ~_{QG} N) +_{Q} [y] (G ~_{QG} N)$
78	16	adantr	$⊢ ((((φ \land h \in SubGrp (G)) \land N \subseteq h) \land x \in h) \land i = \{x\} \underset{˙}{\oplus} N) \to x \in B$
79	78	ad2antrr	$⊢ ((((((φ \land h \in SubGrp (G)) \land N \subseteq h) \land x \in h) \land i = \{x\} \underset{˙}{\oplus} N) \land y \in h) \land j = \{y\} \underset{˙}{\oplus} N) \to x \in B$
80		eqid	$⊢ +_{Q} = +_{Q}$
81	6 1 58 80	qusadd	$⊢ (N \in NrmSGrp (G) \land x \in B \land y \in B) \to [x] (G ~_{QG} N) +_{Q} [y] (G ~_{QG} N) = [(x +_{G} y)] (G ~_{QG} N)$
82	71 79 74 81	syl3anc	$⊢ ((((((φ \land h \in SubGrp (G)) \land N \subseteq h) \land x \in h) \land i = \{x\} \underset{˙}{\oplus} N) \land y \in h) \land j = \{y\} \underset{˙}{\oplus} N) \to [x] (G ~_{QG} N) +_{Q} [y] (G ~_{QG} N) = [(x +_{G} y)] (G ~_{QG} N)$
83	73 60	sseldd	$⊢ ((((((φ \land h \in SubGrp (G)) \land N \subseteq h) \land x \in h) \land i = \{x\} \underset{˙}{\oplus} N) \land y \in h) \land j = \{y\} \underset{˙}{\oplus} N) \to x +_{G} y \in B$
84	1 7 72 83	quslsm	$⊢ ((((((φ \land h \in SubGrp (G)) \land N \subseteq h) \land x \in h) \land i = \{x\} \underset{˙}{\oplus} N) \land y \in h) \land j = \{y\} \underset{˙}{\oplus} N) \to [(x +_{G} y)] (G ~_{QG} N) = \{x +_{G} y\} \underset{˙}{\oplus} N$
85	77 82 84	3eqtrd	$⊢ ((((((φ \land h \in SubGrp (G)) \land N \subseteq h) \land x \in h) \land i = \{x\} \underset{˙}{\oplus} N) \land y \in h) \land j = \{y\} \underset{˙}{\oplus} N) \to i +_{Q} j = \{x +_{G} y\} \underset{˙}{\oplus} N$
86	60 64 85	rspcedvd	$⊢ ((((((φ \land h \in SubGrp (G)) \land N \subseteq h) \land x \in h) \land i = \{x\} \underset{˙}{\oplus} N) \land y \in h) \land j = \{y\} \underset{˙}{\oplus} N) \to \exists z \in h i +_{Q} j = \{z\} \underset{˙}{\oplus} N$
87		ovexd	$⊢ ((((((φ \land h \in SubGrp (G)) \land N \subseteq h) \land x \in h) \land i = \{x\} \underset{˙}{\oplus} N) \land y \in h) \land j = \{y\} \underset{˙}{\oplus} N) \to i +_{Q} j \in V$
88	53 86 87	elrnmptd	$⊢ ((((((φ \land h \in SubGrp (G)) \land N \subseteq h) \land x \in h) \land i = \{x\} \underset{˙}{\oplus} N) \land y \in h) \land j = \{y\} \underset{˙}{\oplus} N) \to i +_{Q} j \in ran (x \in h ⟼ \{x\} \underset{˙}{\oplus} N)$
89	88	adantllr	$⊢ (((((((φ \land h \in SubGrp (G)) \land N \subseteq h) \land x \in h) \land i = \{x\} \underset{˙}{\oplus} N) \land j \in ran (x \in h ⟼ \{x\} \underset{˙}{\oplus} N)) \land y \in h) \land j = \{y\} \underset{˙}{\oplus} N) \to i +_{Q} j \in ran (x \in h ⟼ \{x\} \underset{˙}{\oplus} N)$
90		sneq	$⊢ x = y \to \{x\} = \{y\}$
91	90	oveq1d	$⊢ x = y \to \{x\} \underset{˙}{\oplus} N = \{y\} \underset{˙}{\oplus} N$
92	91	cbvmptv	$⊢ (x \in h ⟼ \{x\} \underset{˙}{\oplus} N) = (y \in h ⟼ \{y\} \underset{˙}{\oplus} N)$
93		ovex	$⊢ \{y\} \underset{˙}{\oplus} N \in V$
94	92 93	elrnmpti	$⊢ j \in ran (x \in h ⟼ \{x\} \underset{˙}{\oplus} N) \leftrightarrow \exists y \in h j = \{y\} \underset{˙}{\oplus} N$
95	94	bilani	$⊢ (((((φ \land h \in SubGrp (G)) \land N \subseteq h) \land x \in h) \land i = \{x\} \underset{˙}{\oplus} N) \land j \in ran (x \in h ⟼ \{x\} \underset{˙}{\oplus} N)) \to \exists y \in h j = \{y\} \underset{˙}{\oplus} N$
96	89 95	r19.29a	$⊢ (((((φ \land h \in SubGrp (G)) \land N \subseteq h) \land x \in h) \land i = \{x\} \underset{˙}{\oplus} N) \land j \in ran (x \in h ⟼ \{x\} \underset{˙}{\oplus} N)) \to i +_{Q} j \in ran (x \in h ⟼ \{x\} \underset{˙}{\oplus} N)$
97	96	ralrimiva	$⊢ ((((φ \land h \in SubGrp (G)) \land N \subseteq h) \land x \in h) \land i = \{x\} \underset{˙}{\oplus} N) \to \forall j \in ran (x \in h ⟼ \{x\} \underset{˙}{\oplus} N) i +_{Q} j \in ran (x \in h ⟼ \{x\} \underset{˙}{\oplus} N)$
98		eqid	$⊢ {inv}_{g} (G) = {inv}_{g} (G)$
99	98	subginvcl	$⊢ (h \in SubGrp (G) \land x \in h) \to {inv}_{g} (G) (x) \in h$
100	99	ad5ant24	$⊢ ((((φ \land h \in SubGrp (G)) \land N \subseteq h) \land x \in h) \land i = \{x\} \underset{˙}{\oplus} N) \to {inv}_{g} (G) (x) \in h$
101		simpr	$⊢ (((((φ \land h \in SubGrp (G)) \land N \subseteq h) \land x \in h) \land i = \{x\} \underset{˙}{\oplus} N) \land y = {inv}_{g} (G) (x)) \to y = {inv}_{g} (G) (x)$
102	101	sneqd	$⊢ (((((φ \land h \in SubGrp (G)) \land N \subseteq h) \land x \in h) \land i = \{x\} \underset{˙}{\oplus} N) \land y = {inv}_{g} (G) (x)) \to \{y\} = \{{inv}_{g} (G) (x)\}$
103	102	oveq1d	$⊢ (((((φ \land h \in SubGrp (G)) \land N \subseteq h) \land x \in h) \land i = \{x\} \underset{˙}{\oplus} N) \land y = {inv}_{g} (G) (x)) \to \{y\} \underset{˙}{\oplus} N = \{{inv}_{g} (G) (x)\} \underset{˙}{\oplus} N$
104	15	adantr	$⊢ (((φ \land h \in SubGrp (G)) \land N \subseteq h) \land x \in h) \to h \subseteq B$
105	99	ad4ant24	$⊢ (((φ \land h \in SubGrp (G)) \land N \subseteq h) \land x \in h) \to {inv}_{g} (G) (x) \in h$
106	104 105	sseldd	$⊢ (((φ \land h \in SubGrp (G)) \land N \subseteq h) \land x \in h) \to {inv}_{g} (G) (x) \in B$
107	1 7 22 106	quslsm	$⊢ (((φ \land h \in SubGrp (G)) \land N \subseteq h) \land x \in h) \to [{inv}_{g} (G) (x)] (G ~_{QG} N) = \{{inv}_{g} (G) (x)\} \underset{˙}{\oplus} N$
108	107	ad2antrr	$⊢ (((((φ \land h \in SubGrp (G)) \land N \subseteq h) \land x \in h) \land i = \{x\} \underset{˙}{\oplus} N) \land y = {inv}_{g} (G) (x)) \to [{inv}_{g} (G) (x)] (G ~_{QG} N) = \{{inv}_{g} (G) (x)\} \underset{˙}{\oplus} N$
109	103 108	eqtr4d	$⊢ (((((φ \land h \in SubGrp (G)) \land N \subseteq h) \land x \in h) \land i = \{x\} \underset{˙}{\oplus} N) \land y = {inv}_{g} (G) (x)) \to \{y\} \underset{˙}{\oplus} N = [{inv}_{g} (G) (x)] (G ~_{QG} N)$
110	109	eqeq2d	$⊢ (((((φ \land h \in SubGrp (G)) \land N \subseteq h) \land x \in h) \land i = \{x\} \underset{˙}{\oplus} N) \land y = {inv}_{g} (G) (x)) \to ({inv}_{g} (Q) (i) = \{y\} \underset{˙}{\oplus} N \leftrightarrow {inv}_{g} (Q) (i) = [{inv}_{g} (G) (x)] (G ~_{QG} N))$
111	67	fveq2d	$⊢ ((((φ \land h \in SubGrp (G)) \land N \subseteq h) \land x \in h) \land i = \{x\} \underset{˙}{\oplus} N) \to {inv}_{g} (Q) (i) = {inv}_{g} (Q) ([x] (G ~_{QG} N))$
112		eqid	$⊢ {inv}_{g} (Q) = {inv}_{g} (Q)$
113	6 1 98 112	qusinv	$⊢ (N \in NrmSGrp (G) \land x \in B) \to {inv}_{g} (Q) ([x] (G ~_{QG} N)) = [{inv}_{g} (G) (x)] (G ~_{QG} N)$
114	70 78 113	syl2anc	$⊢ ((((φ \land h \in SubGrp (G)) \land N \subseteq h) \land x \in h) \land i = \{x\} \underset{˙}{\oplus} N) \to {inv}_{g} (Q) ([x] (G ~_{QG} N)) = [{inv}_{g} (G) (x)] (G ~_{QG} N)$
115	111 114	eqtrd	$⊢ ((((φ \land h \in SubGrp (G)) \land N \subseteq h) \land x \in h) \land i = \{x\} \underset{˙}{\oplus} N) \to {inv}_{g} (Q) (i) = [{inv}_{g} (G) (x)] (G ~_{QG} N)$
116	100 110 115	rspcedvd	$⊢ ((((φ \land h \in SubGrp (G)) \land N \subseteq h) \land x \in h) \land i = \{x\} \underset{˙}{\oplus} N) \to \exists y \in h {inv}_{g} (Q) (i) = \{y\} \underset{˙}{\oplus} N$
117		fvexd	$⊢ ((((φ \land h \in SubGrp (G)) \land N \subseteq h) \land x \in h) \land i = \{x\} \underset{˙}{\oplus} N) \to {inv}_{g} (Q) (i) \in V$
118	92 116 117	elrnmptd	$⊢ ((((φ \land h \in SubGrp (G)) \land N \subseteq h) \land x \in h) \land i = \{x\} \underset{˙}{\oplus} N) \to {inv}_{g} (Q) (i) \in ran (x \in h ⟼ \{x\} \underset{˙}{\oplus} N)$
119	97 118	jca	$⊢ ((((φ \land h \in SubGrp (G)) \land N \subseteq h) \land x \in h) \land i = \{x\} \underset{˙}{\oplus} N) \to (\forall j \in ran (x \in h ⟼ \{x\} \underset{˙}{\oplus} N) i +_{Q} j \in ran (x \in h ⟼ \{x\} \underset{˙}{\oplus} N) \land {inv}_{g} (Q) (i) \in ran (x \in h ⟼ \{x\} \underset{˙}{\oplus} N))$
120	119	adantllr	$⊢ (((((φ \land h \in SubGrp (G)) \land N \subseteq h) \land i \in ran (x \in h ⟼ \{x\} \underset{˙}{\oplus} N)) \land x \in h) \land i = \{x\} \underset{˙}{\oplus} N) \to (\forall j \in ran (x \in h ⟼ \{x\} \underset{˙}{\oplus} N) i +_{Q} j \in ran (x \in h ⟼ \{x\} \underset{˙}{\oplus} N) \land {inv}_{g} (Q) (i) \in ran (x \in h ⟼ \{x\} \underset{˙}{\oplus} N))$
121		ovex	$⊢ \{x\} \underset{˙}{\oplus} N \in V$
122	33 121	elrnmpti	$⊢ i \in ran (x \in h ⟼ \{x\} \underset{˙}{\oplus} N) \leftrightarrow \exists x \in h i = \{x\} \underset{˙}{\oplus} N$
123	122	bilani	$⊢ (((φ \land h \in SubGrp (G)) \land N \subseteq h) \land i \in ran (x \in h ⟼ \{x\} \underset{˙}{\oplus} N)) \to \exists x \in h i = \{x\} \underset{˙}{\oplus} N$
124	46 50 120 123	r19.29af2	$⊢ (((φ \land h \in SubGrp (G)) \land N \subseteq h) \land i \in ran (x \in h ⟼ \{x\} \underset{˙}{\oplus} N)) \to (\forall j \in ran (x \in h ⟼ \{x\} \underset{˙}{\oplus} N) i +_{Q} j \in ran (x \in h ⟼ \{x\} \underset{˙}{\oplus} N) \land {inv}_{g} (Q) (i) \in ran (x \in h ⟼ \{x\} \underset{˙}{\oplus} N))$
125	124	ralrimiva	$⊢ ((φ \land h \in SubGrp (G)) \land N \subseteq h) \to \forall i \in ran (x \in h ⟼ \{x\} \underset{˙}{\oplus} N) (\forall j \in ran (x \in h ⟼ \{x\} \underset{˙}{\oplus} N) i +_{Q} j \in ran (x \in h ⟼ \{x\} \underset{˙}{\oplus} N) \land {inv}_{g} (Q) (i) \in ran (x \in h ⟼ \{x\} \underset{˙}{\oplus} N))$
126		eqid	$⊢ {Base}_{Q} = {Base}_{Q}$
127	126 80 112	issubg2	$⊢ Q \in Grp \to (ran (x \in h ⟼ \{x\} \underset{˙}{\oplus} N) \in SubGrp (Q) \leftrightarrow (ran (x \in h ⟼ \{x\} \underset{˙}{\oplus} N) \subseteq {Base}_{Q} \land ran (x \in h ⟼ \{x\} \underset{˙}{\oplus} N) \neq \emptyset \land \forall i \in ran (x \in h ⟼ \{x\} \underset{˙}{\oplus} N) (\forall j \in ran (x \in h ⟼ \{x\} \underset{˙}{\oplus} N) i +_{Q} j \in ran (x \in h ⟼ \{x\} \underset{˙}{\oplus} N) \land {inv}_{g} (Q) (i) \in ran (x \in h ⟼ \{x\} \underset{˙}{\oplus} N))))$
128	127	biimpar	$⊢ (Q \in Grp \land (ran (x \in h ⟼ \{x\} \underset{˙}{\oplus} N) \subseteq {Base}_{Q} \land ran (x \in h ⟼ \{x\} \underset{˙}{\oplus} N) \neq \emptyset \land \forall i \in ran (x \in h ⟼ \{x\} \underset{˙}{\oplus} N) (\forall j \in ran (x \in h ⟼ \{x\} \underset{˙}{\oplus} N) i +_{Q} j \in ran (x \in h ⟼ \{x\} \underset{˙}{\oplus} N) \land {inv}_{g} (Q) (i) \in ran (x \in h ⟼ \{x\} \underset{˙}{\oplus} N)))) \to ran (x \in h ⟼ \{x\} \underset{˙}{\oplus} N) \in SubGrp (Q)$
129	13 35 42 125 128	syl13anc	$⊢ ((φ \land h \in SubGrp (G)) \land N \subseteq h) \to ran (x \in h ⟼ \{x\} \underset{˙}{\oplus} N) \in SubGrp (Q)$
130	129 3	eleqtrrdi	$⊢ ((φ \land h \in SubGrp (G)) \land N \subseteq h) \to ran (x \in h ⟼ \{x\} \underset{˙}{\oplus} N) \in T$

Metamath Proof Explorer

Theorem nsgqusf1olem1

Proof