Step | Hyp | Ref
| Expression |
1 | | ovexd 6956 |
. . . 4
⊢ (𝜑 → (𝑇 ⊕ 𝑈) ∈ V) |
2 | | lsmhash.t |
. . . . 5
⊢ (𝜑 → 𝑇 ∈ (SubGrp‘𝐺)) |
3 | | lsmhash.u |
. . . . 5
⊢ (𝜑 → 𝑈 ∈ (SubGrp‘𝐺)) |
4 | 2, 3 | xpexd 7238 |
. . . 4
⊢ (𝜑 → (𝑇 × 𝑈) ∈ V) |
5 | | eqid 2778 |
. . . . . . . 8
⊢
(+g‘𝐺) = (+g‘𝐺) |
6 | | lsmhash.p |
. . . . . . . 8
⊢ ⊕ =
(LSSum‘𝐺) |
7 | | lsmhash.o |
. . . . . . . 8
⊢ 0 =
(0g‘𝐺) |
8 | | lsmhash.z |
. . . . . . . 8
⊢ 𝑍 = (Cntz‘𝐺) |
9 | | lsmhash.i |
. . . . . . . 8
⊢ (𝜑 → (𝑇 ∩ 𝑈) = { 0 }) |
10 | | lsmhash.s |
. . . . . . . 8
⊢ (𝜑 → 𝑇 ⊆ (𝑍‘𝑈)) |
11 | | eqid 2778 |
. . . . . . . 8
⊢
(proj1‘𝐺) = (proj1‘𝐺) |
12 | 5, 6, 7, 8, 2, 3, 9, 10, 11 | pj1f 18494 |
. . . . . . 7
⊢ (𝜑 → (𝑇(proj1‘𝐺)𝑈):(𝑇 ⊕ 𝑈)⟶𝑇) |
13 | 12 | ffvelrnda 6623 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑇 ⊕ 𝑈)) → ((𝑇(proj1‘𝐺)𝑈)‘𝑥) ∈ 𝑇) |
14 | 5, 6, 7, 8, 2, 3, 9, 10, 11 | pj2f 18495 |
. . . . . . 7
⊢ (𝜑 → (𝑈(proj1‘𝐺)𝑇):(𝑇 ⊕ 𝑈)⟶𝑈) |
15 | 14 | ffvelrnda 6623 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑇 ⊕ 𝑈)) → ((𝑈(proj1‘𝐺)𝑇)‘𝑥) ∈ 𝑈) |
16 | | opelxpi 5392 |
. . . . . 6
⊢ ((((𝑇(proj1‘𝐺)𝑈)‘𝑥) ∈ 𝑇 ∧ ((𝑈(proj1‘𝐺)𝑇)‘𝑥) ∈ 𝑈) → 〈((𝑇(proj1‘𝐺)𝑈)‘𝑥), ((𝑈(proj1‘𝐺)𝑇)‘𝑥)〉 ∈ (𝑇 × 𝑈)) |
17 | 13, 15, 16 | syl2anc 579 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑇 ⊕ 𝑈)) → 〈((𝑇(proj1‘𝐺)𝑈)‘𝑥), ((𝑈(proj1‘𝐺)𝑇)‘𝑥)〉 ∈ (𝑇 × 𝑈)) |
18 | 17 | ex 403 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ (𝑇 ⊕ 𝑈) → 〈((𝑇(proj1‘𝐺)𝑈)‘𝑥), ((𝑈(proj1‘𝐺)𝑇)‘𝑥)〉 ∈ (𝑇 × 𝑈))) |
19 | 2, 3 | jca 507 |
. . . . . 6
⊢ (𝜑 → (𝑇 ∈ (SubGrp‘𝐺) ∧ 𝑈 ∈ (SubGrp‘𝐺))) |
20 | | xp1st 7477 |
. . . . . . 7
⊢ (𝑦 ∈ (𝑇 × 𝑈) → (1st ‘𝑦) ∈ 𝑇) |
21 | | xp2nd 7478 |
. . . . . . 7
⊢ (𝑦 ∈ (𝑇 × 𝑈) → (2nd ‘𝑦) ∈ 𝑈) |
22 | 20, 21 | jca 507 |
. . . . . 6
⊢ (𝑦 ∈ (𝑇 × 𝑈) → ((1st ‘𝑦) ∈ 𝑇 ∧ (2nd ‘𝑦) ∈ 𝑈)) |
23 | 5, 6 | lsmelvali 18449 |
. . . . . 6
⊢ (((𝑇 ∈ (SubGrp‘𝐺) ∧ 𝑈 ∈ (SubGrp‘𝐺)) ∧ ((1st ‘𝑦) ∈ 𝑇 ∧ (2nd ‘𝑦) ∈ 𝑈)) → ((1st ‘𝑦)(+g‘𝐺)(2nd ‘𝑦)) ∈ (𝑇 ⊕ 𝑈)) |
24 | 19, 22, 23 | syl2an 589 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑇 × 𝑈)) → ((1st ‘𝑦)(+g‘𝐺)(2nd ‘𝑦)) ∈ (𝑇 ⊕ 𝑈)) |
25 | 24 | ex 403 |
. . . 4
⊢ (𝜑 → (𝑦 ∈ (𝑇 × 𝑈) → ((1st ‘𝑦)(+g‘𝐺)(2nd ‘𝑦)) ∈ (𝑇 ⊕ 𝑈))) |
26 | 2 | adantr 474 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ (𝑇 ⊕ 𝑈) ∧ 𝑦 ∈ (𝑇 × 𝑈))) → 𝑇 ∈ (SubGrp‘𝐺)) |
27 | 3 | adantr 474 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ (𝑇 ⊕ 𝑈) ∧ 𝑦 ∈ (𝑇 × 𝑈))) → 𝑈 ∈ (SubGrp‘𝐺)) |
28 | 9 | adantr 474 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ (𝑇 ⊕ 𝑈) ∧ 𝑦 ∈ (𝑇 × 𝑈))) → (𝑇 ∩ 𝑈) = { 0 }) |
29 | 10 | adantr 474 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ (𝑇 ⊕ 𝑈) ∧ 𝑦 ∈ (𝑇 × 𝑈))) → 𝑇 ⊆ (𝑍‘𝑈)) |
30 | | simprl 761 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ (𝑇 ⊕ 𝑈) ∧ 𝑦 ∈ (𝑇 × 𝑈))) → 𝑥 ∈ (𝑇 ⊕ 𝑈)) |
31 | 20 | ad2antll 719 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ (𝑇 ⊕ 𝑈) ∧ 𝑦 ∈ (𝑇 × 𝑈))) → (1st ‘𝑦) ∈ 𝑇) |
32 | 21 | ad2antll 719 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ (𝑇 ⊕ 𝑈) ∧ 𝑦 ∈ (𝑇 × 𝑈))) → (2nd ‘𝑦) ∈ 𝑈) |
33 | 5, 6, 7, 8, 26, 27, 28, 29, 11, 30, 31, 32 | pj1eq 18497 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ (𝑇 ⊕ 𝑈) ∧ 𝑦 ∈ (𝑇 × 𝑈))) → (𝑥 = ((1st ‘𝑦)(+g‘𝐺)(2nd ‘𝑦)) ↔ (((𝑇(proj1‘𝐺)𝑈)‘𝑥) = (1st ‘𝑦) ∧ ((𝑈(proj1‘𝐺)𝑇)‘𝑥) = (2nd ‘𝑦)))) |
34 | | eqcom 2785 |
. . . . . . . 8
⊢ (((𝑇(proj1‘𝐺)𝑈)‘𝑥) = (1st ‘𝑦) ↔ (1st ‘𝑦) = ((𝑇(proj1‘𝐺)𝑈)‘𝑥)) |
35 | | eqcom 2785 |
. . . . . . . 8
⊢ (((𝑈(proj1‘𝐺)𝑇)‘𝑥) = (2nd ‘𝑦) ↔ (2nd ‘𝑦) = ((𝑈(proj1‘𝐺)𝑇)‘𝑥)) |
36 | 34, 35 | anbi12i 620 |
. . . . . . 7
⊢ ((((𝑇(proj1‘𝐺)𝑈)‘𝑥) = (1st ‘𝑦) ∧ ((𝑈(proj1‘𝐺)𝑇)‘𝑥) = (2nd ‘𝑦)) ↔ ((1st ‘𝑦) = ((𝑇(proj1‘𝐺)𝑈)‘𝑥) ∧ (2nd ‘𝑦) = ((𝑈(proj1‘𝐺)𝑇)‘𝑥))) |
37 | 33, 36 | syl6bb 279 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ (𝑇 ⊕ 𝑈) ∧ 𝑦 ∈ (𝑇 × 𝑈))) → (𝑥 = ((1st ‘𝑦)(+g‘𝐺)(2nd ‘𝑦)) ↔ ((1st ‘𝑦) = ((𝑇(proj1‘𝐺)𝑈)‘𝑥) ∧ (2nd ‘𝑦) = ((𝑈(proj1‘𝐺)𝑇)‘𝑥)))) |
38 | | eqop 7487 |
. . . . . . 7
⊢ (𝑦 ∈ (𝑇 × 𝑈) → (𝑦 = 〈((𝑇(proj1‘𝐺)𝑈)‘𝑥), ((𝑈(proj1‘𝐺)𝑇)‘𝑥)〉 ↔ ((1st ‘𝑦) = ((𝑇(proj1‘𝐺)𝑈)‘𝑥) ∧ (2nd ‘𝑦) = ((𝑈(proj1‘𝐺)𝑇)‘𝑥)))) |
39 | 38 | ad2antll 719 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ (𝑇 ⊕ 𝑈) ∧ 𝑦 ∈ (𝑇 × 𝑈))) → (𝑦 = 〈((𝑇(proj1‘𝐺)𝑈)‘𝑥), ((𝑈(proj1‘𝐺)𝑇)‘𝑥)〉 ↔ ((1st ‘𝑦) = ((𝑇(proj1‘𝐺)𝑈)‘𝑥) ∧ (2nd ‘𝑦) = ((𝑈(proj1‘𝐺)𝑇)‘𝑥)))) |
40 | 37, 39 | bitr4d 274 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ (𝑇 ⊕ 𝑈) ∧ 𝑦 ∈ (𝑇 × 𝑈))) → (𝑥 = ((1st ‘𝑦)(+g‘𝐺)(2nd ‘𝑦)) ↔ 𝑦 = 〈((𝑇(proj1‘𝐺)𝑈)‘𝑥), ((𝑈(proj1‘𝐺)𝑇)‘𝑥)〉)) |
41 | 40 | ex 403 |
. . . 4
⊢ (𝜑 → ((𝑥 ∈ (𝑇 ⊕ 𝑈) ∧ 𝑦 ∈ (𝑇 × 𝑈)) → (𝑥 = ((1st ‘𝑦)(+g‘𝐺)(2nd ‘𝑦)) ↔ 𝑦 = 〈((𝑇(proj1‘𝐺)𝑈)‘𝑥), ((𝑈(proj1‘𝐺)𝑇)‘𝑥)〉))) |
42 | 1, 4, 18, 25, 41 | en3d 8278 |
. . 3
⊢ (𝜑 → (𝑇 ⊕ 𝑈) ≈ (𝑇 × 𝑈)) |
43 | | hasheni 13453 |
. . 3
⊢ ((𝑇 ⊕ 𝑈) ≈ (𝑇 × 𝑈) → (♯‘(𝑇 ⊕ 𝑈)) = (♯‘(𝑇 × 𝑈))) |
44 | 42, 43 | syl 17 |
. 2
⊢ (𝜑 → (♯‘(𝑇 ⊕ 𝑈)) = (♯‘(𝑇 × 𝑈))) |
45 | | lsmhash.1 |
. . 3
⊢ (𝜑 → 𝑇 ∈ Fin) |
46 | | lsmhash.2 |
. . 3
⊢ (𝜑 → 𝑈 ∈ Fin) |
47 | | hashxp 13535 |
. . 3
⊢ ((𝑇 ∈ Fin ∧ 𝑈 ∈ Fin) →
(♯‘(𝑇 ×
𝑈)) = ((♯‘𝑇) · (♯‘𝑈))) |
48 | 45, 46, 47 | syl2anc 579 |
. 2
⊢ (𝜑 → (♯‘(𝑇 × 𝑈)) = ((♯‘𝑇) · (♯‘𝑈))) |
49 | 44, 48 | eqtrd 2814 |
1
⊢ (𝜑 → (♯‘(𝑇 ⊕ 𝑈)) = ((♯‘𝑇) · (♯‘𝑈))) |