lsmhash

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

	Ref	Expression
Hypotheses	lsmhash.p	⊢ ⊕ = ( LSSum ‘ 𝐺 )
	lsmhash.o	⊢ 0 = ( 0_g ‘ 𝐺 )
	lsmhash.z	⊢ 𝑍 = ( Cntz ‘ 𝐺 )
	lsmhash.t	⊢ ( 𝜑 → 𝑇 ∈ ( SubGrp ‘ 𝐺 ) )
	lsmhash.u	⊢ ( 𝜑 → 𝑈 ∈ ( SubGrp ‘ 𝐺 ) )
	lsmhash.i	⊢ ( 𝜑 → ( 𝑇 ∩ 𝑈 ) = { 0 } )
	lsmhash.s	⊢ ( 𝜑 → 𝑇 ⊆ ( 𝑍 ‘ 𝑈 ) )
	lsmhash.1	⊢ ( 𝜑 → 𝑇 ∈ Fin )
	lsmhash.2	⊢ ( 𝜑 → 𝑈 ∈ Fin )
Assertion	lsmhash	⊢ ( 𝜑 → ( ♯ ‘ ( 𝑇 ⊕ 𝑈 ) ) = ( ( ♯ ‘ 𝑇 ) · ( ♯ ‘ 𝑈 ) ) )

Proof

