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	⊢ 𝐶 = { 𝑔 ∈ Abel ∣ ( Base ‘ 𝑔 ) = ℂ }
	toycom.2	⊢ + = ( +g ‘ 𝐾 )
Assertion	toycom	⊢ ( ( 𝐾 ∈ 𝐶 ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐴 + 𝐵 ) = ( 𝐵 + 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		toycom.1	⊢ 𝐶 = { 𝑔 ∈ Abel ∣ ( Base ‘ 𝑔 ) = ℂ }
2		toycom.2	⊢ + = ( +g ‘ 𝐾 )
3		ssrab2	⊢ { 𝑔 ∈ Abel ∣ ( Base ‘ 𝑔 ) = ℂ } ⊆ Abel
4	1 3	eqsstri	⊢ 𝐶 ⊆ Abel
5	4	sseli	⊢ ( 𝐾 ∈ 𝐶 → 𝐾 ∈ Abel )
6	5	3ad2ant1	⊢ ( ( 𝐾 ∈ 𝐶 ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → 𝐾 ∈ Abel )
7		simp2	⊢ ( ( 𝐾 ∈ 𝐶 ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → 𝐴 ∈ ℂ )
8		fveq2	⊢ ( 𝑔 = 𝐾 → ( Base ‘ 𝑔 ) = ( Base ‘ 𝐾 ) )
9	8	eqeq1d	⊢ ( 𝑔 = 𝐾 → ( ( Base ‘ 𝑔 ) = ℂ ↔ ( Base ‘ 𝐾 ) = ℂ ) )
10	9 1	elrab2	⊢ ( 𝐾 ∈ 𝐶 ↔ ( 𝐾 ∈ Abel ∧ ( Base ‘ 𝐾 ) = ℂ ) )
11	10	simprbi	⊢ ( 𝐾 ∈ 𝐶 → ( Base ‘ 𝐾 ) = ℂ )
12	11	3ad2ant1	⊢ ( ( 𝐾 ∈ 𝐶 ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( Base ‘ 𝐾 ) = ℂ )
13	7 12	eleqtrrd	⊢ ( ( 𝐾 ∈ 𝐶 ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → 𝐴 ∈ ( Base ‘ 𝐾 ) )
14		simp3	⊢ ( ( 𝐾 ∈ 𝐶 ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → 𝐵 ∈ ℂ )
15	14 12	eleqtrrd	⊢ ( ( 𝐾 ∈ 𝐶 ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → 𝐵 ∈ ( Base ‘ 𝐾 ) )
16		eqid	⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
17		eqid	⊢ ( +g ‘ 𝐾 ) = ( +g ‘ 𝐾 )
18	16 17	ablcom	⊢ ( ( 𝐾 ∈ Abel ∧ 𝐴 ∈ ( Base ‘ 𝐾 ) ∧ 𝐵 ∈ ( Base ‘ 𝐾 ) ) → ( 𝐴 ( +g ‘ 𝐾 ) 𝐵 ) = ( 𝐵 ( +g ‘ 𝐾 ) 𝐴 ) )
19	6 13 15 18	syl3anc	⊢ ( ( 𝐾 ∈ 𝐶 ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐴 ( +g ‘ 𝐾 ) 𝐵 ) = ( 𝐵 ( +g ‘ 𝐾 ) 𝐴 ) )
20	2	oveqi	⊢ ( 𝐴 + 𝐵 ) = ( 𝐴 ( +g ‘ 𝐾 ) 𝐵 )
21	2	oveqi	⊢ ( 𝐵 + 𝐴 ) = ( 𝐵 ( +g ‘ 𝐾 ) 𝐴 )
22	19 20 21	3eqtr4g	⊢ ( ( 𝐾 ∈ 𝐶 ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐴 + 𝐵 ) = ( 𝐵 + 𝐴 ) )