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

Theorem ecopovtrn 8389
Description: Assuming that operation 𝐹 is commutative (second hypothesis), closed (third hypothesis), associative (fourth hypothesis), and has the cancellation property (fifth hypothesis), show that the relation , specified by the first hypothesis, is transitive. (Contributed by NM, 11-Feb-1996.) (Revised by Mario Carneiro, 26-Apr-2015.)
Hypotheses
Ref Expression
ecopopr.1 = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (𝑆 × 𝑆) ∧ 𝑦 ∈ (𝑆 × 𝑆)) ∧ ∃𝑧𝑤𝑣𝑢((𝑥 = ⟨𝑧, 𝑤⟩ ∧ 𝑦 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 + 𝑢) = (𝑤 + 𝑣)))}
ecopopr.com (𝑥 + 𝑦) = (𝑦 + 𝑥)
ecopopr.cl ((𝑥𝑆𝑦𝑆) → (𝑥 + 𝑦) ∈ 𝑆)
ecopopr.ass ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧))
ecopopr.can ((𝑥𝑆𝑦𝑆) → ((𝑥 + 𝑦) = (𝑥 + 𝑧) → 𝑦 = 𝑧))
Assertion
Ref Expression
ecopovtrn ((𝐴 𝐵𝐵 𝐶) → 𝐴 𝐶)
Distinct variable groups:   𝑥,𝑦,𝑧,𝑤,𝑣,𝑢, +   𝑥,𝑆,𝑦,𝑧,𝑤,𝑣,𝑢
Allowed substitution hints:   𝐴(𝑥,𝑦,𝑧,𝑤,𝑣,𝑢)   𝐵(𝑥,𝑦,𝑧,𝑤,𝑣,𝑢)   𝐶(𝑥,𝑦,𝑧,𝑤,𝑣,𝑢)   (𝑥,𝑦,𝑧,𝑤,𝑣,𝑢)