Step	Hyp	Ref	Expression
1		lsmhash.p	⊢ ⊕ = ( LSSum ‘ 𝐺 )
2		lsmhash.o	⊢ 0 = ( 0_g ‘ 𝐺 )
3		lsmhash.z	⊢ 𝑍 = ( Cntz ‘ 𝐺 )
4		lsmhash.t	⊢ ( 𝜑 → 𝑇 ∈ ( SubGrp ‘ 𝐺 ) )
5		lsmhash.u	⊢ ( 𝜑 → 𝑈 ∈ ( SubGrp ‘ 𝐺 ) )
6		lsmhash.i	⊢ ( 𝜑 → ( 𝑇 ∩ 𝑈 ) = { 0 } )
7		lsmhash.s	⊢ ( 𝜑 → 𝑇 ⊆ ( 𝑍 ‘ 𝑈 ) )
8		lsmhash.1	⊢ ( 𝜑 → 𝑇 ∈ Fin )
9		lsmhash.2	⊢ ( 𝜑 → 𝑈 ∈ Fin )
10		ovexd	⊢ ( 𝜑 → ( 𝑇 ⊕ 𝑈 ) ∈ V )
11		eqid	⊢ ( 𝑥 ∈ ( 𝑇 ⊕ 𝑈 ) ↦ ⟨ ( ( 𝑇 ( proj₁ ‘ 𝐺 ) 𝑈 ) ‘ 𝑥 ) , ( ( 𝑈 ( proj₁ ‘ 𝐺 ) 𝑇 ) ‘ 𝑥 ) ⟩ ) = ( 𝑥 ∈ ( 𝑇 ⊕ 𝑈 ) ↦ ⟨ ( ( 𝑇 ( proj₁ ‘ 𝐺 ) 𝑈 ) ‘ 𝑥 ) , ( ( 𝑈 ( proj₁ ‘ 𝐺 ) 𝑇 ) ‘ 𝑥 ) ⟩ )
12		eqid	⊢ ( +_g ‘ 𝐺 ) = ( +_g ‘ 𝐺 )
13		eqid	⊢ ( proj₁ ‘ 𝐺 ) = ( proj₁ ‘ 𝐺 )
14	12 1 2 3 4 5 6 7 13	pj1f	⊢ ( 𝜑 → ( 𝑇 ( proj₁ ‘ 𝐺 ) 𝑈 ) : ( 𝑇 ⊕ 𝑈 ) ⟶ 𝑇 )
15	14	ffvelrnda	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑇 ⊕ 𝑈 ) ) → ( ( 𝑇 ( proj₁ ‘ 𝐺 ) 𝑈 ) ‘ 𝑥 ) ∈ 𝑇 )
16	12 1 2 3 4 5 6 7 13	pj2f	⊢ ( 𝜑 → ( 𝑈 ( proj₁ ‘ 𝐺 ) 𝑇 ) : ( 𝑇 ⊕ 𝑈 ) ⟶ 𝑈 )
17	16	ffvelrnda	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑇 ⊕ 𝑈 ) ) → ( ( 𝑈 ( proj₁ ‘ 𝐺 ) 𝑇 ) ‘ 𝑥 ) ∈ 𝑈 )
18	15 17	opelxpd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑇 ⊕ 𝑈 ) ) → ⟨ ( ( 𝑇 ( proj₁ ‘ 𝐺 ) 𝑈 ) ‘ 𝑥 ) , ( ( 𝑈 ( proj₁ ‘ 𝐺 ) 𝑇 ) ‘ 𝑥 ) ⟩ ∈ ( 𝑇 × 𝑈 ) )
19	4 5	jca	⊢ ( 𝜑 → ( 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) )
20		xp1st	⊢ ( 𝑦 ∈ ( 𝑇 × 𝑈 ) → ( 1^st ‘ 𝑦 ) ∈ 𝑇 )
21		xp2nd	⊢ ( 𝑦 ∈ ( 𝑇 × 𝑈 ) → ( 2^nd ‘ 𝑦 ) ∈ 𝑈 )
22	20 21	jca	⊢ ( 𝑦 ∈ ( 𝑇 × 𝑈 ) → ( ( 1^st ‘ 𝑦 ) ∈ 𝑇 ∧ ( 2^nd ‘ 𝑦 ) ∈ 𝑈 ) )
23	12 1	lsmelvali	⊢ ( ( ( 𝑇 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝐺 ) ) ∧ ( ( 1^st ‘ 𝑦 ) ∈ 𝑇 ∧ ( 2^nd ‘ 𝑦 ) ∈ 𝑈 ) ) → ( ( 1^st ‘ 𝑦 ) ( +_g ‘ 𝐺 ) ( 2^nd ‘ 𝑦 ) ) ∈ ( 𝑇 ⊕ 𝑈 ) )
24	19 22 23	syl2an	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑇 × 𝑈 ) ) → ( ( 1^st ‘ 𝑦 ) ( +_g ‘ 𝐺 ) ( 2^nd ‘ 𝑦 ) ) ∈ ( 𝑇 ⊕ 𝑈 ) )
25	4	adantr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝑇 ⊕ 𝑈 ) ∧ 𝑦 ∈ ( 𝑇 × 𝑈 ) ) ) → 𝑇 ∈ ( SubGrp ‘ 𝐺 ) )
26	5	adantr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝑇 ⊕ 𝑈 ) ∧ 𝑦 ∈ ( 𝑇 × 𝑈 ) ) ) → 𝑈 ∈ ( SubGrp ‘ 𝐺 ) )
27	6	adantr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝑇 ⊕ 𝑈 ) ∧ 𝑦 ∈ ( 𝑇 × 𝑈 ) ) ) → ( 𝑇 ∩ 𝑈 ) = { 0 } )
28	7	adantr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝑇 ⊕ 𝑈 ) ∧ 𝑦 ∈ ( 𝑇 × 𝑈 ) ) ) → 𝑇 ⊆ ( 𝑍 ‘ 𝑈 ) )
29		simprl	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝑇 ⊕ 𝑈 ) ∧ 𝑦 ∈ ( 𝑇 × 𝑈 ) ) ) → 𝑥 ∈ ( 𝑇 ⊕ 𝑈 ) )
30	20	ad2antll	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝑇 ⊕ 𝑈 ) ∧ 𝑦 ∈ ( 𝑇 × 𝑈 ) ) ) → ( 1^st ‘ 𝑦 ) ∈ 𝑇 )
31	21	ad2antll	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝑇 ⊕ 𝑈 ) ∧ 𝑦 ∈ ( 𝑇 × 𝑈 ) ) ) → ( 2^nd ‘ 𝑦 ) ∈ 𝑈 )
32	12 1 2 3 25 26 27 28 13 29 30 31	pj1eq	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝑇 ⊕ 𝑈 ) ∧ 𝑦 ∈ ( 𝑇 × 𝑈 ) ) ) → ( 𝑥 = ( ( 1^st ‘ 𝑦 ) ( +_g ‘ 𝐺 ) ( 2^nd ‘ 𝑦 ) ) ↔ ( ( ( 𝑇 ( proj₁ ‘ 𝐺 ) 𝑈 ) ‘ 𝑥 ) = ( 1^st ‘ 𝑦 ) ∧ ( ( 𝑈 ( proj₁ ‘ 𝐺 ) 𝑇 ) ‘ 𝑥 ) = ( 2^nd ‘ 𝑦 ) ) ) )
33		eqcom	⊢ ( ( ( 𝑇 ( proj₁ ‘ 𝐺 ) 𝑈 ) ‘ 𝑥 ) = ( 1^st ‘ 𝑦 ) ↔ ( 1^st ‘ 𝑦 ) = ( ( 𝑇 ( proj₁ ‘ 𝐺 ) 𝑈 ) ‘ 𝑥 ) )
34		eqcom	⊢ ( ( ( 𝑈 ( proj₁ ‘ 𝐺 ) 𝑇 ) ‘ 𝑥 ) = ( 2^nd ‘ 𝑦 ) ↔ ( 2^nd ‘ 𝑦 ) = ( ( 𝑈 ( proj₁ ‘ 𝐺 ) 𝑇 ) ‘ 𝑥 ) )
35	33 34	anbi12i	⊢ ( ( ( ( 𝑇 ( proj₁ ‘ 𝐺 ) 𝑈 ) ‘ 𝑥 ) = ( 1^st ‘ 𝑦 ) ∧ ( ( 𝑈 ( proj₁ ‘ 𝐺 ) 𝑇 ) ‘ 𝑥 ) = ( 2^nd ‘ 𝑦 ) ) ↔ ( ( 1^st ‘ 𝑦 ) = ( ( 𝑇 ( proj₁ ‘ 𝐺 ) 𝑈 ) ‘ 𝑥 ) ∧ ( 2^nd ‘ 𝑦 ) = ( ( 𝑈 ( proj₁ ‘ 𝐺 ) 𝑇 ) ‘ 𝑥 ) ) )
36	32 35	bitrdi	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝑇 ⊕ 𝑈 ) ∧ 𝑦 ∈ ( 𝑇 × 𝑈 ) ) ) → ( 𝑥 = ( ( 1^st ‘ 𝑦 ) ( +_g ‘ 𝐺 ) ( 2^nd ‘ 𝑦 ) ) ↔ ( ( 1^st ‘ 𝑦 ) = ( ( 𝑇 ( proj₁ ‘ 𝐺 ) 𝑈 ) ‘ 𝑥 ) ∧ ( 2^nd ‘ 𝑦 ) = ( ( 𝑈 ( proj₁ ‘ 𝐺 ) 𝑇 ) ‘ 𝑥 ) ) ) )
37		eqop	⊢ ( 𝑦 ∈ ( 𝑇 × 𝑈 ) → ( 𝑦 = ⟨ ( ( 𝑇 ( proj₁ ‘ 𝐺 ) 𝑈 ) ‘ 𝑥 ) , ( ( 𝑈 ( proj₁ ‘ 𝐺 ) 𝑇 ) ‘ 𝑥 ) ⟩ ↔ ( ( 1^st ‘ 𝑦 ) = ( ( 𝑇 ( proj₁ ‘ 𝐺 ) 𝑈 ) ‘ 𝑥 ) ∧ ( 2^nd ‘ 𝑦 ) = ( ( 𝑈 ( proj₁ ‘ 𝐺 ) 𝑇 ) ‘ 𝑥 ) ) ) )
38	37	ad2antll	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝑇 ⊕ 𝑈 ) ∧ 𝑦 ∈ ( 𝑇 × 𝑈 ) ) ) → ( 𝑦 = ⟨ ( ( 𝑇 ( proj₁ ‘ 𝐺 ) 𝑈 ) ‘ 𝑥 ) , ( ( 𝑈 ( proj₁ ‘ 𝐺 ) 𝑇 ) ‘ 𝑥 ) ⟩ ↔ ( ( 1^st ‘ 𝑦 ) = ( ( 𝑇 ( proj₁ ‘ 𝐺 ) 𝑈 ) ‘ 𝑥 ) ∧ ( 2^nd ‘ 𝑦 ) = ( ( 𝑈 ( proj₁ ‘ 𝐺 ) 𝑇 ) ‘ 𝑥 ) ) ) )
39	36 38	bitr4d	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝑇 ⊕ 𝑈 ) ∧ 𝑦 ∈ ( 𝑇 × 𝑈 ) ) ) → ( 𝑥 = ( ( 1^st ‘ 𝑦 ) ( +_g ‘ 𝐺 ) ( 2^nd ‘ 𝑦 ) ) ↔ 𝑦 = ⟨ ( ( 𝑇 ( proj₁ ‘ 𝐺 ) 𝑈 ) ‘ 𝑥 ) , ( ( 𝑈 ( proj₁ ‘ 𝐺 ) 𝑇 ) ‘ 𝑥 ) ⟩ ) )
40	11 18 24 39	f1o2d	⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝑇 ⊕ 𝑈 ) ↦ ⟨ ( ( 𝑇 ( proj₁ ‘ 𝐺 ) 𝑈 ) ‘ 𝑥 ) , ( ( 𝑈 ( proj₁ ‘ 𝐺 ) 𝑇 ) ‘ 𝑥 ) ⟩ ) : ( 𝑇 ⊕ 𝑈 ) –1-1-onto→ ( 𝑇 × 𝑈 ) )
41	10 40	hasheqf1od	⊢ ( 𝜑 → ( ♯ ‘ ( 𝑇 ⊕ 𝑈 ) ) = ( ♯ ‘ ( 𝑇 × 𝑈 ) ) )
42		hashxp	⊢ ( ( 𝑇 ∈ Fin ∧ 𝑈 ∈ Fin ) → ( ♯ ‘ ( 𝑇 × 𝑈 ) ) = ( ( ♯ ‘ 𝑇 ) · ( ♯ ‘ 𝑈 ) ) )
43	8 9 42	syl2anc	⊢ ( 𝜑 → ( ♯ ‘ ( 𝑇 × 𝑈 ) ) = ( ( ♯ ‘ 𝑇 ) · ( ♯ ‘ 𝑈 ) ) )
44	41 43	eqtrd	⊢ ( 𝜑 → ( ♯ ‘ ( 𝑇 ⊕ 𝑈 ) ) = ( ( ♯ ‘ 𝑇 ) · ( ♯ ‘ 𝑈 ) ) )

Metamath Proof Explorer

Theorem lsmhash

Proof