trlcocnv - Mathbox for Norm Megill

	Mathbox for Norm Megill		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > trlcocnv		Structured version Visualization version GIF version

Theorem trlcocnv 38346

Description: Swap the arguments of the trace of a composition with converse. (Contributed by NM, 1-Jul-2013.)

**Hypotheses**
Ref	Expression
trlcocnv.h	⊢ 𝐻 = (LHyp‘𝐾)
trlcocnv.t	⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)
trlcocnv.r	⊢ 𝑅 = ((trL‘𝐾)‘𝑊)

**Assertion**
Ref	Expression
trlcocnv	⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) → (𝑅‘(𝐹 ∘ ^◡𝐺)) = (𝑅‘(𝐺 ∘ ^◡𝐹)))

**Proof of Theorem trlcocnv**
Step	Hyp	Ref	Expression
1		cnvco 5722	. . . 4 ⊢ ^◡(𝐹 ∘ ^◡𝐺) = (^◡^◡𝐺 ∘ ^◡𝐹)
2		cocnvcnv1 6084	. . . 4 ⊢ (^◡^◡𝐺 ∘ ^◡𝐹) = (𝐺 ∘ ^◡𝐹)
3	1, 2	eqtri 2761	. . 3 ⊢ ^◡(𝐹 ∘ ^◡𝐺) = (𝐺 ∘ ^◡𝐹)
4	3	fveq2i 6671	. 2 ⊢ (𝑅‘^◡(𝐹 ∘ ^◡𝐺)) = (𝑅‘(𝐺 ∘ ^◡𝐹))
5		simp1 1137	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
6		trlcocnv.h	. . . . . 6 ⊢ 𝐻 = (LHyp‘𝐾)
7		trlcocnv.t	. . . . . 6 ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)
8	6, 7	ltrncnv 37772	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐺 ∈ 𝑇) → ^◡𝐺 ∈ 𝑇)
9	8	3adant2 1132	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) → ^◡𝐺 ∈ 𝑇)
10	6, 7	ltrnco 38345	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ ^◡𝐺 ∈ 𝑇) → (𝐹 ∘ ^◡𝐺) ∈ 𝑇)
11	9, 10	syld3an3 1410	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) → (𝐹 ∘ ^◡𝐺) ∈ 𝑇)
12		trlcocnv.r	. . . 4 ⊢ 𝑅 = ((trL‘𝐾)‘𝑊)
13	6, 7, 12	trlcnv 37791	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∘ ^◡𝐺) ∈ 𝑇) → (𝑅‘^◡(𝐹 ∘ ^◡𝐺)) = (𝑅‘(𝐹 ∘ ^◡𝐺)))
14	5, 11, 13	syl2anc 587	. 2 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) → (𝑅‘^◡(𝐹 ∘ ^◡𝐺)) = (𝑅‘(𝐹 ∘ ^◡𝐺)))
15	4, 14	syl5reqr 2788	1 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) → (𝑅‘(𝐹 ∘ ^◡𝐺)) = (𝑅‘(𝐺 ∘ ^◡𝐹)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 399 ∧ w3a 1088 = wceq 1542 ∈ wcel 2113 ^◡ccnv 5518 ∘ ccom 5523 ‘cfv 6333 HLchlt 36976 LHypclh 37610 LTrncltrn 37727 trLctrl 37784

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1916 ax-6 1974 ax-7 2019 ax-8 2115 ax-9 2123 ax-10 2144 ax-11 2161 ax-12 2178 ax-ext 2710 ax-rep 5151 ax-sep 5164 ax-nul 5171 ax-pow 5229 ax-pr 5293 ax-un 7473 ax-riotaBAD 36579

This theorem depends on definitions: df-bi 210 df-an 400 df-or 847 df-3or 1089 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1787 df-nf 1791 df-sb 2074 df-mo 2540 df-eu 2570 df-clab 2717 df-cleq 2730 df-clel 2811 df-nfc 2881 df-ne 2935 df-ral 3058 df-rex 3059 df-reu 3060 df-rmo 3061 df-rab 3062 df-v 3399 df-sbc 3680 df-csb 3789 df-dif 3844 df-un 3846 df-in 3848 df-ss 3858 df-nul 4210 df-if 4412 df-pw 4487 df-sn 4514 df-pr 4516 df-op 4520 df-uni 4794 df-iun 4880 df-iin 4881 df-br 5028 df-opab 5090 df-mpt 5108 df-id 5425 df-xp 5525 df-rel 5526 df-cnv 5527 df-co 5528 df-dm 5529 df-rn 5530 df-res 5531 df-ima 5532 df-iota 6291 df-fun 6335 df-fn 6336 df-f 6337 df-f1 6338 df-fo 6339 df-f1o 6340 df-fv 6341 df-riota 7121 df-ov 7167 df-oprab 7168 df-mpo 7169 df-1st 7707 df-2nd 7708 df-undef 7961 df-map 8432 df-proset 17647 df-poset 17665 df-plt 17677 df-lub 17693 df-glb 17694 df-join 17695 df-meet 17696 df-p0 17758 df-p1 17759 df-lat 17765 df-clat 17827 df-oposet 36802 df-ol 36804 df-oml 36805 df-covers 36892 df-ats 36893 df-atl 36924 df-cvlat 36948 df-hlat 36977 df-llines 37124 df-lplanes 37125 df-lvols 37126 df-lines 37127 df-psubsp 37129 df-pmap 37130 df-padd 37422 df-lhyp 37614 df-laut 37615 df-ldil 37730 df-ltrn 37731 df-trl 37785

This theorem is referenced by: cdlemk9bN 38466 cdlemk14 38480 cdlemk21N 38499 cdlemk20 38500 cdlemk22 38519 cdlemkfid1N 38547

W3C validator