lsmhash

Description: The order of the direct product of groups. (Contributed by Mario Carneiro, 21-Apr-2016)

	Ref	Expression
Hypotheses	lsmhash.p	$⊢ \underset{˙}{\oplus} = LSSum (G)$
	lsmhash.o	$⊢ \underset{˙}{0} = 0_{G}$
	lsmhash.z	$⊢ Z = Cntz (G)$
	lsmhash.t	$⊢ φ \to T \in SubGrp (G)$
	lsmhash.u	$⊢ φ \to U \in SubGrp (G)$
	lsmhash.i	$⊢ φ \to T \cap U = \{\underset{˙}{0}\}$
	lsmhash.s	$⊢ φ \to T \subseteq Z (U)$
	lsmhash.1	$⊢ φ \to T \in Fin$
	lsmhash.2	$⊢ φ \to U \in Fin$
Assertion	lsmhash	$⊢ φ \to \|T \underset{˙}{\oplus} U\| = \|T\| \|U\|$

Proof

Step	Hyp	Ref	Expression
1		lsmhash.p	$⊢ \underset{˙}{\oplus} = LSSum (G)$
2		lsmhash.o	$⊢ \underset{˙}{0} = 0_{G}$
3		lsmhash.z	$⊢ Z = Cntz (G)$
4		lsmhash.t	$⊢ φ \to T \in SubGrp (G)$
5		lsmhash.u	$⊢ φ \to U \in SubGrp (G)$
6		lsmhash.i	$⊢ φ \to T \cap U = \{\underset{˙}{0}\}$
7		lsmhash.s	$⊢ φ \to T \subseteq Z (U)$
8		lsmhash.1	$⊢ φ \to T \in Fin$
9		lsmhash.2	$⊢ φ \to U \in Fin$
10		ovexd	$⊢ φ \to T \underset{˙}{\oplus} U \in V$
11		eqid	$⊢ (x \in (T \underset{˙}{\oplus} U) ⟼ ⟨(T {proj}_{1} (G) U) (x), (U {proj}_{1} (G) T) (x)⟩) = (x \in (T \underset{˙}{\oplus} U) ⟼ ⟨(T {proj}_{1} (G) U) (x), (U {proj}_{1} (G) T) (x)⟩)$
12		eqid	$⊢ +_{G} = +_{G}$
13		eqid	$⊢ {proj}_{1} (G) = {proj}_{1} (G)$
14	12 1 2 3 4 5 6 7 13	pj1f	$⊢ φ \to (T {proj}_{1} (G) U) : T \underset{˙}{\oplus} U ⟶ T$
15	14	ffvelcdmda	$⊢ (φ \land x \in (T \underset{˙}{\oplus} U)) \to (T {proj}_{1} (G) U) (x) \in T$
16	12 1 2 3 4 5 6 7 13	pj2f	$⊢ φ \to (U {proj}_{1} (G) T) : T \underset{˙}{\oplus} U ⟶ U$
17	16	ffvelcdmda	$⊢ (φ \land x \in (T \underset{˙}{\oplus} U)) \to (U {proj}_{1} (G) T) (x) \in U$
18	15 17	opelxpd	$⊢ (φ \land x \in (T \underset{˙}{\oplus} U)) \to ⟨(T {proj}_{1} (G) U) (x), (U {proj}_{1} (G) T) (x)⟩ \in (T \times U)$
19	4 5	jca	$⊢ φ \to (T \in SubGrp (G) \land U \in SubGrp (G))$
20		xp1st	$⊢ y \in (T \times U) \to 1^{st} (y) \in T$
21		xp2nd	$⊢ y \in (T \times U) \to 2^{nd} (y) \in U$
22	20 21	jca	$⊢ y \in (T \times U) \to (1^{st} (y) \in T \land 2^{nd} (y) \in U)$
23	12 1	lsmelvali	$⊢ ((T \in SubGrp (G) \land U \in SubGrp (G)) \land (1^{st} (y) \in T \land 2^{nd} (y) \in U)) \to 1^{st} (y) +_{G} 2^{nd} (y) \in (T \underset{˙}{\oplus} U)$
24	19 22 23	syl2an	$⊢ (φ \land y \in (T \times U)) \to 1^{st} (y) +_{G} 2^{nd} (y) \in (T \underset{˙}{\oplus} U)$
25	4	adantr	$⊢ (φ \land (x \in (T \underset{˙}{\oplus} U) \land y \in (T \times U))) \to T \in SubGrp (G)$
26	5	adantr	$⊢ (φ \land (x \in (T \underset{˙}{\oplus} U) \land y \in (T \times U))) \to U \in SubGrp (G)$
27	6	adantr	$⊢ (φ \land (x \in (T \underset{˙}{\oplus} U) \land y \in (T \times U))) \to T \cap U = \{\underset{˙}{0}\}$
28	7	adantr	$⊢ (φ \land (x \in (T \underset{˙}{\oplus} U) \land y \in (T \times U))) \to T \subseteq Z (U)$
29		simprl	$⊢ (φ \land (x \in (T \underset{˙}{\oplus} U) \land y \in (T \times U))) \to x \in (T \underset{˙}{\oplus} U)$
30	20	ad2antll	$⊢ (φ \land (x \in (T \underset{˙}{\oplus} U) \land y \in (T \times U))) \to 1^{st} (y) \in T$
31	21	ad2antll	$⊢ (φ \land (x \in (T \underset{˙}{\oplus} U) \land y \in (T \times U))) \to 2^{nd} (y) \in U$
32	12 1 2 3 25 26 27 28 13 29 30 31	pj1eq	$⊢ (φ \land (x \in (T \underset{˙}{\oplus} U) \land y \in (T \times U))) \to (x = 1^{st} (y) +_{G} 2^{nd} (y) \leftrightarrow ((T {proj}_{1} (G) U) (x) = 1^{st} (y) \land (U {proj}_{1} (G) T) (x) = 2^{nd} (y)))$
33		eqcom	$⊢ (T {proj}_{1} (G) U) (x) = 1^{st} (y) \leftrightarrow 1^{st} (y) = (T {proj}_{1} (G) U) (x)$
34		eqcom	$⊢ (U {proj}_{1} (G) T) (x) = 2^{nd} (y) \leftrightarrow 2^{nd} (y) = (U {proj}_{1} (G) T) (x)$
35	33 34	anbi12i	$⊢ ((T {proj}_{1} (G) U) (x) = 1^{st} (y) \land (U {proj}_{1} (G) T) (x) = 2^{nd} (y)) \leftrightarrow (1^{st} (y) = (T {proj}_{1} (G) U) (x) \land 2^{nd} (y) = (U {proj}_{1} (G) T) (x))$
36	32 35	bitrdi	$⊢ (φ \land (x \in (T \underset{˙}{\oplus} U) \land y \in (T \times U))) \to (x = 1^{st} (y) +_{G} 2^{nd} (y) \leftrightarrow (1^{st} (y) = (T {proj}_{1} (G) U) (x) \land 2^{nd} (y) = (U {proj}_{1} (G) T) (x)))$
37		eqop	$⊢ y \in (T \times U) \to (y = ⟨(T {proj}_{1} (G) U) (x), (U {proj}_{1} (G) T) (x)⟩ \leftrightarrow (1^{st} (y) = (T {proj}_{1} (G) U) (x) \land 2^{nd} (y) = (U {proj}_{1} (G) T) (x)))$
38	37	ad2antll	$⊢ (φ \land (x \in (T \underset{˙}{\oplus} U) \land y \in (T \times U))) \to (y = ⟨(T {proj}_{1} (G) U) (x), (U {proj}_{1} (G) T) (x)⟩ \leftrightarrow (1^{st} (y) = (T {proj}_{1} (G) U) (x) \land 2^{nd} (y) = (U {proj}_{1} (G) T) (x)))$
39	36 38	bitr4d	$⊢ (φ \land (x \in (T \underset{˙}{\oplus} U) \land y \in (T \times U))) \to (x = 1^{st} (y) +_{G} 2^{nd} (y) \leftrightarrow y = ⟨(T {proj}_{1} (G) U) (x), (U {proj}_{1} (G) T) (x)⟩)$
40	11 18 24 39	f1o2d	$⊢ φ \to (x \in (T \underset{˙}{\oplus} U) ⟼ ⟨(T {proj}_{1} (G) U) (x), (U {proj}_{1} (G) T) (x)⟩) : T \underset{˙}{\oplus} U \underset{1-1 onto}{⟶} T \times U$
41	10 40	hasheqf1od	$⊢ φ \to \|T \underset{˙}{\oplus} U\| = \|T \times U\|$
42		hashxp	$⊢ (T \in Fin \land U \in Fin) \to \|T \times U\| = \|T\| \|U\|$
43	8 9 42	syl2anc	$⊢ φ \to \|T \times U\| = \|T\| \|U\|$
44	41 43	eqtrd	$⊢ φ \to \|T \underset{˙}{\oplus} U\| = \|T\| \|U\|$

Metamath Proof Explorer

Theorem lsmhash

Proof