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

Theorem ecopovtrn 8019
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 5350 . . . . . . 7 {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (𝑆 × 𝑆) ∧ 𝑦 ∈ (𝑆 × 𝑆)) ∧ ∃𝑧𝑤𝑣𝑢((𝑥 = ⟨𝑧, 𝑤⟩ ∧ 𝑦 = ⟨𝑣, 𝑢⟩) ∧ (𝑧 + 𝑢) = (𝑤 + 𝑣)))} ⊆ ((𝑆 × 𝑆) × (𝑆 × 𝑆))
31, 2eqsstri 3776 . . . . . 6 ⊆ ((𝑆 × 𝑆) × (𝑆 × 𝑆))
43brel 5325 . . . . 5 (𝐴 𝐵 → (𝐴 ∈ (𝑆 × 𝑆) ∧ 𝐵 ∈ (𝑆 × 𝑆)))
54simpld 477 . . . 4 (𝐴 𝐵𝐴 ∈ (𝑆 × 𝑆))
63brel 5325 . . . 4 (𝐵 𝐶 → (𝐵 ∈ (𝑆 × 𝑆) ∧ 𝐶 ∈ (𝑆 × 𝑆)))
75, 6anim12i 591 . . 3 ((𝐴 𝐵𝐵 𝐶) → (𝐴 ∈ (𝑆 × 𝑆) ∧ (𝐵 ∈ (𝑆 × 𝑆) ∧ 𝐶 ∈ (𝑆 × 𝑆))))
8 3anass 1081 . . 3 ((𝐴 ∈ (𝑆 × 𝑆) ∧ 𝐵 ∈ (𝑆 × 𝑆) ∧ 𝐶 ∈ (𝑆 × 𝑆)) ↔ (𝐴 ∈ (𝑆 × 𝑆) ∧ (𝐵 ∈ (𝑆 × 𝑆) ∧ 𝐶 ∈ (𝑆 × 𝑆))))
97, 8sylibr 224 . 2 ((𝐴 𝐵𝐵 𝐶) → (𝐴 ∈ (𝑆 × 𝑆) ∧ 𝐵 ∈ (𝑆 × 𝑆) ∧ 𝐶 ∈ (𝑆 × 𝑆)))
10 eqid 2760 . . 3 (𝑆 × 𝑆) = (𝑆 × 𝑆)
11 breq1 4807 . . . . 5 (⟨𝑓, 𝑔⟩ = 𝐴 → (⟨𝑓, 𝑔, 𝑡⟩ ↔ 𝐴 , 𝑡⟩))
1211anbi1d 743 . . . 4 (⟨𝑓, 𝑔⟩ = 𝐴 → ((⟨𝑓, 𝑔, 𝑡⟩ ∧ ⟨, 𝑡𝑠, 𝑟⟩) ↔ (𝐴 , 𝑡⟩ ∧ ⟨, 𝑡𝑠, 𝑟⟩)))
13 breq1 4807 . . . 4 (⟨𝑓, 𝑔⟩ = 𝐴 → (⟨𝑓, 𝑔𝑠, 𝑟⟩ ↔ 𝐴 𝑠, 𝑟⟩))
1412, 13imbi12d 333 . . 3 (⟨𝑓, 𝑔⟩ = 𝐴 → (((⟨𝑓, 𝑔, 𝑡⟩ ∧ ⟨, 𝑡𝑠, 𝑟⟩) → ⟨𝑓, 𝑔𝑠, 𝑟⟩) ↔ ((𝐴 , 𝑡⟩ ∧ ⟨, 𝑡𝑠, 𝑟⟩) → 𝐴 𝑠, 𝑟⟩)))
15 breq2 4808 . . . . 5 (⟨, 𝑡⟩ = 𝐵 → (𝐴 , 𝑡⟩ ↔ 𝐴 𝐵))
16 breq1 4807 . . . . 5 (⟨, 𝑡⟩ = 𝐵 → (⟨, 𝑡𝑠, 𝑟⟩ ↔ 𝐵 𝑠, 𝑟⟩))
1715, 16anbi12d 749 . . . 4 (⟨, 𝑡⟩ = 𝐵 → ((𝐴 , 𝑡⟩ ∧ ⟨, 𝑡𝑠, 𝑟⟩) ↔ (𝐴 𝐵𝐵 𝑠, 𝑟⟩)))
1817imbi1d 330 . . 3 (⟨, 𝑡⟩ = 𝐵 → (((𝐴 , 𝑡⟩ ∧ ⟨, 𝑡𝑠, 𝑟⟩) → 𝐴 𝑠, 𝑟⟩) ↔ ((𝐴 𝐵𝐵 𝑠, 𝑟⟩) → 𝐴 𝑠, 𝑟⟩)))
19 breq2 4808 . . . . 5 (⟨𝑠, 𝑟⟩ = 𝐶 → (𝐵 𝑠, 𝑟⟩ ↔ 𝐵 𝐶))
2019anbi2d 742 . . . 4 (⟨𝑠, 𝑟⟩ = 𝐶 → ((𝐴 𝐵𝐵 𝑠, 𝑟⟩) ↔ (𝐴 𝐵𝐵 𝐶)))
21 breq2 4808 . . . 4 (⟨𝑠, 𝑟⟩ = 𝐶 → (𝐴 𝑠, 𝑟⟩ ↔ 𝐴 𝐶))
2220, 21imbi12d 333 . . 3 (⟨𝑠, 𝑟⟩ = 𝐶 → (((𝐴 𝐵𝐵 𝑠, 𝑟⟩) → 𝐴 𝑠, 𝑟⟩) ↔ ((𝐴 𝐵𝐵 𝐶) → 𝐴 𝐶)))
231ecopoveq 8017 . . . . . . . 8 (((𝑓𝑆𝑔𝑆) ∧ (𝑆𝑡𝑆)) → (⟨𝑓, 𝑔, 𝑡⟩ ↔ (𝑓 + 𝑡) = (𝑔 + )))
24233adant3 1127 . . . . . . 7 (((𝑓𝑆𝑔𝑆) ∧ (𝑆𝑡𝑆) ∧ (𝑠𝑆𝑟𝑆)) → (⟨𝑓, 𝑔, 𝑡⟩ ↔ (𝑓 + 𝑡) = (𝑔 + )))
251ecopoveq 8017 . . . . . . . 8 (((𝑆𝑡𝑆) ∧ (𝑠𝑆𝑟𝑆)) → (⟨, 𝑡𝑠, 𝑟⟩ ↔ ( + 𝑟) = (𝑡 + 𝑠)))
26253adant1 1125 . . . . . . 7 (((𝑓𝑆𝑔𝑆) ∧ (𝑆𝑡𝑆) ∧ (𝑠𝑆𝑟𝑆)) → (⟨, 𝑡𝑠, 𝑟⟩ ↔ ( + 𝑟) = (𝑡 + 𝑠)))
2724, 26anbi12d 749 . . . . . 6 (((𝑓𝑆𝑔𝑆) ∧ (𝑆𝑡𝑆) ∧ (𝑠𝑆𝑟𝑆)) → ((⟨𝑓, 𝑔, 𝑡⟩ ∧ ⟨, 𝑡𝑠, 𝑟⟩) ↔ ((𝑓 + 𝑡) = (𝑔 + ) ∧ ( + 𝑟) = (𝑡 + 𝑠))))
28 oveq12 6823 . . . . . . 7 (((𝑓 + 𝑡) = (𝑔 + ) ∧ ( + 𝑟) = (𝑡 + 𝑠)) → ((𝑓 + 𝑡) + ( + 𝑟)) = ((𝑔 + ) + (𝑡 + 𝑠)))
29 vex 3343 . . . . . . . 8 ∈ V
30 vex 3343 . . . . . . . 8 𝑡 ∈ V
31 vex 3343 . . . . . . . 8 𝑓 ∈ V
32 ecopopr.com . . . . . . . 8 (𝑥 + 𝑦) = (𝑦 + 𝑥)
33 ecopopr.ass . . . . . . . 8 ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧))
34 vex 3343 . . . . . . . 8 𝑟 ∈ V
3529, 30, 31, 32, 33, 34caov411 7032 . . . . . . 7 (( + 𝑡) + (𝑓 + 𝑟)) = ((𝑓 + 𝑡) + ( + 𝑟))
36 vex 3343 . . . . . . . . 9 𝑔 ∈ V
37 vex 3343 . . . . . . . . 9 𝑠 ∈ V
3836, 30, 29, 32, 33, 37caov411 7032 . . . . . . . 8 ((𝑔 + 𝑡) + ( + 𝑠)) = (( + 𝑡) + (𝑔 + 𝑠))
3936, 30, 29, 32, 33, 37caov4 7031 . . . . . . . 8 ((𝑔 + 𝑡) + ( + 𝑠)) = ((𝑔 + ) + (𝑡 + 𝑠))
4038, 39eqtr3i 2784 . . . . . . 7 (( + 𝑡) + (𝑔 + 𝑠)) = ((𝑔 + ) + (𝑡 + 𝑠))
4128, 35, 403eqtr4g 2819 . . . . . 6 (((𝑓 + 𝑡) = (𝑔 + ) ∧ ( + 𝑟) = (𝑡 + 𝑠)) → (( + 𝑡) + (𝑓 + 𝑟)) = (( + 𝑡) + (𝑔 + 𝑠)))
4227, 41syl6bi 243 . . . . 5 (((𝑓𝑆𝑔𝑆) ∧ (𝑆𝑡𝑆) ∧ (𝑠𝑆𝑟𝑆)) → ((⟨𝑓, 𝑔, 𝑡⟩ ∧ ⟨, 𝑡𝑠, 𝑟⟩) → (( + 𝑡) + (𝑓 + 𝑟)) = (( + 𝑡) + (𝑔 + 𝑠))))
43 ecopopr.cl . . . . . . . . . . 11 ((𝑥𝑆𝑦𝑆) → (𝑥 + 𝑦) ∈ 𝑆)
4443caovcl 6994 . . . . . . . . . 10 ((𝑆𝑡𝑆) → ( + 𝑡) ∈ 𝑆)
4543caovcl 6994 . . . . . . . . . 10 ((𝑓𝑆𝑟𝑆) → (𝑓 + 𝑟) ∈ 𝑆)
46 ovex 6842 . . . . . . . . . . 11 (𝑔 + 𝑠) ∈ V
47 ecopopr.can . . . . . . . . . . 11 ((𝑥𝑆𝑦𝑆) → ((𝑥 + 𝑦) = (𝑥 + 𝑧) → 𝑦 = 𝑧))
4846, 47caovcan 7004 . . . . . . . . . 10 ((( + 𝑡) ∈ 𝑆 ∧ (𝑓 + 𝑟) ∈ 𝑆) → ((( + 𝑡) + (𝑓 + 𝑟)) = (( + 𝑡) + (𝑔 + 𝑠)) → (𝑓 + 𝑟) = (𝑔 + 𝑠)))
4944, 45, 48syl2an 495 . . . . . . . . 9 (((𝑆𝑡𝑆) ∧ (𝑓𝑆𝑟𝑆)) → ((( + 𝑡) + (𝑓 + 𝑟)) = (( + 𝑡) + (𝑔 + 𝑠)) → (𝑓 + 𝑟) = (𝑔 + 𝑠)))
50493impb 1108 . . . . . . . 8 (((𝑆𝑡𝑆) ∧ 𝑓𝑆𝑟𝑆) → ((( + 𝑡) + (𝑓 + 𝑟)) = (( + 𝑡) + (𝑔 + 𝑠)) → (𝑓 + 𝑟) = (𝑔 + 𝑠)))
51503com12 1118 . . . . . . 7 ((𝑓𝑆 ∧ (𝑆𝑡𝑆) ∧ 𝑟𝑆) → ((( + 𝑡) + (𝑓 + 𝑟)) = (( + 𝑡) + (𝑔 + 𝑠)) → (𝑓 + 𝑟) = (𝑔 + 𝑠)))
52513adant3l 1194 . . . . . 6 ((𝑓𝑆 ∧ (𝑆𝑡𝑆) ∧ (𝑠𝑆𝑟𝑆)) → ((( + 𝑡) + (𝑓 + 𝑟)) = (( + 𝑡) + (𝑔 + 𝑠)) → (𝑓 + 𝑟) = (𝑔 + 𝑠)))
53523adant1r 1188 . . . . 5 (((𝑓𝑆𝑔𝑆) ∧ (𝑆𝑡𝑆) ∧ (𝑠𝑆𝑟𝑆)) → ((( + 𝑡) + (𝑓 + 𝑟)) = (( + 𝑡) + (𝑔 + 𝑠)) → (𝑓 + 𝑟) = (𝑔 + 𝑠)))
5442, 53syld 47 . . . 4 (((𝑓𝑆𝑔𝑆) ∧ (𝑆𝑡𝑆) ∧ (𝑠𝑆𝑟𝑆)) → ((⟨𝑓, 𝑔, 𝑡⟩ ∧ ⟨, 𝑡𝑠, 𝑟⟩) → (𝑓 + 𝑟) = (𝑔 + 𝑠)))
551ecopoveq 8017 . . . . 5 (((𝑓𝑆𝑔𝑆) ∧ (𝑠𝑆𝑟𝑆)) → (⟨𝑓, 𝑔𝑠, 𝑟⟩ ↔ (𝑓 + 𝑟) = (𝑔 + 𝑠)))
56553adant2 1126 . . . 4 (((𝑓𝑆𝑔𝑆) ∧ (𝑆𝑡𝑆) ∧ (𝑠𝑆𝑟𝑆)) → (⟨𝑓, 𝑔𝑠, 𝑟⟩ ↔ (𝑓 + 𝑟) = (𝑔 + 𝑠)))
5754, 56sylibrd 249 . . 3 (((𝑓𝑆𝑔𝑆) ∧ (𝑆𝑡𝑆) ∧ (𝑠𝑆𝑟𝑆)) → ((⟨𝑓, 𝑔, 𝑡⟩ ∧ ⟨, 𝑡𝑠, 𝑟⟩) → ⟨𝑓, 𝑔𝑠, 𝑟⟩))
5810, 14, 18, 22, 573optocl 5354 . 2 ((𝐴 ∈ (𝑆 × 𝑆) ∧ 𝐵 ∈ (𝑆 × 𝑆) ∧ 𝐶 ∈ (𝑆 × 𝑆)) → ((𝐴 𝐵𝐵 𝐶) → 𝐴 𝐶))
599, 58mpcom 38 1 ((𝐴 𝐵𝐵 𝐶) → 𝐴 𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 383  w3a 1072   = wceq 1632  wex 1853  wcel 2139  cop 4327   class class class wbr 4804  {copab 4864   × cxp 5264  (class class class)co 6814
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-sep 4933  ax-nul 4941  ax-pr 5055
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-eu 2611  df-mo 2612  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ral 3055  df-rex 3056  df-rab 3059  df-v 3342  df-sbc 3577  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-nul 4059  df-if 4231  df-sn 4322  df-pr 4324  df-op 4328  df-uni 4589  df-br 4805  df-opab 4865  df-xp 5272  df-iota 6012  df-fv 6057  df-ov 6817
This theorem is referenced by:  ecopover  8020
  Copyright terms: Public domain W3C validator