MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mhmlem Structured version   Visualization version   GIF version
Theorem mhmlem 18896
Description: Lemma for mhmmnd 18898 and ghmgrp 18900. (Contributed by Paul Chapman, 25-Apr-2008.) (Revised by Mario Carneiro, 12-May-2014.) (Revised by Thierry Arnoux, 25-Jan-2020.)
Hypotheses
Ref Expression
ghmgrp.f ((𝜑 ∧ ð‘Ĩ ∈ 𝑋 ∧ ð‘Ķ ∈ 𝑋) → (ðđ‘(ð‘Ĩ + ð‘Ķ)) = ((ðđ‘ð‘Ĩ) âĻĢ (ðđ‘ð‘Ķ)))
mhmlem.a (𝜑 → ðī ∈ 𝑋)
mhmlem.b (𝜑 → ðĩ ∈ 𝑋)
Assertion
Ref Expression
mhmlem (𝜑 → (ðđ‘(ðī + ðĩ)) = ((ðđ‘ðī) âĻĢ (ðđ‘ðĩ)))
Distinct variable groups:   ð‘Ĩ,ðđ,ð‘Ķ   ð‘Ĩ, + ,ð‘Ķ   ð‘Ĩ,𝑋,ð‘Ķ   ð‘Ĩ, âĻĢ ,ð‘Ķ   𝜑,ð‘Ĩ,ð‘Ķ   ð‘Ĩ,ðī,ð‘Ķ   ð‘Ķ,ðĩ
Allowed substitution hint:   ðĩ(ð‘Ĩ)
Proof of Theorem mhmlem
StepHypRef Expression
1 id 22 . 2 (𝜑 → 𝜑)
2 mhmlem.a . 2 (𝜑 → ðī ∈ 𝑋)
3 mhmlem.b . 2 (𝜑 → ðĩ ∈ 𝑋)
4 eleq1 2820 . . . . . 6 (ð‘Ĩ = ðī → (ð‘Ĩ ∈ 𝑋 ↔ ðī ∈ 𝑋))
543anbi2d 1441 . . . . 5 (ð‘Ĩ = ðī → ((𝜑 ∧ ð‘Ĩ ∈ 𝑋 ∧ ð‘Ķ ∈ 𝑋) ↔ (𝜑 ∧ ðī ∈ 𝑋 ∧ ð‘Ķ ∈ 𝑋)))
6 fvoveq1 7400 . . . . . 6 (ð‘Ĩ = ðī → (ðđ‘(ð‘Ĩ + ð‘Ķ)) = (ðđ‘(ðī + ð‘Ķ)))
7 fveq2 6862 . . . . . . 7 (ð‘Ĩ = ðī → (ðđ‘ð‘Ĩ) = (ðđ‘ðī))
87oveq1d 7392 . . . . . 6 (ð‘Ĩ = ðī → ((ðđ‘ð‘Ĩ) âĻĢ (ðđ‘ð‘Ķ)) = ((ðđ‘ðī) âĻĢ (ðđ‘ð‘Ķ)))
96, 8eqeq12d 2747 . . . . 5 (ð‘Ĩ = ðī → ((ðđ‘(ð‘Ĩ + ð‘Ķ)) = ((ðđ‘ð‘Ĩ) âĻĢ (ðđ‘ð‘Ķ)) ↔ (ðđ‘(ðī + ð‘Ķ)) = ((ðđ‘ðī) âĻĢ (ðđ‘ð‘Ķ))))
105, 9imbi12d 344 . . . 4 (ð‘Ĩ = ðī → (((𝜑 ∧ ð‘Ĩ ∈ 𝑋 ∧ ð‘Ķ ∈ 𝑋) → (ðđ‘(ð‘Ĩ + ð‘Ķ)) = ((ðđ‘ð‘Ĩ) âĻĢ (ðđ‘ð‘Ķ))) ↔ ((𝜑 ∧ ðī ∈ 𝑋 ∧ ð‘Ķ ∈ 𝑋) → (ðđ‘(ðī + ð‘Ķ)) = ((ðđ‘ðī) âĻĢ (ðđ‘ð‘Ķ)))))
11 eleq1 2820 . . . . . 6 (ð‘Ķ = ðĩ → (ð‘Ķ ∈ 𝑋 ↔ ðĩ ∈ 𝑋))
12113anbi3d 1442 . . . . 5 (ð‘Ķ = ðĩ → ((𝜑 ∧ ðī ∈ 𝑋 ∧ ð‘Ķ ∈ 𝑋) ↔ (𝜑 ∧ ðī ∈ 𝑋 ∧ ðĩ ∈ 𝑋)))
13 oveq2 7385 . . . . . . 7 (ð‘Ķ = ðĩ → (ðī + ð‘Ķ) = (ðī + ðĩ))
1413fveq2d 6866 . . . . . 6 (ð‘Ķ = ðĩ → (ðđ‘(ðī + ð‘Ķ)) = (ðđ‘(ðī + ðĩ)))
15 fveq2 6862 . . . . . . 7 (ð‘Ķ = ðĩ → (ðđ‘ð‘Ķ) = (ðđ‘ðĩ))
1615oveq2d 7393 . . . . . 6 (ð‘Ķ = ðĩ → ((ðđ‘ðī) âĻĢ (ðđ‘ð‘Ķ)) = ((ðđ‘ðī) âĻĢ (ðđ‘ðĩ)))
1714, 16eqeq12d 2747 . . . . 5 (ð‘Ķ = ðĩ → ((ðđ‘(ðī + ð‘Ķ)) = ((ðđ‘ðī) âĻĢ (ðđ‘ð‘Ķ)) ↔ (ðđ‘(ðī + ðĩ)) = ((ðđ‘ðī) âĻĢ (ðđ‘ðĩ))))
1812, 17imbi12d 344 . . . 4 (ð‘Ķ = ðĩ → (((𝜑 ∧ ðī ∈ 𝑋 ∧ ð‘Ķ ∈ 𝑋) → (ðđ‘(ðī + ð‘Ķ)) = ((ðđ‘ðī) âĻĢ (ðđ‘ð‘Ķ))) ↔ ((𝜑 ∧ ðī ∈ 𝑋 ∧ ðĩ ∈ 𝑋) → (ðđ‘(ðī + ðĩ)) = ((ðđ‘ðī) âĻĢ (ðđ‘ðĩ)))))
19 ghmgrp.f . . . 4 ((𝜑 ∧ ð‘Ĩ ∈ 𝑋 ∧ ð‘Ķ ∈ 𝑋) → (ðđ‘(ð‘Ĩ + ð‘Ķ)) = ((ðđ‘ð‘Ĩ) âĻĢ (ðđ‘ð‘Ķ)))
2010, 18, 19vtocl2g 3545 . . 3 ((ðī ∈ 𝑋 ∧ ðĩ ∈ 𝑋) → ((𝜑 ∧ ðī ∈ 𝑋 ∧ ðĩ ∈ 𝑋) → (ðđ‘(ðī + ðĩ)) = ((ðđ‘ðī) âĻĢ (ðđ‘ðĩ))))
212, 3, 20syl2anc 584 . 2 (𝜑 → ((𝜑 ∧ ðī ∈ 𝑋 ∧ ðĩ ∈ 𝑋) → (ðđ‘(ðī + ðĩ)) = ((ðđ‘ðī) âĻĢ (ðđ‘ðĩ))))
221, 2, 3, 21mp3and 1464 1 (𝜑 → (ðđ‘(ðī + ðĩ)) = ((ðđ‘ðī) âĻĢ (ðđ‘ðĩ)))
Colors of variables: wff setvar class
Syntax hints:   → wi 4   ∧ w3a 1087   = wceq 1541   ∈ wcel 2106  â€˜cfv 6516  (class class class)co 7377
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-rab 3419  df-v 3461  df-dif 3931  df-un 3933  df-in 3935  df-ss 3945  df-nul 4303  df-if 4507  df-sn 4607  df-pr 4609  df-op 4613  df-uni 4886  df-br 5126  df-iota 6468  df-fv 6524  df-ov 7380
This theorem is referenced by:  mhmid  18897  mhmmnd  18898  ghmgrp  18900  ghmcmn  19639
  Copyright terms: Public domain W3C validator