Step | Hyp | Ref
| Expression |
1 | | ovex 6577 |
. . . . 5
⊢ (𝑇 ⊕ 𝑈) ∈ V |
2 | 1 | a1i 11 |
. . . 4
⊢ (𝜑 → (𝑇 ⊕ 𝑈) ∈ V) |
3 | | lsmhash.t |
. . . . 5
⊢ (𝜑 → 𝑇 ∈ (SubGrp‘𝐺)) |
4 | | lsmhash.u |
. . . . 5
⊢ (𝜑 → 𝑈 ∈ (SubGrp‘𝐺)) |
5 | | xpexg 6858 |
. . . . 5
⊢ ((𝑇 ∈ (SubGrp‘𝐺) ∧ 𝑈 ∈ (SubGrp‘𝐺)) → (𝑇 × 𝑈) ∈ V) |
6 | 3, 4, 5 | syl2anc 691 |
. . . 4
⊢ (𝜑 → (𝑇 × 𝑈) ∈ V) |
7 | | eqid 2610 |
. . . . . . . 8
⊢
(+g‘𝐺) = (+g‘𝐺) |
8 | | lsmhash.p |
. . . . . . . 8
⊢ ⊕ =
(LSSum‘𝐺) |
9 | | lsmhash.o |
. . . . . . . 8
⊢ 0 =
(0g‘𝐺) |
10 | | lsmhash.z |
. . . . . . . 8
⊢ 𝑍 = (Cntz‘𝐺) |
11 | | lsmhash.i |
. . . . . . . 8
⊢ (𝜑 → (𝑇 ∩ 𝑈) = { 0 }) |
12 | | lsmhash.s |
. . . . . . . 8
⊢ (𝜑 → 𝑇 ⊆ (𝑍‘𝑈)) |
13 | | eqid 2610 |
. . . . . . . 8
⊢
(proj1‘𝐺) = (proj1‘𝐺) |
14 | 7, 8, 9, 10, 3, 4,
11, 12, 13 | pj1f 17933 |
. . . . . . 7
⊢ (𝜑 → (𝑇(proj1‘𝐺)𝑈):(𝑇 ⊕ 𝑈)⟶𝑇) |
15 | 14 | ffvelrnda 6267 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑇 ⊕ 𝑈)) → ((𝑇(proj1‘𝐺)𝑈)‘𝑥) ∈ 𝑇) |
16 | 7, 8, 9, 10, 3, 4,
11, 12, 13 | pj2f 17934 |
. . . . . . 7
⊢ (𝜑 → (𝑈(proj1‘𝐺)𝑇):(𝑇 ⊕ 𝑈)⟶𝑈) |
17 | 16 | ffvelrnda 6267 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑇 ⊕ 𝑈)) → ((𝑈(proj1‘𝐺)𝑇)‘𝑥) ∈ 𝑈) |
18 | | opelxpi 5072 |
. . . . . 6
⊢ ((((𝑇(proj1‘𝐺)𝑈)‘𝑥) ∈ 𝑇 ∧ ((𝑈(proj1‘𝐺)𝑇)‘𝑥) ∈ 𝑈) → 〈((𝑇(proj1‘𝐺)𝑈)‘𝑥), ((𝑈(proj1‘𝐺)𝑇)‘𝑥)〉 ∈ (𝑇 × 𝑈)) |
19 | 15, 17, 18 | syl2anc 691 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑇 ⊕ 𝑈)) → 〈((𝑇(proj1‘𝐺)𝑈)‘𝑥), ((𝑈(proj1‘𝐺)𝑇)‘𝑥)〉 ∈ (𝑇 × 𝑈)) |
20 | 19 | ex 449 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ (𝑇 ⊕ 𝑈) → 〈((𝑇(proj1‘𝐺)𝑈)‘𝑥), ((𝑈(proj1‘𝐺)𝑇)‘𝑥)〉 ∈ (𝑇 × 𝑈))) |
21 | 3, 4 | jca 553 |
. . . . . 6
⊢ (𝜑 → (𝑇 ∈ (SubGrp‘𝐺) ∧ 𝑈 ∈ (SubGrp‘𝐺))) |
22 | | xp1st 7089 |
. . . . . . 7
⊢ (𝑦 ∈ (𝑇 × 𝑈) → (1st ‘𝑦) ∈ 𝑇) |
23 | | xp2nd 7090 |
. . . . . . 7
⊢ (𝑦 ∈ (𝑇 × 𝑈) → (2nd ‘𝑦) ∈ 𝑈) |
24 | 22, 23 | jca 553 |
. . . . . 6
⊢ (𝑦 ∈ (𝑇 × 𝑈) → ((1st ‘𝑦) ∈ 𝑇 ∧ (2nd ‘𝑦) ∈ 𝑈)) |
25 | 7, 8 | lsmelvali 17888 |
. . . . . 6
⊢ (((𝑇 ∈ (SubGrp‘𝐺) ∧ 𝑈 ∈ (SubGrp‘𝐺)) ∧ ((1st ‘𝑦) ∈ 𝑇 ∧ (2nd ‘𝑦) ∈ 𝑈)) → ((1st ‘𝑦)(+g‘𝐺)(2nd ‘𝑦)) ∈ (𝑇 ⊕ 𝑈)) |
26 | 21, 24, 25 | syl2an 493 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑇 × 𝑈)) → ((1st ‘𝑦)(+g‘𝐺)(2nd ‘𝑦)) ∈ (𝑇 ⊕ 𝑈)) |
27 | 26 | ex 449 |
. . . 4
⊢ (𝜑 → (𝑦 ∈ (𝑇 × 𝑈) → ((1st ‘𝑦)(+g‘𝐺)(2nd ‘𝑦)) ∈ (𝑇 ⊕ 𝑈))) |
28 | 3 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ (𝑇 ⊕ 𝑈) ∧ 𝑦 ∈ (𝑇 × 𝑈))) → 𝑇 ∈ (SubGrp‘𝐺)) |
29 | 4 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ (𝑇 ⊕ 𝑈) ∧ 𝑦 ∈ (𝑇 × 𝑈))) → 𝑈 ∈ (SubGrp‘𝐺)) |
30 | 11 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ (𝑇 ⊕ 𝑈) ∧ 𝑦 ∈ (𝑇 × 𝑈))) → (𝑇 ∩ 𝑈) = { 0 }) |
31 | 12 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ (𝑇 ⊕ 𝑈) ∧ 𝑦 ∈ (𝑇 × 𝑈))) → 𝑇 ⊆ (𝑍‘𝑈)) |
32 | | simprl 790 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ (𝑇 ⊕ 𝑈) ∧ 𝑦 ∈ (𝑇 × 𝑈))) → 𝑥 ∈ (𝑇 ⊕ 𝑈)) |
33 | 22 | ad2antll 761 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ (𝑇 ⊕ 𝑈) ∧ 𝑦 ∈ (𝑇 × 𝑈))) → (1st ‘𝑦) ∈ 𝑇) |
34 | 23 | ad2antll 761 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ (𝑇 ⊕ 𝑈) ∧ 𝑦 ∈ (𝑇 × 𝑈))) → (2nd ‘𝑦) ∈ 𝑈) |
35 | 7, 8, 9, 10, 28, 29, 30, 31, 13, 32, 33, 34 | pj1eq 17936 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ (𝑇 ⊕ 𝑈) ∧ 𝑦 ∈ (𝑇 × 𝑈))) → (𝑥 = ((1st ‘𝑦)(+g‘𝐺)(2nd ‘𝑦)) ↔ (((𝑇(proj1‘𝐺)𝑈)‘𝑥) = (1st ‘𝑦) ∧ ((𝑈(proj1‘𝐺)𝑇)‘𝑥) = (2nd ‘𝑦)))) |
36 | | eqcom 2617 |
. . . . . . . 8
⊢ (((𝑇(proj1‘𝐺)𝑈)‘𝑥) = (1st ‘𝑦) ↔ (1st ‘𝑦) = ((𝑇(proj1‘𝐺)𝑈)‘𝑥)) |
37 | | eqcom 2617 |
. . . . . . . 8
⊢ (((𝑈(proj1‘𝐺)𝑇)‘𝑥) = (2nd ‘𝑦) ↔ (2nd ‘𝑦) = ((𝑈(proj1‘𝐺)𝑇)‘𝑥)) |
38 | 36, 37 | anbi12i 729 |
. . . . . . 7
⊢ ((((𝑇(proj1‘𝐺)𝑈)‘𝑥) = (1st ‘𝑦) ∧ ((𝑈(proj1‘𝐺)𝑇)‘𝑥) = (2nd ‘𝑦)) ↔ ((1st ‘𝑦) = ((𝑇(proj1‘𝐺)𝑈)‘𝑥) ∧ (2nd ‘𝑦) = ((𝑈(proj1‘𝐺)𝑇)‘𝑥))) |
39 | 35, 38 | syl6bb 275 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ (𝑇 ⊕ 𝑈) ∧ 𝑦 ∈ (𝑇 × 𝑈))) → (𝑥 = ((1st ‘𝑦)(+g‘𝐺)(2nd ‘𝑦)) ↔ ((1st ‘𝑦) = ((𝑇(proj1‘𝐺)𝑈)‘𝑥) ∧ (2nd ‘𝑦) = ((𝑈(proj1‘𝐺)𝑇)‘𝑥)))) |
40 | | eqop 7099 |
. . . . . . 7
⊢ (𝑦 ∈ (𝑇 × 𝑈) → (𝑦 = 〈((𝑇(proj1‘𝐺)𝑈)‘𝑥), ((𝑈(proj1‘𝐺)𝑇)‘𝑥)〉 ↔ ((1st ‘𝑦) = ((𝑇(proj1‘𝐺)𝑈)‘𝑥) ∧ (2nd ‘𝑦) = ((𝑈(proj1‘𝐺)𝑇)‘𝑥)))) |
41 | 40 | ad2antll 761 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ (𝑇 ⊕ 𝑈) ∧ 𝑦 ∈ (𝑇 × 𝑈))) → (𝑦 = 〈((𝑇(proj1‘𝐺)𝑈)‘𝑥), ((𝑈(proj1‘𝐺)𝑇)‘𝑥)〉 ↔ ((1st ‘𝑦) = ((𝑇(proj1‘𝐺)𝑈)‘𝑥) ∧ (2nd ‘𝑦) = ((𝑈(proj1‘𝐺)𝑇)‘𝑥)))) |
42 | 39, 41 | bitr4d 270 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ (𝑇 ⊕ 𝑈) ∧ 𝑦 ∈ (𝑇 × 𝑈))) → (𝑥 = ((1st ‘𝑦)(+g‘𝐺)(2nd ‘𝑦)) ↔ 𝑦 = 〈((𝑇(proj1‘𝐺)𝑈)‘𝑥), ((𝑈(proj1‘𝐺)𝑇)‘𝑥)〉)) |
43 | 42 | ex 449 |
. . . 4
⊢ (𝜑 → ((𝑥 ∈ (𝑇 ⊕ 𝑈) ∧ 𝑦 ∈ (𝑇 × 𝑈)) → (𝑥 = ((1st ‘𝑦)(+g‘𝐺)(2nd ‘𝑦)) ↔ 𝑦 = 〈((𝑇(proj1‘𝐺)𝑈)‘𝑥), ((𝑈(proj1‘𝐺)𝑇)‘𝑥)〉))) |
44 | 2, 6, 20, 27, 43 | en3d 7878 |
. . 3
⊢ (𝜑 → (𝑇 ⊕ 𝑈) ≈ (𝑇 × 𝑈)) |
45 | | hasheni 12998 |
. . 3
⊢ ((𝑇 ⊕ 𝑈) ≈ (𝑇 × 𝑈) → (#‘(𝑇 ⊕ 𝑈)) = (#‘(𝑇 × 𝑈))) |
46 | 44, 45 | syl 17 |
. 2
⊢ (𝜑 → (#‘(𝑇 ⊕ 𝑈)) = (#‘(𝑇 × 𝑈))) |
47 | | lsmhash.1 |
. . 3
⊢ (𝜑 → 𝑇 ∈ Fin) |
48 | | lsmhash.2 |
. . 3
⊢ (𝜑 → 𝑈 ∈ Fin) |
49 | | hashxp 13081 |
. . 3
⊢ ((𝑇 ∈ Fin ∧ 𝑈 ∈ Fin) →
(#‘(𝑇 × 𝑈)) = ((#‘𝑇) · (#‘𝑈))) |
50 | 47, 48, 49 | syl2anc 691 |
. 2
⊢ (𝜑 → (#‘(𝑇 × 𝑈)) = ((#‘𝑇) · (#‘𝑈))) |
51 | 46, 50 | eqtrd 2644 |
1
⊢ (𝜑 → (#‘(𝑇 ⊕ 𝑈)) = ((#‘𝑇) · (#‘𝑈))) |