Metamath Proof Explorer


Theorem ablo4

Description: Commutative/associative law for Abelian groups. (Contributed by NM, 26-Apr-2007) (New usage is discouraged.)

Ref Expression
Hypothesis ablcom.1 𝑋 = ran 𝐺
Assertion ablo4 ( ( 𝐺 ∈ AbelOp ∧ ( 𝐴𝑋𝐵𝑋 ) ∧ ( 𝐶𝑋𝐷𝑋 ) ) → ( ( 𝐴 𝐺 𝐵 ) 𝐺 ( 𝐶 𝐺 𝐷 ) ) = ( ( 𝐴 𝐺 𝐶 ) 𝐺 ( 𝐵 𝐺 𝐷 ) ) )

Proof

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 ∧ ( 𝐴𝑋𝐵𝑋 ) ∧ ( 𝐶𝑋𝐷𝑋 ) ) → ( ( 𝐴 𝐺 𝐵 ) 𝐺 ( 𝐶 𝐺 𝐷 ) ) = ( ( 𝐴 𝐺 𝐶 ) 𝐺 ( 𝐵 𝐺 𝐷 ) ) )