Metamath Proof Explorer

Theorem archiabllem2b

Description: Lemma for archiabl . (Contributed by Thierry Arnoux, 1-May-2018)

Ref Expression
Hypotheses archiabllem.b ⊢ 𝐵 = ( Base ‘ 𝑊 )
archiabllem.0 ⊢ 0 = ( 0g ‘ 𝑊 )
archiabllem.e ⊢ ≤ = ( le ‘ 𝑊 )
archiabllem.t ⊢ < = ( lt ‘ 𝑊 )
archiabllem.m ⊢ · = ( .g ‘ 𝑊 )
archiabllem.g ⊢ ( 𝜑 → 𝑊 ∈ oGrp )
archiabllem.a ⊢ ( 𝜑 → 𝑊 ∈ Archi )
archiabllem2.1 ⊢ + = ( +g ‘ 𝑊 )
archiabllem2.2 ⊢ ( 𝜑 → ( oppg ‘ 𝑊 ) ∈ oGrp )
archiabllem2.3 ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ∧ 0 < 𝑎 ) → ∃ 𝑏 ∈ 𝐵 ( 0 < 𝑏 ∧ 𝑏 < 𝑎 ) )
archiabllem2b.4 ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
archiabllem2b.5 ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
Assertion archiabllem2b ( 𝜑 → ( 𝑋 + 𝑌 ) = ( 𝑌 + 𝑋 ) )

Proof

Step Hyp Ref Expression
1 archiabllem.b ⊢ 𝐵 = ( Base ‘ 𝑊 )
2 archiabllem.0 ⊢ 0 = ( 0g ‘ 𝑊 )
3 archiabllem.e ⊢ ≤ = ( le ‘ 𝑊 )
4 archiabllem.t ⊢ < = ( lt ‘ 𝑊 )
5 archiabllem.m ⊢ · = ( .g ‘ 𝑊 )
6 archiabllem.g ⊢ ( 𝜑 → 𝑊 ∈ oGrp )
7 archiabllem.a ⊢ ( 𝜑 → 𝑊 ∈ Archi )
8 archiabllem2.1 ⊢ + = ( +g ‘ 𝑊 )
9 archiabllem2.2 ⊢ ( 𝜑 → ( oppg ‘ 𝑊 ) ∈ oGrp )
10 archiabllem2.3 ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ∧ 0 < 𝑎 ) → ∃ 𝑏 ∈ 𝐵 ( 0 < 𝑏 ∧ 𝑏 < 𝑎 ) )
11 archiabllem2b.4 ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
12 archiabllem2b.5 ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
13 1 2 3 4 5 6 7 8 9 10 11 12 archiabllem2c ⊢ ( 𝜑 → ¬ ( 𝑋 + 𝑌 ) < ( 𝑌 + 𝑋 ) )
14 1 2 3 4 5 6 7 8 9 10 12 11 archiabllem2c ⊢ ( 𝜑 → ¬ ( 𝑌 + 𝑋 ) < ( 𝑋 + 𝑌 ) )
15 isogrp ⊢ ( 𝑊 ∈ oGrp ↔ ( 𝑊 ∈ Grp ∧ 𝑊 ∈ oMnd ) )
16 15 simprbi ⊢ ( 𝑊 ∈ oGrp → 𝑊 ∈ oMnd )
17 omndtos ⊢ ( 𝑊 ∈ oMnd → 𝑊 ∈ Toset )
18 6 16 17 3syl ⊢ ( 𝜑 → 𝑊 ∈ Toset )
19 ogrpgrp ⊢ ( 𝑊 ∈ oGrp → 𝑊 ∈ Grp )
20 6 19 syl ⊢ ( 𝜑 → 𝑊 ∈ Grp )
21 1 8 grpcl ⊢ ( ( 𝑊 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 + 𝑌 ) ∈ 𝐵 )
22 20 11 12 21 syl3anc ⊢ ( 𝜑 → ( 𝑋 + 𝑌 ) ∈ 𝐵 )
23 1 8 grpcl ⊢ ( ( 𝑊 ∈ Grp ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) → ( 𝑌 + 𝑋 ) ∈ 𝐵 )
24 20 12 11 23 syl3anc ⊢ ( 𝜑 → ( 𝑌 + 𝑋 ) ∈ 𝐵 )
25 1 4 tlt3 ⊢ ( ( 𝑊 ∈ Toset ∧ ( 𝑋 + 𝑌 ) ∈ 𝐵 ∧ ( 𝑌 + 𝑋 ) ∈ 𝐵 ) → ( ( 𝑋 + 𝑌 ) = ( 𝑌 + 𝑋 ) ∨ ( 𝑋 + 𝑌 ) < ( 𝑌 + 𝑋 ) ∨ ( 𝑌 + 𝑋 ) < ( 𝑋 + 𝑌 ) ) )
26 18 22 24 25 syl3anc ⊢ ( 𝜑 → ( ( 𝑋 + 𝑌 ) = ( 𝑌 + 𝑋 ) ∨ ( 𝑋 + 𝑌 ) < ( 𝑌 + 𝑋 ) ∨ ( 𝑌 + 𝑋 ) < ( 𝑋 + 𝑌 ) ) )
27 13 14 26 ecase23d ⊢ ( 𝜑 → ( 𝑋 + 𝑌 ) = ( 𝑌 + 𝑋 ) )