lsmmod2

Description: Modular law dual for subgroup sum. Similar to part of Theorem 16.9 of MaedaMaeda p. 70. (Contributed by NM, 8-Jan-2015) (Revised by Mario Carneiro, 21-Apr-2016)

		Ref	Expression
	Hypothesis	lsmmod.p	$⊢ \underset{˙}{\oplus} = LSSum (G)$
	Assertion	lsmmod2	$⊢ ((S \in SubGrp (G) \land T \in SubGrp (G) \land U \in SubGrp (G)) \land U \subseteq S) \to S \cap (T \underset{˙}{\oplus} U) = (S \cap T) \underset{˙}{\oplus} U$

Proof

Step	Hyp	Ref	Expression
1		lsmmod.p	$⊢ \underset{˙}{\oplus} = LSSum (G)$
2		simpl3	$⊢ ((S \in SubGrp (G) \land T \in SubGrp (G) \land U \in SubGrp (G)) \land U \subseteq S) \to U \in SubGrp (G)$
3		eqid	$⊢ {opp}_{𝑔} (G) = {opp}_{𝑔} (G)$
4	3	oppgsubg	$⊢ SubGrp (G) = SubGrp ({opp}_{𝑔} (G))$
5	2 4	eleqtrdi	$⊢ ((S \in SubGrp (G) \land T \in SubGrp (G) \land U \in SubGrp (G)) \land U \subseteq S) \to U \in SubGrp ({opp}_{𝑔} (G))$
6		simpl2	$⊢ ((S \in SubGrp (G) \land T \in SubGrp (G) \land U \in SubGrp (G)) \land U \subseteq S) \to T \in SubGrp (G)$
7	6 4	eleqtrdi	$⊢ ((S \in SubGrp (G) \land T \in SubGrp (G) \land U \in SubGrp (G)) \land U \subseteq S) \to T \in SubGrp ({opp}_{𝑔} (G))$
8		simpl1	$⊢ ((S \in SubGrp (G) \land T \in SubGrp (G) \land U \in SubGrp (G)) \land U \subseteq S) \to S \in SubGrp (G)$
9	8 4	eleqtrdi	$⊢ ((S \in SubGrp (G) \land T \in SubGrp (G) \land U \in SubGrp (G)) \land U \subseteq S) \to S \in SubGrp ({opp}_{𝑔} (G))$
10		simpr	$⊢ ((S \in SubGrp (G) \land T \in SubGrp (G) \land U \in SubGrp (G)) \land U \subseteq S) \to U \subseteq S$
11		eqid	$⊢ LSSum ({opp}_{𝑔} (G)) = LSSum ({opp}_{𝑔} (G))$
12	11	lsmmod	$⊢ ((U \in SubGrp ({opp}_{𝑔} (G)) \land T \in SubGrp ({opp}_{𝑔} (G)) \land S \in SubGrp ({opp}_{𝑔} (G))) \land U \subseteq S) \to U LSSum ({opp}_{𝑔} (G)) (T \cap S) = (U LSSum ({opp}_{𝑔} (G)) T) \cap S$
13	5 7 9 10 12	syl31anc	$⊢ ((S \in SubGrp (G) \land T \in SubGrp (G) \land U \in SubGrp (G)) \land U \subseteq S) \to U LSSum ({opp}_{𝑔} (G)) (T \cap S) = (U LSSum ({opp}_{𝑔} (G)) T) \cap S$
14	13	eqcomd	$⊢ ((S \in SubGrp (G) \land T \in SubGrp (G) \land U \in SubGrp (G)) \land U \subseteq S) \to (U LSSum ({opp}_{𝑔} (G)) T) \cap S = U LSSum ({opp}_{𝑔} (G)) (T \cap S)$
15		incom	$⊢ (U LSSum ({opp}_{𝑔} (G)) T) \cap S = S \cap (U LSSum ({opp}_{𝑔} (G)) T)$
16		incom	$⊢ T \cap S = S \cap T$
17	16	oveq2i	$⊢ U LSSum ({opp}_{𝑔} (G)) (T \cap S) = U LSSum ({opp}_{𝑔} (G)) (S \cap T)$
18	14 15 17	3eqtr3g	$⊢ ((S \in SubGrp (G) \land T \in SubGrp (G) \land U \in SubGrp (G)) \land U \subseteq S) \to S \cap (U LSSum ({opp}_{𝑔} (G)) T) = U LSSum ({opp}_{𝑔} (G)) (S \cap T)$
19	3 1	oppglsm	$⊢ U LSSum ({opp}_{𝑔} (G)) T = T \underset{˙}{\oplus} U$
20	19	ineq2i	$⊢ S \cap (U LSSum ({opp}_{𝑔} (G)) T) = S \cap (T \underset{˙}{\oplus} U)$
21	3 1	oppglsm	$⊢ U LSSum ({opp}_{𝑔} (G)) (S \cap T) = (S \cap T) \underset{˙}{\oplus} U$
22	18 20 21	3eqtr3g	$⊢ ((S \in SubGrp (G) \land T \in SubGrp (G) \land U \in SubGrp (G)) \land U \subseteq S) \to S \cap (T \underset{˙}{\oplus} U) = (S \cap T) \underset{˙}{\oplus} U$

Metamath Proof Explorer

Theorem lsmmod2

Proof