Metamath Proof Explorer

Theorem symggrplem

Description: Lemma for symggrp and efmndsgrp . Conditions for an operation to be associative. Formerly part of proof for symggrp . (Contributed by AV, 28-Jan-2024)

Ref Expression
Hypotheses symggrplem.c 
|- ( ( x e. B /\ y e. B ) -> ( x .+ y ) e. B )
symggrplem.p 
|- ( ( x e. B /\ y e. B ) -> ( x .+ y ) = ( x o. y ) )
Assertion symggrplem 
|- ( ( X e. B /\ Y e. B /\ Z e. B ) -> ( ( X .+ Y ) .+ Z ) = ( X .+ ( Y .+ Z ) ) )

Proof

Step Hyp Ref Expression
1 symggrplem.c 
 |-  ( ( x e. B /\ y e. B ) -> ( x .+ y ) e. B )
2 symggrplem.p 
 |-  ( ( x e. B /\ y e. B ) -> ( x .+ y ) = ( x o. y ) )
3 coass 
 |-  ( ( X o. Y ) o. Z ) = ( X o. ( Y o. Z ) )
4 oveq1 
 |-  ( x = X -> ( x .+ y ) = ( X .+ y ) )
5 4 eleq1d 
 |-  ( x = X -> ( ( x .+ y ) e. B <-> ( X .+ y ) e. B ) )
6 oveq2 
 |-  ( y = Y -> ( X .+ y ) = ( X .+ Y ) )
7 6 eleq1d 
 |-  ( y = Y -> ( ( X .+ y ) e. B <-> ( X .+ Y ) e. B ) )
8 5 7 1 vtocl2ga 
 |-  ( ( X e. B /\ Y e. B ) -> ( X .+ Y ) e. B )
9 oveq1 
 |-  ( x = ( X .+ Y ) -> ( x .+ y ) = ( ( X .+ Y ) .+ y ) )
10 coeq1 
 |-  ( x = ( X .+ Y ) -> ( x o. y ) = ( ( X .+ Y ) o. y ) )
11 9 10 eqeq12d 
 |-  ( x = ( X .+ Y ) -> ( ( x .+ y ) = ( x o. y ) <-> ( ( X .+ Y ) .+ y ) = ( ( X .+ Y ) o. y ) ) )
12 oveq2 
 |-  ( y = Z -> ( ( X .+ Y ) .+ y ) = ( ( X .+ Y ) .+ Z ) )
13 coeq2 
 |-  ( y = Z -> ( ( X .+ Y ) o. y ) = ( ( X .+ Y ) o. Z ) )
14 12 13 eqeq12d 
 |-  ( y = Z -> ( ( ( X .+ Y ) .+ y ) = ( ( X .+ Y ) o. y ) <-> ( ( X .+ Y ) .+ Z ) = ( ( X .+ Y ) o. Z ) ) )
15 11 14 2 vtocl2ga 
 |-  ( ( ( X .+ Y ) e. B /\ Z e. B ) -> ( ( X .+ Y ) .+ Z ) = ( ( X .+ Y ) o. Z ) )
16 8 15 stoic3 
 |-  ( ( X e. B /\ Y e. B /\ Z e. B ) -> ( ( X .+ Y ) .+ Z ) = ( ( X .+ Y ) o. Z ) )
17 coeq1 
 |-  ( x = X -> ( x o. y ) = ( X o. y ) )
18 4 17 eqeq12d 
 |-  ( x = X -> ( ( x .+ y ) = ( x o. y ) <-> ( X .+ y ) = ( X o. y ) ) )
19 coeq2 
 |-  ( y = Y -> ( X o. y ) = ( X o. Y ) )
20 6 19 eqeq12d 
 |-  ( y = Y -> ( ( X .+ y ) = ( X o. y ) <-> ( X .+ Y ) = ( X o. Y ) ) )
21 18 20 2 vtocl2ga 
 |-  ( ( X e. B /\ Y e. B ) -> ( X .+ Y ) = ( X o. Y ) )
