Step | Hyp | Ref
| Expression |
1 | | simpll 766 |
. . . 4
⊢ (((𝑀 ∈ Smgrp ∧ 𝑆 ⊆ 𝐵) ∧ (𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐶)) → 𝑀 ∈ Smgrp) |
2 | | cntzsgrpcl.c |
. . . . . 6
⊢ 𝐶 = (𝑍‘𝑆) |
3 | | cntzsgrpcl.b |
. . . . . . 7
⊢ 𝐵 = (Base‘𝑀) |
4 | | cntzsgrpcl.z |
. . . . . . 7
⊢ 𝑍 = (Cntz‘𝑀) |
5 | 3, 4 | cntzssv 19278 |
. . . . . 6
⊢ (𝑍‘𝑆) ⊆ 𝐵 |
6 | 2, 5 | eqsstri 4014 |
. . . . 5
⊢ 𝐶 ⊆ 𝐵 |
7 | | simprl 770 |
. . . . 5
⊢ (((𝑀 ∈ Smgrp ∧ 𝑆 ⊆ 𝐵) ∧ (𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐶)) → 𝑦 ∈ 𝐶) |
8 | 6, 7 | sselid 3978 |
. . . 4
⊢ (((𝑀 ∈ Smgrp ∧ 𝑆 ⊆ 𝐵) ∧ (𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐶)) → 𝑦 ∈ 𝐵) |
9 | | simprr 772 |
. . . . 5
⊢ (((𝑀 ∈ Smgrp ∧ 𝑆 ⊆ 𝐵) ∧ (𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐶)) → 𝑧 ∈ 𝐶) |
10 | 6, 9 | sselid 3978 |
. . . 4
⊢ (((𝑀 ∈ Smgrp ∧ 𝑆 ⊆ 𝐵) ∧ (𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐶)) → 𝑧 ∈ 𝐵) |
11 | | eqid 2728 |
. . . . 5
⊢
(+g‘𝑀) = (+g‘𝑀) |
12 | 3, 11 | sgrpcl 18685 |
. . . 4
⊢ ((𝑀 ∈ Smgrp ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) → (𝑦(+g‘𝑀)𝑧) ∈ 𝐵) |
13 | 1, 8, 10, 12 | syl3anc 1369 |
. . 3
⊢ (((𝑀 ∈ Smgrp ∧ 𝑆 ⊆ 𝐵) ∧ (𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐶)) → (𝑦(+g‘𝑀)𝑧) ∈ 𝐵) |
14 | 1 | adantr 480 |
. . . . . 6
⊢ ((((𝑀 ∈ Smgrp ∧ 𝑆 ⊆ 𝐵) ∧ (𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐶)) ∧ 𝑥 ∈ 𝑆) → 𝑀 ∈ Smgrp) |
15 | 8 | adantr 480 |
. . . . . 6
⊢ ((((𝑀 ∈ Smgrp ∧ 𝑆 ⊆ 𝐵) ∧ (𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐶)) ∧ 𝑥 ∈ 𝑆) → 𝑦 ∈ 𝐵) |
16 | 10 | adantr 480 |
. . . . . 6
⊢ ((((𝑀 ∈ Smgrp ∧ 𝑆 ⊆ 𝐵) ∧ (𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐶)) ∧ 𝑥 ∈ 𝑆) → 𝑧 ∈ 𝐵) |
17 | | simpr 484 |
. . . . . . . 8
⊢ ((𝑀 ∈ Smgrp ∧ 𝑆 ⊆ 𝐵) → 𝑆 ⊆ 𝐵) |
18 | 17 | sselda 3980 |
. . . . . . 7
⊢ (((𝑀 ∈ Smgrp ∧ 𝑆 ⊆ 𝐵) ∧ 𝑥 ∈ 𝑆) → 𝑥 ∈ 𝐵) |
19 | 18 | adantlr 714 |
. . . . . 6
⊢ ((((𝑀 ∈ Smgrp ∧ 𝑆 ⊆ 𝐵) ∧ (𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐶)) ∧ 𝑥 ∈ 𝑆) → 𝑥 ∈ 𝐵) |
20 | 3, 11 | sgrpass 18684 |
. . . . . 6
⊢ ((𝑀 ∈ Smgrp ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵)) → ((𝑦(+g‘𝑀)𝑧)(+g‘𝑀)𝑥) = (𝑦(+g‘𝑀)(𝑧(+g‘𝑀)𝑥))) |
21 | 14, 15, 16, 19, 20 | syl13anc 1370 |
. . . . 5
⊢ ((((𝑀 ∈ Smgrp ∧ 𝑆 ⊆ 𝐵) ∧ (𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐶)) ∧ 𝑥 ∈ 𝑆) → ((𝑦(+g‘𝑀)𝑧)(+g‘𝑀)𝑥) = (𝑦(+g‘𝑀)(𝑧(+g‘𝑀)𝑥))) |
22 | 2 | eleq2i 2821 |
. . . . . . . . 9
⊢ (𝑧 ∈ 𝐶 ↔ 𝑧 ∈ (𝑍‘𝑆)) |
23 | 11, 4 | cntzi 19279 |
. . . . . . . . 9
⊢ ((𝑧 ∈ (𝑍‘𝑆) ∧ 𝑥 ∈ 𝑆) → (𝑧(+g‘𝑀)𝑥) = (𝑥(+g‘𝑀)𝑧)) |
24 | 22, 23 | sylanb 580 |
. . . . . . . 8
⊢ ((𝑧 ∈ 𝐶 ∧ 𝑥 ∈ 𝑆) → (𝑧(+g‘𝑀)𝑥) = (𝑥(+g‘𝑀)𝑧)) |
25 | 9, 24 | sylan 579 |
. . . . . . 7
⊢ ((((𝑀 ∈ Smgrp ∧ 𝑆 ⊆ 𝐵) ∧ (𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐶)) ∧ 𝑥 ∈ 𝑆) → (𝑧(+g‘𝑀)𝑥) = (𝑥(+g‘𝑀)𝑧)) |
26 | 25 | oveq2d 7436 |
. . . . . 6
⊢ ((((𝑀 ∈ Smgrp ∧ 𝑆 ⊆ 𝐵) ∧ (𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐶)) ∧ 𝑥 ∈ 𝑆) → (𝑦(+g‘𝑀)(𝑧(+g‘𝑀)𝑥)) = (𝑦(+g‘𝑀)(𝑥(+g‘𝑀)𝑧))) |
27 | 3, 11 | sgrpass 18684 |
. . . . . . 7
⊢ ((𝑀 ∈ Smgrp ∧ (𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → ((𝑦(+g‘𝑀)𝑥)(+g‘𝑀)𝑧) = (𝑦(+g‘𝑀)(𝑥(+g‘𝑀)𝑧))) |
28 | 14, 15, 19, 16, 27 | syl13anc 1370 |
. . . . . 6
⊢ ((((𝑀 ∈ Smgrp ∧ 𝑆 ⊆ 𝐵) ∧ (𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐶)) ∧ 𝑥 ∈ 𝑆) → ((𝑦(+g‘𝑀)𝑥)(+g‘𝑀)𝑧) = (𝑦(+g‘𝑀)(𝑥(+g‘𝑀)𝑧))) |
29 | 2 | eleq2i 2821 |
. . . . . . . . 9
⊢ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ (𝑍‘𝑆)) |
30 | 11, 4 | cntzi 19279 |
. . . . . . . . 9
⊢ ((𝑦 ∈ (𝑍‘𝑆) ∧ 𝑥 ∈ 𝑆) → (𝑦(+g‘𝑀)𝑥) = (𝑥(+g‘𝑀)𝑦)) |
31 | 29, 30 | sylanb 580 |
. . . . . . . 8
⊢ ((𝑦 ∈ 𝐶 ∧ 𝑥 ∈ 𝑆) → (𝑦(+g‘𝑀)𝑥) = (𝑥(+g‘𝑀)𝑦)) |
32 | 7, 31 | sylan 579 |
. . . . . . 7
⊢ ((((𝑀 ∈ Smgrp ∧ 𝑆 ⊆ 𝐵) ∧ (𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐶)) ∧ 𝑥 ∈ 𝑆) → (𝑦(+g‘𝑀)𝑥) = (𝑥(+g‘𝑀)𝑦)) |
33 | 32 | oveq1d 7435 |
. . . . . 6
⊢ ((((𝑀 ∈ Smgrp ∧ 𝑆 ⊆ 𝐵) ∧ (𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐶)) ∧ 𝑥 ∈ 𝑆) → ((𝑦(+g‘𝑀)𝑥)(+g‘𝑀)𝑧) = ((𝑥(+g‘𝑀)𝑦)(+g‘𝑀)𝑧)) |
34 | 26, 28, 33 | 3eqtr2d 2774 |
. . . . 5
⊢ ((((𝑀 ∈ Smgrp ∧ 𝑆 ⊆ 𝐵) ∧ (𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐶)) ∧ 𝑥 ∈ 𝑆) → (𝑦(+g‘𝑀)(𝑧(+g‘𝑀)𝑥)) = ((𝑥(+g‘𝑀)𝑦)(+g‘𝑀)𝑧)) |
35 | 3, 11 | sgrpass 18684 |
. . . . . 6
⊢ ((𝑀 ∈ Smgrp ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → ((𝑥(+g‘𝑀)𝑦)(+g‘𝑀)𝑧) = (𝑥(+g‘𝑀)(𝑦(+g‘𝑀)𝑧))) |
36 | 14, 19, 15, 16, 35 | syl13anc 1370 |
. . . . 5
⊢ ((((𝑀 ∈ Smgrp ∧ 𝑆 ⊆ 𝐵) ∧ (𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐶)) ∧ 𝑥 ∈ 𝑆) → ((𝑥(+g‘𝑀)𝑦)(+g‘𝑀)𝑧) = (𝑥(+g‘𝑀)(𝑦(+g‘𝑀)𝑧))) |
37 | 21, 34, 36 | 3eqtrd 2772 |
. . . 4
⊢ ((((𝑀 ∈ Smgrp ∧ 𝑆 ⊆ 𝐵) ∧ (𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐶)) ∧ 𝑥 ∈ 𝑆) → ((𝑦(+g‘𝑀)𝑧)(+g‘𝑀)𝑥) = (𝑥(+g‘𝑀)(𝑦(+g‘𝑀)𝑧))) |
38 | 37 | ralrimiva 3143 |
. . 3
⊢ (((𝑀 ∈ Smgrp ∧ 𝑆 ⊆ 𝐵) ∧ (𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐶)) → ∀𝑥 ∈ 𝑆 ((𝑦(+g‘𝑀)𝑧)(+g‘𝑀)𝑥) = (𝑥(+g‘𝑀)(𝑦(+g‘𝑀)𝑧))) |
39 | 2 | eleq2i 2821 |
. . . . 5
⊢ ((𝑦(+g‘𝑀)𝑧) ∈ 𝐶 ↔ (𝑦(+g‘𝑀)𝑧) ∈ (𝑍‘𝑆)) |
40 | 3, 11, 4 | elcntz 19272 |
. . . . 5
⊢ (𝑆 ⊆ 𝐵 → ((𝑦(+g‘𝑀)𝑧) ∈ (𝑍‘𝑆) ↔ ((𝑦(+g‘𝑀)𝑧) ∈ 𝐵 ∧ ∀𝑥 ∈ 𝑆 ((𝑦(+g‘𝑀)𝑧)(+g‘𝑀)𝑥) = (𝑥(+g‘𝑀)(𝑦(+g‘𝑀)𝑧))))) |
41 | 39, 40 | bitrid 283 |
. . . 4
⊢ (𝑆 ⊆ 𝐵 → ((𝑦(+g‘𝑀)𝑧) ∈ 𝐶 ↔ ((𝑦(+g‘𝑀)𝑧) ∈ 𝐵 ∧ ∀𝑥 ∈ 𝑆 ((𝑦(+g‘𝑀)𝑧)(+g‘𝑀)𝑥) = (𝑥(+g‘𝑀)(𝑦(+g‘𝑀)𝑧))))) |
42 | 41 | ad2antlr 726 |
. . 3
⊢ (((𝑀 ∈ Smgrp ∧ 𝑆 ⊆ 𝐵) ∧ (𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐶)) → ((𝑦(+g‘𝑀)𝑧) ∈ 𝐶 ↔ ((𝑦(+g‘𝑀)𝑧) ∈ 𝐵 ∧ ∀𝑥 ∈ 𝑆 ((𝑦(+g‘𝑀)𝑧)(+g‘𝑀)𝑥) = (𝑥(+g‘𝑀)(𝑦(+g‘𝑀)𝑧))))) |
43 | 13, 38, 42 | mpbir2and 712 |
. 2
⊢ (((𝑀 ∈ Smgrp ∧ 𝑆 ⊆ 𝐵) ∧ (𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐶)) → (𝑦(+g‘𝑀)𝑧) ∈ 𝐶) |
44 | 43 | ralrimivva 3197 |
1
⊢ ((𝑀 ∈ Smgrp ∧ 𝑆 ⊆ 𝐵) → ∀𝑦 ∈ 𝐶 ∀𝑧 ∈ 𝐶 (𝑦(+g‘𝑀)𝑧) ∈ 𝐶) |