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

Theorem ecopovtrn 8007
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 5332 . . . . . . 7 {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (𝑆 × 𝑆) ∧ 𝑦 ∈ (𝑆 × 𝑆)) ∧ ∃𝑧𝑤𝑣𝑢((𝑥 = ⟨𝑧, 𝑤⟩ ∧ 𝑦 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 + 𝑢) = (𝑤 + 𝑣)))} ⊆ ((𝑆 × 𝑆) × (𝑆 × 𝑆))
31, 2eqsstri 3784 . . . . . 6 ⊆ ((𝑆 × 𝑆) × (𝑆 × 𝑆))
43brel 5307 . . . . 5 (𝐴 𝐵 → (𝐴 ∈ (𝑆 × 𝑆) ∧ 𝐵 ∈ (𝑆 × 𝑆)))
54simpld 482 . . . 4 (𝐴 𝐵𝐴 ∈ (𝑆 × 𝑆))
63brel 5307 . . . 4 (𝐵 𝐶 → (𝐵 ∈ (𝑆 × 𝑆) ∧ 𝐶 ∈ (𝑆 × 𝑆)))
75, 6anim12i 600 . . 3 ((𝐴 𝐵𝐵 𝐶) → (𝐴 ∈ (𝑆 × 𝑆) ∧ (𝐵 ∈ (𝑆 × 𝑆) ∧ 𝐶 ∈ (𝑆 × 𝑆))))
8 3anass 1080 . . 3 ((𝐴 ∈ (𝑆 × 𝑆) ∧ 𝐵 ∈ (𝑆 × 𝑆) ∧ 𝐶 ∈ (𝑆 × 𝑆)) ↔ (𝐴 ∈ (𝑆 × 𝑆) ∧ (𝐵 ∈ (𝑆 × 𝑆) ∧ 𝐶 ∈ (𝑆 × 𝑆))))
97, 8sylibr 224 . 2 ((𝐴 𝐵𝐵 𝐶) → (𝐴 ∈ (𝑆 × 𝑆) ∧ 𝐵 ∈ (𝑆 × 𝑆) ∧ 𝐶 ∈ (𝑆 × 𝑆)))
10 eqid 2771 . . 3 (𝑆 × 𝑆) = (𝑆 × 𝑆)
11 breq1 4790 . . . . 5 (⟨𝑓, 𝑔⟩ = 𝐴 → (⟨𝑓, 𝑔, 𝑡⟩ ↔ 𝐴 , 𝑡⟩))
1211anbi1d 615 . . . 4 (⟨𝑓, 𝑔⟩ = 𝐴 → ((⟨𝑓, 𝑔, 𝑡⟩ ∧ ⟨, 𝑡𝑠, 𝑟⟩) ↔ (𝐴 , 𝑡⟩ ∧ ⟨, 𝑡𝑠, 𝑟⟩)))
13 breq1 4790 . . . 4 (⟨𝑓, 𝑔⟩ = 𝐴 → (⟨𝑓, 𝑔𝑠, 𝑟⟩ ↔ 𝐴 𝑠, 𝑟⟩))
1412, 13imbi12d 333 . . 3 (⟨𝑓, 𝑔⟩ = 𝐴 → (((⟨𝑓, 𝑔, 𝑡⟩ ∧ ⟨, 𝑡𝑠, 𝑟⟩) → ⟨𝑓, 𝑔𝑠, 𝑟⟩) ↔ ((𝐴 , 𝑡⟩ ∧ ⟨, 𝑡𝑠, 𝑟⟩) → 𝐴 𝑠, 𝑟⟩)))
15 breq2 4791 . . . . 5 (⟨, 𝑡⟩ = 𝐵 → (𝐴 , 𝑡⟩ ↔ 𝐴 𝐵))
16 breq1 4790 . . . . 5 (⟨, 𝑡⟩ = 𝐵 → (⟨, 𝑡𝑠, 𝑟⟩ ↔ 𝐵 𝑠, 𝑟⟩))
1715, 16anbi12d 616 . . . 4 (⟨, 𝑡⟩ = 𝐵 → ((𝐴 , 𝑡⟩ ∧ ⟨, 𝑡𝑠, 𝑟⟩) ↔ (𝐴 𝐵𝐵 𝑠, 𝑟⟩)))
1817imbi1d 330 . . 3 (⟨, 𝑡⟩ = 𝐵 → (((𝐴 , 𝑡⟩ ∧ ⟨, 𝑡𝑠, 𝑟⟩) → 𝐴 𝑠, 𝑟⟩) ↔ ((𝐴 𝐵𝐵 𝑠, 𝑟⟩) → 𝐴 𝑠, 𝑟⟩)))
19 breq2 4791 . . . . 5 (⟨𝑠, 𝑟⟩ = 𝐶 → (𝐵 𝑠, 𝑟⟩ ↔ 𝐵 𝐶))
2019anbi2d 614 . . . 4 (⟨𝑠, 𝑟⟩ = 𝐶 → ((𝐴 𝐵𝐵 𝑠, 𝑟⟩) ↔ (𝐴 𝐵𝐵 𝐶)))
21 breq2 4791 . . . 4 (⟨𝑠, 𝑟⟩ = 𝐶 → (𝐴 𝑠, 𝑟⟩ ↔ 𝐴 𝐶))
2220, 21imbi12d 333 . . 3 (⟨𝑠, 𝑟⟩ = 𝐶 → (((𝐴 𝐵𝐵 𝑠, 𝑟⟩) → 𝐴 𝑠, 𝑟⟩) ↔ ((𝐴 𝐵𝐵 𝐶) → 𝐴 𝐶)))
231ecopoveq 8005 . . . . . . . 8 (((𝑓𝑆𝑔𝑆) ∧ (𝑆𝑡𝑆)) → (⟨𝑓, 𝑔, 𝑡⟩ ↔ (𝑓 + 𝑡) = (𝑔 + )))
24233adant3 1126 . . . . . . 7 (((𝑓𝑆𝑔𝑆) ∧ (𝑆𝑡𝑆) ∧ (𝑠𝑆𝑟𝑆)) → (⟨𝑓, 𝑔, 𝑡⟩ ↔ (𝑓 + 𝑡) = (𝑔 + )))
251ecopoveq 8005 . . . . . . . 8 (((𝑆𝑡𝑆) ∧ (𝑠𝑆𝑟𝑆)) → (⟨, 𝑡𝑠, 𝑟⟩ ↔ ( + 𝑟) = (𝑡 + 𝑠)))
26253adant1 1124 . . . . . . 7 (((𝑓𝑆𝑔𝑆) ∧ (𝑆𝑡𝑆) ∧ (𝑠𝑆𝑟𝑆)) → (⟨, 𝑡𝑠, 𝑟⟩ ↔ ( + 𝑟) = (𝑡 + 𝑠)))
2724, 26anbi12d 616 . . . . . 6 (((𝑓𝑆𝑔𝑆) ∧ (𝑆𝑡𝑆) ∧ (𝑠𝑆𝑟𝑆)) → ((⟨𝑓, 𝑔, 𝑡⟩ ∧ ⟨, 𝑡𝑠, 𝑟⟩) ↔ ((𝑓 + 𝑡) = (𝑔 + ) ∧ ( + 𝑟) = (𝑡 + 𝑠))))
28 oveq12 6805 . . . . . . 7 (((𝑓 + 𝑡) = (𝑔 + ) ∧ ( + 𝑟) = (𝑡 + 𝑠)) → ((𝑓 + 𝑡) + ( + 𝑟)) = ((𝑔 + ) + (𝑡 + 𝑠)))
29 vex 3354 . . . . . . . 8 ∈ V
30 vex 3354 . . . . . . . 8 𝑡 ∈ V
31 vex 3354 . . . . . . . 8 𝑓 ∈ V
32 ecopopr.com . . . . . . . 8 (𝑥 + 𝑦) = (𝑦 + 𝑥)
33 ecopopr.ass . . . . . . . 8 ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧))
34 vex 3354 . . . . . . . 8 𝑟 ∈ V
3529, 30, 31, 32, 33, 34caov411 7017 . . . . . . 7 (( + 𝑡) + (𝑓 + 𝑟)) = ((𝑓 + 𝑡) + ( + 𝑟))
36 vex 3354 . . . . . . . . 9 𝑔 ∈ V
37 vex 3354 . . . . . . . . 9 𝑠 ∈ V
3836, 30, 29, 32, 33, 37caov411 7017 . . . . . . . 8 ((𝑔 + 𝑡) + ( + 𝑠)) = (( + 𝑡) + (𝑔 + 𝑠))
3936, 30, 29, 32, 33, 37caov4 7016 . . . . . . . 8 ((𝑔 + 𝑡) + ( + 𝑠)) = ((𝑔 + ) + (𝑡 + 𝑠))
4038, 39eqtr3i 2795 . . . . . . 7 (( + 𝑡) + (𝑔 + 𝑠)) = ((𝑔 + ) + (𝑡 + 𝑠))
4128, 35, 403eqtr4g 2830 . . . . . 6 (((𝑓 + 𝑡) = (𝑔 + ) ∧ ( + 𝑟) = (𝑡 + 𝑠)) → (( + 𝑡) + (𝑓 + 𝑟)) = (( + 𝑡) + (𝑔 + 𝑠)))
4227, 41syl6bi 243 . . . . 5 (((𝑓𝑆𝑔𝑆) ∧ (𝑆𝑡𝑆) ∧ (𝑠𝑆𝑟𝑆)) → ((⟨𝑓, 𝑔, 𝑡⟩ ∧ ⟨, 𝑡𝑠, 𝑟⟩) → (( + 𝑡) + (𝑓 + 𝑟)) = (( + 𝑡) + (𝑔 + 𝑠))))
43 ecopopr.cl . . . . . . . . . . 11 ((𝑥𝑆𝑦𝑆) → (𝑥 + 𝑦) ∈ 𝑆)
4443caovcl 6979 . . . . . . . . . 10 ((𝑆𝑡𝑆) → ( + 𝑡) ∈ 𝑆)
4543caovcl 6979 . . . . . . . . . 10 ((𝑓𝑆𝑟𝑆) → (𝑓 + 𝑟) ∈ 𝑆)
46 ovex 6827 . . . . . . . . . . 11 (𝑔 + 𝑠) ∈ V
47 ecopopr.can . . . . . . . . . . 11 ((𝑥𝑆𝑦𝑆) → ((𝑥 + 𝑦) = (𝑥 + 𝑧) → 𝑦 = 𝑧))
4846, 47caovcan 6989 . . . . . . . . . 10 ((( + 𝑡) ∈ 𝑆 ∧ (𝑓 + 𝑟) ∈ 𝑆) → ((( + 𝑡) + (𝑓 + 𝑟)) = (( + 𝑡) + (𝑔 + 𝑠)) → (𝑓 + 𝑟) = (𝑔 + 𝑠)))
4944, 45, 48syl2an 583 . . . . . . . . 9 (((𝑆𝑡𝑆) ∧ (𝑓𝑆𝑟𝑆)) → ((( + 𝑡) + (𝑓 + 𝑟)) = (( + 𝑡) + (𝑔 + 𝑠)) → (𝑓 + 𝑟) = (𝑔 + 𝑠)))
50493impb 1107 . . . . . . . 8 (((𝑆𝑡𝑆) ∧ 𝑓𝑆𝑟𝑆) → ((( + 𝑡) + (𝑓 + 𝑟)) = (( + 𝑡) + (𝑔 + 𝑠)) → (𝑓 + 𝑟) = (𝑔 + 𝑠)))
51503com12 1117 . . . . . . 7 ((𝑓𝑆 ∧ (𝑆𝑡𝑆) ∧ 𝑟𝑆) → ((( + 𝑡) + (𝑓 + 𝑟)) = (( + 𝑡) + (𝑔 + 𝑠)) → (𝑓 + 𝑟) = (𝑔 + 𝑠)))
52513adant3l 1193 . . . . . 6 ((𝑓𝑆 ∧ (𝑆𝑡𝑆) ∧ (𝑠𝑆𝑟𝑆)) → ((( + 𝑡) + (𝑓 + 𝑟)) = (( + 𝑡) + (𝑔 + 𝑠)) → (𝑓 + 𝑟) = (𝑔 + 𝑠)))
53523adant1r 1187 . . . . 5 (((𝑓𝑆𝑔𝑆) ∧ (𝑆𝑡𝑆) ∧ (𝑠𝑆𝑟𝑆)) → ((( + 𝑡) + (𝑓 + 𝑟)) = (( + 𝑡) + (𝑔 + 𝑠)) → (𝑓 + 𝑟) = (𝑔 + 𝑠)))
5442, 53syld 47 . . . 4 (((𝑓𝑆𝑔𝑆) ∧ (𝑆𝑡𝑆) ∧ (𝑠𝑆𝑟𝑆)) → ((⟨𝑓, 𝑔, 𝑡⟩ ∧ ⟨, 𝑡𝑠, 𝑟⟩) → (𝑓 + 𝑟) = (𝑔 + 𝑠)))
551ecopoveq 8005 . . . . 5 (((𝑓𝑆𝑔𝑆) ∧ (𝑠𝑆𝑟𝑆)) → (⟨𝑓, 𝑔𝑠, 𝑟⟩ ↔ (𝑓 + 𝑟) = (𝑔 + 𝑠)))
56553adant2 1125 . . . 4 (((𝑓𝑆𝑔𝑆) ∧ (𝑆𝑡𝑆) ∧ (𝑠𝑆𝑟𝑆)) → (⟨𝑓, 𝑔𝑠, 𝑟⟩ ↔ (𝑓 + 𝑟) = (𝑔 + 𝑠)))
5754, 56sylibrd 249 . . 3 (((𝑓𝑆𝑔𝑆) ∧ (𝑆𝑡𝑆) ∧ (𝑠𝑆𝑟𝑆)) → ((⟨𝑓, 𝑔, 𝑡⟩ ∧ ⟨, 𝑡𝑠, 𝑟⟩) → ⟨𝑓, 𝑔𝑠, 𝑟⟩))
5810, 14, 18, 22, 573optocl 5336 . 2 ((𝐴 ∈ (𝑆 × 𝑆) ∧ 𝐵 ∈ (𝑆 × 𝑆) ∧ 𝐶 ∈ (𝑆 × 𝑆)) → ((𝐴 𝐵𝐵 𝐶) → 𝐴 𝐶))
599, 58mpcom 38 1 ((𝐴 𝐵𝐵 𝐶) → 𝐴 𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 382  w3a 1071   = wceq 1631  wex 1852  wcel 2145  cop 4323   class class class wbr 4787  {copab 4847   × cxp 5248  (class class class)co 6796
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-sep 4916  ax-nul 4924  ax-pr 5035
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ral 3066  df-rex 3067  df-rab 3070  df-v 3353  df-sbc 3588  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-nul 4064  df-if 4227  df-sn 4318  df-pr 4320  df-op 4324  df-uni 4576  df-br 4788  df-opab 4848  df-xp 5256  df-iota 5993  df-fv 6038  df-ov 6799
This theorem is referenced by:  ecopover  8008
  Copyright terms: Public domain W3C validator