Proof of Theorem ecopovtrn
Dummy variables 𝑓 𝑔 𝑡 𝑠 𝑟 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ecopopr.1 . . . . . . 7 = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (𝑆 × 𝑆) ∧ 𝑦 ∈ (𝑆 × 𝑆)) ∧ ∃𝑧𝑤𝑣𝑢((𝑥 = ⟨𝑧, 𝑤⟩ ∧ 𝑦 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 + 𝑢) = (𝑤 + 𝑣)))}
2 opabssxp 5636 . . . . . . 7 {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (𝑆 × 𝑆) ∧ 𝑦 ∈ (𝑆 × 𝑆)) ∧ ∃𝑧𝑤𝑣𝑢((𝑥 = ⟨𝑧, 𝑤⟩ ∧ 𝑦 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 + 𝑢) = (𝑤 + 𝑣)))} ⊆ ((𝑆 × 𝑆) × (𝑆 × 𝑆))
31, 2eqsstri 3998 . . . . . 6 ⊆ ((𝑆 × 𝑆) × (𝑆 × 𝑆))
43brel 5610 . . . . 5 (𝐴 𝐵 → (𝐴 ∈ (𝑆 × 𝑆) ∧ 𝐵 ∈ (𝑆 × 𝑆)))
54simpld 495 . . . 4 (𝐴 𝐵𝐴 ∈ (𝑆 × 𝑆))
63brel 5610 . . . 4 (𝐵 𝐶 → (𝐵 ∈ (𝑆 × 𝑆) ∧ 𝐶 ∈ (𝑆 × 𝑆)))
75, 6anim12i 612 . . 3 ((𝐴 𝐵𝐵 𝐶) → (𝐴 ∈ (𝑆 × 𝑆) ∧ (𝐵 ∈ (𝑆 × 𝑆) ∧ 𝐶 ∈ (𝑆 × 𝑆))))
8 3anass 1087 . . 3 ((𝐴 ∈ (𝑆 × 𝑆) ∧ 𝐵 ∈ (𝑆 × 𝑆) ∧ 𝐶 ∈ (𝑆 × 𝑆)) ↔ (𝐴 ∈ (𝑆 × 𝑆) ∧ (𝐵 ∈ (𝑆 × 𝑆) ∧ 𝐶 ∈ (𝑆 × 𝑆))))
97, 8sylibr 235 . 2 ((𝐴 𝐵𝐵 𝐶) → (𝐴 ∈ (𝑆 × 𝑆) ∧ 𝐵 ∈ (𝑆 × 𝑆) ∧ 𝐶 ∈ (𝑆 × 𝑆)))
10 eqid 2818 . . 3 (𝑆 × 𝑆) = (𝑆 × 𝑆)
11 breq1 5060 . . . . 5 (⟨𝑓, 𝑔⟩ = 𝐴 → (⟨𝑓, 𝑔, 𝑡⟩ ↔ 𝐴 , 𝑡⟩))
1211anbi1d 629 . . . 4 (⟨𝑓, 𝑔⟩ = 𝐴 → ((⟨𝑓, 𝑔, 𝑡⟩ ∧ ⟨, 𝑡𝑠, 𝑟⟩) ↔ (𝐴 , 𝑡⟩ ∧ ⟨, 𝑡𝑠, 𝑟⟩)))
13 breq1 5060 . . . 4 (⟨𝑓, 𝑔⟩ = 𝐴 → (⟨𝑓, 𝑔𝑠, 𝑟⟩ ↔ 𝐴 𝑠, 𝑟⟩))
1412, 13imbi12d 346 . . 3 (⟨𝑓, 𝑔⟩ = 𝐴 → (((⟨𝑓, 𝑔, 𝑡⟩ ∧ ⟨, 𝑡𝑠, 𝑟⟩) → ⟨𝑓, 𝑔𝑠, 𝑟⟩) ↔ ((𝐴 , 𝑡⟩ ∧ ⟨, 𝑡𝑠, 𝑟⟩) → 𝐴 𝑠, 𝑟⟩)))
15 breq2 5061 . . . . 5 (⟨, 𝑡⟩ = 𝐵 → (𝐴 , 𝑡⟩ ↔ 𝐴 𝐵))
16 breq1 5060 . . . . 5 (⟨, 𝑡⟩ = 𝐵 → (⟨, 𝑡𝑠, 𝑟⟩ ↔ 𝐵 𝑠, 𝑟⟩))
1715, 16anbi12d 630 . . . 4 (⟨, 𝑡⟩ = 𝐵 → ((𝐴 , 𝑡⟩ ∧ ⟨, 𝑡𝑠, 𝑟⟩) ↔ (𝐴 𝐵𝐵 𝑠, 𝑟⟩)))
1817imbi1d 343 . . 3 (⟨, 𝑡⟩ = 𝐵 → (((𝐴 , 𝑡⟩ ∧ ⟨, 𝑡𝑠, 𝑟⟩) → 𝐴 𝑠, 𝑟⟩) ↔ ((𝐴 𝐵𝐵 𝑠, 𝑟⟩) → 𝐴 𝑠, 𝑟⟩)))
19 breq2 5061 . . . . 5 (⟨𝑠, 𝑟⟩ = 𝐶 → (𝐵 𝑠, 𝑟⟩ ↔ 𝐵 𝐶))
2019anbi2d 628 . . . 4 (⟨𝑠, 𝑟⟩ = 𝐶 → ((𝐴 𝐵𝐵 𝑠, 𝑟⟩) ↔ (𝐴 𝐵𝐵 𝐶)))
21 breq2 5061 . . . 4 (⟨𝑠, 𝑟⟩ = 𝐶 → (𝐴 𝑠, 𝑟⟩ ↔ 𝐴 𝐶))
2220, 21imbi12d 346 . . 3 (⟨𝑠, 𝑟⟩ = 𝐶 → (((𝐴 𝐵𝐵 𝑠, 𝑟⟩) → 𝐴 𝑠, 𝑟⟩) ↔ ((𝐴 𝐵𝐵 𝐶) → 𝐴 𝐶)))
231ecopoveq 8387 . . . . . . . 8 (((𝑓𝑆𝑔𝑆) ∧ (𝑆𝑡𝑆)) → (⟨𝑓, 𝑔, 𝑡⟩ ↔ (𝑓 + 𝑡) = (𝑔 + )))
24233adant3 1124 . . . . . . 7 (((𝑓𝑆𝑔𝑆) ∧ (𝑆𝑡𝑆) ∧ (𝑠𝑆𝑟𝑆)) → (⟨𝑓, 𝑔, 𝑡⟩ ↔ (𝑓 + 𝑡) = (𝑔 + )))
251ecopoveq 8387 . . . . . . . 8 (((𝑆𝑡𝑆) ∧ (𝑠𝑆𝑟𝑆)) → (⟨, 𝑡𝑠, 𝑟⟩ ↔ ( + 𝑟) = (𝑡 + 𝑠)))
26253adant1 1122 . . . . . . 7 (((𝑓𝑆𝑔𝑆) ∧ (𝑆𝑡𝑆) ∧ (𝑠𝑆𝑟𝑆)) → (⟨, 𝑡𝑠, 𝑟⟩ ↔ ( + 𝑟) = (𝑡 + 𝑠)))
2724, 26anbi12d 630 . . . . . 6 (((𝑓𝑆𝑔𝑆) ∧ (𝑆𝑡𝑆) ∧ (𝑠𝑆𝑟𝑆)) → ((⟨𝑓, 𝑔, 𝑡⟩ ∧ ⟨, 𝑡𝑠, 𝑟⟩) ↔ ((𝑓 + 𝑡) = (𝑔 + ) ∧ ( + 𝑟) = (𝑡 + 𝑠))))
28 oveq12 7154 . . . . . . 7 (((𝑓 + 𝑡) = (𝑔 + ) ∧ ( + 𝑟) = (𝑡 + 𝑠)) → ((𝑓 + 𝑡) + ( + 𝑟)) = ((𝑔 + ) + (𝑡 + 𝑠)))
29 vex 3495 . . . . . . . 8 ∈ V
30 vex 3495 . . . . . . . 8 𝑡 ∈ V
31 vex 3495 . . . . . . . 8 𝑓 ∈ V
32 ecopopr.com . . . . . . . 8 (𝑥 + 𝑦) = (𝑦 + 𝑥)
33 ecopopr.ass . . . . . . . 8 ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧))
34 vex 3495 . . . . . . . 8 𝑟 ∈ V
3529, 30, 31, 32, 33, 34caov411 7369 . . . . . . 7 (( + 𝑡) + (𝑓 + 𝑟)) = ((𝑓 + 𝑡) + ( + 𝑟))
36 vex 3495 . . . . . . . . 9 𝑔 ∈ V
37 vex 3495 . . . . . . . . 9 𝑠 ∈ V
3836, 30, 29, 32, 33, 37caov411 7369 . . . . . . . 8 ((𝑔 + 𝑡) + ( + 𝑠)) = (( + 𝑡) + (𝑔 + 𝑠))
3936, 30, 29, 32, 33, 37caov4 7368 . . . . . . . 8 ((𝑔 + 𝑡) + ( + 𝑠)) = ((𝑔 + ) + (𝑡 + 𝑠))
4038, 39eqtr3i 2843 . . . . . . 7 (( + 𝑡) + (𝑔 + 𝑠)) = ((𝑔 + ) + (𝑡 + 𝑠))
4128, 35, 403eqtr4g 2878 . . . . . 6 (((𝑓 + 𝑡) = (𝑔 + ) ∧ ( + 𝑟) = (𝑡 + 𝑠)) → (( + 𝑡) + (𝑓 + 𝑟)) = (( + 𝑡) + (𝑔 + 𝑠)))
4227, 41syl6bi 254 . . . . 5 (((𝑓𝑆𝑔𝑆) ∧ (𝑆𝑡𝑆) ∧ (𝑠𝑆𝑟𝑆)) → ((⟨𝑓, 𝑔, 𝑡⟩ ∧ ⟨, 𝑡𝑠, 𝑟⟩) → (( + 𝑡) + (𝑓 + 𝑟)) = (( + 𝑡) + (𝑔 + 𝑠))))
43 ecopopr.cl . . . . . . . . . . 11 ((𝑥𝑆𝑦𝑆) → (𝑥 + 𝑦) ∈ 𝑆)
4443caovcl 7331 . . . . . . . . . 10 ((𝑆𝑡𝑆) → ( + 𝑡) ∈ 𝑆)
4543caovcl 7331 . . . . . . . . . 10 ((𝑓𝑆𝑟𝑆) → (𝑓 + 𝑟) ∈ 𝑆)
46 ovex 7178 . . . . . . . . . . 11 (𝑔 + 𝑠) ∈ V
47 ecopopr.can . . . . . . . . . . 11 ((𝑥𝑆𝑦𝑆) → ((𝑥 + 𝑦) = (𝑥 + 𝑧) → 𝑦 = 𝑧))
4846, 47caovcan 7341 . . . . . . . . . 10 ((( + 𝑡) ∈ 𝑆 ∧ (𝑓 + 𝑟) ∈ 𝑆) → ((( + 𝑡) + (𝑓 + 𝑟)) = (( + 𝑡) + (𝑔 + 𝑠)) → (𝑓 + 𝑟) = (𝑔 + 𝑠)))
4944, 45, 48syl2an 595 . . . . . . . . 9 (((𝑆𝑡𝑆) ∧ (𝑓𝑆𝑟𝑆)) → ((( + 𝑡) + (𝑓 + 𝑟)) = (( + 𝑡) + (𝑔 + 𝑠)) → (𝑓 + 𝑟) = (𝑔 + 𝑠)))
50493impb 1107 . . . . . . . 8 (((𝑆𝑡𝑆) ∧ 𝑓𝑆𝑟𝑆) → ((( + 𝑡) + (𝑓 + 𝑟)) = (( + 𝑡) + (𝑔 + 𝑠)) → (𝑓 + 𝑟) = (𝑔 + 𝑠)))
51503com12 1115 . . . . . . 7 ((𝑓𝑆 ∧ (𝑆𝑡𝑆) ∧ 𝑟𝑆) → ((( + 𝑡) + (𝑓 + 𝑟)) = (( + 𝑡) + (𝑔 + 𝑠)) → (𝑓 + 𝑟) = (𝑔 + 𝑠)))
52513adant3l 1172 . . . . . 6 ((𝑓𝑆 ∧ (𝑆𝑡𝑆) ∧ (𝑠𝑆𝑟𝑆)) → ((( + 𝑡) + (𝑓 + 𝑟)) = (( + 𝑡) + (𝑔 + 𝑠)) → (𝑓 + 𝑟) = (𝑔 + 𝑠)))
53523adant1r 1169 . . . . 5 (((𝑓𝑆𝑔𝑆) ∧ (𝑆𝑡𝑆) ∧ (𝑠𝑆𝑟𝑆)) → ((( + 𝑡) + (𝑓 + 𝑟)) = (( + 𝑡) + (𝑔 + 𝑠)) → (𝑓 + 𝑟) = (𝑔 + 𝑠)))
5442, 53syld 47 . . . 4 (((𝑓𝑆𝑔𝑆) ∧ (𝑆𝑡𝑆) ∧ (𝑠𝑆𝑟𝑆)) → ((⟨𝑓, 𝑔, 𝑡⟩ ∧ ⟨, 𝑡𝑠, 𝑟⟩) → (𝑓 + 𝑟) = (𝑔 + 𝑠)))
551ecopoveq 8387 . . . . 5 (((𝑓𝑆𝑔𝑆) ∧ (𝑠𝑆𝑟𝑆)) → (⟨𝑓, 𝑔𝑠, 𝑟⟩ ↔ (𝑓 + 𝑟) = (𝑔 + 𝑠)))
56553adant2 1123 . . . 4 (((𝑓𝑆𝑔𝑆) ∧ (𝑆𝑡𝑆) ∧ (𝑠𝑆𝑟𝑆)) → (⟨𝑓, 𝑔𝑠, 𝑟⟩ ↔ (𝑓 + 𝑟) = (𝑔 + 𝑠)))
5754, 56sylibrd 260 . . 3 (((𝑓𝑆𝑔𝑆) ∧ (𝑆𝑡𝑆) ∧ (𝑠𝑆𝑟𝑆)) → ((⟨𝑓, 𝑔, 𝑡⟩ ∧ ⟨, 𝑡𝑠, 𝑟⟩) → ⟨𝑓, 𝑔𝑠, 𝑟⟩))
5810, 14, 18, 22, 573optocl 5640 . 2 ((𝐴 ∈ (𝑆 × 𝑆) ∧ 𝐵 ∈ (𝑆 × 𝑆) ∧ 𝐶 ∈ (𝑆 × 𝑆)) → ((𝐴 𝐵𝐵 𝐶) → 𝐴 𝐶))
599, 58mpcom 38 1 ((𝐴 𝐵𝐵 𝐶) → 𝐴 𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wa 396  w3a 1079   = wceq 1528  wex 1771  wcel 2105  cop 4563   class class class wbr 5057  {copab 5119   × cxp 5546  (class class class)co 7145
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790  ax-sep 5194  ax-nul 5201  ax-pr 5320
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2615  df-eu 2647  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-ral 3140  df-rex 3141  df-rab 3144  df-v 3494  df-sbc 3770  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-nul 4289  df-if 4464  df-sn 4558  df-pr 4560  df-op 4564  df-uni 4831  df-br 5058  df-opab 5120  df-xp 5554  df-iota 6307  df-fv 6356  df-ov 7148
This theorem is referenced by:  ecopover  8390
  Copyright terms: Public domain W3C validator