Metamath Proof Explorer


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=gAbel|Baseg=
toycom.2 +˙=+K
Assertion toycom KCABA+˙B=B+˙A

Proof

Step Hyp Ref Expression
1 toycom.1 C=gAbel|Baseg=
2 toycom.2 +˙=+K
3 ssrab2 gAbel|Baseg=Abel
4 1 3 eqsstri CAbel
5 4 sseli KCKAbel
6 5 3ad2ant1 KCABKAbel
7 simp2 KCABA
8 fveq2 g=KBaseg=BaseK
9 8 eqeq1d g=KBaseg=BaseK=
10 9 1 elrab2 KCKAbelBaseK=
11 10 simprbi KCBaseK=
12 11 3ad2ant1 KCABBaseK=
13 7 12 eleqtrrd KCABABaseK
14 simp3 KCABB
15 14 12 eleqtrrd KCABBBaseK
16 eqid BaseK=BaseK
17 eqid +K=+K
18 16 17 ablcom KAbelABaseKBBaseKA+KB=B+KA
19 6 13 15 18 syl3anc KCABA+KB=B+KA
20 2 oveqi A+˙B=A+KB
21 2 oveqi B+˙A=B+KA
22 19 20 21 3eqtr4g KCABA+˙B=B+˙A