oppglsm

Description: The subspace sum operation in the opposite group. (Contributed by Mario Carneiro, 19-Apr-2016) (Proof shortened by AV, 2-Mar-2024)

	Ref	Expression
Hypotheses	oppglsm.o	$⊢ O = {opp}_{𝑔} (G)$
	oppglsm.p	$⊢ \underset{˙}{\oplus} = LSSum (G)$
Assertion	oppglsm	$⊢ T LSSum (O) U = U \underset{˙}{\oplus} T$

Proof

Step	Hyp	Ref	Expression
1		oppglsm.o	$⊢ O = {opp}_{𝑔} (G)$
2		oppglsm.p	$⊢ \underset{˙}{\oplus} = LSSum (G)$
3	1	fvexi	$⊢ O \in V$
4		eqid	$⊢ {Base}_{G} = {Base}_{G}$
5	1 4	oppgbas	$⊢ {Base}_{G} = {Base}_{O}$
6		eqid	$⊢ +_{O} = +_{O}$
7		eqid	$⊢ LSSum (O) = LSSum (O)$
8	5 6 7	lsmfval	$⊢ O \in V \to LSSum (O) = (t \in 𝒫 {Base}_{G}, u \in 𝒫 {Base}_{G} ⟼ ran (x \in t, y \in u ⟼ x +_{O} y))$
9	3 8	ax-mp	$⊢ LSSum (O) = (t \in 𝒫 {Base}_{G}, u \in 𝒫 {Base}_{G} ⟼ ran (x \in t, y \in u ⟼ x +_{O} y))$
10		eqid	$⊢ +_{G} = +_{G}$
11	4 10 2	lsmfval	$⊢ G \in V \to \underset{˙}{\oplus} = (u \in 𝒫 {Base}_{G}, t \in 𝒫 {Base}_{G} ⟼ ran (y \in u, x \in t ⟼ y +_{G} x))$
12	11	tposeqd	$⊢ G \in V \to tpos \underset{˙}{\oplus} = tpos (u \in 𝒫 {Base}_{G}, t \in 𝒫 {Base}_{G} ⟼ ran (y \in u, x \in t ⟼ y +_{G} x))$
13		eqid	$⊢ (y \in u, x \in t ⟼ y +_{G} x) = (y \in u, x \in t ⟼ y +_{G} x)$
14	13	reldmmpo	$⊢ Rel dom (y \in u, x \in t ⟼ y +_{G} x)$
15	13	mpofun	$⊢ Fun (y \in u, x \in t ⟼ y +_{G} x)$
16		funforn	$⊢ Fun (y \in u, x \in t ⟼ y +_{G} x) \leftrightarrow (y \in u, x \in t ⟼ y +_{G} x) : dom (y \in u, x \in t ⟼ y +_{G} x) \underset{onto}{⟶} ran (y \in u, x \in t ⟼ y +_{G} x)$
17	15 16	mpbi	$⊢ (y \in u, x \in t ⟼ y +_{G} x) : dom (y \in u, x \in t ⟼ y +_{G} x) \underset{onto}{⟶} ran (y \in u, x \in t ⟼ y +_{G} x)$
18		tposfo2	$⊢ Rel dom (y \in u, x \in t ⟼ y +_{G} x) \to ((y \in u, x \in t ⟼ y +_{G} x) : dom (y \in u, x \in t ⟼ y +_{G} x) \underset{onto}{⟶} ran (y \in u, x \in t ⟼ y +_{G} x) \to tpos (y \in u, x \in t ⟼ y +_{G} x) : {dom (y \in u, x \in t ⟼ y +_{G} x)}^{-1} \underset{onto}{⟶} ran (y \in u, x \in t ⟼ y +_{G} x))$
19	14 17 18	mp2	$⊢ tpos (y \in u, x \in t ⟼ y +_{G} x) : {dom (y \in u, x \in t ⟼ y +_{G} x)}^{-1} \underset{onto}{⟶} ran (y \in u, x \in t ⟼ y +_{G} x)$
20		forn	$⊢ tpos (y \in u, x \in t ⟼ y +_{G} x) : {dom (y \in u, x \in t ⟼ y +_{G} x)}^{-1} \underset{onto}{⟶} ran (y \in u, x \in t ⟼ y +_{G} x) \to ran tpos (y \in u, x \in t ⟼ y +_{G} x) = ran (y \in u, x \in t ⟼ y +_{G} x)$
21	19 20	ax-mp	$⊢ ran tpos (y \in u, x \in t ⟼ y +_{G} x) = ran (y \in u, x \in t ⟼ y +_{G} x)$
22	10 1 6	oppgplus	$⊢ x +_{O} y = y +_{G} x$
23	22	eqcomi	$⊢ y +_{G} x = x +_{O} y$
24	23	a1i	$⊢ (y \in u \land x \in t) \to y +_{G} x = x +_{O} y$
25	24	mpoeq3ia	$⊢ (y \in u, x \in t ⟼ y +_{G} x) = (y \in u, x \in t ⟼ x +_{O} y)$
26	25	tposmpo	$⊢ tpos (y \in u, x \in t ⟼ y +_{G} x) = (x \in t, y \in u ⟼ x +_{O} y)$
27	26	rneqi	$⊢ ran tpos (y \in u, x \in t ⟼ y +_{G} x) = ran (x \in t, y \in u ⟼ x +_{O} y)$
28	21 27	eqtr3i	$⊢ ran (y \in u, x \in t ⟼ y +_{G} x) = ran (x \in t, y \in u ⟼ x +_{O} y)$
29	28	a1i	$⊢ (u \in 𝒫 {Base}_{G} \land t \in 𝒫 {Base}_{G}) \to ran (y \in u, x \in t ⟼ y +_{G} x) = ran (x \in t, y \in u ⟼ x +_{O} y)$
30	29	mpoeq3ia	$⊢ (u \in 𝒫 {Base}_{G}, t \in 𝒫 {Base}_{G} ⟼ ran (y \in u, x \in t ⟼ y +_{G} x)) = (u \in 𝒫 {Base}_{G}, t \in 𝒫 {Base}_{G} ⟼ ran (x \in t, y \in u ⟼ x +_{O} y))$
31	30	tposmpo	$⊢ tpos (u \in 𝒫 {Base}_{G}, t \in 𝒫 {Base}_{G} ⟼ ran (y \in u, x \in t ⟼ y +_{G} x)) = (t \in 𝒫 {Base}_{G}, u \in 𝒫 {Base}_{G} ⟼ ran (x \in t, y \in u ⟼ x +_{O} y))$
32	12 31	eqtrdi	$⊢ G \in V \to tpos \underset{˙}{\oplus} = (t \in 𝒫 {Base}_{G}, u \in 𝒫 {Base}_{G} ⟼ ran (x \in t, y \in u ⟼ x +_{O} y))$
33	9 32	eqtr4id	$⊢ G \in V \to LSSum (O) = tpos \underset{˙}{\oplus}$
34	33	oveqd	$⊢ G \in V \to T LSSum (O) U = T tpos \underset{˙}{\oplus} U$
35		ovtpos	$⊢ T tpos \underset{˙}{\oplus} U = U \underset{˙}{\oplus} T$
36	34 35	eqtrdi	$⊢ G \in V \to T LSSum (O) U = U \underset{˙}{\oplus} T$
37		eqid	$⊢ (t \in 𝒫 {Base}_{G}, u \in 𝒫 {Base}_{G} ⟼ \emptyset) = (t \in 𝒫 {Base}_{G}, u \in 𝒫 {Base}_{G} ⟼ \emptyset)$
38		0ex	$⊢ \emptyset \in V$
39		eqidd	$⊢ (t = T \land u = U) \to \emptyset = \emptyset$
40	37 38 39	elovmpo	$⊢ x \in (T (t \in 𝒫 {Base}_{G}, u \in 𝒫 {Base}_{G} ⟼ \emptyset) U) \leftrightarrow (T \in 𝒫 {Base}_{G} \land U \in 𝒫 {Base}_{G} \land x \in \emptyset)$
41	40	simp3bi	$⊢ x \in (T (t \in 𝒫 {Base}_{G}, u \in 𝒫 {Base}_{G} ⟼ \emptyset) U) \to x \in \emptyset$
42	41	ssriv	$⊢ T (t \in 𝒫 {Base}_{G}, u \in 𝒫 {Base}_{G} ⟼ \emptyset) U \subseteq \emptyset$
43		ss0	$⊢ T (t \in 𝒫 {Base}_{G}, u \in 𝒫 {Base}_{G} ⟼ \emptyset) U \subseteq \emptyset \to T (t \in 𝒫 {Base}_{G}, u \in 𝒫 {Base}_{G} ⟼ \emptyset) U = \emptyset$
44	42 43	ax-mp	$⊢ T (t \in 𝒫 {Base}_{G}, u \in 𝒫 {Base}_{G} ⟼ \emptyset) U = \emptyset$
45		elpwi	$⊢ t \in 𝒫 {Base}_{G} \to t \subseteq {Base}_{G}$
46	45	3ad2ant2	$⊢ (\neg G \in V \land t \in 𝒫 {Base}_{G} \land u \in 𝒫 {Base}_{G}) \to t \subseteq {Base}_{G}$
47		fvprc	$⊢ \neg G \in V \to {Base}_{G} = \emptyset$
48	47	3ad2ant1	$⊢ (\neg G \in V \land t \in 𝒫 {Base}_{G} \land u \in 𝒫 {Base}_{G}) \to {Base}_{G} = \emptyset$
49	46 48	sseqtrd	$⊢ (\neg G \in V \land t \in 𝒫 {Base}_{G} \land u \in 𝒫 {Base}_{G}) \to t \subseteq \emptyset$
50		ss0	$⊢ t \subseteq \emptyset \to t = \emptyset$
51	49 50	syl	$⊢ (\neg G \in V \land t \in 𝒫 {Base}_{G} \land u \in 𝒫 {Base}_{G}) \to t = \emptyset$
52	51	orcd	$⊢ (\neg G \in V \land t \in 𝒫 {Base}_{G} \land u \in 𝒫 {Base}_{G}) \to (t = \emptyset \lor u = \emptyset)$
53		0mpo0	$⊢ (t = \emptyset \lor u = \emptyset) \to (x \in t, y \in u ⟼ x +_{O} y) = \emptyset$
54	52 53	syl	$⊢ (\neg G \in V \land t \in 𝒫 {Base}_{G} \land u \in 𝒫 {Base}_{G}) \to (x \in t, y \in u ⟼ x +_{O} y) = \emptyset$
55	54	rneqd	$⊢ (\neg G \in V \land t \in 𝒫 {Base}_{G} \land u \in 𝒫 {Base}_{G}) \to ran (x \in t, y \in u ⟼ x +_{O} y) = ran \emptyset$
56		rn0	$⊢ ran \emptyset = \emptyset$
57	55 56	eqtrdi	$⊢ (\neg G \in V \land t \in 𝒫 {Base}_{G} \land u \in 𝒫 {Base}_{G}) \to ran (x \in t, y \in u ⟼ x +_{O} y) = \emptyset$
58	57	mpoeq3dva	$⊢ \neg G \in V \to (t \in 𝒫 {Base}_{G}, u \in 𝒫 {Base}_{G} ⟼ ran (x \in t, y \in u ⟼ x +_{O} y)) = (t \in 𝒫 {Base}_{G}, u \in 𝒫 {Base}_{G} ⟼ \emptyset)$
59	9 58	syl5eq	$⊢ \neg G \in V \to LSSum (O) = (t \in 𝒫 {Base}_{G}, u \in 𝒫 {Base}_{G} ⟼ \emptyset)$
60	59	oveqd	$⊢ \neg G \in V \to T LSSum (O) U = T (t \in 𝒫 {Base}_{G}, u \in 𝒫 {Base}_{G} ⟼ \emptyset) U$
61		fvprc	$⊢ \neg G \in V \to LSSum (G) = \emptyset$
62	2 61	syl5eq	$⊢ \neg G \in V \to \underset{˙}{\oplus} = \emptyset$
63	62	oveqd	$⊢ \neg G \in V \to U \underset{˙}{\oplus} T = U \emptyset T$
64		0ov	$⊢ U \emptyset T = \emptyset$
65	63 64	eqtrdi	$⊢ \neg G \in V \to U \underset{˙}{\oplus} T = \emptyset$
66	44 60 65	3eqtr4a	$⊢ \neg G \in V \to T LSSum (O) U = U \underset{˙}{\oplus} T$
67	36 66	pm2.61i	$⊢ T LSSum (O) U = U \underset{˙}{\oplus} T$

Metamath Proof Explorer

Theorem oppglsm

Proof