quslsm

Description: Express the image by the quotient map in terms of direct sum. (Contributed by Thierry Arnoux, 27-Jul-2024)

	Ref	Expression
Hypotheses	quslsm.b	$⊢ B = {Base}_{G}$
	quslsm.p	$⊢ \underset{˙}{\oplus} = LSSum (G)$
	quslsm.n	$⊢ φ \to S \in SubGrp (G)$
	quslsm.s	$⊢ φ \to X \in B$
Assertion	quslsm	$⊢ φ \to [X] (G ~_{QG} S) = \{X\} \underset{˙}{\oplus} S$

Proof

Step	Hyp	Ref	Expression
1		quslsm.b	$⊢ B = {Base}_{G}$
2		quslsm.p	$⊢ \underset{˙}{\oplus} = LSSum (G)$
3		quslsm.n	$⊢ φ \to S \in SubGrp (G)$
4		quslsm.s	$⊢ φ \to X \in B$
5		subgrcl	$⊢ S \in SubGrp (G) \to G \in Grp$
6	3 5	syl	$⊢ φ \to G \in Grp$
7	1	subgss	$⊢ S \in SubGrp (G) \to S \subseteq B$
8	3 7	syl	$⊢ φ \to S \subseteq B$
9		eqid	$⊢ {inv}_{g} (G) = {inv}_{g} (G)$
10		eqid	$⊢ +_{G} = +_{G}$
11		eqid	$⊢ G ~_{QG} S = G ~_{QG} S$
12	1 9 10 11	eqgfval	$⊢ (G \in Grp \land S \subseteq B) \to G ~_{QG} S = \{⟨i, j⟩ \| (\{i, j\} \subseteq B \land {inv}_{g} (G) (i) +_{G} j \in S)\}$
13	6 8 12	syl2anc	$⊢ φ \to G ~_{QG} S = \{⟨i, j⟩ \| (\{i, j\} \subseteq B \land {inv}_{g} (G) (i) +_{G} j \in S)\}$
14		simpr	$⊢ ((φ \land \{i, j\} \subseteq B) \land {inv}_{g} (G) (i) +_{G} j \in S) \to {inv}_{g} (G) (i) +_{G} j \in S$
15		oveq2	$⊢ k = {inv}_{g} (G) (i) +_{G} j \to i +_{G} k = i +_{G} ({inv}_{g} (G) (i) +_{G} j)$
16	15	eqeq1d	$⊢ k = {inv}_{g} (G) (i) +_{G} j \to (i +_{G} k = j \leftrightarrow i +_{G} ({inv}_{g} (G) (i) +_{G} j) = j)$
17	16	adantl	$⊢ (((φ \land \{i, j\} \subseteq B) \land {inv}_{g} (G) (i) +_{G} j \in S) \land k = {inv}_{g} (G) (i) +_{G} j) \to (i +_{G} k = j \leftrightarrow i +_{G} ({inv}_{g} (G) (i) +_{G} j) = j)$
18	6	adantr	$⊢ (φ \land \{i, j\} \subseteq B) \to G \in Grp$
19		vex	$⊢ i \in V$
20		vex	$⊢ j \in V$
21	19 20	prss	$⊢ (i \in B \land j \in B) \leftrightarrow \{i, j\} \subseteq B$
22	21	bicomi	$⊢ \{i, j\} \subseteq B \leftrightarrow (i \in B \land j \in B)$
23	22	simplbi	$⊢ \{i, j\} \subseteq B \to i \in B$
24	23	adantl	$⊢ (φ \land \{i, j\} \subseteq B) \to i \in B$
25		eqid	$⊢ 0_{G} = 0_{G}$
26	1 10 25 9	grprinv	$⊢ (G \in Grp \land i \in B) \to i +_{G} {inv}_{g} (G) (i) = 0_{G}$
27	18 24 26	syl2anc	$⊢ (φ \land \{i, j\} \subseteq B) \to i +_{G} {inv}_{g} (G) (i) = 0_{G}$
28	27	oveq1d	$⊢ (φ \land \{i, j\} \subseteq B) \to (i +_{G} {inv}_{g} (G) (i)) +_{G} j = 0_{G} +_{G} j$
29	1 9	grpinvcl	$⊢ (G \in Grp \land i \in B) \to {inv}_{g} (G) (i) \in B$
30	18 24 29	syl2anc	$⊢ (φ \land \{i, j\} \subseteq B) \to {inv}_{g} (G) (i) \in B$
31	22	simprbi	$⊢ \{i, j\} \subseteq B \to j \in B$
32	31	adantl	$⊢ (φ \land \{i, j\} \subseteq B) \to j \in B$
33	1 10	grpass	$⊢ (G \in Grp \land (i \in B \land {inv}_{g} (G) (i) \in B \land j \in B)) \to (i +_{G} {inv}_{g} (G) (i)) +_{G} j = i +_{G} ({inv}_{g} (G) (i) +_{G} j)$
34	18 24 30 32 33	syl13anc	$⊢ (φ \land \{i, j\} \subseteq B) \to (i +_{G} {inv}_{g} (G) (i)) +_{G} j = i +_{G} ({inv}_{g} (G) (i) +_{G} j)$
35	1 10 25	grplid	$⊢ (G \in Grp \land j \in B) \to 0_{G} +_{G} j = j$
36	18 32 35	syl2anc	$⊢ (φ \land \{i, j\} \subseteq B) \to 0_{G} +_{G} j = j$
37	28 34 36	3eqtr3d	$⊢ (φ \land \{i, j\} \subseteq B) \to i +_{G} ({inv}_{g} (G) (i) +_{G} j) = j$
38	37	adantr	$⊢ ((φ \land \{i, j\} \subseteq B) \land {inv}_{g} (G) (i) +_{G} j \in S) \to i +_{G} ({inv}_{g} (G) (i) +_{G} j) = j$
39	14 17 38	rspcedvd	$⊢ ((φ \land \{i, j\} \subseteq B) \land {inv}_{g} (G) (i) +_{G} j \in S) \to \exists k \in S i +_{G} k = j$
40		oveq2	$⊢ i +_{G} k = j \to {inv}_{g} (G) (i) +_{G} (i +_{G} k) = {inv}_{g} (G) (i) +_{G} j$
41	40	adantl	$⊢ (((φ \land \{i, j\} \subseteq B) \land k \in S) \land i +_{G} k = j) \to {inv}_{g} (G) (i) +_{G} (i +_{G} k) = {inv}_{g} (G) (i) +_{G} j$
42		simpll	$⊢ ((φ \land \{i, j\} \subseteq B) \land k \in S) \to φ$
43	24	adantr	$⊢ ((φ \land \{i, j\} \subseteq B) \land k \in S) \to i \in B$
44	8	adantr	$⊢ (φ \land \{i, j\} \subseteq B) \to S \subseteq B$
45	44	sselda	$⊢ ((φ \land \{i, j\} \subseteq B) \land k \in S) \to k \in B$
46	6	3ad2ant1	$⊢ (φ \land i \in B \land k \in B) \to G \in Grp$
47		simp2	$⊢ (φ \land i \in B \land k \in B) \to i \in B$
48	1 10 25 9	grplinv	$⊢ (G \in Grp \land i \in B) \to {inv}_{g} (G) (i) +_{G} i = 0_{G}$
49	46 47 48	syl2anc	$⊢ (φ \land i \in B \land k \in B) \to {inv}_{g} (G) (i) +_{G} i = 0_{G}$
50	49	oveq1d	$⊢ (φ \land i \in B \land k \in B) \to ({inv}_{g} (G) (i) +_{G} i) +_{G} k = 0_{G} +_{G} k$
51	46 47 29	syl2anc	$⊢ (φ \land i \in B \land k \in B) \to {inv}_{g} (G) (i) \in B$
52		simp3	$⊢ (φ \land i \in B \land k \in B) \to k \in B$
53	1 10	grpass	$⊢ (G \in Grp \land ({inv}_{g} (G) (i) \in B \land i \in B \land k \in B)) \to ({inv}_{g} (G) (i) +_{G} i) +_{G} k = {inv}_{g} (G) (i) +_{G} (i +_{G} k)$
54	46 51 47 52 53	syl13anc	$⊢ (φ \land i \in B \land k \in B) \to ({inv}_{g} (G) (i) +_{G} i) +_{G} k = {inv}_{g} (G) (i) +_{G} (i +_{G} k)$
55	1 10 25	grplid	$⊢ (G \in Grp \land k \in B) \to 0_{G} +_{G} k = k$
56	46 52 55	syl2anc	$⊢ (φ \land i \in B \land k \in B) \to 0_{G} +_{G} k = k$
57	50 54 56	3eqtr3d	$⊢ (φ \land i \in B \land k \in B) \to {inv}_{g} (G) (i) +_{G} (i +_{G} k) = k$
58	42 43 45 57	syl3anc	$⊢ ((φ \land \{i, j\} \subseteq B) \land k \in S) \to {inv}_{g} (G) (i) +_{G} (i +_{G} k) = k$
59	58	adantr	$⊢ (((φ \land \{i, j\} \subseteq B) \land k \in S) \land i +_{G} k = j) \to {inv}_{g} (G) (i) +_{G} (i +_{G} k) = k$
60	41 59	eqtr3d	$⊢ (((φ \land \{i, j\} \subseteq B) \land k \in S) \land i +_{G} k = j) \to {inv}_{g} (G) (i) +_{G} j = k$
61		simplr	$⊢ (((φ \land \{i, j\} \subseteq B) \land k \in S) \land i +_{G} k = j) \to k \in S$
62	60 61	eqeltrd	$⊢ (((φ \land \{i, j\} \subseteq B) \land k \in S) \land i +_{G} k = j) \to {inv}_{g} (G) (i) +_{G} j \in S$
63	62	r19.29an	$⊢ ((φ \land \{i, j\} \subseteq B) \land \exists k \in S i +_{G} k = j) \to {inv}_{g} (G) (i) +_{G} j \in S$
64	39 63	impbida	$⊢ (φ \land \{i, j\} \subseteq B) \to ({inv}_{g} (G) (i) +_{G} j \in S \leftrightarrow \exists k \in S i +_{G} k = j)$
65	64	pm5.32da	$⊢ φ \to ((\{i, j\} \subseteq B \land {inv}_{g} (G) (i) +_{G} j \in S) \leftrightarrow (\{i, j\} \subseteq B \land \exists k \in S i +_{G} k = j))$
66	65	opabbidv	$⊢ φ \to \{⟨i, j⟩ \| (\{i, j\} \subseteq B \land {inv}_{g} (G) (i) +_{G} j \in S)\} = \{⟨i, j⟩ \| (\{i, j\} \subseteq B \land \exists k \in S i +_{G} k = j)\}$
67	13 66	eqtrd	$⊢ φ \to G ~_{QG} S = \{⟨i, j⟩ \| (\{i, j\} \subseteq B \land \exists k \in S i +_{G} k = j)\}$
68	67	eceq2d	$⊢ φ \to [X] (G ~_{QG} S) = [X] \{⟨i, j⟩ \| (\{i, j\} \subseteq B \land \exists k \in S i +_{G} k = j)\}$
69		eqid	$⊢ \{⟨i, j⟩ \| (\{i, j\} \subseteq B \land \exists k \in S i +_{G} k = j)\} = \{⟨i, j⟩ \| (\{i, j\} \subseteq B \land \exists k \in S i +_{G} k = j)\}$
70	6	grpmndd	$⊢ φ \to G \in Mnd$
71	1 10 2 69 70 8 4	lsmsnorb2	$⊢ φ \to \{X\} \underset{˙}{\oplus} S = [X] \{⟨i, j⟩ \| (\{i, j\} \subseteq B \land \exists k \in S i +_{G} k = j)\}$
72	68 71	eqtr4d	$⊢ φ \to [X] (G ~_{QG} S) = \{X\} \underset{˙}{\oplus} S$

Metamath Proof Explorer

Theorem quslsm

Proof