Step | Hyp | Ref
| Expression |
1 | | submrcl 18441 |
. . 3
⊢ (𝐴 ∈ (SubMnd‘𝑀) → 𝑀 ∈ Mnd) |
2 | | ssinss1 4171 |
. . . . . . . . 9
⊢ (𝐴 ⊆ (Base‘𝑀) → (𝐴 ∩ 𝐵) ⊆ (Base‘𝑀)) |
3 | 2 | 3ad2ant1 1132 |
. . . . . . . 8
⊢ ((𝐴 ⊆ (Base‘𝑀) ∧
(0g‘𝑀)
∈ 𝐴 ∧
∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐴 (𝑎(+g‘𝑀)𝑏) ∈ 𝐴) → (𝐴 ∩ 𝐵) ⊆ (Base‘𝑀)) |
4 | 3 | ad2antrl 725 |
. . . . . . 7
⊢ ((𝑀 ∈ Mnd ∧ ((𝐴 ⊆ (Base‘𝑀) ∧
(0g‘𝑀)
∈ 𝐴 ∧
∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐴 (𝑎(+g‘𝑀)𝑏) ∈ 𝐴) ∧ (𝐵 ⊆ (Base‘𝑀) ∧ (0g‘𝑀) ∈ 𝐵 ∧ ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 (𝑎(+g‘𝑀)𝑏) ∈ 𝐵))) → (𝐴 ∩ 𝐵) ⊆ (Base‘𝑀)) |
5 | | elin 3903 |
. . . . . . . . . . . . 13
⊢
((0g‘𝑀) ∈ (𝐴 ∩ 𝐵) ↔ ((0g‘𝑀) ∈ 𝐴 ∧ (0g‘𝑀) ∈ 𝐵)) |
6 | 5 | simplbi2com 503 |
. . . . . . . . . . . 12
⊢
((0g‘𝑀) ∈ 𝐵 → ((0g‘𝑀) ∈ 𝐴 → (0g‘𝑀) ∈ (𝐴 ∩ 𝐵))) |
7 | 6 | 3ad2ant2 1133 |
. . . . . . . . . . 11
⊢ ((𝐵 ⊆ (Base‘𝑀) ∧
(0g‘𝑀)
∈ 𝐵 ∧
∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 (𝑎(+g‘𝑀)𝑏) ∈ 𝐵) → ((0g‘𝑀) ∈ 𝐴 → (0g‘𝑀) ∈ (𝐴 ∩ 𝐵))) |
8 | 7 | com12 32 |
. . . . . . . . . 10
⊢
((0g‘𝑀) ∈ 𝐴 → ((𝐵 ⊆ (Base‘𝑀) ∧ (0g‘𝑀) ∈ 𝐵 ∧ ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 (𝑎(+g‘𝑀)𝑏) ∈ 𝐵) → (0g‘𝑀) ∈ (𝐴 ∩ 𝐵))) |
9 | 8 | 3ad2ant2 1133 |
. . . . . . . . 9
⊢ ((𝐴 ⊆ (Base‘𝑀) ∧
(0g‘𝑀)
∈ 𝐴 ∧
∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐴 (𝑎(+g‘𝑀)𝑏) ∈ 𝐴) → ((𝐵 ⊆ (Base‘𝑀) ∧ (0g‘𝑀) ∈ 𝐵 ∧ ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 (𝑎(+g‘𝑀)𝑏) ∈ 𝐵) → (0g‘𝑀) ∈ (𝐴 ∩ 𝐵))) |
10 | 9 | imp 407 |
. . . . . . . 8
⊢ (((𝐴 ⊆ (Base‘𝑀) ∧
(0g‘𝑀)
∈ 𝐴 ∧
∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐴 (𝑎(+g‘𝑀)𝑏) ∈ 𝐴) ∧ (𝐵 ⊆ (Base‘𝑀) ∧ (0g‘𝑀) ∈ 𝐵 ∧ ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 (𝑎(+g‘𝑀)𝑏) ∈ 𝐵)) → (0g‘𝑀) ∈ (𝐴 ∩ 𝐵)) |
11 | 10 | adantl 482 |
. . . . . . 7
⊢ ((𝑀 ∈ Mnd ∧ ((𝐴 ⊆ (Base‘𝑀) ∧
(0g‘𝑀)
∈ 𝐴 ∧
∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐴 (𝑎(+g‘𝑀)𝑏) ∈ 𝐴) ∧ (𝐵 ⊆ (Base‘𝑀) ∧ (0g‘𝑀) ∈ 𝐵 ∧ ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 (𝑎(+g‘𝑀)𝑏) ∈ 𝐵))) → (0g‘𝑀) ∈ (𝐴 ∩ 𝐵)) |
12 | | elin 3903 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (𝐴 ∩ 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)) |
13 | | elin 3903 |
. . . . . . . . . 10
⊢ (𝑦 ∈ (𝐴 ∩ 𝐵) ↔ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) |
14 | 12, 13 | anbi12i 627 |
. . . . . . . . 9
⊢ ((𝑥 ∈ (𝐴 ∩ 𝐵) ∧ 𝑦 ∈ (𝐴 ∩ 𝐵)) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))) |
15 | | oveq1 7282 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑎 = 𝑥 → (𝑎(+g‘𝑀)𝑏) = (𝑥(+g‘𝑀)𝑏)) |
16 | 15 | eleq1d 2823 |
. . . . . . . . . . . . . . . 16
⊢ (𝑎 = 𝑥 → ((𝑎(+g‘𝑀)𝑏) ∈ 𝐴 ↔ (𝑥(+g‘𝑀)𝑏) ∈ 𝐴)) |
17 | | oveq2 7283 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑏 = 𝑦 → (𝑥(+g‘𝑀)𝑏) = (𝑥(+g‘𝑀)𝑦)) |
18 | 17 | eleq1d 2823 |
. . . . . . . . . . . . . . . 16
⊢ (𝑏 = 𝑦 → ((𝑥(+g‘𝑀)𝑏) ∈ 𝐴 ↔ (𝑥(+g‘𝑀)𝑦) ∈ 𝐴)) |
19 | | simpl 483 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ 𝐴) |
20 | 19 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → 𝑥 ∈ 𝐴) |
21 | | eqidd 2739 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑎 = 𝑥) → 𝐴 = 𝐴) |
22 | | simpl 483 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝑦 ∈ 𝐴) |
23 | 22 | adantl 482 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → 𝑦 ∈ 𝐴) |
24 | 16, 18, 20, 21, 23 | rspc2vd 3883 |
. . . . . . . . . . . . . . 15
⊢ (((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → (∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐴 (𝑎(+g‘𝑀)𝑏) ∈ 𝐴 → (𝑥(+g‘𝑀)𝑦) ∈ 𝐴)) |
25 | 24 | com12 32 |
. . . . . . . . . . . . . 14
⊢
(∀𝑎 ∈
𝐴 ∀𝑏 ∈ 𝐴 (𝑎(+g‘𝑀)𝑏) ∈ 𝐴 → (((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → (𝑥(+g‘𝑀)𝑦) ∈ 𝐴)) |
26 | 25 | 3ad2ant3 1134 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ⊆ (Base‘𝑀) ∧
(0g‘𝑀)
∈ 𝐴 ∧
∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐴 (𝑎(+g‘𝑀)𝑏) ∈ 𝐴) → (((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → (𝑥(+g‘𝑀)𝑦) ∈ 𝐴)) |
27 | 26 | ad2antrl 725 |
. . . . . . . . . . . 12
⊢ ((𝑀 ∈ Mnd ∧ ((𝐴 ⊆ (Base‘𝑀) ∧
(0g‘𝑀)
∈ 𝐴 ∧
∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐴 (𝑎(+g‘𝑀)𝑏) ∈ 𝐴) ∧ (𝐵 ⊆ (Base‘𝑀) ∧ (0g‘𝑀) ∈ 𝐵 ∧ ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 (𝑎(+g‘𝑀)𝑏) ∈ 𝐵))) → (((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → (𝑥(+g‘𝑀)𝑦) ∈ 𝐴)) |
28 | 27 | imp 407 |
. . . . . . . . . . 11
⊢ (((𝑀 ∈ Mnd ∧ ((𝐴 ⊆ (Base‘𝑀) ∧
(0g‘𝑀)
∈ 𝐴 ∧
∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐴 (𝑎(+g‘𝑀)𝑏) ∈ 𝐴) ∧ (𝐵 ⊆ (Base‘𝑀) ∧ (0g‘𝑀) ∈ 𝐵 ∧ ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 (𝑎(+g‘𝑀)𝑏) ∈ 𝐵))) ∧ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))) → (𝑥(+g‘𝑀)𝑦) ∈ 𝐴) |
29 | 15 | eleq1d 2823 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑎 = 𝑥 → ((𝑎(+g‘𝑀)𝑏) ∈ 𝐵 ↔ (𝑥(+g‘𝑀)𝑏) ∈ 𝐵)) |
30 | 17 | eleq1d 2823 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑏 = 𝑦 → ((𝑥(+g‘𝑀)𝑏) ∈ 𝐵 ↔ (𝑥(+g‘𝑀)𝑦) ∈ 𝐵)) |
31 | | simpr 485 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ 𝐵) |
32 | 31 | adantr 481 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → 𝑥 ∈ 𝐵) |
33 | | eqidd 2739 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) ∧ 𝑎 = 𝑥) → 𝐵 = 𝐵) |
34 | | simpr 485 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝑦 ∈ 𝐵) |
35 | 34 | adantl 482 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → 𝑦 ∈ 𝐵) |
36 | 29, 30, 32, 33, 35 | rspc2vd 3883 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → (∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 (𝑎(+g‘𝑀)𝑏) ∈ 𝐵 → (𝑥(+g‘𝑀)𝑦) ∈ 𝐵)) |
37 | 36 | com12 32 |
. . . . . . . . . . . . . . 15
⊢
(∀𝑎 ∈
𝐵 ∀𝑏 ∈ 𝐵 (𝑎(+g‘𝑀)𝑏) ∈ 𝐵 → (((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → (𝑥(+g‘𝑀)𝑦) ∈ 𝐵)) |
38 | 37 | 3ad2ant3 1134 |
. . . . . . . . . . . . . 14
⊢ ((𝐵 ⊆ (Base‘𝑀) ∧
(0g‘𝑀)
∈ 𝐵 ∧
∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 (𝑎(+g‘𝑀)𝑏) ∈ 𝐵) → (((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → (𝑥(+g‘𝑀)𝑦) ∈ 𝐵)) |
39 | 38 | adantl 482 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ⊆ (Base‘𝑀) ∧
(0g‘𝑀)
∈ 𝐴 ∧
∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐴 (𝑎(+g‘𝑀)𝑏) ∈ 𝐴) ∧ (𝐵 ⊆ (Base‘𝑀) ∧ (0g‘𝑀) ∈ 𝐵 ∧ ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 (𝑎(+g‘𝑀)𝑏) ∈ 𝐵)) → (((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → (𝑥(+g‘𝑀)𝑦) ∈ 𝐵)) |
40 | 39 | adantl 482 |
. . . . . . . . . . . 12
⊢ ((𝑀 ∈ Mnd ∧ ((𝐴 ⊆ (Base‘𝑀) ∧
(0g‘𝑀)
∈ 𝐴 ∧
∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐴 (𝑎(+g‘𝑀)𝑏) ∈ 𝐴) ∧ (𝐵 ⊆ (Base‘𝑀) ∧ (0g‘𝑀) ∈ 𝐵 ∧ ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 (𝑎(+g‘𝑀)𝑏) ∈ 𝐵))) → (((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → (𝑥(+g‘𝑀)𝑦) ∈ 𝐵)) |
41 | 40 | imp 407 |
. . . . . . . . . . 11
⊢ (((𝑀 ∈ Mnd ∧ ((𝐴 ⊆ (Base‘𝑀) ∧
(0g‘𝑀)
∈ 𝐴 ∧
∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐴 (𝑎(+g‘𝑀)𝑏) ∈ 𝐴) ∧ (𝐵 ⊆ (Base‘𝑀) ∧ (0g‘𝑀) ∈ 𝐵 ∧ ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 (𝑎(+g‘𝑀)𝑏) ∈ 𝐵))) ∧ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))) → (𝑥(+g‘𝑀)𝑦) ∈ 𝐵) |
42 | 28, 41 | elind 4128 |
. . . . . . . . . 10
⊢ (((𝑀 ∈ Mnd ∧ ((𝐴 ⊆ (Base‘𝑀) ∧
(0g‘𝑀)
∈ 𝐴 ∧
∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐴 (𝑎(+g‘𝑀)𝑏) ∈ 𝐴) ∧ (𝐵 ⊆ (Base‘𝑀) ∧ (0g‘𝑀) ∈ 𝐵 ∧ ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 (𝑎(+g‘𝑀)𝑏) ∈ 𝐵))) ∧ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))) → (𝑥(+g‘𝑀)𝑦) ∈ (𝐴 ∩ 𝐵)) |
43 | 42 | ex 413 |
. . . . . . . . 9
⊢ ((𝑀 ∈ Mnd ∧ ((𝐴 ⊆ (Base‘𝑀) ∧
(0g‘𝑀)
∈ 𝐴 ∧
∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐴 (𝑎(+g‘𝑀)𝑏) ∈ 𝐴) ∧ (𝐵 ⊆ (Base‘𝑀) ∧ (0g‘𝑀) ∈ 𝐵 ∧ ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 (𝑎(+g‘𝑀)𝑏) ∈ 𝐵))) → (((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → (𝑥(+g‘𝑀)𝑦) ∈ (𝐴 ∩ 𝐵))) |
44 | 14, 43 | syl5bi 241 |
. . . . . . . 8
⊢ ((𝑀 ∈ Mnd ∧ ((𝐴 ⊆ (Base‘𝑀) ∧
(0g‘𝑀)
∈ 𝐴 ∧
∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐴 (𝑎(+g‘𝑀)𝑏) ∈ 𝐴) ∧ (𝐵 ⊆ (Base‘𝑀) ∧ (0g‘𝑀) ∈ 𝐵 ∧ ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 (𝑎(+g‘𝑀)𝑏) ∈ 𝐵))) → ((𝑥 ∈ (𝐴 ∩ 𝐵) ∧ 𝑦 ∈ (𝐴 ∩ 𝐵)) → (𝑥(+g‘𝑀)𝑦) ∈ (𝐴 ∩ 𝐵))) |
45 | 44 | ralrimivv 3122 |
. . . . . . 7
⊢ ((𝑀 ∈ Mnd ∧ ((𝐴 ⊆ (Base‘𝑀) ∧
(0g‘𝑀)
∈ 𝐴 ∧
∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐴 (𝑎(+g‘𝑀)𝑏) ∈ 𝐴) ∧ (𝐵 ⊆ (Base‘𝑀) ∧ (0g‘𝑀) ∈ 𝐵 ∧ ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 (𝑎(+g‘𝑀)𝑏) ∈ 𝐵))) → ∀𝑥 ∈ (𝐴 ∩ 𝐵)∀𝑦 ∈ (𝐴 ∩ 𝐵)(𝑥(+g‘𝑀)𝑦) ∈ (𝐴 ∩ 𝐵)) |
46 | 4, 11, 45 | 3jca 1127 |
. . . . . 6
⊢ ((𝑀 ∈ Mnd ∧ ((𝐴 ⊆ (Base‘𝑀) ∧
(0g‘𝑀)
∈ 𝐴 ∧
∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐴 (𝑎(+g‘𝑀)𝑏) ∈ 𝐴) ∧ (𝐵 ⊆ (Base‘𝑀) ∧ (0g‘𝑀) ∈ 𝐵 ∧ ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 (𝑎(+g‘𝑀)𝑏) ∈ 𝐵))) → ((𝐴 ∩ 𝐵) ⊆ (Base‘𝑀) ∧ (0g‘𝑀) ∈ (𝐴 ∩ 𝐵) ∧ ∀𝑥 ∈ (𝐴 ∩ 𝐵)∀𝑦 ∈ (𝐴 ∩ 𝐵)(𝑥(+g‘𝑀)𝑦) ∈ (𝐴 ∩ 𝐵))) |
47 | 46 | ex 413 |
. . . . 5
⊢ (𝑀 ∈ Mnd → (((𝐴 ⊆ (Base‘𝑀) ∧
(0g‘𝑀)
∈ 𝐴 ∧
∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐴 (𝑎(+g‘𝑀)𝑏) ∈ 𝐴) ∧ (𝐵 ⊆ (Base‘𝑀) ∧ (0g‘𝑀) ∈ 𝐵 ∧ ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 (𝑎(+g‘𝑀)𝑏) ∈ 𝐵)) → ((𝐴 ∩ 𝐵) ⊆ (Base‘𝑀) ∧ (0g‘𝑀) ∈ (𝐴 ∩ 𝐵) ∧ ∀𝑥 ∈ (𝐴 ∩ 𝐵)∀𝑦 ∈ (𝐴 ∩ 𝐵)(𝑥(+g‘𝑀)𝑦) ∈ (𝐴 ∩ 𝐵)))) |
48 | | eqid 2738 |
. . . . . . 7
⊢
(Base‘𝑀) =
(Base‘𝑀) |
49 | | eqid 2738 |
. . . . . . 7
⊢
(0g‘𝑀) = (0g‘𝑀) |
50 | | eqid 2738 |
. . . . . . 7
⊢
(+g‘𝑀) = (+g‘𝑀) |
51 | 48, 49, 50 | issubm 18442 |
. . . . . 6
⊢ (𝑀 ∈ Mnd → (𝐴 ∈ (SubMnd‘𝑀) ↔ (𝐴 ⊆ (Base‘𝑀) ∧ (0g‘𝑀) ∈ 𝐴 ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐴 (𝑎(+g‘𝑀)𝑏) ∈ 𝐴))) |
52 | 48, 49, 50 | issubm 18442 |
. . . . . 6
⊢ (𝑀 ∈ Mnd → (𝐵 ∈ (SubMnd‘𝑀) ↔ (𝐵 ⊆ (Base‘𝑀) ∧ (0g‘𝑀) ∈ 𝐵 ∧ ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 (𝑎(+g‘𝑀)𝑏) ∈ 𝐵))) |
53 | 51, 52 | anbi12d 631 |
. . . . 5
⊢ (𝑀 ∈ Mnd → ((𝐴 ∈ (SubMnd‘𝑀) ∧ 𝐵 ∈ (SubMnd‘𝑀)) ↔ ((𝐴 ⊆ (Base‘𝑀) ∧ (0g‘𝑀) ∈ 𝐴 ∧ ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐴 (𝑎(+g‘𝑀)𝑏) ∈ 𝐴) ∧ (𝐵 ⊆ (Base‘𝑀) ∧ (0g‘𝑀) ∈ 𝐵 ∧ ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 (𝑎(+g‘𝑀)𝑏) ∈ 𝐵)))) |
54 | 48, 49, 50 | issubm 18442 |
. . . . 5
⊢ (𝑀 ∈ Mnd → ((𝐴 ∩ 𝐵) ∈ (SubMnd‘𝑀) ↔ ((𝐴 ∩ 𝐵) ⊆ (Base‘𝑀) ∧ (0g‘𝑀) ∈ (𝐴 ∩ 𝐵) ∧ ∀𝑥 ∈ (𝐴 ∩ 𝐵)∀𝑦 ∈ (𝐴 ∩ 𝐵)(𝑥(+g‘𝑀)𝑦) ∈ (𝐴 ∩ 𝐵)))) |
55 | 47, 53, 54 | 3imtr4d 294 |
. . . 4
⊢ (𝑀 ∈ Mnd → ((𝐴 ∈ (SubMnd‘𝑀) ∧ 𝐵 ∈ (SubMnd‘𝑀)) → (𝐴 ∩ 𝐵) ∈ (SubMnd‘𝑀))) |
56 | 55 | expd 416 |
. . 3
⊢ (𝑀 ∈ Mnd → (𝐴 ∈ (SubMnd‘𝑀) → (𝐵 ∈ (SubMnd‘𝑀) → (𝐴 ∩ 𝐵) ∈ (SubMnd‘𝑀)))) |
57 | 1, 56 | mpcom 38 |
. 2
⊢ (𝐴 ∈ (SubMnd‘𝑀) → (𝐵 ∈ (SubMnd‘𝑀) → (𝐴 ∩ 𝐵) ∈ (SubMnd‘𝑀))) |
58 | 57 | imp 407 |
1
⊢ ((𝐴 ∈ (SubMnd‘𝑀) ∧ 𝐵 ∈ (SubMnd‘𝑀)) → (𝐴 ∩ 𝐵) ∈ (SubMnd‘𝑀)) |