Step | Hyp | Ref
| Expression |
1 | | ovexd 7180 |
. . . 4
⊢ (𝜑 → (𝑇 ⊕ 𝑈) ∈ V) |
2 | | lsmhash.t |
. . . . 5
⊢ (𝜑 → 𝑇 ∈ (SubGrp‘𝐺)) |
3 | | lsmhash.u |
. . . . 5
⊢ (𝜑 → 𝑈 ∈ (SubGrp‘𝐺)) |
4 | 2, 3 | xpexd 7463 |
. . . 4
⊢ (𝜑 → (𝑇 × 𝑈) ∈ V) |
5 | | eqid 2818 |
. . . . . . . 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 2818 |
. . . . . . . 8
⊢
(proj1‘𝐺) = (proj1‘𝐺) |
12 | 5, 6, 7, 8, 2, 3, 9, 10, 11 | pj1f 18752 |
. . . . . . 7
⊢ (𝜑 → (𝑇(proj1‘𝐺)𝑈):(𝑇 ⊕ 𝑈)⟶𝑇) |
13 | 12 | ffvelrnda 6843 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑇 ⊕ 𝑈)) → ((𝑇(proj1‘𝐺)𝑈)‘𝑥) ∈ 𝑇) |
14 | 5, 6, 7, 8, 2, 3, 9, 10, 11 | pj2f 18753 |
. . . . . . 7
⊢ (𝜑 → (𝑈(proj1‘𝐺)𝑇):(𝑇 ⊕ 𝑈)⟶𝑈) |
15 | 14 | ffvelrnda 6843 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑇 ⊕ 𝑈)) → ((𝑈(proj1‘𝐺)𝑇)‘𝑥) ∈ 𝑈) |
16 | 13, 15 | opelxpd 5586 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝑇 ⊕ 𝑈)) → 〈((𝑇(proj1‘𝐺)𝑈)‘𝑥), ((𝑈(proj1‘𝐺)𝑇)‘𝑥)〉 ∈ (𝑇 × 𝑈)) |
17 | 16 | ex 413 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ (𝑇 ⊕ 𝑈) → 〈((𝑇(proj1‘𝐺)𝑈)‘𝑥), ((𝑈(proj1‘𝐺)𝑇)‘𝑥)〉 ∈ (𝑇 × 𝑈))) |
18 | 2, 3 | jca 512 |
. . . . . 6
⊢ (𝜑 → (𝑇 ∈ (SubGrp‘𝐺) ∧ 𝑈 ∈ (SubGrp‘𝐺))) |
19 | | xp1st 7710 |
. . . . . . 7
⊢ (𝑦 ∈ (𝑇 × 𝑈) → (1st ‘𝑦) ∈ 𝑇) |
20 | | xp2nd 7711 |
. . . . . . 7
⊢ (𝑦 ∈ (𝑇 × 𝑈) → (2nd ‘𝑦) ∈ 𝑈) |
21 | 19, 20 | jca 512 |
. . . . . 6
⊢ (𝑦 ∈ (𝑇 × 𝑈) → ((1st ‘𝑦) ∈ 𝑇 ∧ (2nd ‘𝑦) ∈ 𝑈)) |
22 | 5, 6 | lsmelvali 18704 |
. . . . . 6
⊢ (((𝑇 ∈ (SubGrp‘𝐺) ∧ 𝑈 ∈ (SubGrp‘𝐺)) ∧ ((1st ‘𝑦) ∈ 𝑇 ∧ (2nd ‘𝑦) ∈ 𝑈)) → ((1st ‘𝑦)(+g‘𝐺)(2nd ‘𝑦)) ∈ (𝑇 ⊕ 𝑈)) |
23 | 18, 21, 22 | syl2an 595 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑇 × 𝑈)) → ((1st ‘𝑦)(+g‘𝐺)(2nd ‘𝑦)) ∈ (𝑇 ⊕ 𝑈)) |
24 | 23 | ex 413 |
. . . 4
⊢ (𝜑 → (𝑦 ∈ (𝑇 × 𝑈) → ((1st ‘𝑦)(+g‘𝐺)(2nd ‘𝑦)) ∈ (𝑇 ⊕ 𝑈))) |
25 | 2 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ (𝑇 ⊕ 𝑈) ∧ 𝑦 ∈ (𝑇 × 𝑈))) → 𝑇 ∈ (SubGrp‘𝐺)) |
26 | 3 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ (𝑇 ⊕ 𝑈) ∧ 𝑦 ∈ (𝑇 × 𝑈))) → 𝑈 ∈ (SubGrp‘𝐺)) |
27 | 9 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ (𝑇 ⊕ 𝑈) ∧ 𝑦 ∈ (𝑇 × 𝑈))) → (𝑇 ∩ 𝑈) = { 0 }) |
28 | 10 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ (𝑇 ⊕ 𝑈) ∧ 𝑦 ∈ (𝑇 × 𝑈))) → 𝑇 ⊆ (𝑍‘𝑈)) |
29 | | simprl 767 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ (𝑇 ⊕ 𝑈) ∧ 𝑦 ∈ (𝑇 × 𝑈))) → 𝑥 ∈ (𝑇 ⊕ 𝑈)) |
30 | 19 | ad2antll 725 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ (𝑇 ⊕ 𝑈) ∧ 𝑦 ∈ (𝑇 × 𝑈))) → (1st ‘𝑦) ∈ 𝑇) |
31 | 20 | ad2antll 725 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ (𝑇 ⊕ 𝑈) ∧ 𝑦 ∈ (𝑇 × 𝑈))) → (2nd ‘𝑦) ∈ 𝑈) |
32 | 5, 6, 7, 8, 25, 26, 27, 28, 11, 29, 30, 31 | pj1eq 18755 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ (𝑇 ⊕ 𝑈) ∧ 𝑦 ∈ (𝑇 × 𝑈))) → (𝑥 = ((1st ‘𝑦)(+g‘𝐺)(2nd ‘𝑦)) ↔ (((𝑇(proj1‘𝐺)𝑈)‘𝑥) = (1st ‘𝑦) ∧ ((𝑈(proj1‘𝐺)𝑇)‘𝑥) = (2nd ‘𝑦)))) |
33 | | eqcom 2825 |
. . . . . . . 8
⊢ (((𝑇(proj1‘𝐺)𝑈)‘𝑥) = (1st ‘𝑦) ↔ (1st ‘𝑦) = ((𝑇(proj1‘𝐺)𝑈)‘𝑥)) |
34 | | eqcom 2825 |
. . . . . . . 8
⊢ (((𝑈(proj1‘𝐺)𝑇)‘𝑥) = (2nd ‘𝑦) ↔ (2nd ‘𝑦) = ((𝑈(proj1‘𝐺)𝑇)‘𝑥)) |
35 | 33, 34 | anbi12i 626 |
. . . . . . 7
⊢ ((((𝑇(proj1‘𝐺)𝑈)‘𝑥) = (1st ‘𝑦) ∧ ((𝑈(proj1‘𝐺)𝑇)‘𝑥) = (2nd ‘𝑦)) ↔ ((1st ‘𝑦) = ((𝑇(proj1‘𝐺)𝑈)‘𝑥) ∧ (2nd ‘𝑦) = ((𝑈(proj1‘𝐺)𝑇)‘𝑥))) |
36 | 32, 35 | syl6bb 288 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ (𝑇 ⊕ 𝑈) ∧ 𝑦 ∈ (𝑇 × 𝑈))) → (𝑥 = ((1st ‘𝑦)(+g‘𝐺)(2nd ‘𝑦)) ↔ ((1st ‘𝑦) = ((𝑇(proj1‘𝐺)𝑈)‘𝑥) ∧ (2nd ‘𝑦) = ((𝑈(proj1‘𝐺)𝑇)‘𝑥)))) |
37 | | eqop 7720 |
. . . . . . 7
⊢ (𝑦 ∈ (𝑇 × 𝑈) → (𝑦 = 〈((𝑇(proj1‘𝐺)𝑈)‘𝑥), ((𝑈(proj1‘𝐺)𝑇)‘𝑥)〉 ↔ ((1st ‘𝑦) = ((𝑇(proj1‘𝐺)𝑈)‘𝑥) ∧ (2nd ‘𝑦) = ((𝑈(proj1‘𝐺)𝑇)‘𝑥)))) |
38 | 37 | ad2antll 725 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ (𝑇 ⊕ 𝑈) ∧ 𝑦 ∈ (𝑇 × 𝑈))) → (𝑦 = 〈((𝑇(proj1‘𝐺)𝑈)‘𝑥), ((𝑈(proj1‘𝐺)𝑇)‘𝑥)〉 ↔ ((1st ‘𝑦) = ((𝑇(proj1‘𝐺)𝑈)‘𝑥) ∧ (2nd ‘𝑦) = ((𝑈(proj1‘𝐺)𝑇)‘𝑥)))) |
39 | 36, 38 | bitr4d 283 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ (𝑇 ⊕ 𝑈) ∧ 𝑦 ∈ (𝑇 × 𝑈))) → (𝑥 = ((1st ‘𝑦)(+g‘𝐺)(2nd ‘𝑦)) ↔ 𝑦 = 〈((𝑇(proj1‘𝐺)𝑈)‘𝑥), ((𝑈(proj1‘𝐺)𝑇)‘𝑥)〉)) |
40 | 39 | ex 413 |
. . . 4
⊢ (𝜑 → ((𝑥 ∈ (𝑇 ⊕ 𝑈) ∧ 𝑦 ∈ (𝑇 × 𝑈)) → (𝑥 = ((1st ‘𝑦)(+g‘𝐺)(2nd ‘𝑦)) ↔ 𝑦 = 〈((𝑇(proj1‘𝐺)𝑈)‘𝑥), ((𝑈(proj1‘𝐺)𝑇)‘𝑥)〉))) |
41 | 1, 4, 17, 24, 40 | en3d 8534 |
. . 3
⊢ (𝜑 → (𝑇 ⊕ 𝑈) ≈ (𝑇 × 𝑈)) |
42 | | hasheni 13696 |
. . 3
⊢ ((𝑇 ⊕ 𝑈) ≈ (𝑇 × 𝑈) → (♯‘(𝑇 ⊕ 𝑈)) = (♯‘(𝑇 × 𝑈))) |
43 | 41, 42 | syl 17 |
. 2
⊢ (𝜑 → (♯‘(𝑇 ⊕ 𝑈)) = (♯‘(𝑇 × 𝑈))) |
44 | | lsmhash.1 |
. . 3
⊢ (𝜑 → 𝑇 ∈ Fin) |
45 | | lsmhash.2 |
. . 3
⊢ (𝜑 → 𝑈 ∈ Fin) |
46 | | hashxp 13783 |
. . 3
⊢ ((𝑇 ∈ Fin ∧ 𝑈 ∈ Fin) →
(♯‘(𝑇 ×
𝑈)) = ((♯‘𝑇) · (♯‘𝑈))) |
47 | 44, 45, 46 | syl2anc 584 |
. 2
⊢ (𝜑 → (♯‘(𝑇 × 𝑈)) = ((♯‘𝑇) · (♯‘𝑈))) |
48 | 43, 47 | eqtrd 2853 |
1
⊢ (𝜑 → (♯‘(𝑇 ⊕ 𝑈)) = ((♯‘𝑇) · (♯‘𝑈))) |