Step |
Hyp |
Ref |
Expression |
1 |
|
ablcom.1 |
⊢ 𝑋 = ran 𝐺 |
2 |
|
simprll |
⊢ ( ( 𝐺 ∈ AbelOp ∧ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ ( 𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ) ) → 𝐴 ∈ 𝑋 ) |
3 |
|
simprlr |
⊢ ( ( 𝐺 ∈ AbelOp ∧ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ ( 𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ) ) → 𝐵 ∈ 𝑋 ) |
4 |
|
simprrl |
⊢ ( ( 𝐺 ∈ AbelOp ∧ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ ( 𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ) ) → 𝐶 ∈ 𝑋 ) |
5 |
2 3 4
|
3jca |
⊢ ( ( 𝐺 ∈ AbelOp ∧ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ ( 𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ) ) → ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) |
6 |
1
|
ablo32 |
⊢ ( ( 𝐺 ∈ AbelOp ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( ( 𝐴 𝐺 𝐵 ) 𝐺 𝐶 ) = ( ( 𝐴 𝐺 𝐶 ) 𝐺 𝐵 ) ) |
7 |
5 6
|
syldan |
⊢ ( ( 𝐺 ∈ AbelOp ∧ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ ( 𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ) ) → ( ( 𝐴 𝐺 𝐵 ) 𝐺 𝐶 ) = ( ( 𝐴 𝐺 𝐶 ) 𝐺 𝐵 ) ) |
8 |
7
|
oveq1d |
⊢ ( ( 𝐺 ∈ AbelOp ∧ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ ( 𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ) ) → ( ( ( 𝐴 𝐺 𝐵 ) 𝐺 𝐶 ) 𝐺 𝐷 ) = ( ( ( 𝐴 𝐺 𝐶 ) 𝐺 𝐵 ) 𝐺 𝐷 ) ) |
9 |
|
ablogrpo |
⊢ ( 𝐺 ∈ AbelOp → 𝐺 ∈ GrpOp ) |
10 |
1
|
grpocl |
⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 𝐺 𝐵 ) ∈ 𝑋 ) |
11 |
10
|
3expb |
⊢ ( ( 𝐺 ∈ GrpOp ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( 𝐴 𝐺 𝐵 ) ∈ 𝑋 ) |
12 |
11
|
adantrr |
⊢ ( ( 𝐺 ∈ GrpOp ∧ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ ( 𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ) ) → ( 𝐴 𝐺 𝐵 ) ∈ 𝑋 ) |
13 |
|
simprrl |
⊢ ( ( 𝐺 ∈ GrpOp ∧ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ ( 𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ) ) → 𝐶 ∈ 𝑋 ) |
14 |
|
simprrr |
⊢ ( ( 𝐺 ∈ GrpOp ∧ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ ( 𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ) ) → 𝐷 ∈ 𝑋 ) |
15 |
12 13 14
|
3jca |
⊢ ( ( 𝐺 ∈ GrpOp ∧ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ ( 𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ) ) → ( ( 𝐴 𝐺 𝐵 ) ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ) |
16 |
1
|
grpoass |
⊢ ( ( 𝐺 ∈ GrpOp ∧ ( ( 𝐴 𝐺 𝐵 ) ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ) → ( ( ( 𝐴 𝐺 𝐵 ) 𝐺 𝐶 ) 𝐺 𝐷 ) = ( ( 𝐴 𝐺 𝐵 ) 𝐺 ( 𝐶 𝐺 𝐷 ) ) ) |
17 |
15 16
|
syldan |
⊢ ( ( 𝐺 ∈ GrpOp ∧ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ ( 𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ) ) → ( ( ( 𝐴 𝐺 𝐵 ) 𝐺 𝐶 ) 𝐺 𝐷 ) = ( ( 𝐴 𝐺 𝐵 ) 𝐺 ( 𝐶 𝐺 𝐷 ) ) ) |
18 |
9 17
|
sylan |
⊢ ( ( 𝐺 ∈ AbelOp ∧ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ ( 𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ) ) → ( ( ( 𝐴 𝐺 𝐵 ) 𝐺 𝐶 ) 𝐺 𝐷 ) = ( ( 𝐴 𝐺 𝐵 ) 𝐺 ( 𝐶 𝐺 𝐷 ) ) ) |
19 |
1
|
grpocl |
⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) → ( 𝐴 𝐺 𝐶 ) ∈ 𝑋 ) |
20 |
19
|
3expb |
⊢ ( ( 𝐺 ∈ GrpOp ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( 𝐴 𝐺 𝐶 ) ∈ 𝑋 ) |
21 |
20
|
adantrlr |
⊢ ( ( 𝐺 ∈ GrpOp ∧ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ 𝐶 ∈ 𝑋 ) ) → ( 𝐴 𝐺 𝐶 ) ∈ 𝑋 ) |
22 |
21
|
adantrrr |
⊢ ( ( 𝐺 ∈ GrpOp ∧ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ ( 𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ) ) → ( 𝐴 𝐺 𝐶 ) ∈ 𝑋 ) |
23 |
|
simprlr |
⊢ ( ( 𝐺 ∈ GrpOp ∧ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ ( 𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ) ) → 𝐵 ∈ 𝑋 ) |
24 |
22 23 14
|
3jca |
⊢ ( ( 𝐺 ∈ GrpOp ∧ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ ( 𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ) ) → ( ( 𝐴 𝐺 𝐶 ) ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ) |
25 |
1
|
grpoass |
⊢ ( ( 𝐺 ∈ GrpOp ∧ ( ( 𝐴 𝐺 𝐶 ) ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ) → ( ( ( 𝐴 𝐺 𝐶 ) 𝐺 𝐵 ) 𝐺 𝐷 ) = ( ( 𝐴 𝐺 𝐶 ) 𝐺 ( 𝐵 𝐺 𝐷 ) ) ) |
26 |
24 25
|
syldan |
⊢ ( ( 𝐺 ∈ GrpOp ∧ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ ( 𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ) ) → ( ( ( 𝐴 𝐺 𝐶 ) 𝐺 𝐵 ) 𝐺 𝐷 ) = ( ( 𝐴 𝐺 𝐶 ) 𝐺 ( 𝐵 𝐺 𝐷 ) ) ) |
27 |
9 26
|
sylan |
⊢ ( ( 𝐺 ∈ AbelOp ∧ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ ( 𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ) ) → ( ( ( 𝐴 𝐺 𝐶 ) 𝐺 𝐵 ) 𝐺 𝐷 ) = ( ( 𝐴 𝐺 𝐶 ) 𝐺 ( 𝐵 𝐺 𝐷 ) ) ) |
28 |
8 18 27
|
3eqtr3d |
⊢ ( ( 𝐺 ∈ AbelOp ∧ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ ( 𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ) ) → ( ( 𝐴 𝐺 𝐵 ) 𝐺 ( 𝐶 𝐺 𝐷 ) ) = ( ( 𝐴 𝐺 𝐶 ) 𝐺 ( 𝐵 𝐺 𝐷 ) ) ) |
29 |
28
|
3impb |
⊢ ( ( 𝐺 ∈ AbelOp ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ ( 𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋 ) ) → ( ( 𝐴 𝐺 𝐵 ) 𝐺 ( 𝐶 𝐺 𝐷 ) ) = ( ( 𝐴 𝐺 𝐶 ) 𝐺 ( 𝐵 𝐺 𝐷 ) ) ) |