Theorem caovord2d 6115

Description: Operation ordering law with commuted arguments. (Contributed by Mario Carneiro, 30-Dec-2014.)

Hypotheses

Ref	Expression
caovordg.1	⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → (𝑥𝑅𝑦 ↔ (𝑧𝐹𝑥)𝑅(𝑧𝐹𝑦)))
caovordd.2	⊢ (𝜑 → 𝐴 ∈ 𝑆)
caovordd.3	⊢ (𝜑 → 𝐵 ∈ 𝑆)
caovordd.4	⊢ (𝜑 → 𝐶 ∈ 𝑆)
caovord2d.com	⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥𝐹𝑦) = (𝑦𝐹𝑥))

Assertion

Ref	Expression
caovord2d	⊢ (𝜑 → (𝐴𝑅𝐵 ↔ (𝐴𝐹𝐶)𝑅(𝐵𝐹𝐶)))

Distinct variable groups:   𝑥,𝑦,𝑧,𝐴   𝑥,𝐵,𝑦,𝑧   𝑥,𝐶,𝑦,𝑧   𝜑,𝑥,𝑦,𝑧   𝑥,𝐹,𝑦,𝑧   𝑥,𝑅,𝑦,𝑧   𝑥,𝑆,𝑦,𝑧

Proof of Theorem caovord2d

Step	Hyp	Ref	Expression
1		caovordg.1	. . 3 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆)) → (𝑥𝑅𝑦 ↔ (𝑧𝐹𝑥)𝑅(𝑧𝐹𝑦)))
2		caovordd.2	. . 3 ⊢ (𝜑 → 𝐴 ∈ 𝑆)
3		caovordd.3	. . 3 ⊢ (𝜑 → 𝐵 ∈ 𝑆)
4		caovordd.4	. . 3 ⊢ (𝜑 → 𝐶 ∈ 𝑆)
5	1, 2, 3, 4	caovordd 6114	. 2 ⊢ (𝜑 → (𝐴𝑅𝐵 ↔ (𝐶𝐹𝐴)𝑅(𝐶𝐹𝐵)))
6		caovord2d.com	. . . 4 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥𝐹𝑦) = (𝑦𝐹𝑥))
7	6, 4, 2	caovcomd 6102	. . 3 ⊢ (𝜑 → (𝐶𝐹𝐴) = (𝐴𝐹𝐶))
8	6, 4, 3	caovcomd 6102	. . 3 ⊢ (𝜑 → (𝐶𝐹𝐵) = (𝐵𝐹𝐶))
9	7, 8	breq12d 4056	. 2 ⊢ (𝜑 → ((𝐶𝐹𝐴)𝑅(𝐶𝐹𝐵) ↔ (𝐴𝐹𝐶)𝑅(𝐵𝐹𝐶)))
10	5, 9	bitrd 188	1 ⊢ (𝜑 → (𝐴𝑅𝐵 ↔ (𝐴𝐹𝐶)𝑅(𝐵𝐹𝐶)))

Syntax hints:   → wi 4   ∧ wa 104   ↔ wb 105   ∧ w3a 980   = wceq 1372   ∈ wcel 2175   class class class wbr 4043  (class class class)co 5943

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 710  ax-5 1469  ax-7 1470  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-8 1526  ax-10 1527  ax-11 1528  ax-i12 1529  ax-bndl 1531  ax-4 1532  ax-17 1548  ax-i9 1552  ax-ial 1556  ax-i5r 1557  ax-ext 2186

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1375  df-nf 1483  df-sb 1785  df-clab 2191  df-cleq 2197  df-clel 2200  df-nfc 2336  df-ral 2488  df-rex 2489  df-v 2773  df-un 3169  df-sn 3638  df-pr 3639  df-op 3641  df-uni 3850  df-br 4044  df-iota 5231  df-fv 5278  df-ov 5946

This theorem is referenced by:  caovord3d  6116  genplt2i  7622  addnqprllem  7639  addnqprulem  7640  mulnqprl  7680  mulnqpru  7681  distrlem4prl  7696  distrlem4pru  7697  1idprl  7702  1idpru  7703  ltexprlemdisj  7718  ltexprlemloc  7719  ltexprlemfl  7721  ltexprlemfu  7723  prplnqu  7732  recexprlem1ssl  7745  recexprlem1ssu  7746  aptiprleml  7751  aptiprlemu  7752  caucvgprlemcanl  7756  cauappcvgprlemlol  7759  cauappcvgprlemloc  7764  cauappcvgprlemladdfu  7766  cauappcvgprlemladdru  7768  cauappcvgprlemladdrl  7769  cauappcvgprlem1  7771  caucvgprlemnkj  7778  caucvgprlemnbj  7779  caucvgprlemlol  7782  caucvgprlemloc  7787  caucvgprlemladdfu  7789  caucvgprlemladdrl  7790  caucvgprprlemnkltj  7801  caucvgprprlemnbj  7805  caucvgprprlemmu  7807  caucvgprprlemlol  7810  caucvgprprlemloc  7815  caucvgprprlemexbt  7818  caucvgprprlemexb  7819  caucvgprprlemaddq  7820  lttrsr  7874  ltsosr  7876  prsrlt  7899  caucvgsrlemoffcau  7910  caucvgsrlemoffgt1  7911  caucvgsrlemoffres  7912  caucvgsr  7914