Theorem ercpbl 13330

Description: Translate the function compatibility relation to a quotient set. (Contributed by Mario Carneiro, 24-Feb-2015.) (Revised by Mario Carneiro, 12-Aug-2015.) (Revised by AV, 12-Jul-2024.)

Hypotheses

Ref	Expression
ercpbl.r	⊢ (𝜑 → ∼ Er 𝑉)
ercpbl.v	⊢ (𝜑 → 𝑉 ∈ 𝑊)
ercpbl.f	⊢ 𝐹 = (𝑥 ∈ 𝑉 ↦ [𝑥] ∼ )
ercpbl.c	⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) → (𝑎 + 𝑏) ∈ 𝑉)
ercpbl.e	⊢ (𝜑 → ((𝐴 ∼ 𝐶 ∧ 𝐵 ∼ 𝐷) → (𝐴 + 𝐵) ∼ (𝐶 + 𝐷)))

Assertion

Ref	Expression
ercpbl	⊢ ((𝜑 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉)) → (((𝐹‘𝐴) = (𝐹‘𝐶) ∧ (𝐹‘𝐵) = (𝐹‘𝐷)) → (𝐹‘(𝐴 + 𝐵)) = (𝐹‘(𝐶 + 𝐷))))

Distinct variable groups:   𝑥, ∼   𝑎,𝑏,𝑥,𝐴   𝐵,𝑏,𝑥   𝑥,𝐶   𝑥,𝐷   𝑉,𝑎,𝑏,𝑥   + ,𝑎,𝑏,𝑥   𝜑,𝑎,𝑏,𝑥

Allowed substitution hints:   𝐵(𝑎)   𝐶(𝑎,𝑏)   𝐷(𝑎,𝑏)   ∼ (𝑎,𝑏)   𝐹(𝑥,𝑎,𝑏)   𝑊(𝑥,𝑎,𝑏)

Proof of Theorem ercpbl

