MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  eroveu Structured version   Visualization version   GIF version

Theorem eroveu 8370
Description: Lemma for erov 8372 and eroprf 8373. (Contributed by Jeff Madsen, 10-Jun-2010.) (Revised by Mario Carneiro, 9-Jul-2014.)
Hypotheses
Ref Expression
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 ((𝜑 ∧ ((𝑟𝐴𝑠𝐴) ∧ (𝑡𝐵𝑢𝐵))) → ((𝑟𝑅𝑠𝑡𝑆𝑢) → (𝑟 + 𝑡)𝑇(𝑠 + 𝑢)))
Assertion
Ref Expression
eroveu ((𝜑 ∧ (𝑋𝐽𝑌𝐾)) → ∃!𝑧𝑝𝐴𝑞𝐵 ((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇))
Distinct variable groups:   𝑞,𝑝,𝑟,𝑠,𝑡,𝑢,𝑧,𝐴   𝐵,𝑝,𝑞,𝑟,𝑠,𝑡,𝑢,𝑧   𝐽,𝑝,𝑞,𝑧   𝑅,𝑝,𝑞,𝑟,𝑠,𝑡,𝑢,𝑧   𝐾,𝑝,𝑞,𝑧   𝑆,𝑝,𝑞,𝑟,𝑠,𝑡,𝑢,𝑧   + ,𝑝,𝑞,𝑟,𝑠,𝑡,𝑢,𝑧   𝜑,𝑝,𝑞,𝑟,𝑠,𝑡,𝑢,𝑧   𝑇,𝑝,𝑞,𝑟,𝑠,𝑡,𝑢,𝑧   𝑋,𝑝,𝑞,𝑟,𝑠,𝑡,𝑢,𝑧   𝑌,𝑝,𝑞,𝑟,𝑠,𝑡,𝑢,𝑧
Allowed substitution hints:   𝐶(𝑧,𝑢,𝑡,𝑠,𝑟,𝑞,𝑝)   𝑈(𝑧,𝑢,𝑡,𝑠,𝑟,𝑞,𝑝)   𝐽(𝑢,𝑡,𝑠,𝑟)   𝐾(𝑢,𝑡,𝑠,𝑟)   𝑉(𝑧,𝑢,𝑡,𝑠,𝑟,𝑞,𝑝)   𝑊(𝑧,𝑢,𝑡,𝑠,𝑟,𝑞,𝑝)   𝑍(𝑧,𝑢,𝑡,𝑠,𝑟,𝑞,𝑝)

Proof of Theorem eroveu
Dummy variable 𝑤 is distinct from all other variables.
StepHypRef Expression
1 elqsi 8328 . . . . . . . 8 (𝑋 ∈ (𝐴 / 𝑅) → ∃𝑝𝐴 𝑋 = [𝑝]𝑅)
2 eropr.1 . . . . . . . 8 𝐽 = (𝐴 / 𝑅)
31, 2eleq2s 2929 . . . . . . 7 (𝑋𝐽 → ∃𝑝𝐴 𝑋 = [𝑝]𝑅)
4 elqsi 8328 . . . . . . . 8 (𝑌 ∈ (𝐵 / 𝑆) → ∃𝑞𝐵 𝑌 = [𝑞]𝑆)
5 eropr.2 . . . . . . . 8 𝐾 = (𝐵 / 𝑆)
64, 5eleq2s 2929 . . . . . . 7 (𝑌𝐾 → ∃𝑞𝐵 𝑌 = [𝑞]𝑆)
73, 6anim12i 614 . . . . . 6 ((𝑋𝐽𝑌𝐾) → (∃𝑝𝐴 𝑋 = [𝑝]𝑅 ∧ ∃𝑞𝐵 𝑌 = [𝑞]𝑆))
87adantl 484 . . . . 5 ((𝜑 ∧ (𝑋𝐽𝑌𝐾)) → (∃𝑝𝐴 𝑋 = [𝑝]𝑅 ∧ ∃𝑞𝐵 𝑌 = [𝑞]𝑆))
9 reeanv 3354 . . . . 5 (∃𝑝𝐴𝑞𝐵 (𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ↔ (∃𝑝𝐴 𝑋 = [𝑝]𝑅 ∧ ∃𝑞𝐵 𝑌 = [𝑞]𝑆))
108, 9sylibr 236 . . . 4 ((𝜑 ∧ (𝑋𝐽𝑌𝐾)) → ∃𝑝𝐴𝑞𝐵 (𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆))
11 eropr.3 . . . . . . . 8 (𝜑𝑇𝑍)
1211adantr 483 . . . . . . 7 ((𝜑 ∧ (𝑋𝐽𝑌𝐾)) → 𝑇𝑍)
13 ecexg 8271 . . . . . . 7 (𝑇𝑍 → [(𝑝 + 𝑞)]𝑇 ∈ V)
14 elisset 3484 . . . . . . 7 ([(𝑝 + 𝑞)]𝑇 ∈ V → ∃𝑧 𝑧 = [(𝑝 + 𝑞)]𝑇)
1512, 13, 143syl 18 . . . . . 6 ((𝜑 ∧ (𝑋𝐽𝑌𝐾)) → ∃𝑧 𝑧 = [(𝑝 + 𝑞)]𝑇)
1615biantrud 534 . . . . 5 ((𝜑 ∧ (𝑋𝐽𝑌𝐾)) → ((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ↔ ((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ ∃𝑧 𝑧 = [(𝑝 + 𝑞)]𝑇)))
17162rexbidv 3287 . . . 4 ((𝜑 ∧ (𝑋𝐽𝑌𝐾)) → (∃𝑝𝐴𝑞𝐵 (𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ↔ ∃𝑝𝐴𝑞𝐵 ((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ ∃𝑧 𝑧 = [(𝑝 + 𝑞)]𝑇)))
1810, 17mpbid 234 . . 3 ((𝜑 ∧ (𝑋𝐽𝑌𝐾)) → ∃𝑝𝐴𝑞𝐵 ((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ ∃𝑧 𝑧 = [(𝑝 + 𝑞)]𝑇))
19 19.42v 1954 . . . . . . . 8 (∃𝑧((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇) ↔ ((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ ∃𝑧 𝑧 = [(𝑝 + 𝑞)]𝑇))
2019bicomi 226 . . . . . . 7 (((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ ∃𝑧 𝑧 = [(𝑝 + 𝑞)]𝑇) ↔ ∃𝑧((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇))
2120rexbii 3234 . . . . . 6 (∃𝑞𝐵 ((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ ∃𝑧 𝑧 = [(𝑝 + 𝑞)]𝑇) ↔ ∃𝑞𝐵𝑧((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇))
22 rexcom4 3236 . . . . . 6 (∃𝑞𝐵𝑧((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇) ↔ ∃𝑧𝑞𝐵 ((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇))
2321, 22bitri 277 . . . . 5 (∃𝑞𝐵 ((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ ∃𝑧 𝑧 = [(𝑝 + 𝑞)]𝑇) ↔ ∃𝑧𝑞𝐵 ((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇))
2423rexbii 3234 . . . 4 (∃𝑝𝐴𝑞𝐵 ((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ ∃𝑧 𝑧 = [(𝑝 + 𝑞)]𝑇) ↔ ∃𝑝𝐴𝑧𝑞𝐵 ((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇))
25 rexcom4 3236 . . . 4 (∃𝑝𝐴𝑧𝑞𝐵 ((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇) ↔ ∃𝑧𝑝𝐴𝑞𝐵 ((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇))
2624, 25bitri 277 . . 3 (∃𝑝𝐴𝑞𝐵 ((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ ∃𝑧 𝑧 = [(𝑝 + 𝑞)]𝑇) ↔ ∃𝑧𝑝𝐴𝑞𝐵 ((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇))
2718, 26sylib 220 . 2 ((𝜑 ∧ (𝑋𝐽𝑌𝐾)) → ∃𝑧𝑝𝐴𝑞𝐵 ((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇))
28 reeanv 3354 . . . . . 6 (∃𝑟𝐴𝑠𝐴 (∃𝑡𝐵 ((𝑋 = [𝑟]𝑅𝑌 = [𝑡]𝑆) ∧ 𝑧 = [(𝑟 + 𝑡)]𝑇) ∧ ∃𝑢𝐵 ((𝑋 = [𝑠]𝑅𝑌 = [𝑢]𝑆) ∧ 𝑤 = [(𝑠 + 𝑢)]𝑇)) ↔ (∃𝑟𝐴𝑡𝐵 ((𝑋 = [𝑟]𝑅𝑌 = [𝑡]𝑆) ∧ 𝑧 = [(𝑟 + 𝑡)]𝑇) ∧ ∃𝑠𝐴𝑢𝐵 ((𝑋 = [𝑠]𝑅𝑌 = [𝑢]𝑆) ∧ 𝑤 = [(𝑠 + 𝑢)]𝑇)))
29 eceq1 8305 . . . . . . . . . . 11 (𝑝 = 𝑟 → [𝑝]𝑅 = [𝑟]𝑅)
3029eqeq2d 2831 . . . . . . . . . 10 (𝑝 = 𝑟 → (𝑋 = [𝑝]𝑅𝑋 = [𝑟]𝑅))
3130anbi1d 631 . . . . . . . . 9 (𝑝 = 𝑟 → ((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ↔ (𝑋 = [𝑟]𝑅𝑌 = [𝑞]𝑆)))
32 oveq1 7140 . . . . . . . . . . 11 (𝑝 = 𝑟 → (𝑝 + 𝑞) = (𝑟 + 𝑞))
3332eceq1d 8306 . . . . . . . . . 10 (𝑝 = 𝑟 → [(𝑝 + 𝑞)]𝑇 = [(𝑟 + 𝑞)]𝑇)
3433eqeq2d 2831 . . . . . . . . 9 (𝑝 = 𝑟 → (𝑧 = [(𝑝 + 𝑞)]𝑇𝑧 = [(𝑟 + 𝑞)]𝑇))
3531, 34anbi12d 632 . . . . . . . 8 (𝑝 = 𝑟 → (((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇) ↔ ((𝑋 = [𝑟]𝑅𝑌 = [𝑞]𝑆) ∧ 𝑧 = [(𝑟 + 𝑞)]𝑇)))
36 eceq1 8305 . . . . . . . . . . 11 (𝑞 = 𝑡 → [𝑞]𝑆 = [𝑡]𝑆)
3736eqeq2d 2831 . . . . . . . . . 10 (𝑞 = 𝑡 → (𝑌 = [𝑞]𝑆𝑌 = [𝑡]𝑆))
3837anbi2d 630 . . . . . . . . 9 (𝑞 = 𝑡 → ((𝑋 = [𝑟]𝑅𝑌 = [𝑞]𝑆) ↔ (𝑋 = [𝑟]𝑅𝑌 = [𝑡]𝑆)))
39 oveq2 7141 . . . . . . . . . . 11 (𝑞 = 𝑡 → (𝑟 + 𝑞) = (𝑟 + 𝑡))
4039eceq1d 8306 . . . . . . . . . 10 (𝑞 = 𝑡 → [(𝑟 + 𝑞)]𝑇 = [(𝑟 + 𝑡)]𝑇)
4140eqeq2d 2831 . . . . . . . . 9 (𝑞 = 𝑡 → (𝑧 = [(𝑟 + 𝑞)]𝑇𝑧 = [(𝑟 + 𝑡)]𝑇))
4238, 41anbi12d 632 . . . . . . . 8 (𝑞 = 𝑡 → (((𝑋 = [𝑟]𝑅𝑌 = [𝑞]𝑆) ∧ 𝑧 = [(𝑟 + 𝑞)]𝑇) ↔ ((𝑋 = [𝑟]𝑅𝑌 = [𝑡]𝑆) ∧ 𝑧 = [(𝑟 + 𝑡)]𝑇)))
4335, 42cbvrex2vw 3441 . . . . . . 7 (∃𝑝𝐴𝑞𝐵 ((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇) ↔ ∃𝑟𝐴𝑡𝐵 ((𝑋 = [𝑟]𝑅𝑌 = [𝑡]𝑆) ∧ 𝑧 = [(𝑟 + 𝑡)]𝑇))
44 eceq1 8305 . . . . . . . . . . 11 (𝑝 = 𝑠 → [𝑝]𝑅 = [𝑠]𝑅)
4544eqeq2d 2831 . . . . . . . . . 10 (𝑝 = 𝑠 → (𝑋 = [𝑝]𝑅𝑋 = [𝑠]𝑅))
4645anbi1d 631 . . . . . . . . 9 (𝑝 = 𝑠 → ((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ↔ (𝑋 = [𝑠]𝑅𝑌 = [𝑞]𝑆)))
47 oveq1 7140 . . . . . . . . . . 11 (𝑝 = 𝑠 → (𝑝 + 𝑞) = (𝑠 + 𝑞))
4847eceq1d 8306 . . . . . . . . . 10 (𝑝 = 𝑠 → [(𝑝 + 𝑞)]𝑇 = [(𝑠 + 𝑞)]𝑇)
4948eqeq2d 2831 . . . . . . . . 9 (𝑝 = 𝑠 → (𝑤 = [(𝑝 + 𝑞)]𝑇𝑤 = [(𝑠 + 𝑞)]𝑇))
5046, 49anbi12d 632 . . . . . . . 8 (𝑝 = 𝑠 → (((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ 𝑤 = [(𝑝 + 𝑞)]𝑇) ↔ ((𝑋 = [𝑠]𝑅𝑌 = [𝑞]𝑆) ∧ 𝑤 = [(𝑠 + 𝑞)]𝑇)))
51 eceq1 8305 . . . . . . . . . . 11 (𝑞 = 𝑢 → [𝑞]𝑆 = [𝑢]𝑆)
5251eqeq2d 2831 . . . . . . . . . 10 (𝑞 = 𝑢 → (𝑌 = [𝑞]𝑆𝑌 = [𝑢]𝑆))
5352anbi2d 630 . . . . . . . . 9 (𝑞 = 𝑢 → ((𝑋 = [𝑠]𝑅𝑌 = [𝑞]𝑆) ↔ (𝑋 = [𝑠]𝑅𝑌 = [𝑢]𝑆)))
54 oveq2 7141 . . . . . . . . . . 11 (𝑞 = 𝑢 → (𝑠 + 𝑞) = (𝑠 + 𝑢))
5554eceq1d 8306 . . . . . . . . . 10 (𝑞 = 𝑢 → [(𝑠 + 𝑞)]𝑇 = [(𝑠 + 𝑢)]𝑇)
5655eqeq2d 2831 . . . . . . . . 9 (𝑞 = 𝑢 → (𝑤 = [(𝑠 + 𝑞)]𝑇𝑤 = [(𝑠 + 𝑢)]𝑇))
5753, 56anbi12d 632 . . . . . . . 8 (𝑞 = 𝑢 → (((𝑋 = [𝑠]𝑅𝑌 = [𝑞]𝑆) ∧ 𝑤 = [(𝑠 + 𝑞)]𝑇) ↔ ((𝑋 = [𝑠]𝑅𝑌 = [𝑢]𝑆) ∧ 𝑤 = [(𝑠 + 𝑢)]𝑇)))
5850, 57cbvrex2vw 3441 . . . . . . 7 (∃𝑝𝐴𝑞𝐵 ((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ 𝑤 = [(𝑝 + 𝑞)]𝑇) ↔ ∃𝑠𝐴𝑢𝐵 ((𝑋 = [𝑠]𝑅𝑌 = [𝑢]𝑆) ∧ 𝑤 = [(𝑠 + 𝑢)]𝑇))
5943, 58anbi12i 628 . . . . . 6 ((∃𝑝𝐴𝑞𝐵 ((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇) ∧ ∃𝑝𝐴𝑞𝐵 ((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ 𝑤 = [(𝑝 + 𝑞)]𝑇)) ↔ (∃𝑟𝐴𝑡𝐵 ((𝑋 = [𝑟]𝑅𝑌 = [𝑡]𝑆) ∧ 𝑧 = [(𝑟 + 𝑡)]𝑇) ∧ ∃𝑠𝐴𝑢𝐵 ((𝑋 = [𝑠]𝑅𝑌 = [𝑢]𝑆) ∧ 𝑤 = [(𝑠 + 𝑢)]𝑇)))
6028, 59bitr4i 280 . . . . 5 (∃𝑟𝐴𝑠𝐴 (∃𝑡𝐵 ((𝑋 = [𝑟]𝑅𝑌 = [𝑡]𝑆) ∧ 𝑧 = [(𝑟 + 𝑡)]𝑇) ∧ ∃𝑢𝐵 ((𝑋 = [𝑠]𝑅𝑌 = [𝑢]𝑆) ∧ 𝑤 = [(𝑠 + 𝑢)]𝑇)) ↔ (∃𝑝𝐴𝑞𝐵 ((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇) ∧ ∃𝑝𝐴𝑞𝐵 ((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ 𝑤 = [(𝑝 + 𝑞)]𝑇)))
61 reeanv 3354 . . . . . . 7 (∃𝑡𝐵𝑢𝐵 (((𝑋 = [𝑟]𝑅𝑌 = [𝑡]𝑆) ∧ 𝑧 = [(𝑟 + 𝑡)]𝑇) ∧ ((𝑋 = [𝑠]𝑅𝑌 = [𝑢]𝑆) ∧ 𝑤 = [(𝑠 + 𝑢)]𝑇)) ↔ (∃𝑡𝐵 ((𝑋 = [𝑟]𝑅𝑌 = [𝑡]𝑆) ∧ 𝑧 = [(𝑟 + 𝑡)]𝑇) ∧ ∃𝑢𝐵 ((𝑋 = [𝑠]𝑅𝑌 = [𝑢]𝑆) ∧ 𝑤 = [(𝑠 + 𝑢)]𝑇)))
62 eropr.11 . . . . . . . . . . . . . 14 ((𝜑 ∧ ((𝑟𝐴𝑠𝐴) ∧ (𝑡𝐵𝑢𝐵))) → ((𝑟𝑅𝑠𝑡𝑆𝑢) → (𝑟 + 𝑡)𝑇(𝑠 + 𝑢)))
63 eropr.4 . . . . . . . . . . . . . . . . 17 (𝜑𝑅 Er 𝑈)
6463adantr 483 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ((𝑟𝐴𝑠𝐴) ∧ (𝑡𝐵𝑢𝐵))) → 𝑅 Er 𝑈)
65 eropr.7 . . . . . . . . . . . . . . . . . 18 (𝜑𝐴𝑈)
6665adantr 483 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ ((𝑟𝐴𝑠𝐴) ∧ (𝑡𝐵𝑢𝐵))) → 𝐴𝑈)
67 simprll 777 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ ((𝑟𝐴𝑠𝐴) ∧ (𝑡𝐵𝑢𝐵))) → 𝑟𝐴)
6866, 67sseldd 3947 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ((𝑟𝐴𝑠𝐴) ∧ (𝑡𝐵𝑢𝐵))) → 𝑟𝑈)
6964, 68erth 8316 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ((𝑟𝐴𝑠𝐴) ∧ (𝑡𝐵𝑢𝐵))) → (𝑟𝑅𝑠 ↔ [𝑟]𝑅 = [𝑠]𝑅))
70 eropr.5 . . . . . . . . . . . . . . . . 17 (𝜑𝑆 Er 𝑉)
7170adantr 483 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ((𝑟𝐴𝑠𝐴) ∧ (𝑡𝐵𝑢𝐵))) → 𝑆 Er 𝑉)
72 eropr.8 . . . . . . . . . . . . . . . . . 18 (𝜑𝐵𝑉)
7372adantr 483 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ ((𝑟𝐴𝑠𝐴) ∧ (𝑡𝐵𝑢𝐵))) → 𝐵𝑉)
74 simprrl 779 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ ((𝑟𝐴𝑠𝐴) ∧ (𝑡𝐵𝑢𝐵))) → 𝑡𝐵)
7573, 74sseldd 3947 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ((𝑟𝐴𝑠𝐴) ∧ (𝑡𝐵𝑢𝐵))) → 𝑡𝑉)
7671, 75erth 8316 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ((𝑟𝐴𝑠𝐴) ∧ (𝑡𝐵𝑢𝐵))) → (𝑡𝑆𝑢 ↔ [𝑡]𝑆 = [𝑢]𝑆))
7769, 76anbi12d 632 . . . . . . . . . . . . . 14 ((𝜑 ∧ ((𝑟𝐴𝑠𝐴) ∧ (𝑡𝐵𝑢𝐵))) → ((𝑟𝑅𝑠𝑡𝑆𝑢) ↔ ([𝑟]𝑅 = [𝑠]𝑅 ∧ [𝑡]𝑆 = [𝑢]𝑆)))
78 eropr.6 . . . . . . . . . . . . . . . 16 (𝜑𝑇 Er 𝑊)
7978adantr 483 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ((𝑟𝐴𝑠𝐴) ∧ (𝑡𝐵𝑢𝐵))) → 𝑇 Er 𝑊)
80 eropr.9 . . . . . . . . . . . . . . . . 17 (𝜑𝐶𝑊)
8180adantr 483 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ((𝑟𝐴𝑠𝐴) ∧ (𝑡𝐵𝑢𝐵))) → 𝐶𝑊)
82 eropr.10 . . . . . . . . . . . . . . . . . 18 (𝜑+ :(𝐴 × 𝐵)⟶𝐶)
8382adantr 483 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ ((𝑟𝐴𝑠𝐴) ∧ (𝑡𝐵𝑢𝐵))) → + :(𝐴 × 𝐵)⟶𝐶)
8483, 67, 74fovrnd 7298 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ((𝑟𝐴𝑠𝐴) ∧ (𝑡𝐵𝑢𝐵))) → (𝑟 + 𝑡) ∈ 𝐶)
8581, 84sseldd 3947 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ((𝑟𝐴𝑠𝐴) ∧ (𝑡𝐵𝑢𝐵))) → (𝑟 + 𝑡) ∈ 𝑊)
8679, 85erth 8316 . . . . . . . . . . . . . 14 ((𝜑 ∧ ((𝑟𝐴𝑠𝐴) ∧ (𝑡𝐵𝑢𝐵))) → ((𝑟 + 𝑡)𝑇(𝑠 + 𝑢) ↔ [(𝑟 + 𝑡)]𝑇 = [(𝑠 + 𝑢)]𝑇))
8762, 77, 863imtr3d 295 . . . . . . . . . . . . 13 ((𝜑 ∧ ((𝑟𝐴𝑠𝐴) ∧ (𝑡𝐵𝑢𝐵))) → (([𝑟]𝑅 = [𝑠]𝑅 ∧ [𝑡]𝑆 = [𝑢]𝑆) → [(𝑟 + 𝑡)]𝑇 = [(𝑠 + 𝑢)]𝑇))
88 eqeq2 2832 . . . . . . . . . . . . . 14 (𝑤 = [(𝑠 + 𝑢)]𝑇 → ([(𝑟 + 𝑡)]𝑇 = 𝑤 ↔ [(𝑟 + 𝑡)]𝑇 = [(𝑠 + 𝑢)]𝑇))
8988biimprcd 252 . . . . . . . . . . . . 13 ([(𝑟 + 𝑡)]𝑇 = [(𝑠 + 𝑢)]𝑇 → (𝑤 = [(𝑠 + 𝑢)]𝑇 → [(𝑟 + 𝑡)]𝑇 = 𝑤))
9087, 89syl6 35 . . . . . . . . . . . 12 ((𝜑 ∧ ((𝑟𝐴𝑠𝐴) ∧ (𝑡𝐵𝑢𝐵))) → (([𝑟]𝑅 = [𝑠]𝑅 ∧ [𝑡]𝑆 = [𝑢]𝑆) → (𝑤 = [(𝑠 + 𝑢)]𝑇 → [(𝑟 + 𝑡)]𝑇 = 𝑤)))
9190impd 413 . . . . . . . . . . 11 ((𝜑 ∧ ((𝑟𝐴𝑠𝐴) ∧ (𝑡𝐵𝑢𝐵))) → ((([𝑟]𝑅 = [𝑠]𝑅 ∧ [𝑡]𝑆 = [𝑢]𝑆) ∧ 𝑤 = [(𝑠 + 𝑢)]𝑇) → [(𝑟 + 𝑡)]𝑇 = 𝑤))
92 eqeq1 2824 . . . . . . . . . . . . . . 15 (𝑋 = [𝑟]𝑅 → (𝑋 = [𝑠]𝑅 ↔ [𝑟]𝑅 = [𝑠]𝑅))
93 eqeq1 2824 . . . . . . . . . . . . . . 15 (𝑌 = [𝑡]𝑆 → (𝑌 = [𝑢]𝑆 ↔ [𝑡]𝑆 = [𝑢]𝑆))
9492, 93bi2anan9 637 . . . . . . . . . . . . . 14 ((𝑋 = [𝑟]𝑅𝑌 = [𝑡]𝑆) → ((𝑋 = [𝑠]𝑅𝑌 = [𝑢]𝑆) ↔ ([𝑟]𝑅 = [𝑠]𝑅 ∧ [𝑡]𝑆 = [𝑢]𝑆)))
9594anbi1d 631 . . . . . . . . . . . . 13 ((𝑋 = [𝑟]𝑅𝑌 = [𝑡]𝑆) → (((𝑋 = [𝑠]𝑅𝑌 = [𝑢]𝑆) ∧ 𝑤 = [(𝑠 + 𝑢)]𝑇) ↔ (([𝑟]𝑅 = [𝑠]𝑅 ∧ [𝑡]𝑆 = [𝑢]𝑆) ∧ 𝑤 = [(𝑠 + 𝑢)]𝑇)))
9695adantr 483 . . . . . . . . . . . 12 (((𝑋 = [𝑟]𝑅𝑌 = [𝑡]𝑆) ∧ 𝑧 = [(𝑟 + 𝑡)]𝑇) → (((𝑋 = [𝑠]𝑅𝑌 = [𝑢]𝑆) ∧ 𝑤 = [(𝑠 + 𝑢)]𝑇) ↔ (([𝑟]𝑅 = [𝑠]𝑅 ∧ [𝑡]𝑆 = [𝑢]𝑆) ∧ 𝑤 = [(𝑠 + 𝑢)]𝑇)))
97 eqeq1 2824 . . . . . . . . . . . . 13 (𝑧 = [(𝑟 + 𝑡)]𝑇 → (𝑧 = 𝑤 ↔ [(𝑟 + 𝑡)]𝑇 = 𝑤))
9897adantl 484 . . . . . . . . . . . 12 (((𝑋 = [𝑟]𝑅𝑌 = [𝑡]𝑆) ∧ 𝑧 = [(𝑟 + 𝑡)]𝑇) → (𝑧 = 𝑤 ↔ [(𝑟 + 𝑡)]𝑇 = 𝑤))
9996, 98imbi12d 347 . . . . . . . . . . 11 (((𝑋 = [𝑟]𝑅𝑌 = [𝑡]𝑆) ∧ 𝑧 = [(𝑟 + 𝑡)]𝑇) → ((((𝑋 = [𝑠]𝑅𝑌 = [𝑢]𝑆) ∧ 𝑤 = [(𝑠 + 𝑢)]𝑇) → 𝑧 = 𝑤) ↔ ((([𝑟]𝑅 = [𝑠]𝑅 ∧ [𝑡]𝑆 = [𝑢]𝑆) ∧ 𝑤 = [(𝑠 + 𝑢)]𝑇) → [(𝑟 + 𝑡)]𝑇 = 𝑤)))
10091, 99syl5ibrcom 249 . . . . . . . . . 10 ((𝜑 ∧ ((𝑟𝐴𝑠𝐴) ∧ (𝑡𝐵𝑢𝐵))) → (((𝑋 = [𝑟]𝑅𝑌 = [𝑡]𝑆) ∧ 𝑧 = [(𝑟 + 𝑡)]𝑇) → (((𝑋 = [𝑠]𝑅𝑌 = [𝑢]𝑆) ∧ 𝑤 = [(𝑠 + 𝑢)]𝑇) → 𝑧 = 𝑤)))
101100impd 413 . . . . . . . . 9 ((𝜑 ∧ ((𝑟𝐴𝑠𝐴) ∧ (𝑡𝐵𝑢𝐵))) → ((((𝑋 = [𝑟]𝑅𝑌 = [𝑡]𝑆) ∧ 𝑧 = [(𝑟 + 𝑡)]𝑇) ∧ ((𝑋 = [𝑠]𝑅𝑌 = [𝑢]𝑆) ∧ 𝑤 = [(𝑠 + 𝑢)]𝑇)) → 𝑧 = 𝑤))
102101anassrs 470 . . . . . . . 8 (((𝜑 ∧ (𝑟𝐴𝑠𝐴)) ∧ (𝑡𝐵𝑢𝐵)) → ((((𝑋 = [𝑟]𝑅𝑌 = [𝑡]𝑆) ∧ 𝑧 = [(𝑟 + 𝑡)]𝑇) ∧ ((𝑋 = [𝑠]𝑅𝑌 = [𝑢]𝑆) ∧ 𝑤 = [(𝑠 + 𝑢)]𝑇)) → 𝑧 = 𝑤))
103102rexlimdvva 3281 . . . . . . 7 ((𝜑 ∧ (𝑟𝐴𝑠𝐴)) → (∃𝑡𝐵𝑢𝐵 (((𝑋 = [𝑟]𝑅𝑌 = [𝑡]𝑆) ∧ 𝑧 = [(𝑟 + 𝑡)]𝑇) ∧ ((𝑋 = [𝑠]𝑅𝑌 = [𝑢]𝑆) ∧ 𝑤 = [(𝑠 + 𝑢)]𝑇)) → 𝑧 = 𝑤))
10461, 103syl5bir 245 . . . . . 6 ((𝜑 ∧ (𝑟𝐴𝑠𝐴)) → ((∃𝑡𝐵 ((𝑋 = [𝑟]𝑅𝑌 = [𝑡]𝑆) ∧ 𝑧 = [(𝑟 + 𝑡)]𝑇) ∧ ∃𝑢𝐵 ((𝑋 = [𝑠]𝑅𝑌 = [𝑢]𝑆) ∧ 𝑤 = [(𝑠 + 𝑢)]𝑇)) → 𝑧 = 𝑤))
105104rexlimdvva 3281 . . . . 5 (𝜑 → (∃𝑟𝐴𝑠𝐴 (∃𝑡𝐵 ((𝑋 = [𝑟]𝑅𝑌 = [𝑡]𝑆) ∧ 𝑧 = [(𝑟 + 𝑡)]𝑇) ∧ ∃𝑢𝐵 ((𝑋 = [𝑠]𝑅𝑌 = [𝑢]𝑆) ∧ 𝑤 = [(𝑠 + 𝑢)]𝑇)) → 𝑧 = 𝑤))
10660, 105syl5bir 245 . . . 4 (𝜑 → ((∃𝑝𝐴𝑞𝐵 ((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇) ∧ ∃𝑝𝐴𝑞𝐵 ((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ 𝑤 = [(𝑝 + 𝑞)]𝑇)) → 𝑧 = 𝑤))
107106adantr 483 . . 3 ((𝜑 ∧ (𝑋𝐽𝑌𝐾)) → ((∃𝑝𝐴𝑞𝐵 ((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇) ∧ ∃𝑝𝐴𝑞𝐵 ((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ 𝑤 = [(𝑝 + 𝑞)]𝑇)) → 𝑧 = 𝑤))
108107alrimivv 1929 . 2 ((𝜑 ∧ (𝑋𝐽𝑌𝐾)) → ∀𝑧𝑤((∃𝑝𝐴𝑞𝐵 ((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇) ∧ ∃𝑝𝐴𝑞𝐵 ((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ 𝑤 = [(𝑝 + 𝑞)]𝑇)) → 𝑧 = 𝑤))
109 eqeq1 2824 . . . . 5 (𝑧 = 𝑤 → (𝑧 = [(𝑝 + 𝑞)]𝑇𝑤 = [(𝑝 + 𝑞)]𝑇))
110109anbi2d 630 . . . 4 (𝑧 = 𝑤 → (((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇) ↔ ((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ 𝑤 = [(𝑝 + 𝑞)]𝑇)))
1111102rexbidv 3287 . . 3 (𝑧 = 𝑤 → (∃𝑝𝐴𝑞𝐵 ((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇) ↔ ∃𝑝𝐴𝑞𝐵 ((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ 𝑤 = [(𝑝 + 𝑞)]𝑇)))
112111eu4 2698 . 2 (∃!𝑧𝑝𝐴𝑞𝐵 ((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇) ↔ (∃𝑧𝑝𝐴𝑞𝐵 ((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇) ∧ ∀𝑧𝑤((∃𝑝𝐴𝑞𝐵 ((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇) ∧ ∃𝑝𝐴𝑞𝐵 ((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ 𝑤 = [(𝑝 + 𝑞)]𝑇)) → 𝑧 = 𝑤)))
11327, 108, 112sylanbrc 585 1 ((𝜑 ∧ (𝑋𝐽𝑌𝐾)) → ∃!𝑧𝑝𝐴𝑞𝐵 ((𝑋 = [𝑝]𝑅𝑌 = [𝑞]𝑆) ∧ 𝑧 = [(𝑝 + 𝑞)]𝑇))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 208  wa 398  wal 1535   = wceq 1537  wex 1780  wcel 2114  ∃!weu 2652  wrex 3126  Vcvv 3473  wss 3913   class class class wbr 5042   × cxp 5529  wf 6327  (class class class)co 7133   Er wer 8264  [cec 8265   / cqs 8266
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2792  ax-sep 5179  ax-nul 5186  ax-pr 5306  ax-un 7439
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2653  df-clab 2799  df-cleq 2813  df-clel 2891  df-nfc 2959  df-ne 3007  df-ral 3130  df-rex 3131  df-rab 3134  df-v 3475  df-sbc 3753  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4270  df-if 4444  df-sn 4544  df-pr 4546  df-op 4550  df-uni 4815  df-br 5043  df-opab 5105  df-id 5436  df-xp 5537  df-rel 5538  df-cnv 5539  df-co 5540  df-dm 5541  df-rn 5542  df-res 5543  df-ima 5544  df-iota 6290  df-fun 6333  df-fn 6334  df-f 6335  df-fv 6339  df-ov 7136  df-er 8267  df-ec 8269  df-qs 8273
This theorem is referenced by:  erovlem  8371  erov  8372  eroprf  8373
  Copyright terms: Public domain W3C validator