Step | Hyp | Ref
| Expression |
1 | | dsmmcl.p |
. . 3
⊢ 𝑃 = (𝑆Xs𝑅) |
2 | | eqid 2610 |
. . 3
⊢
(Base‘𝑃) =
(Base‘𝑃) |
3 | | dsmmacl.a |
. . 3
⊢ + =
(+g‘𝑃) |
4 | | dsmmcl.s |
. . 3
⊢ (𝜑 → 𝑆 ∈ 𝑉) |
5 | | dsmmcl.i |
. . 3
⊢ (𝜑 → 𝐼 ∈ 𝑊) |
6 | | dsmmcl.r |
. . 3
⊢ (𝜑 → 𝑅:𝐼⟶Mnd) |
7 | | dsmmacl.j |
. . . . 5
⊢ (𝜑 → 𝐽 ∈ 𝐻) |
8 | | eqid 2610 |
. . . . . 6
⊢ (𝑆 ⊕m 𝑅) = (𝑆 ⊕m 𝑅) |
9 | | dsmmcl.h |
. . . . . 6
⊢ 𝐻 = (Base‘(𝑆 ⊕m 𝑅)) |
10 | | ffn 5958 |
. . . . . . 7
⊢ (𝑅:𝐼⟶Mnd → 𝑅 Fn 𝐼) |
11 | 6, 10 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝑅 Fn 𝐼) |
12 | 1, 8, 2, 9, 5, 11 | dsmmelbas 19902 |
. . . . 5
⊢ (𝜑 → (𝐽 ∈ 𝐻 ↔ (𝐽 ∈ (Base‘𝑃) ∧ {𝑎 ∈ 𝐼 ∣ (𝐽‘𝑎) ≠ (0g‘(𝑅‘𝑎))} ∈ Fin))) |
13 | 7, 12 | mpbid 221 |
. . . 4
⊢ (𝜑 → (𝐽 ∈ (Base‘𝑃) ∧ {𝑎 ∈ 𝐼 ∣ (𝐽‘𝑎) ≠ (0g‘(𝑅‘𝑎))} ∈ Fin)) |
14 | 13 | simpld 474 |
. . 3
⊢ (𝜑 → 𝐽 ∈ (Base‘𝑃)) |
15 | | dsmmacl.k |
. . . . 5
⊢ (𝜑 → 𝐾 ∈ 𝐻) |
16 | 1, 8, 2, 9, 5, 11 | dsmmelbas 19902 |
. . . . 5
⊢ (𝜑 → (𝐾 ∈ 𝐻 ↔ (𝐾 ∈ (Base‘𝑃) ∧ {𝑎 ∈ 𝐼 ∣ (𝐾‘𝑎) ≠ (0g‘(𝑅‘𝑎))} ∈ Fin))) |
17 | 15, 16 | mpbid 221 |
. . . 4
⊢ (𝜑 → (𝐾 ∈ (Base‘𝑃) ∧ {𝑎 ∈ 𝐼 ∣ (𝐾‘𝑎) ≠ (0g‘(𝑅‘𝑎))} ∈ Fin)) |
18 | 17 | simpld 474 |
. . 3
⊢ (𝜑 → 𝐾 ∈ (Base‘𝑃)) |
19 | 1, 2, 3, 4, 5, 6, 14, 18 | prdsplusgcl 17144 |
. 2
⊢ (𝜑 → (𝐽 + 𝐾) ∈ (Base‘𝑃)) |
20 | 4 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐼) → 𝑆 ∈ 𝑉) |
21 | 5 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐼) → 𝐼 ∈ 𝑊) |
22 | 11 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐼) → 𝑅 Fn 𝐼) |
23 | 14 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐼) → 𝐽 ∈ (Base‘𝑃)) |
24 | 18 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐼) → 𝐾 ∈ (Base‘𝑃)) |
25 | | simpr 476 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐼) → 𝑎 ∈ 𝐼) |
26 | 1, 2, 20, 21, 22, 23, 24, 3, 25 | prdsplusgfval 15957 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐼) → ((𝐽 + 𝐾)‘𝑎) = ((𝐽‘𝑎)(+g‘(𝑅‘𝑎))(𝐾‘𝑎))) |
27 | 26 | neeq1d 2841 |
. . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐼) → (((𝐽 + 𝐾)‘𝑎) ≠ (0g‘(𝑅‘𝑎)) ↔ ((𝐽‘𝑎)(+g‘(𝑅‘𝑎))(𝐾‘𝑎)) ≠ (0g‘(𝑅‘𝑎)))) |
28 | 27 | rabbidva 3163 |
. . 3
⊢ (𝜑 → {𝑎 ∈ 𝐼 ∣ ((𝐽 + 𝐾)‘𝑎) ≠ (0g‘(𝑅‘𝑎))} = {𝑎 ∈ 𝐼 ∣ ((𝐽‘𝑎)(+g‘(𝑅‘𝑎))(𝐾‘𝑎)) ≠ (0g‘(𝑅‘𝑎))}) |
29 | 13 | simprd 478 |
. . . . 5
⊢ (𝜑 → {𝑎 ∈ 𝐼 ∣ (𝐽‘𝑎) ≠ (0g‘(𝑅‘𝑎))} ∈ Fin) |
30 | 17 | simprd 478 |
. . . . 5
⊢ (𝜑 → {𝑎 ∈ 𝐼 ∣ (𝐾‘𝑎) ≠ (0g‘(𝑅‘𝑎))} ∈ Fin) |
31 | | unfi 8112 |
. . . . 5
⊢ (({𝑎 ∈ 𝐼 ∣ (𝐽‘𝑎) ≠ (0g‘(𝑅‘𝑎))} ∈ Fin ∧ {𝑎 ∈ 𝐼 ∣ (𝐾‘𝑎) ≠ (0g‘(𝑅‘𝑎))} ∈ Fin) → ({𝑎 ∈ 𝐼 ∣ (𝐽‘𝑎) ≠ (0g‘(𝑅‘𝑎))} ∪ {𝑎 ∈ 𝐼 ∣ (𝐾‘𝑎) ≠ (0g‘(𝑅‘𝑎))}) ∈ Fin) |
32 | 29, 30, 31 | syl2anc 691 |
. . . 4
⊢ (𝜑 → ({𝑎 ∈ 𝐼 ∣ (𝐽‘𝑎) ≠ (0g‘(𝑅‘𝑎))} ∪ {𝑎 ∈ 𝐼 ∣ (𝐾‘𝑎) ≠ (0g‘(𝑅‘𝑎))}) ∈ Fin) |
33 | | neorian 2876 |
. . . . . . . . . 10
⊢ (((𝐽‘𝑎) ≠ (0g‘(𝑅‘𝑎)) ∨ (𝐾‘𝑎) ≠ (0g‘(𝑅‘𝑎))) ↔ ¬ ((𝐽‘𝑎) = (0g‘(𝑅‘𝑎)) ∧ (𝐾‘𝑎) = (0g‘(𝑅‘𝑎)))) |
34 | 33 | bicomi 213 |
. . . . . . . . 9
⊢ (¬
((𝐽‘𝑎) = (0g‘(𝑅‘𝑎)) ∧ (𝐾‘𝑎) = (0g‘(𝑅‘𝑎))) ↔ ((𝐽‘𝑎) ≠ (0g‘(𝑅‘𝑎)) ∨ (𝐾‘𝑎) ≠ (0g‘(𝑅‘𝑎)))) |
35 | 34 | con1bii 345 |
. . . . . . . 8
⊢ (¬
((𝐽‘𝑎) ≠
(0g‘(𝑅‘𝑎)) ∨ (𝐾‘𝑎) ≠ (0g‘(𝑅‘𝑎))) ↔ ((𝐽‘𝑎) = (0g‘(𝑅‘𝑎)) ∧ (𝐾‘𝑎) = (0g‘(𝑅‘𝑎)))) |
36 | 6 | ffvelrnda 6267 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐼) → (𝑅‘𝑎) ∈ Mnd) |
37 | | eqid 2610 |
. . . . . . . . . . . 12
⊢
(Base‘(𝑅‘𝑎)) = (Base‘(𝑅‘𝑎)) |
38 | | eqid 2610 |
. . . . . . . . . . . 12
⊢
(0g‘(𝑅‘𝑎)) = (0g‘(𝑅‘𝑎)) |
39 | 37, 38 | mndidcl 17131 |
. . . . . . . . . . 11
⊢ ((𝑅‘𝑎) ∈ Mnd →
(0g‘(𝑅‘𝑎)) ∈ (Base‘(𝑅‘𝑎))) |
40 | 36, 39 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐼) → (0g‘(𝑅‘𝑎)) ∈ (Base‘(𝑅‘𝑎))) |
41 | | eqid 2610 |
. . . . . . . . . . 11
⊢
(+g‘(𝑅‘𝑎)) = (+g‘(𝑅‘𝑎)) |
42 | 37, 41, 38 | mndlid 17134 |
. . . . . . . . . 10
⊢ (((𝑅‘𝑎) ∈ Mnd ∧
(0g‘(𝑅‘𝑎)) ∈ (Base‘(𝑅‘𝑎))) → ((0g‘(𝑅‘𝑎))(+g‘(𝑅‘𝑎))(0g‘(𝑅‘𝑎))) = (0g‘(𝑅‘𝑎))) |
43 | 36, 40, 42 | syl2anc 691 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐼) → ((0g‘(𝑅‘𝑎))(+g‘(𝑅‘𝑎))(0g‘(𝑅‘𝑎))) = (0g‘(𝑅‘𝑎))) |
44 | | oveq12 6558 |
. . . . . . . . . 10
⊢ (((𝐽‘𝑎) = (0g‘(𝑅‘𝑎)) ∧ (𝐾‘𝑎) = (0g‘(𝑅‘𝑎))) → ((𝐽‘𝑎)(+g‘(𝑅‘𝑎))(𝐾‘𝑎)) = ((0g‘(𝑅‘𝑎))(+g‘(𝑅‘𝑎))(0g‘(𝑅‘𝑎)))) |
45 | 44 | eqeq1d 2612 |
. . . . . . . . 9
⊢ (((𝐽‘𝑎) = (0g‘(𝑅‘𝑎)) ∧ (𝐾‘𝑎) = (0g‘(𝑅‘𝑎))) → (((𝐽‘𝑎)(+g‘(𝑅‘𝑎))(𝐾‘𝑎)) = (0g‘(𝑅‘𝑎)) ↔ ((0g‘(𝑅‘𝑎))(+g‘(𝑅‘𝑎))(0g‘(𝑅‘𝑎))) = (0g‘(𝑅‘𝑎)))) |
46 | 43, 45 | syl5ibrcom 236 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐼) → (((𝐽‘𝑎) = (0g‘(𝑅‘𝑎)) ∧ (𝐾‘𝑎) = (0g‘(𝑅‘𝑎))) → ((𝐽‘𝑎)(+g‘(𝑅‘𝑎))(𝐾‘𝑎)) = (0g‘(𝑅‘𝑎)))) |
47 | 35, 46 | syl5bi 231 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐼) → (¬ ((𝐽‘𝑎) ≠ (0g‘(𝑅‘𝑎)) ∨ (𝐾‘𝑎) ≠ (0g‘(𝑅‘𝑎))) → ((𝐽‘𝑎)(+g‘(𝑅‘𝑎))(𝐾‘𝑎)) = (0g‘(𝑅‘𝑎)))) |
48 | 47 | necon1ad 2799 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐼) → (((𝐽‘𝑎)(+g‘(𝑅‘𝑎))(𝐾‘𝑎)) ≠ (0g‘(𝑅‘𝑎)) → ((𝐽‘𝑎) ≠ (0g‘(𝑅‘𝑎)) ∨ (𝐾‘𝑎) ≠ (0g‘(𝑅‘𝑎))))) |
49 | 48 | ss2rabdv 3646 |
. . . . 5
⊢ (𝜑 → {𝑎 ∈ 𝐼 ∣ ((𝐽‘𝑎)(+g‘(𝑅‘𝑎))(𝐾‘𝑎)) ≠ (0g‘(𝑅‘𝑎))} ⊆ {𝑎 ∈ 𝐼 ∣ ((𝐽‘𝑎) ≠ (0g‘(𝑅‘𝑎)) ∨ (𝐾‘𝑎) ≠ (0g‘(𝑅‘𝑎)))}) |
50 | | unrab 3857 |
. . . . 5
⊢ ({𝑎 ∈ 𝐼 ∣ (𝐽‘𝑎) ≠ (0g‘(𝑅‘𝑎))} ∪ {𝑎 ∈ 𝐼 ∣ (𝐾‘𝑎) ≠ (0g‘(𝑅‘𝑎))}) = {𝑎 ∈ 𝐼 ∣ ((𝐽‘𝑎) ≠ (0g‘(𝑅‘𝑎)) ∨ (𝐾‘𝑎) ≠ (0g‘(𝑅‘𝑎)))} |
51 | 49, 50 | syl6sseqr 3615 |
. . . 4
⊢ (𝜑 → {𝑎 ∈ 𝐼 ∣ ((𝐽‘𝑎)(+g‘(𝑅‘𝑎))(𝐾‘𝑎)) ≠ (0g‘(𝑅‘𝑎))} ⊆ ({𝑎 ∈ 𝐼 ∣ (𝐽‘𝑎) ≠ (0g‘(𝑅‘𝑎))} ∪ {𝑎 ∈ 𝐼 ∣ (𝐾‘𝑎) ≠ (0g‘(𝑅‘𝑎))})) |
52 | | ssfi 8065 |
. . . 4
⊢ ((({𝑎 ∈ 𝐼 ∣ (𝐽‘𝑎) ≠ (0g‘(𝑅‘𝑎))} ∪ {𝑎 ∈ 𝐼 ∣ (𝐾‘𝑎) ≠ (0g‘(𝑅‘𝑎))}) ∈ Fin ∧ {𝑎 ∈ 𝐼 ∣ ((𝐽‘𝑎)(+g‘(𝑅‘𝑎))(𝐾‘𝑎)) ≠ (0g‘(𝑅‘𝑎))} ⊆ ({𝑎 ∈ 𝐼 ∣ (𝐽‘𝑎) ≠ (0g‘(𝑅‘𝑎))} ∪ {𝑎 ∈ 𝐼 ∣ (𝐾‘𝑎) ≠ (0g‘(𝑅‘𝑎))})) → {𝑎 ∈ 𝐼 ∣ ((𝐽‘𝑎)(+g‘(𝑅‘𝑎))(𝐾‘𝑎)) ≠ (0g‘(𝑅‘𝑎))} ∈ Fin) |
53 | 32, 51, 52 | syl2anc 691 |
. . 3
⊢ (𝜑 → {𝑎 ∈ 𝐼 ∣ ((𝐽‘𝑎)(+g‘(𝑅‘𝑎))(𝐾‘𝑎)) ≠ (0g‘(𝑅‘𝑎))} ∈ Fin) |
54 | 28, 53 | eqeltrd 2688 |
. 2
⊢ (𝜑 → {𝑎 ∈ 𝐼 ∣ ((𝐽 + 𝐾)‘𝑎) ≠ (0g‘(𝑅‘𝑎))} ∈ Fin) |
55 | 1, 8, 2, 9, 5, 11 | dsmmelbas 19902 |
. 2
⊢ (𝜑 → ((𝐽 + 𝐾) ∈ 𝐻 ↔ ((𝐽 + 𝐾) ∈ (Base‘𝑃) ∧ {𝑎 ∈ 𝐼 ∣ ((𝐽 + 𝐾)‘𝑎) ≠ (0g‘(𝑅‘𝑎))} ∈ Fin))) |
56 | 19, 54, 55 | mpbir2and 959 |
1
⊢ (𝜑 → (𝐽 + 𝐾) ∈ 𝐻) |