Dummy variables 𝑐 𝑑 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		ercpbl.e	. . 3 ⊢ (𝜑 → ((𝐴 ∼ 𝐶 ∧ 𝐵 ∼ 𝐷) → (𝐴 + 𝐵) ∼ (𝐶 + 𝐷)))
2	1	3ad2ant1 1023	. 2 ⊢ ((𝜑 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉)) → ((𝐴 ∼ 𝐶 ∧ 𝐵 ∼ 𝐷) → (𝐴 + 𝐵) ∼ (𝐶 + 𝐷)))
3		ercpbl.r	. . . . 5 ⊢ (𝜑 → ∼ Er 𝑉)
4	3	3ad2ant1 1023	. . . 4 ⊢ ((𝜑 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉)) → ∼ Er 𝑉)
5		ercpbl.v	. . . . 5 ⊢ (𝜑 → 𝑉 ∈ 𝑊)
6	5	3ad2ant1 1023	. . . 4 ⊢ ((𝜑 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉)) → 𝑉 ∈ 𝑊)
7		ercpbl.f	. . . 4 ⊢ 𝐹 = (𝑥 ∈ 𝑉 ↦ [𝑥] ∼ )
8		simp2l 1028	. . . 4 ⊢ ((𝜑 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉)) → 𝐴 ∈ 𝑉)
9		simp3l 1030	. . . 4 ⊢ ((𝜑 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉)) → 𝐶 ∈ 𝑉)
10	4, 6, 7, 8, 9	ercpbllemg 13329	. . 3 ⊢ ((𝜑 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉)) → ((𝐹‘𝐴) = (𝐹‘𝐶) ↔ 𝐴 ∼ 𝐶))
11		simp2r 1029	. . . 4 ⊢ ((𝜑 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉)) → 𝐵 ∈ 𝑉)
12		simp3r 1031	. . . 4 ⊢ ((𝜑 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉)) → 𝐷 ∈ 𝑉)
13	4, 6, 7, 11, 12	ercpbllemg 13329	. . 3 ⊢ ((𝜑 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉)) → ((𝐹‘𝐵) = (𝐹‘𝐷) ↔ 𝐵 ∼ 𝐷))
14	10, 13	anbi12d 473	. 2 ⊢ ((𝜑 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉)) → (((𝐹‘𝐴) = (𝐹‘𝐶) ∧ (𝐹‘𝐵) = (𝐹‘𝐷)) ↔ (𝐴 ∼ 𝐶 ∧ 𝐵 ∼ 𝐷)))
15		ercpbl.c	. . . . 5 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) → (𝑎 + 𝑏) ∈ 𝑉)
16	15	caovclg 6129	. . . 4 ⊢ ((𝜑 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) → (𝐴 + 𝐵) ∈ 𝑉)
17	16	3adant3 1022	. . 3 ⊢ ((𝜑 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉)) → (𝐴 + 𝐵) ∈ 𝑉)
18		simprl 529	. . . . 5 ⊢ ((𝜑 ∧ (𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉)) → 𝐶 ∈ 𝑉)
19		simprr 531	. . . . 5 ⊢ ((𝜑 ∧ (𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉)) → 𝐷 ∈ 𝑉)
20	15	ralrimivva 2592	. . . . . . 7 ⊢ (𝜑 → ∀𝑎 ∈ 𝑉 ∀𝑏 ∈ 𝑉 (𝑎 + 𝑏) ∈ 𝑉)
21		oveq1 5981	. . . . . . . . 9 ⊢ (𝑎 = 𝑐 → (𝑎 + 𝑏) = (𝑐 + 𝑏))
22	21	eleq1d 2278	. . . . . . . 8 ⊢ (𝑎 = 𝑐 → ((𝑎 + 𝑏) ∈ 𝑉 ↔ (𝑐 + 𝑏) ∈ 𝑉))
23		oveq2 5982	. . . . . . . . 9 ⊢ (𝑏 = 𝑑 → (𝑐 + 𝑏) = (𝑐 + 𝑑))
24	23	eleq1d 2278	. . . . . . . 8 ⊢ (𝑏 = 𝑑 → ((𝑐 + 𝑏) ∈ 𝑉 ↔ (𝑐 + 𝑑) ∈ 𝑉))
25	22, 24	cbvral2v 2758	. . . . . . 7 ⊢ (∀𝑎 ∈ 𝑉 ∀𝑏 ∈ 𝑉 (𝑎 + 𝑏) ∈ 𝑉 ↔ ∀𝑐 ∈ 𝑉 ∀𝑑 ∈ 𝑉 (𝑐 + 𝑑) ∈ 𝑉)
26	20, 25	sylib 122	. . . . . 6 ⊢ (𝜑 → ∀𝑐 ∈ 𝑉 ∀𝑑 ∈ 𝑉 (𝑐 + 𝑑) ∈ 𝑉)
27	26	adantr 276	. . . . 5 ⊢ ((𝜑 ∧ (𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉)) → ∀𝑐 ∈ 𝑉 ∀𝑑 ∈ 𝑉 (𝑐 + 𝑑) ∈ 𝑉)
28		ovrspc2v 6000	. . . . 5 ⊢ (((𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉) ∧ ∀𝑐 ∈ 𝑉 ∀𝑑 ∈ 𝑉 (𝑐 + 𝑑) ∈ 𝑉) → (𝐶 + 𝐷) ∈ 𝑉)
29	18, 19, 27, 28	syl21anc 1251	. . . 4 ⊢ ((𝜑 ∧ (𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉)) → (𝐶 + 𝐷) ∈ 𝑉)
30	29	3adant2 1021	. . 3 ⊢ ((𝜑 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉)) → (𝐶 + 𝐷) ∈ 𝑉)
31	4, 6, 7, 17, 30	ercpbllemg 13329	. 2 ⊢ ((𝜑 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉)) → ((𝐹‘(𝐴 + 𝐵)) = (𝐹‘(𝐶 + 𝐷)) ↔ (𝐴 + 𝐵) ∼ (𝐶 + 𝐷)))
32	2, 14, 31	3imtr4d 203	1 ⊢ ((𝜑 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉)) → (((𝐹‘𝐴) = (𝐹‘𝐶) ∧ (𝐹‘𝐵) = (𝐹‘𝐷)) → (𝐹‘(𝐴 + 𝐵)) = (𝐹‘(𝐶 + 𝐷))))

Syntax hints:   → wi 4   ∧ wa 104   ∧ w3a 983   = wceq 1375   ∈ wcel 2180  ∀wral 2488   class class class wbr 4062   ↦ cmpt 4124  ‘cfv 5294  (class class class)co 5974   Er wer 6647  [cec 6648

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 713  ax-5 1473  ax-7 1474  ax-gen 1475  ax-ie1 1519  ax-ie2 1520  ax-8 1530  ax-10 1531  ax-11 1532  ax-i12 1533  ax-bndl 1535  ax-4 1536  ax-17 1552  ax-i9 1556  ax-ial 1560  ax-i5r 1561  ax-14 2183  ax-ext 2191  ax-sep 4181  ax-pow 4237  ax-pr 4272

This theorem depends on definitions:  df-bi 117  df-3an 985  df-tru 1378  df-nf 1487  df-sb 1789  df-eu 2060  df-mo 2061  df-clab 2196  df-cleq 2202  df-clel 2205  df-nfc 2341  df-ral 2493  df-rex 2494  df-v 2781  df-sbc 3009  df-csb 3105  df-un 3181  df-in 3183  df-ss 3190  df-pw 3631  df-sn 3652  df-pr 3653  df-op 3655  df-uni 3868  df-br 4063  df-opab 4125  df-mpt 4126  df-id 4361  df-xp 4702  df-rel 4703  df-cnv 4704  df-co 4705  df-dm 4706  df-rn 4707  df-res 4708  df-ima 4709  df-iota 5254  df-fun 5296  df-fv 5302  df-ov 5977  df-er 6650  df-ec 6652

This theorem is referenced by:  qusaddvallemg  13332  qusaddflemg  13333  qusgrp2  13616  qusrng  13887  qusring2  13995