Description: Commutation is symmetric. Theorem 2(v) in Kalmbach p. 22. ( cmcmi analog.) (Contributed by NM, 7-Nov-2011) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Hypotheses | cmtcom.b | ⊢ 𝐵 = ( Base ‘ 𝐾 ) | |
cmtcom.c | ⊢ 𝐶 = ( cm ‘ 𝐾 ) | ||
Assertion | cmtcomN | ⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 𝐶 𝑌 ↔ 𝑌 𝐶 𝑋 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cmtcom.b | ⊢ 𝐵 = ( Base ‘ 𝐾 ) | |
2 | cmtcom.c | ⊢ 𝐶 = ( cm ‘ 𝐾 ) | |
3 | 1 2 | cmtcomlemN | ⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 𝐶 𝑌 → 𝑌 𝐶 𝑋 ) ) |
4 | 1 2 | cmtcomlemN | ⊢ ( ( 𝐾 ∈ OML ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) → ( 𝑌 𝐶 𝑋 → 𝑋 𝐶 𝑌 ) ) |
5 | 4 | 3com23 | ⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑌 𝐶 𝑋 → 𝑋 𝐶 𝑌 ) ) |
6 | 3 5 | impbid | ⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 𝐶 𝑌 ↔ 𝑌 𝐶 𝑋 ) ) |