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=\left\{g\in \mathrm{Abel}|{\mathrm{Base}}_g=ℂ\right\}$$
	toycom.2	$$⊢\underset{\dot{}}{+}={+}_K$$
Assertion	toycom	$$⊢\left(K\in C\wedge A\in ℂ\wedge B\in ℂ\right)\to A\underset{\dot{}}{+}B=B\underset{\dot{}}{+}A$$

Proof

Step	Hyp	Ref	Expression
1		toycom.1	$$⊢C=\left\{g\in \mathrm{Abel}|{\mathrm{Base}}_g=ℂ\right\}$$
2		toycom.2	$$⊢\underset{\dot{}}{+}={+}_K$$
3		ssrab2	$$⊢\left\{g\in \mathrm{Abel}|{\mathrm{Base}}_g=ℂ\right\}\subseteq \mathrm{Abel}$$
4	1 3	eqsstri	$$⊢C\subseteq \mathrm{Abel}$$
5	4	sseli	$$⊢K\in C\to K\in \mathrm{Abel}$$
6	5	3ad2ant1	$$⊢\left(K\in C\wedge A\in ℂ\wedge B\in ℂ\right)\to K\in \mathrm{Abel}$$
7		simp2	$$⊢\left(K\in C\wedge A\in ℂ\wedge B\in ℂ\right)\to A\in ℂ$$
8		fveq2	$$⊢g=K\to {\mathrm{Base}}_g={\mathrm{Base}}_K$$
9	8	eqeq1d	$$⊢g=K\to \left({\mathrm{Base}}_g=ℂ\leftrightarrow {\mathrm{Base}}_K=ℂ\right)$$
10	9 1	elrab2	$$⊢K\in C\leftrightarrow \left(K\in \mathrm{Abel}\wedge {\mathrm{Base}}_K=ℂ\right)$$
11	10	simprbi	$$⊢K\in C\to {\mathrm{Base}}_K=ℂ$$
12	11	3ad2ant1	$$⊢\left(K\in C\wedge A\in ℂ\wedge B\in ℂ\right)\to {\mathrm{Base}}_K=ℂ$$
13	7 12	eleqtrrd	$$⊢\left(K\in C\wedge A\in ℂ\wedge B\in ℂ\right)\to A\in {\mathrm{Base}}_K$$
14		simp3	$$⊢\left(K\in C\wedge A\in ℂ\wedge B\in ℂ\right)\to B\in ℂ$$
15	14 12	eleqtrrd	$$⊢\left(K\in C\wedge A\in ℂ\wedge B\in ℂ\right)\to B\in {\mathrm{Base}}_K$$
16		eqid	$$⊢{\mathrm{Base}}_K={\mathrm{Base}}_K$$
17		eqid	$$⊢{+}_K={+}_K$$
18	16 17	ablcom	$$⊢\left(K\in \mathrm{Abel}\wedge A\in {\mathrm{Base}}_K\wedge B\in {\mathrm{Base}}_K\right)\to A{+}_{K}B=B{+}_{K}A$$
19	6 13 15 18	syl3anc	$$⊢\left(K\in C\wedge A\in ℂ\wedge B\in ℂ\right)\to A{+}_{K}B=B{+}_{K}A$$
20	2	oveqi	$$⊢A\underset{\dot{}}{+}B=A{+}_{K}B$$
21	2	oveqi	$$⊢B\underset{\dot{}}{+}A=B{+}_{K}A$$
22	19 20 21	3eqtr4g	$$⊢\left(K\in C\wedge A\in ℂ\wedge B\in ℂ\right)\to A\underset{\dot{}}{+}B=B\underset{\dot{}}{+}A$$