Metamath Proof Explorer

Theorem mhmlem

Description: Lemma for mhmmnd and ghmgrp . (Contributed by Paul Chapman, 25-Apr-2008) (Revised by Mario Carneiro, 12-May-2014) (Revised by Thierry Arnoux, 25-Jan-2020)

Ref Expression
Hypotheses ghmgrp.f ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( 𝐹 ‘ ( 𝑥 + 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ⨣ ( 𝐹 ‘ 𝑦 ) ) )
mhmlem.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑋 )
mhmlem.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑋 )
Assertion mhmlem ( 𝜑 → ( 𝐹 ‘ ( 𝐴 + 𝐵 ) ) = ( ( 𝐹 ‘ 𝐴 ) ⨣ ( 𝐹 ‘ 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 ghmgrp.f ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( 𝐹 ‘ ( 𝑥 + 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ⨣ ( 𝐹 ‘ 𝑦 ) ) )
2 mhmlem.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑋 )
3 mhmlem.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑋 )
4 id ⊢ ( 𝜑 → 𝜑 )
5 eleq1 ⊢ ( 𝑥 = 𝐴 → ( 𝑥 ∈ 𝑋 ↔ 𝐴 ∈ 𝑋 ) )
6 5 3anbi2d ⊢ ( 𝑥 = 𝐴 → ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ↔ ( 𝜑 ∧ 𝐴 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) )
7 fvoveq1 ⊢ ( 𝑥 = 𝐴 → ( 𝐹 ‘ ( 𝑥 + 𝑦 ) ) = ( 𝐹 ‘ ( 𝐴 + 𝑦 ) ) )
8 fveq2 ⊢ ( 𝑥 = 𝐴 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝐴 ) )
9 8 oveq1d ⊢ ( 𝑥 = 𝐴 → ( ( 𝐹 ‘ 𝑥 ) ⨣ ( 𝐹 ‘ 𝑦 ) ) = ( ( 𝐹 ‘ 𝐴 ) ⨣ ( 𝐹 ‘ 𝑦 ) ) )
10 7 9 eqeq12d ⊢ ( 𝑥 = 𝐴 → ( ( 𝐹 ‘ ( 𝑥 + 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ⨣ ( 𝐹 ‘ 𝑦 ) ) ↔ ( 𝐹 ‘ ( 𝐴 + 𝑦 ) ) = ( ( 𝐹 ‘ 𝐴 ) ⨣ ( 𝐹 ‘ 𝑦 ) ) ) )
11 6 10 imbi12d ⊢ ( 𝑥 = 𝐴 → ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( 𝐹 ‘ ( 𝑥 + 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ⨣ ( 𝐹 ‘ 𝑦 ) ) ) ↔ ( ( 𝜑 ∧ 𝐴 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( 𝐹 ‘ ( 𝐴 + 𝑦 ) ) = ( ( 𝐹 ‘ 𝐴 ) ⨣ ( 𝐹 ‘ 𝑦 ) ) ) ) )
12 eleq1 ⊢ ( 𝑦 = 𝐵 → ( 𝑦 ∈ 𝑋 ↔ 𝐵 ∈ 𝑋 ) )
13 12 3anbi3d ⊢ ( 𝑦 = 𝐵 → ( ( 𝜑 ∧ 𝐴 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ↔ ( 𝜑 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) )
14 oveq2 ⊢ ( 𝑦 = 𝐵 → ( 𝐴 + 𝑦 ) = ( 𝐴 + 𝐵 ) )
15 14 fveq2d ⊢ ( 𝑦 = 𝐵 → ( 𝐹 ‘ ( 𝐴 + 𝑦 ) ) = ( 𝐹 ‘ ( 𝐴 + 𝐵 ) ) )
16 fveq2 ⊢ ( 𝑦 = 𝐵 → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝐵 ) )
17 16 oveq2d ⊢ ( 𝑦 = 𝐵 → ( ( 𝐹 ‘ 𝐴 ) ⨣ ( 𝐹 ‘ 𝑦 ) ) = ( ( 𝐹 ‘ 𝐴 ) ⨣ ( 𝐹 ‘ 𝐵 ) ) )
18 15 17 eqeq12d ⊢ ( 𝑦 = 𝐵 → ( ( 𝐹 ‘ ( 𝐴 + 𝑦 ) ) = ( ( 𝐹 ‘ 𝐴 ) ⨣ ( 𝐹 ‘ 𝑦 ) ) ↔ ( 𝐹 ‘ ( 𝐴 + 𝐵 ) ) = ( ( 𝐹 ‘ 𝐴 ) ⨣ ( 𝐹 ‘ 𝐵 ) ) ) )
19 13 18 imbi12d ⊢ ( 𝑦 = 𝐵 → ( ( ( 𝜑 ∧ 𝐴 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( 𝐹 ‘ ( 𝐴 + 𝑦 ) ) = ( ( 𝐹 ‘ 𝐴 ) ⨣ ( 𝐹 ‘ 𝑦 ) ) ) ↔ ( ( 𝜑 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐹 ‘ ( 𝐴 + 𝐵 ) ) = ( ( 𝐹 ‘ 𝐴 ) ⨣ ( 𝐹 ‘ 𝐵 ) ) ) ) )
20 11 19 1 vtocl2g ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( 𝜑 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐹 ‘ ( 𝐴 + 𝐵 ) ) = ( ( 𝐹 ‘ 𝐴 ) ⨣ ( 𝐹 ‘ 𝐵 ) ) ) )
21 2 3 20 syl2anc ⊢ ( 𝜑 → ( ( 𝜑 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐹 ‘ ( 𝐴 + 𝐵 ) ) = ( ( 𝐹 ‘ 𝐴 ) ⨣ ( 𝐹 ‘ 𝐵 ) ) ) )
22 4 2 3 21 mp3and ⊢ ( 𝜑 → ( 𝐹 ‘ ( 𝐴 + 𝐵 ) ) = ( ( 𝐹 ‘ 𝐴 ) ⨣ ( 𝐹 ‘ 𝐵 ) ) )