Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > hlcomd | Structured version Visualization version GIF version |
Description: The half-line relation commutes. Theorem 6.6 of [Schwabhauser] p. 44. (Contributed by Thierry Arnoux, 21-Feb-2020.) |
Ref | Expression |
---|---|
ishlg.p | ⊢ 𝑃 = (Base‘𝐺) |
ishlg.i | ⊢ 𝐼 = (Itv‘𝐺) |
ishlg.k | ⊢ 𝐾 = (hlG‘𝐺) |
ishlg.a | ⊢ (𝜑 → 𝐴 ∈ 𝑃) |
ishlg.b | ⊢ (𝜑 → 𝐵 ∈ 𝑃) |
ishlg.c | ⊢ (𝜑 → 𝐶 ∈ 𝑃) |
ishlg.g | ⊢ (𝜑 → 𝐺 ∈ 𝑉) |
hlcomd.1 | ⊢ (𝜑 → 𝐴(𝐾‘𝐶)𝐵) |
Ref | Expression |
---|---|
hlcomd | ⊢ (𝜑 → 𝐵(𝐾‘𝐶)𝐴) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | hlcomd.1 | . 2 ⊢ (𝜑 → 𝐴(𝐾‘𝐶)𝐵) | |
2 | ishlg.p | . . 3 ⊢ 𝑃 = (Base‘𝐺) | |
3 | ishlg.i | . . 3 ⊢ 𝐼 = (Itv‘𝐺) | |
4 | ishlg.k | . . 3 ⊢ 𝐾 = (hlG‘𝐺) | |
5 | ishlg.a | . . 3 ⊢ (𝜑 → 𝐴 ∈ 𝑃) | |
6 | ishlg.b | . . 3 ⊢ (𝜑 → 𝐵 ∈ 𝑃) | |
7 | ishlg.c | . . 3 ⊢ (𝜑 → 𝐶 ∈ 𝑃) | |
8 | ishlg.g | . . 3 ⊢ (𝜑 → 𝐺 ∈ 𝑉) | |
9 | 2, 3, 4, 5, 6, 7, 8 | hlcomb 26974 | . 2 ⊢ (𝜑 → (𝐴(𝐾‘𝐶)𝐵 ↔ 𝐵(𝐾‘𝐶)𝐴)) |
10 | 1, 9 | mpbid 231 | 1 ⊢ (𝜑 → 𝐵(𝐾‘𝐶)𝐴) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1539 ∈ wcel 2106 class class class wbr 5073 ‘cfv 6426 Basecbs 16922 Itvcitv 26804 hlGchlg 26971 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2709 ax-rep 5208 ax-sep 5221 ax-nul 5228 ax-pow 5286 ax-pr 5350 ax-un 7578 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1783 df-nf 1787 df-sb 2068 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2816 df-nfc 2889 df-ne 2944 df-ral 3069 df-rex 3070 df-reu 3071 df-rab 3073 df-v 3431 df-sbc 3716 df-csb 3832 df-dif 3889 df-un 3891 df-in 3893 df-ss 3903 df-nul 4257 df-if 4460 df-pw 4535 df-sn 4562 df-pr 4564 df-op 4568 df-uni 4840 df-iun 4926 df-br 5074 df-opab 5136 df-mpt 5157 df-id 5484 df-xp 5590 df-rel 5591 df-cnv 5592 df-co 5593 df-dm 5594 df-rn 5595 df-res 5596 df-ima 5597 df-iota 6384 df-fun 6428 df-fn 6429 df-f 6430 df-f1 6431 df-fo 6432 df-f1o 6433 df-fv 6434 df-ov 7270 df-hlg 26972 |
This theorem is referenced by: hlcgreulem 26988 opphllem4 27121 opphllem5 27122 opphl 27125 hlpasch 27127 lnopp2hpgb 27134 colhp 27141 cgrahl1 27187 cgrahl2 27188 cgrahl 27198 cgracol 27199 dfcgra2 27201 sacgr 27202 acopy 27204 acopyeu 27205 inaghl 27216 tgasa1 27229 |
Copyright terms: Public domain | W3C validator |