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 ecelqsg âŠĒ ( ( 𝑅 ∈ 𝑋 ∧ 𝑃 ∈ ðī ) → [ 𝑃 ] 𝑅 ∈ ( ðī / 𝑅 ) )
26 25 1 eleqtrrdi âŠĒ ( ( 𝑅 ∈ 𝑋 ∧ 𝑃 ∈ ðī ) → [ 𝑃 ] 𝑅 ∈ ð― )
27 13 26 sylan âŠĒ ( ( 𝜑 ∧ 𝑃 ∈ ðī ) → [ 𝑃 ] 𝑅 ∈ ð― )
28 27 3adant3 âŠĒ ( ( 𝜑 ∧ 𝑃 ∈ ðī ∧ 𝑄 ∈ ðĩ ) → [ 𝑃 ] 𝑅 ∈ ð― )
29 ecelqsg âŠĒ ( ( 𝑆 ∈ 𝑌 ∧ 𝑄 ∈ ðĩ ) → [ 𝑄 ] 𝑆 ∈ ( ðĩ / 𝑆 ) )
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 âŠĒ ( ( 𝜑 ∧ 𝑃 ∈ ðī ∧ 𝑄 ∈ ðĩ ) → ( [ 𝑃 ] 𝑅 âĻĢ [ 𝑄 ] 𝑆 ) = [ ( 𝑃 + 𝑄 ) ] 𝑇 )