22 21 3adant3 
 |-  ( ( X e. B /\ Y e. B /\ Z e. B ) -> ( X .+ Y ) = ( X o. Y ) )
23 22 coeq1d 
 |-  ( ( X e. B /\ Y e. B /\ Z e. B ) -> ( ( X .+ Y ) o. Z ) = ( ( X o. Y ) o. Z ) )
24 16 23 eqtrd 
 |-  ( ( X e. B /\ Y e. B /\ Z e. B ) -> ( ( X .+ Y ) .+ Z ) = ( ( X o. Y ) o. Z ) )
25 simp1 
 |-  ( ( X e. B /\ Y e. B /\ Z e. B ) -> X e. B )
26 oveq1 
 |-  ( x = Y -> ( x .+ y ) = ( Y .+ y ) )
27 26 eleq1d 
 |-  ( x = Y -> ( ( x .+ y ) e. B <-> ( Y .+ y ) e. B ) )
28 oveq2 
 |-  ( y = Z -> ( Y .+ y ) = ( Y .+ Z ) )
29 28 eleq1d 
 |-  ( y = Z -> ( ( Y .+ y ) e. B <-> ( Y .+ Z ) e. B ) )
30 27 29 1 vtocl2ga 
 |-  ( ( Y e. B /\ Z e. B ) -> ( Y .+ Z ) e. B )
31 30 3adant1 
 |-  ( ( X e. B /\ Y e. B /\ Z e. B ) -> ( Y .+ Z ) e. B )
32 oveq2 
 |-  ( y = ( Y .+ Z ) -> ( X .+ y ) = ( X .+ ( Y .+ Z ) ) )
33 coeq2 
 |-  ( y = ( Y .+ Z ) -> ( X o. y ) = ( X o. ( Y .+ Z ) ) )
34 32 33 eqeq12d 
 |-  ( y = ( Y .+ Z ) -> ( ( X .+ y ) = ( X o. y ) <-> ( X .+ ( Y .+ Z ) ) = ( X o. ( Y .+ Z ) ) ) )
35 18 34 2 vtocl2ga 
 |-  ( ( X e. B /\ ( Y .+ Z ) e. B ) -> ( X .+ ( Y .+ Z ) ) = ( X o. ( Y .+ Z ) ) )
36 25 31 35 syl2anc 
 |-  ( ( X e. B /\ Y e. B /\ Z e. B ) -> ( X .+ ( Y .+ Z ) ) = ( X o. ( Y .+ Z ) ) )
37 coeq1 
 |-  ( x = Y -> ( x o. y ) = ( Y o. y ) )
38 26 37 eqeq12d 
 |-  ( x = Y -> ( ( x .+ y ) = ( x o. y ) <-> ( Y .+ y ) = ( Y o. y ) ) )
39 coeq2 
 |-  ( y = Z -> ( Y o. y ) = ( Y o. Z ) )
40 28 39 eqeq12d 
 |-  ( y = Z -> ( ( Y .+ y ) = ( Y o. y ) <-> ( Y .+ Z ) = ( Y o. Z ) ) )
41 38 40 2 vtocl2ga 
 |-  ( ( Y e. B /\ Z e. B ) -> ( Y .+ Z ) = ( Y o. Z ) )
42 41 3adant1 
 |-  ( ( X e. B /\ Y e. B /\ Z e. B ) -> ( Y .+ Z ) = ( Y o. Z ) )
43 42 coeq2d 
 |-  ( ( X e. B /\ Y e. B /\ Z e. B ) -> ( X o. ( Y .+ Z ) ) = ( X o. ( Y o. Z ) ) )
44 36 43 eqtrd 
 |-  ( ( X e. B /\ Y e. B /\ Z e. B ) -> ( X .+ ( Y .+ Z ) ) = ( X o. ( Y o. Z ) ) )
45 3 24 44 3eqtr4a 
 |-  ( ( X e. B /\ Y e. B /\ Z e. B ) -> ( ( X .+ Y ) .+ Z ) = ( X .+ ( Y .+ Z ) ) )