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 ) ) )

Metamath Proof Explorer

Theorem symggrplem

Proof