This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem erov

Description: The value of an operation defined on equivalence classes. (Contributed by Jeff Madsen, 10-Jun-2010) (Revised by Mario Carneiro, 30-Dec-2014)

Ref Expression
Hypotheses eropr.1 ⊢ 𝐽 = ( 𝐴 / 𝑅 )
eropr.2 ⊢ 𝐾 = ( 𝐵 / 𝑆 )
eropr.3 ⊢ ( 𝜑 → 𝑇 ∈ 𝑍 )
eropr.4 ⊢ ( 𝜑 → 𝑅 Er 𝑈 )
eropr.5 ⊢ ( 𝜑 → 𝑆 Er 𝑉 )
eropr.6 ⊢ ( 𝜑 → 𝑇 Er 𝑊 )
eropr.7 ⊢ ( 𝜑 → 𝐴 ⊆ 𝑈 )
eropr.8 ⊢ ( 𝜑 → 𝐵 ⊆ 𝑉 )
eropr.9 ⊢ ( 𝜑 → 𝐶 ⊆ 𝑊 )
eropr.10 ⊢ ( 𝜑 → + : ( 𝐴 × 𝐵 ) ⟶ 𝐶 )
eropr.11 ⊢ ( ( 𝜑 ∧ ( ( 𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴 ) ∧ ( 𝑡 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ) ) ) → ( ( 𝑟 𝑅 𝑠 ∧ 𝑡 𝑆 𝑢 ) → ( 𝑟 + 𝑡 ) 𝑇 ( 𝑠 + 𝑢 ) ) )
eropr.12 ⊢ ⨣ = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐵 ( ( 𝑥 = [ 𝑝 ] 𝑅 ∧ 𝑦 = [ 𝑞 ] 𝑆 ) ∧ 𝑧 = [ ( 𝑝 + 𝑞 ) ] 𝑇 ) }
eropr.13 ⊢ ( 𝜑 → 𝑅 ∈ 𝑋 )
eropr.14 ⊢ ( 𝜑 → 𝑆 ∈ 𝑌 )
Assertion erov ( ( 𝜑 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐵 ) → ( [ 𝑃 ] 𝑅 ⨣ [ 𝑄 ] 𝑆 ) = [ ( 𝑃 + 𝑄 ) ] 𝑇 )

Proof

