Step |
Hyp |
Ref |
Expression |
1 |
|
cntzsgrpcl.b |
⊢ 𝐵 = ( Base ‘ 𝑀 ) |
2 |
|
cntzsgrpcl.z |
⊢ 𝑍 = ( Cntz ‘ 𝑀 ) |
3 |
|
cntzsgrpcl.c |
⊢ 𝐶 = ( 𝑍 ‘ 𝑆 ) |
4 |
|
simpll |
⊢ ( ( ( 𝑀 ∈ Smgrp ∧ 𝑆 ⊆ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐶 ) ) → 𝑀 ∈ Smgrp ) |
5 |
1 2
|
cntzssv |
⊢ ( 𝑍 ‘ 𝑆 ) ⊆ 𝐵 |
6 |
3 5
|
eqsstri |
⊢ 𝐶 ⊆ 𝐵 |
7 |
|
simprl |
⊢ ( ( ( 𝑀 ∈ Smgrp ∧ 𝑆 ⊆ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐶 ) ) → 𝑦 ∈ 𝐶 ) |
8 |
6 7
|
sselid |
⊢ ( ( ( 𝑀 ∈ Smgrp ∧ 𝑆 ⊆ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐶 ) ) → 𝑦 ∈ 𝐵 ) |
9 |
|
simprr |
⊢ ( ( ( 𝑀 ∈ Smgrp ∧ 𝑆 ⊆ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐶 ) ) → 𝑧 ∈ 𝐶 ) |
10 |
6 9
|
sselid |
⊢ ( ( ( 𝑀 ∈ Smgrp ∧ 𝑆 ⊆ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐶 ) ) → 𝑧 ∈ 𝐵 ) |
11 |
|
eqid |
⊢ ( +g ‘ 𝑀 ) = ( +g ‘ 𝑀 ) |
12 |
1 11
|
sgrpcl |
⊢ ( ( 𝑀 ∈ Smgrp ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) → ( 𝑦 ( +g ‘ 𝑀 ) 𝑧 ) ∈ 𝐵 ) |
13 |
4 8 10 12
|
syl3anc |
⊢ ( ( ( 𝑀 ∈ Smgrp ∧ 𝑆 ⊆ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐶 ) ) → ( 𝑦 ( +g ‘ 𝑀 ) 𝑧 ) ∈ 𝐵 ) |
14 |
4
|
adantr |
⊢ ( ( ( ( 𝑀 ∈ Smgrp ∧ 𝑆 ⊆ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐶 ) ) ∧ 𝑥 ∈ 𝑆 ) → 𝑀 ∈ Smgrp ) |
15 |
8
|
adantr |
⊢ ( ( ( ( 𝑀 ∈ Smgrp ∧ 𝑆 ⊆ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐶 ) ) ∧ 𝑥 ∈ 𝑆 ) → 𝑦 ∈ 𝐵 ) |
16 |
10
|
adantr |
⊢ ( ( ( ( 𝑀 ∈ Smgrp ∧ 𝑆 ⊆ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐶 ) ) ∧ 𝑥 ∈ 𝑆 ) → 𝑧 ∈ 𝐵 ) |
17 |
|
simpr |
⊢ ( ( 𝑀 ∈ Smgrp ∧ 𝑆 ⊆ 𝐵 ) → 𝑆 ⊆ 𝐵 ) |
18 |
17
|
sselda |
⊢ ( ( ( 𝑀 ∈ Smgrp ∧ 𝑆 ⊆ 𝐵 ) ∧ 𝑥 ∈ 𝑆 ) → 𝑥 ∈ 𝐵 ) |
19 |
18
|
adantlr |
⊢ ( ( ( ( 𝑀 ∈ Smgrp ∧ 𝑆 ⊆ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐶 ) ) ∧ 𝑥 ∈ 𝑆 ) → 𝑥 ∈ 𝐵 ) |
20 |
1 11
|
sgrpass |
⊢ ( ( 𝑀 ∈ Smgrp ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵 ) ) → ( ( 𝑦 ( +g ‘ 𝑀 ) 𝑧 ) ( +g ‘ 𝑀 ) 𝑥 ) = ( 𝑦 ( +g ‘ 𝑀 ) ( 𝑧 ( +g ‘ 𝑀 ) 𝑥 ) ) ) |
21 |
14 15 16 19 20
|
syl13anc |
⊢ ( ( ( ( 𝑀 ∈ Smgrp ∧ 𝑆 ⊆ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐶 ) ) ∧ 𝑥 ∈ 𝑆 ) → ( ( 𝑦 ( +g ‘ 𝑀 ) 𝑧 ) ( +g ‘ 𝑀 ) 𝑥 ) = ( 𝑦 ( +g ‘ 𝑀 ) ( 𝑧 ( +g ‘ 𝑀 ) 𝑥 ) ) ) |
22 |
3
|
eleq2i |
⊢ ( 𝑧 ∈ 𝐶 ↔ 𝑧 ∈ ( 𝑍 ‘ 𝑆 ) ) |
23 |
11 2
|
cntzi |
⊢ ( ( 𝑧 ∈ ( 𝑍 ‘ 𝑆 ) ∧ 𝑥 ∈ 𝑆 ) → ( 𝑧 ( +g ‘ 𝑀 ) 𝑥 ) = ( 𝑥 ( +g ‘ 𝑀 ) 𝑧 ) ) |
24 |
22 23
|
sylanb |
⊢ ( ( 𝑧 ∈ 𝐶 ∧ 𝑥 ∈ 𝑆 ) → ( 𝑧 ( +g ‘ 𝑀 ) 𝑥 ) = ( 𝑥 ( +g ‘ 𝑀 ) 𝑧 ) ) |
25 |
9 24
|
sylan |
⊢ ( ( ( ( 𝑀 ∈ Smgrp ∧ 𝑆 ⊆ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐶 ) ) ∧ 𝑥 ∈ 𝑆 ) → ( 𝑧 ( +g ‘ 𝑀 ) 𝑥 ) = ( 𝑥 ( +g ‘ 𝑀 ) 𝑧 ) ) |
26 |
25
|
oveq2d |
⊢ ( ( ( ( 𝑀 ∈ Smgrp ∧ 𝑆 ⊆ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐶 ) ) ∧ 𝑥 ∈ 𝑆 ) → ( 𝑦 ( +g ‘ 𝑀 ) ( 𝑧 ( +g ‘ 𝑀 ) 𝑥 ) ) = ( 𝑦 ( +g ‘ 𝑀 ) ( 𝑥 ( +g ‘ 𝑀 ) 𝑧 ) ) ) |
27 |
1 11
|
sgrpass |
⊢ ( ( 𝑀 ∈ Smgrp ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) → ( ( 𝑦 ( +g ‘ 𝑀 ) 𝑥 ) ( +g ‘ 𝑀 ) 𝑧 ) = ( 𝑦 ( +g ‘ 𝑀 ) ( 𝑥 ( +g ‘ 𝑀 ) 𝑧 ) ) ) |
28 |
14 15 19 16 27
|
syl13anc |
⊢ ( ( ( ( 𝑀 ∈ Smgrp ∧ 𝑆 ⊆ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐶 ) ) ∧ 𝑥 ∈ 𝑆 ) → ( ( 𝑦 ( +g ‘ 𝑀 ) 𝑥 ) ( +g ‘ 𝑀 ) 𝑧 ) = ( 𝑦 ( +g ‘ 𝑀 ) ( 𝑥 ( +g ‘ 𝑀 ) 𝑧 ) ) ) |
29 |
3
|
eleq2i |
⊢ ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ ( 𝑍 ‘ 𝑆 ) ) |
30 |
11 2
|
cntzi |
⊢ ( ( 𝑦 ∈ ( 𝑍 ‘ 𝑆 ) ∧ 𝑥 ∈ 𝑆 ) → ( 𝑦 ( +g ‘ 𝑀 ) 𝑥 ) = ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) ) |
31 |
29 30
|
sylanb |
⊢ ( ( 𝑦 ∈ 𝐶 ∧ 𝑥 ∈ 𝑆 ) → ( 𝑦 ( +g ‘ 𝑀 ) 𝑥 ) = ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) ) |
32 |
7 31
|
sylan |
⊢ ( ( ( ( 𝑀 ∈ Smgrp ∧ 𝑆 ⊆ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐶 ) ) ∧ 𝑥 ∈ 𝑆 ) → ( 𝑦 ( +g ‘ 𝑀 ) 𝑥 ) = ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) ) |
33 |
32
|
oveq1d |
⊢ ( ( ( ( 𝑀 ∈ Smgrp ∧ 𝑆 ⊆ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐶 ) ) ∧ 𝑥 ∈ 𝑆 ) → ( ( 𝑦 ( +g ‘ 𝑀 ) 𝑥 ) ( +g ‘ 𝑀 ) 𝑧 ) = ( ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) ( +g ‘ 𝑀 ) 𝑧 ) ) |
34 |
26 28 33
|
3eqtr2d |
⊢ ( ( ( ( 𝑀 ∈ Smgrp ∧ 𝑆 ⊆ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐶 ) ) ∧ 𝑥 ∈ 𝑆 ) → ( 𝑦 ( +g ‘ 𝑀 ) ( 𝑧 ( +g ‘ 𝑀 ) 𝑥 ) ) = ( ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) ( +g ‘ 𝑀 ) 𝑧 ) ) |
35 |
1 11
|
sgrpass |
⊢ ( ( 𝑀 ∈ Smgrp ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) → ( ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) ( +g ‘ 𝑀 ) 𝑧 ) = ( 𝑥 ( +g ‘ 𝑀 ) ( 𝑦 ( +g ‘ 𝑀 ) 𝑧 ) ) ) |
36 |
14 19 15 16 35
|
syl13anc |
⊢ ( ( ( ( 𝑀 ∈ Smgrp ∧ 𝑆 ⊆ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐶 ) ) ∧ 𝑥 ∈ 𝑆 ) → ( ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) ( +g ‘ 𝑀 ) 𝑧 ) = ( 𝑥 ( +g ‘ 𝑀 ) ( 𝑦 ( +g ‘ 𝑀 ) 𝑧 ) ) ) |
37 |
21 34 36
|
3eqtrd |
⊢ ( ( ( ( 𝑀 ∈ Smgrp ∧ 𝑆 ⊆ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐶 ) ) ∧ 𝑥 ∈ 𝑆 ) → ( ( 𝑦 ( +g ‘ 𝑀 ) 𝑧 ) ( +g ‘ 𝑀 ) 𝑥 ) = ( 𝑥 ( +g ‘ 𝑀 ) ( 𝑦 ( +g ‘ 𝑀 ) 𝑧 ) ) ) |
38 |
37
|
ralrimiva |
⊢ ( ( ( 𝑀 ∈ Smgrp ∧ 𝑆 ⊆ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐶 ) ) → ∀ 𝑥 ∈ 𝑆 ( ( 𝑦 ( +g ‘ 𝑀 ) 𝑧 ) ( +g ‘ 𝑀 ) 𝑥 ) = ( 𝑥 ( +g ‘ 𝑀 ) ( 𝑦 ( +g ‘ 𝑀 ) 𝑧 ) ) ) |
39 |
3
|
eleq2i |
⊢ ( ( 𝑦 ( +g ‘ 𝑀 ) 𝑧 ) ∈ 𝐶 ↔ ( 𝑦 ( +g ‘ 𝑀 ) 𝑧 ) ∈ ( 𝑍 ‘ 𝑆 ) ) |
40 |
1 11 2
|
elcntz |
⊢ ( 𝑆 ⊆ 𝐵 → ( ( 𝑦 ( +g ‘ 𝑀 ) 𝑧 ) ∈ ( 𝑍 ‘ 𝑆 ) ↔ ( ( 𝑦 ( +g ‘ 𝑀 ) 𝑧 ) ∈ 𝐵 ∧ ∀ 𝑥 ∈ 𝑆 ( ( 𝑦 ( +g ‘ 𝑀 ) 𝑧 ) ( +g ‘ 𝑀 ) 𝑥 ) = ( 𝑥 ( +g ‘ 𝑀 ) ( 𝑦 ( +g ‘ 𝑀 ) 𝑧 ) ) ) ) ) |
41 |
39 40
|
bitrid |
⊢ ( 𝑆 ⊆ 𝐵 → ( ( 𝑦 ( +g ‘ 𝑀 ) 𝑧 ) ∈ 𝐶 ↔ ( ( 𝑦 ( +g ‘ 𝑀 ) 𝑧 ) ∈ 𝐵 ∧ ∀ 𝑥 ∈ 𝑆 ( ( 𝑦 ( +g ‘ 𝑀 ) 𝑧 ) ( +g ‘ 𝑀 ) 𝑥 ) = ( 𝑥 ( +g ‘ 𝑀 ) ( 𝑦 ( +g ‘ 𝑀 ) 𝑧 ) ) ) ) ) |
42 |
41
|
ad2antlr |
⊢ ( ( ( 𝑀 ∈ Smgrp ∧ 𝑆 ⊆ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐶 ) ) → ( ( 𝑦 ( +g ‘ 𝑀 ) 𝑧 ) ∈ 𝐶 ↔ ( ( 𝑦 ( +g ‘ 𝑀 ) 𝑧 ) ∈ 𝐵 ∧ ∀ 𝑥 ∈ 𝑆 ( ( 𝑦 ( +g ‘ 𝑀 ) 𝑧 ) ( +g ‘ 𝑀 ) 𝑥 ) = ( 𝑥 ( +g ‘ 𝑀 ) ( 𝑦 ( +g ‘ 𝑀 ) 𝑧 ) ) ) ) ) |
43 |
13 38 42
|
mpbir2and |
⊢ ( ( ( 𝑀 ∈ Smgrp ∧ 𝑆 ⊆ 𝐵 ) ∧ ( 𝑦 ∈ 𝐶 ∧ 𝑧 ∈ 𝐶 ) ) → ( 𝑦 ( +g ‘ 𝑀 ) 𝑧 ) ∈ 𝐶 ) |
44 |
43
|
ralrimivva |
⊢ ( ( 𝑀 ∈ Smgrp ∧ 𝑆 ⊆ 𝐵 ) → ∀ 𝑦 ∈ 𝐶 ∀ 𝑧 ∈ 𝐶 ( 𝑦 ( +g ‘ 𝑀 ) 𝑧 ) ∈ 𝐶 ) |