Theorem toycom

Description: Show the commutative law for an operation O on a toy structure class C of commuatitive operations on CC . This illustrates how a structure class can be partially specialized. In practice, we would ordinarily define a new constant such as "CAbel" in place of C . (Contributed by NM, 17-Mar-2013) (Proof modification is discouraged.)

	Ref	Expression
Hypotheses	toycom.1	|- C = { g e. Abel | ( Base ` g ) = CC }
	toycom.2	|- .+ = ( +g ` K )
Assertion	toycom	|- ( ( K e. C /\ A e. CC /\ B e. CC ) -> ( A .+ B ) = ( B .+ A ) )

Proof

Step	Hyp	Ref	Expression
1		toycom.1	|- C = { g e. Abel | ( Base ` g ) = CC }
2		toycom.2	|- .+ = ( +g ` K )
3		ssrab2	|- { g e. Abel | ( Base ` g ) = CC } C_ Abel
4	1 3	eqsstri	|- C C_ Abel
5	4	sseli	|- ( K e. C -> K e. Abel )
6	5	3ad2ant1	|- ( ( K e. C /\ A e. CC /\ B e. CC ) -> K e. Abel )
7		simp2	|- ( ( K e. C /\ A e. CC /\ B e. CC ) -> A e. CC )
8		fveq2	|- ( g = K -> ( Base ` g ) = ( Base ` K ) )
9	8	eqeq1d	|- ( g = K -> ( ( Base ` g ) = CC <-> ( Base ` K ) = CC ) )
10	9 1	elrab2	|- ( K e. C <-> ( K e. Abel /\ ( Base ` K ) = CC ) )
11	10	simprbi	|- ( K e. C -> ( Base ` K ) = CC )
12	11	3ad2ant1	|- ( ( K e. C /\ A e. CC /\ B e. CC ) -> ( Base ` K ) = CC )
13	7 12	eleqtrrd	|- ( ( K e. C /\ A e. CC /\ B e. CC ) -> A e. ( Base ` K ) )
14		simp3	|- ( ( K e. C /\ A e. CC /\ B e. CC ) -> B e. CC )
15	14 12	eleqtrrd	|- ( ( K e. C /\ A e. CC /\ B e. CC ) -> B e. ( Base ` K ) )
16		eqid	|- ( Base ` K ) = ( Base ` K )
17		eqid	|- ( +g ` K ) = ( +g ` K )
18	16 17	ablcom	|- ( ( K e. Abel /\ A e. ( Base ` K ) /\ B e. ( Base ` K ) ) -> ( A ( +g ` K ) B ) = ( B ( +g ` K ) A ) )
19	6 13 15 18	syl3anc	|- ( ( K e. C /\ A e. CC /\ B e. CC ) -> ( A ( +g ` K ) B ) = ( B ( +g ` K ) A ) )
20	2	oveqi	|- ( A .+ B ) = ( A ( +g ` K ) B )
21	2	oveqi	|- ( B .+ A ) = ( B ( +g ` K ) A )
22	19 20 21	3eqtr4g	|- ( ( K e. C /\ A e. CC /\ B e. CC ) -> ( A .+ B ) = ( B .+ A ) )