Step Hyp Ref Expression
1 eropr.1 ⊢ 𝐽 = ( 𝐴 / 𝑅 )
2 eropr.2 ⊢ 𝐾 = ( 𝐵 / 𝑆 )
3 eropr.3 ⊢ ( 𝜑 → 𝑇 ∈ 𝑍 )
4 eropr.4 ⊢ ( 𝜑 → 𝑅 Er 𝑈 )
5 eropr.5 ⊢ ( 𝜑 → 𝑆 Er 𝑉 )
6 eropr.6 ⊢ ( 𝜑 → 𝑇 Er 𝑊 )
7 eropr.7 ⊢ ( 𝜑 → 𝐴 ⊆ 𝑈 )
8 eropr.8 ⊢ ( 𝜑 → 𝐵 ⊆ 𝑉 )
9 eropr.9 ⊢ ( 𝜑 → 𝐶 ⊆ 𝑊 )
10 eropr.10 ⊢ ( 𝜑 → + : ( 𝐴 × 𝐵 ) ⟶ 𝐶 )
11 eropr.11 ⊢ ( ( 𝜑 ∧ ( ( 𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴 ) ∧ ( 𝑡 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ) ) ) → ( ( 𝑟 𝑅 𝑠 ∧ 𝑡 𝑆 𝑢 ) → ( 𝑟 + 𝑡 ) 𝑇 ( 𝑠 + 𝑢 ) ) )
12 eropr.12 ⊢ ⨣ = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐵 ( ( 𝑥 = [ 𝑝 ] 𝑅 ∧ 𝑦 = [ 𝑞 ] 𝑆 ) ∧ 𝑧 = [ ( 𝑝 + 𝑞 ) ] 𝑇 ) }
13 eropr.13 ⊢ ( 𝜑 → 𝑅 ∈ 𝑋 )
14 eropr.14 ⊢ ( 𝜑 → 𝑆 ∈ 𝑌 )
15 1 2 3 4 5 6 7 8 9 10 11 12 erovlem ⊢ ( 𝜑 → ⨣ = ( 𝑥 ∈ 𝐽 , 𝑦 ∈ 𝐾 ↦ ( ℩ 𝑧 ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐵 ( ( 𝑥 = [ 𝑝 ] 𝑅 ∧ 𝑦 = [ 𝑞 ] 𝑆 ) ∧ 𝑧 = [ ( 𝑝 + 𝑞 ) ] 𝑇 ) ) ) )
16 15 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐵 ) → ⨣ = ( 𝑥 ∈ 𝐽 , 𝑦 ∈ 𝐾 ↦ ( ℩ 𝑧 ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐵 ( ( 𝑥 = [ 𝑝 ] 𝑅 ∧ 𝑦 = [ 𝑞 ] 𝑆 ) ∧ 𝑧 = [ ( 𝑝 + 𝑞 ) ] 𝑇 ) ) ) )
17 simprl ⊢ ( ( ( 𝜑 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐵 ) ∧ ( 𝑥 = [ 𝑃 ] 𝑅 ∧ 𝑦 = [ 𝑄 ] 𝑆 ) ) → 𝑥 = [ 𝑃 ] 𝑅 )
18 17 eqeq1d ⊢ ( ( ( 𝜑 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐵 ) ∧ ( 𝑥 = [ 𝑃 ] 𝑅 ∧ 𝑦 = [ 𝑄 ] 𝑆 ) ) → ( 𝑥 = [ 𝑝 ] 𝑅 ↔ [ 𝑃 ] 𝑅 = [ 𝑝 ] 𝑅 ) )
19 simprr ⊢ ( ( ( 𝜑 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐵 ) ∧ ( 𝑥 = [ 𝑃 ] 𝑅 ∧ 𝑦 = [ 𝑄 ] 𝑆 ) ) → 𝑦 = [ 𝑄 ] 𝑆 )
20 19 eqeq1d ⊢ ( ( ( 𝜑 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐵 ) ∧ ( 𝑥 = [ 𝑃 ] 𝑅 ∧ 𝑦 = [ 𝑄 ] 𝑆 ) ) → ( 𝑦 = [ 𝑞 ] 𝑆 ↔ [ 𝑄 ] 𝑆 = [ 𝑞 ] 𝑆 ) )
21 18 20 anbi12d ⊢ ( ( ( 𝜑 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐵 ) ∧ ( 𝑥 = [ 𝑃 ] 𝑅 ∧ 𝑦 = [ 𝑄 ] 𝑆 ) ) → ( ( 𝑥 = [ 𝑝 ] 𝑅 ∧ 𝑦 = [ 𝑞 ] 𝑆 ) ↔ ( [ 𝑃 ] 𝑅 = [ 𝑝 ] 𝑅 ∧ [ 𝑄 ] 𝑆 = [ 𝑞 ] 𝑆 ) ) )
22 21 anbi1d ⊢ ( ( ( 𝜑 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐵 ) ∧ ( 𝑥 = [ 𝑃 ] 𝑅 ∧ 𝑦 = [ 𝑄 ] 𝑆 ) ) → ( ( ( 𝑥 = [ 𝑝 ] 𝑅 ∧ 𝑦 = [ 𝑞 ] 𝑆 ) ∧ 𝑧 = [ ( 𝑝 + 𝑞 ) ] 𝑇 ) ↔ ( ( [ 𝑃 ] 𝑅 = [ 𝑝 ] 𝑅 ∧ [ 𝑄 ] 𝑆 = [ 𝑞 ] 𝑆 ) ∧ 𝑧 = [ ( 𝑝 + 𝑞 ) ] 𝑇 ) ) )
23 22 2rexbidv ⊢ ( ( ( 𝜑 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐵 ) ∧ ( 𝑥 = [ 𝑃 ] 𝑅 ∧ 𝑦 = [ 𝑄 ] 𝑆 ) ) → ( ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐵 ( ( 𝑥 = [ 𝑝 ] 𝑅 ∧ 𝑦 = [ 𝑞 ] 𝑆 ) ∧ 𝑧 = [ ( 𝑝 + 𝑞 ) ] 𝑇 ) ↔ ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐵 ( ( [ 𝑃 ] 𝑅 = [ 𝑝 ] 𝑅 ∧ [ 𝑄 ] 𝑆 = [ 𝑞 ] 𝑆 ) ∧ 𝑧 = [ ( 𝑝 + 𝑞 ) ] 𝑇 ) ) )
24 23 iotabidv ⊢ ( ( ( 𝜑 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐵 ) ∧ ( 𝑥 = [ 𝑃 ] 𝑅 ∧ 𝑦 = [ 𝑄 ] 𝑆 ) ) → ( ℩ 𝑧 ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐵 ( ( 𝑥 = [ 𝑝 ] 𝑅 ∧ 𝑦 = [ 𝑞 ] 𝑆 ) ∧ 𝑧 = [ ( 𝑝 + 𝑞 ) ] 𝑇 ) ) = ( ℩ 𝑧 ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐵 ( ( [ 𝑃 ] 𝑅 = [ 𝑝 ] 𝑅 ∧ [ 𝑄 ] 𝑆 = [ 𝑞 ] 𝑆 ) ∧ 𝑧 = [ ( 𝑝 + 𝑞 ) ] 𝑇 ) ) )
25 ecelqsw ⊢ ( ( 𝑅 ∈ 𝑋 ∧ 𝑃 ∈ 𝐴 ) → [ 𝑃 ] 𝑅 ∈ ( 𝐴 / 𝑅 ) )
26 25 1 eleqtrrdi ⊢ ( ( 𝑅 ∈ 𝑋 ∧ 𝑃 ∈ 𝐴 ) → [ 𝑃 ] 𝑅 ∈ 𝐽 )
27 13 26 sylan ⊢ ( ( 𝜑 ∧ 𝑃 ∈ 𝐴 ) → [ 𝑃 ] 𝑅 ∈ 𝐽 )
28 27 3adant3 ⊢ ( ( 𝜑 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐵 ) → [ 𝑃 ] 𝑅 ∈ 𝐽 )
29 ecelqsw ⊢ ( ( 𝑆 ∈ 𝑌 ∧ 𝑄 ∈ 𝐵 ) → [ 𝑄 ] 𝑆 ∈ ( 𝐵 / 𝑆 ) )
30 29 2 eleqtrrdi ⊢ ( ( 𝑆 ∈ 𝑌 ∧ 𝑄 ∈ 𝐵 ) → [ 𝑄 ] 𝑆 ∈ 𝐾 )
31 14 30 sylan ⊢ ( ( 𝜑 ∧ 𝑄 ∈ 𝐵 ) → [ 𝑄 ] 𝑆 ∈ 𝐾 )
32 31 3adant2 ⊢ ( ( 𝜑 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐵 ) → [ 𝑄 ] 𝑆 ∈ 𝐾 )
33 iotaex ⊢ ( ℩ 𝑧 ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐵 ( ( [ 𝑃 ] 𝑅 = [ 𝑝 ] 𝑅 ∧ [ 𝑄 ] 𝑆 = [ 𝑞 ] 𝑆 ) ∧ 𝑧 = [ ( 𝑝 + 𝑞 ) ] 𝑇 ) ) ∈ V
34 33 a1i ⊢ ( ( 𝜑 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐵 ) → ( ℩ 𝑧 ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐵 ( ( [ 𝑃 ] 𝑅 = [ 𝑝 ] 𝑅 ∧ [ 𝑄 ] 𝑆 = [ 𝑞 ] 𝑆 ) ∧ 𝑧 = [ ( 𝑝 + 𝑞 ) ] 𝑇 ) ) ∈ V )
35 16 24 28 32 34 ovmpod ⊢ ( ( 𝜑 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐵 ) → ( [ 𝑃 ] 𝑅 ⨣ [ 𝑄 ] 𝑆 ) = ( ℩ 𝑧 ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐵 ( ( [ 𝑃 ] 𝑅 = [ 𝑝 ] 𝑅 ∧ [ 𝑄 ] 𝑆 = [ 𝑞 ] 𝑆 ) ∧ 𝑧 = [ ( 𝑝 + 𝑞 ) ] 𝑇 ) ) )
36 eqid ⊢ [ 𝑃 ] 𝑅 = [ 𝑃 ] 𝑅
37 eqid ⊢ [ 𝑄 ] 𝑆 = [ 𝑄 ] 𝑆
38 36 37 pm3.2i ⊢ ( [ 𝑃 ] 𝑅 = [ 𝑃 ] 𝑅 ∧ [ 𝑄 ] 𝑆 = [ 𝑄 ] 𝑆 )
39 eqid ⊢ [ ( 𝑃 + 𝑄 ) ] 𝑇 = [ ( 𝑃 + 𝑄 ) ] 𝑇
40 38 39 pm3.2i ⊢ ( ( [ 𝑃 ] 𝑅 = [ 𝑃 ] 𝑅 ∧ [ 𝑄 ] 𝑆 = [ 𝑄 ] 𝑆 ) ∧ [ ( 𝑃 + 𝑄 ) ] 𝑇 = [ ( 𝑃 + 𝑄 ) ] 𝑇 )
41 eceq1 ⊢ ( 𝑝 = 𝑃 → [ 𝑝 ] 𝑅 = [ 𝑃 ] 𝑅 )
42 41 eqeq2d ⊢ ( 𝑝 = 𝑃 → ( [ 𝑃 ] 𝑅 = [ 𝑝 ] 𝑅 ↔ [ 𝑃 ] 𝑅 = [ 𝑃 ] 𝑅 ) )
43 42 anbi1d ⊢ ( 𝑝 = 𝑃 → ( ( [ 𝑃 ] 𝑅 = [ 𝑝 ] 𝑅 ∧ [ 𝑄 ] 𝑆 = [ 𝑞 ] 𝑆 ) ↔ ( [ 𝑃 ] 𝑅 = [ 𝑃 ] 𝑅 ∧ [ 𝑄 ] 𝑆 = [ 𝑞 ] 𝑆 ) ) )
44 oveq1 ⊢ ( 𝑝 = 𝑃 → ( 𝑝 + 𝑞 ) = ( 𝑃 + 𝑞 ) )
45 44 eceq1d ⊢ ( 𝑝 = 𝑃 → [ ( 𝑝 + 𝑞 ) ] 𝑇 = [ ( 𝑃 + 𝑞 ) ] 𝑇 )
46 45 eqeq2d ⊢ ( 𝑝 = 𝑃 → ( [ ( 𝑃 + 𝑄 ) ] 𝑇 = [ ( 𝑝 + 𝑞 ) ] 𝑇 ↔ [ ( 𝑃 + 𝑄 ) ] 𝑇 = [ ( 𝑃 + 𝑞 ) ] 𝑇 ) )
47 43 46 anbi12d ⊢ ( 𝑝 = 𝑃 → ( ( ( [ 𝑃 ] 𝑅 = [ 𝑝 ] 𝑅 ∧ [ 𝑄 ] 𝑆 = [ 𝑞 ] 𝑆 ) ∧ [ ( 𝑃 + 𝑄 ) ] 𝑇 = [ ( 𝑝 + 𝑞 ) ] 𝑇 ) ↔ ( ( [ 𝑃 ] 𝑅 = [ 𝑃 ] 𝑅 ∧ [ 𝑄 ] 𝑆 = [ 𝑞 ] 𝑆 ) ∧ [ ( 𝑃 + 𝑄 ) ] 𝑇 = [ ( 𝑃 + 𝑞 ) ] 𝑇 ) ) )
48 eceq1 ⊢ ( 𝑞 = 𝑄 → [ 𝑞 ] 𝑆 = [ 𝑄 ] 𝑆 )
49 48 eqeq2d ⊢ ( 𝑞 = 𝑄 → ( [ 𝑄 ] 𝑆 = [ 𝑞 ] 𝑆 ↔ [ 𝑄 ] 𝑆 = [ 𝑄 ] 𝑆 ) )
50 49 anbi2d ⊢ ( 𝑞 = 𝑄 → ( ( [ 𝑃 ] 𝑅 = [ 𝑃 ] 𝑅 ∧ [ 𝑄 ] 𝑆 = [ 𝑞 ] 𝑆 ) ↔ ( [ 𝑃 ] 𝑅 = [ 𝑃 ] 𝑅 ∧ [ 𝑄 ] 𝑆 = [ 𝑄 ] 𝑆 ) ) )
51 oveq2 ⊢ ( 𝑞 = 𝑄 → ( 𝑃 + 𝑞 ) = ( 𝑃 + 𝑄 ) )
52 51 eceq1d ⊢ ( 𝑞 = 𝑄 → [ ( 𝑃 + 𝑞 ) ] 𝑇 = [ ( 𝑃 + 𝑄 ) ] 𝑇 )
53 52 eqeq2d ⊢ ( 𝑞 = 𝑄 → ( [ ( 𝑃 + 𝑄 ) ] 𝑇 = [ ( 𝑃 + 𝑞 ) ] 𝑇 ↔ [ ( 𝑃 + 𝑄 ) ] 𝑇 = [ ( 𝑃 + 𝑄 ) ] 𝑇 ) )
54 50 53 anbi12d ⊢ ( 𝑞 = 𝑄 → ( ( ( [ 𝑃 ] 𝑅 = [ 𝑃 ] 𝑅 ∧ [ 𝑄 ] 𝑆 = [ 𝑞 ] 𝑆 ) ∧ [ ( 𝑃 + 𝑄 ) ] 𝑇 = [ ( 𝑃 + 𝑞 ) ] 𝑇 ) ↔ ( ( [ 𝑃 ] 𝑅 = [ 𝑃 ] 𝑅 ∧ [ 𝑄 ] 𝑆 = [ 𝑄 ] 𝑆 ) ∧ [ ( 𝑃 + 𝑄 ) ] 𝑇 = [ ( 𝑃 + 𝑄 ) ] 𝑇 ) ) )
55 47 54 rspc2ev ⊢ ( ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐵 ∧ ( ( [ 𝑃 ] 𝑅 = [ 𝑃 ] 𝑅 ∧ [ 𝑄 ] 𝑆 = [ 𝑄 ] 𝑆 ) ∧ [ ( 𝑃 + 𝑄 ) ] 𝑇 = [ ( 𝑃 + 𝑄 ) ] 𝑇 ) ) → ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐵 ( ( [ 𝑃 ] 𝑅 = [ 𝑝 ] 𝑅 ∧ [ 𝑄 ] 𝑆 = [ 𝑞 ] 𝑆 ) ∧ [ ( 𝑃 + 𝑄 ) ] 𝑇 = [ ( 𝑝 + 𝑞 ) ] 𝑇 ) )
56 40 55 mp3an3 ⊢ ( ( 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐵 ) → ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐵 ( ( [ 𝑃 ] 𝑅 = [ 𝑝 ] 𝑅 ∧ [ 𝑄 ] 𝑆 = [ 𝑞 ] 𝑆 ) ∧ [ ( 𝑃 + 𝑄 ) ] 𝑇 = [ ( 𝑝 + 𝑞 ) ] 𝑇 ) )
57 56 3adant1 ⊢ ( ( 𝜑 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐵 ) → ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐵 ( ( [ 𝑃 ] 𝑅 = [ 𝑝 ] 𝑅 ∧ [ 𝑄 ] 𝑆 = [ 𝑞 ] 𝑆 ) ∧ [ ( 𝑃 + 𝑄 ) ] 𝑇 = [ ( 𝑝 + 𝑞 ) ] 𝑇 ) )
58 ecexg ⊢ ( 𝑇 ∈ 𝑍 → [ ( 𝑃 + 𝑄 ) ] 𝑇 ∈ V )
59 3 58 syl ⊢ ( 𝜑 → [ ( 𝑃 + 𝑄 ) ] 𝑇 ∈ V )
60 59 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐵 ) → [ ( 𝑃 + 𝑄 ) ] 𝑇 ∈ V )
61 simp1 ⊢ ( ( 𝜑 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐵 ) → 𝜑 )
62 1 2 3 4 5 6 7 8 9 10 11 eroveu ⊢ ( ( 𝜑 ∧ ( [ 𝑃 ] 𝑅 ∈ 𝐽 ∧ [ 𝑄 ] 𝑆 ∈ 𝐾 ) ) → ∃! 𝑧 ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐵 ( ( [ 𝑃 ] 𝑅 = [ 𝑝 ] 𝑅 ∧ [ 𝑄 ] 𝑆 = [ 𝑞 ] 𝑆 ) ∧ 𝑧 = [ ( 𝑝 + 𝑞 ) ] 𝑇 ) )
63 61 28 32 62 syl12anc ⊢ ( ( 𝜑 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐵 ) → ∃! 𝑧 ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐵 ( ( [ 𝑃 ] 𝑅 = [ 𝑝 ] 𝑅 ∧ [ 𝑄 ] 𝑆 = [ 𝑞 ] 𝑆 ) ∧ 𝑧 = [ ( 𝑝 + 𝑞 ) ] 𝑇 ) )
64 simpr ⊢ ( ( ( 𝜑 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐵 ) ∧ 𝑧 = [ ( 𝑃 + 𝑄 ) ] 𝑇 ) → 𝑧 = [ ( 𝑃 + 𝑄 ) ] 𝑇 )
65 64 eqeq1d ⊢ ( ( ( 𝜑 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐵 ) ∧ 𝑧 = [ ( 𝑃 + 𝑄 ) ] 𝑇 ) → ( 𝑧 = [ ( 𝑝 + 𝑞 ) ] 𝑇 ↔ [ ( 𝑃 + 𝑄 ) ] 𝑇 = [ ( 𝑝 + 𝑞 ) ] 𝑇 ) )
66 65 anbi2d ⊢ ( ( ( 𝜑 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐵 ) ∧ 𝑧 = [ ( 𝑃 + 𝑄 ) ] 𝑇 ) → ( ( ( [ 𝑃 ] 𝑅 = [ 𝑝 ] 𝑅 ∧ [ 𝑄 ] 𝑆 = [ 𝑞 ] 𝑆 ) ∧ 𝑧 = [ ( 𝑝 + 𝑞 ) ] 𝑇 ) ↔ ( ( [ 𝑃 ] 𝑅 = [ 𝑝 ] 𝑅 ∧ [ 𝑄 ] 𝑆 = [ 𝑞 ] 𝑆 ) ∧ [ ( 𝑃 + 𝑄 ) ] 𝑇 = [ ( 𝑝 + 𝑞 ) ] 𝑇 ) ) )
67 66 2rexbidv ⊢ ( ( ( 𝜑 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐵 ) ∧ 𝑧 = [ ( 𝑃 + 𝑄 ) ] 𝑇 ) → ( ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐵 ( ( [ 𝑃 ] 𝑅 = [ 𝑝 ] 𝑅 ∧ [ 𝑄 ] 𝑆 = [ 𝑞 ] 𝑆 ) ∧ 𝑧 = [ ( 𝑝 + 𝑞 ) ] 𝑇 ) ↔ ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐵 ( ( [ 𝑃 ] 𝑅 = [ 𝑝 ] 𝑅 ∧ [ 𝑄 ] 𝑆 = [ 𝑞 ] 𝑆 ) ∧ [ ( 𝑃 + 𝑄 ) ] 𝑇 = [ ( 𝑝 + 𝑞 ) ] 𝑇 ) ) )
68 60 63 67 iota2d ⊢ ( ( 𝜑 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐵 ) → ( ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐵 ( ( [ 𝑃 ] 𝑅 = [ 𝑝 ] 𝑅 ∧ [ 𝑄 ] 𝑆 = [ 𝑞 ] 𝑆 ) ∧ [ ( 𝑃 + 𝑄 ) ] 𝑇 = [ ( 𝑝 + 𝑞 ) ] 𝑇 ) ↔ ( ℩ 𝑧 ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐵 ( ( [ 𝑃 ] 𝑅 = [ 𝑝 ] 𝑅 ∧ [ 𝑄 ] 𝑆 = [ 𝑞 ] 𝑆 ) ∧ 𝑧 = [ ( 𝑝 + 𝑞 ) ] 𝑇 ) ) = [ ( 𝑃 + 𝑄 ) ] 𝑇 ) )
69 57 68 mpbid ⊢ ( ( 𝜑 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐵 ) → ( ℩ 𝑧 ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐵 ( ( [ 𝑃 ] 𝑅 = [ 𝑝 ] 𝑅 ∧ [ 𝑄 ] 𝑆 = [ 𝑞 ] 𝑆 ) ∧ 𝑧 = [ ( 𝑝 + 𝑞 ) ] 𝑇 ) ) = [ ( 𝑃 + 𝑄 ) ] 𝑇 )
70 35 69 eqtrd ⊢ ( ( 𝜑 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐵 ) → ( [ 𝑃 ] 𝑅 ⨣ [ 𝑄 ] 𝑆 ) = [ ( 𝑃 + 𝑄 ) ] 𝑇 )