Step |
Hyp |
Ref |
Expression |
1 |
|
cmt2.b |
⊢ 𝐵 = ( Base ‘ 𝐾 ) |
2 |
|
cmt2.o |
⊢ ⊥ = ( oc ‘ 𝐾 ) |
3 |
|
cmt2.c |
⊢ 𝐶 = ( cm ‘ 𝐾 ) |
4 |
1 2 3
|
cmt2N |
⊢ ( ( 𝐾 ∈ OML ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) → ( 𝑌 𝐶 𝑋 ↔ 𝑌 𝐶 ( ⊥ ‘ 𝑋 ) ) ) |
5 |
4
|
3com23 |
⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑌 𝐶 𝑋 ↔ 𝑌 𝐶 ( ⊥ ‘ 𝑋 ) ) ) |
6 |
1 3
|
cmtcomN |
⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 𝐶 𝑌 ↔ 𝑌 𝐶 𝑋 ) ) |
7 |
|
omlop |
⊢ ( 𝐾 ∈ OML → 𝐾 ∈ OP ) |
8 |
7
|
3ad2ant1 |
⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → 𝐾 ∈ OP ) |
9 |
|
simp2 |
⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → 𝑋 ∈ 𝐵 ) |
10 |
1 2
|
opoccl |
⊢ ( ( 𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ) → ( ⊥ ‘ 𝑋 ) ∈ 𝐵 ) |
11 |
8 9 10
|
syl2anc |
⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ⊥ ‘ 𝑋 ) ∈ 𝐵 ) |
12 |
1 3
|
cmtcomN |
⊢ ( ( 𝐾 ∈ OML ∧ ( ⊥ ‘ 𝑋 ) ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( ⊥ ‘ 𝑋 ) 𝐶 𝑌 ↔ 𝑌 𝐶 ( ⊥ ‘ 𝑋 ) ) ) |
13 |
11 12
|
syld3an2 |
⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( ⊥ ‘ 𝑋 ) 𝐶 𝑌 ↔ 𝑌 𝐶 ( ⊥ ‘ 𝑋 ) ) ) |
14 |
5 6 13
|
3bitr4d |
⊢ ( ( 𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 𝐶 𝑌 ↔ ( ⊥ ‘ 𝑋 ) 𝐶 𝑌 ) ) |