Theorem cdlemkuu 38836

Description: Convert between function and operation forms of 𝑌. TODO: Use operation form everywhere. (Contributed by NM, 6-Jul-2013.)

Hypotheses

Ref	Expression
cdlemk3.b	⊢ 𝐵 = (Base‘𝐾)
cdlemk3.l	⊢ ≤ = (le‘𝐾)
cdlemk3.j	⊢ ∨ = (join‘𝐾)
cdlemk3.m	⊢ ∧ = (meet‘𝐾)
cdlemk3.a	⊢ 𝐴 = (Atoms‘𝐾)
cdlemk3.h	⊢ 𝐻 = (LHyp‘𝐾)
cdlemk3.t	⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)
cdlemk3.r	⊢ 𝑅 = ((trL‘𝐾)‘𝑊)
cdlemk3.s	⊢ 𝑆 = (𝑓 ∈ 𝑇 ↦ (℩𝑖 ∈ 𝑇 (𝑖‘𝑃) = ((𝑃 ∨ (𝑅‘𝑓)) ∧ ((𝑁‘𝑃) ∨ (𝑅‘(𝑓 ∘ ◡𝐹))))))
cdlemk3.u1	⊢ 𝑌 = (𝑑 ∈ 𝑇, 𝑒 ∈ 𝑇 ↦ (℩𝑗 ∈ 𝑇 (𝑗‘𝑃) = ((𝑃 ∨ (𝑅‘𝑒)) ∧ (((𝑆‘𝑑)‘𝑃) ∨ (𝑅‘(𝑒 ∘ ◡𝑑))))))
cdlemk3.o2	⊢ 𝑄 = (𝑆‘𝐷)
cdlemk3.u2	⊢ 𝑍 = (𝑒 ∈ 𝑇 ↦ (℩𝑗 ∈ 𝑇 (𝑗‘𝑃) = ((𝑃 ∨ (𝑅‘𝑒)) ∧ ((𝑄‘𝑃) ∨ (𝑅‘(𝑒 ∘ ◡𝐷))))))

Assertion

Ref	Expression
cdlemkuu	⊢ ((𝐷 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) → (𝐷𝑌𝐺) = (𝑍‘𝐺))

Distinct variable groups:   𝑒,𝑑,𝑓,𝑖, ∧   ≤ ,𝑖   ∨ ,𝑑,𝑒,𝑓,𝑖   𝐴,𝑖   𝑗,𝑑,𝐷,𝑒,𝑓,𝑖   𝑓,𝐹,𝑖   𝐺,𝑑,𝑒,𝑗   𝑖,𝐻   𝑖,𝐾   𝑓,𝑁,𝑖   𝑃,𝑑,𝑒,𝑓,𝑖   𝑄,𝑑,𝑒   𝑅,𝑑,𝑒,𝑓,𝑖   𝑇,𝑑,𝑒,𝑓,𝑖   𝑊,𝑑,𝑒,𝑓,𝑖

Allowed substitution hints:   𝐴(𝑒,𝑓,𝑗,𝑑)   𝐵(𝑒,𝑓,𝑖,𝑗,𝑑)   𝑃(𝑗)   𝑄(𝑓,𝑖,𝑗)   𝑅(𝑗)   𝑆(𝑒,𝑓,𝑖,𝑗,𝑑)   𝑇(𝑗)   𝐹(𝑒,𝑗,𝑑)   𝐺(𝑓,𝑖)   𝐻(𝑒,𝑓,𝑗,𝑑)   ∨ (𝑗)   𝐾(𝑒,𝑓,𝑗,𝑑)   ≤ (𝑒,𝑓,𝑗,𝑑)   ∧ (𝑗)   𝑁(𝑒,𝑗,𝑑)   𝑊(𝑗)   𝑌(𝑒,𝑓,𝑖,𝑗,𝑑)   𝑍(𝑒,𝑓,𝑖,𝑗,𝑑)

Proof of Theorem cdlemkuu

Step	Hyp	Ref	Expression
1		fveq2 6756	. . . . . . . . 9 ⊢ (𝑑 = 𝐷 → (𝑆‘𝑑) = (𝑆‘𝐷))
2		cdlemk3.o2	. . . . . . . . 9 ⊢ 𝑄 = (𝑆‘𝐷)
3	1, 2	eqtr4di 2797	. . . . . . . 8 ⊢ (𝑑 = 𝐷 → (𝑆‘𝑑) = 𝑄)
4	3	fveq1d 6758	. . . . . . 7 ⊢ (𝑑 = 𝐷 → ((𝑆‘𝑑)‘𝑃) = (𝑄‘𝑃))
5		cnveq 5771	. . . . . . . . 9 ⊢ (𝑑 = 𝐷 → ◡𝑑 = ◡𝐷)
6	5	coeq2d 5760	. . . . . . . 8 ⊢ (𝑑 = 𝐷 → (𝑒 ∘ ◡𝑑) = (𝑒 ∘ ◡𝐷))
7	6	fveq2d 6760	. . . . . . 7 ⊢ (𝑑 = 𝐷 → (𝑅‘(𝑒 ∘ ◡𝑑)) = (𝑅‘(𝑒 ∘ ◡𝐷)))
8	4, 7	oveq12d 7273	. . . . . 6 ⊢ (𝑑 = 𝐷 → (((𝑆‘𝑑)‘𝑃) ∨ (𝑅‘(𝑒 ∘ ◡𝑑))) = ((𝑄‘𝑃) ∨ (𝑅‘(𝑒 ∘ ◡𝐷))))
9	8	oveq2d 7271	. . . . 5 ⊢ (𝑑 = 𝐷 → ((𝑃 ∨ (𝑅‘𝑒)) ∧ (((𝑆‘𝑑)‘𝑃) ∨ (𝑅‘(𝑒 ∘ ◡𝑑)))) = ((𝑃 ∨ (𝑅‘𝑒)) ∧ ((𝑄‘𝑃) ∨ (𝑅‘(𝑒 ∘ ◡𝐷)))))
10	9	eqeq2d 2749	. . . 4 ⊢ (𝑑 = 𝐷 → ((𝑗‘𝑃) = ((𝑃 ∨ (𝑅‘𝑒)) ∧ (((𝑆‘𝑑)‘𝑃) ∨ (𝑅‘(𝑒 ∘ ◡𝑑)))) ↔ (𝑗‘𝑃) = ((𝑃 ∨ (𝑅‘𝑒)) ∧ ((𝑄‘𝑃) ∨ (𝑅‘(𝑒 ∘ ◡𝐷))))))
11	10	riotabidv 7214	. . 3 ⊢ (𝑑 = 𝐷 → (℩𝑗 ∈ 𝑇 (𝑗‘𝑃) = ((𝑃 ∨ (𝑅‘𝑒)) ∧ (((𝑆‘𝑑)‘𝑃) ∨ (𝑅‘(𝑒 ∘ ◡𝑑))))) = (℩𝑗 ∈ 𝑇 (𝑗‘𝑃) = ((𝑃 ∨ (𝑅‘𝑒)) ∧ ((𝑄‘𝑃) ∨ (𝑅‘(𝑒 ∘ ◡𝐷))))))
12		fveq2 6756	. . . . . . 7 ⊢ (𝑒 = 𝐺 → (𝑅‘𝑒) = (𝑅‘𝐺))
13	12	oveq2d 7271	. . . . . 6 ⊢ (𝑒 = 𝐺 → (𝑃 ∨ (𝑅‘𝑒)) = (𝑃 ∨ (𝑅‘𝐺)))
14		coeq1 5755	. . . . . . . 8 ⊢ (𝑒 = 𝐺 → (𝑒 ∘ ◡𝐷) = (𝐺 ∘ ◡𝐷))
15	14	fveq2d 6760	. . . . . . 7 ⊢ (𝑒 = 𝐺 → (𝑅‘(𝑒 ∘ ◡𝐷)) = (𝑅‘(𝐺 ∘ ◡𝐷)))
16	15	oveq2d 7271	. . . . . 6 ⊢ (𝑒 = 𝐺 → ((𝑄‘𝑃) ∨ (𝑅‘(𝑒 ∘ ◡𝐷))) = ((𝑄‘𝑃) ∨ (𝑅‘(𝐺 ∘ ◡𝐷))))
17	13, 16	oveq12d 7273	. . . . 5 ⊢ (𝑒 = 𝐺 → ((𝑃 ∨ (𝑅‘𝑒)) ∧ ((𝑄‘𝑃) ∨ (𝑅‘(𝑒 ∘ ◡𝐷)))) = ((𝑃 ∨ (𝑅‘𝐺)) ∧ ((𝑄‘𝑃) ∨ (𝑅‘(𝐺 ∘ ◡𝐷)))))
18	17	eqeq2d 2749	. . . 4 ⊢ (𝑒 = 𝐺 → ((𝑗‘𝑃) = ((𝑃 ∨ (𝑅‘𝑒)) ∧ ((𝑄‘𝑃) ∨ (𝑅‘(𝑒 ∘ ◡𝐷)))) ↔ (𝑗‘𝑃) = ((𝑃 ∨ (𝑅‘𝐺)) ∧ ((𝑄‘𝑃) ∨ (𝑅‘(𝐺 ∘ ◡𝐷))))))
19	18	riotabidv 7214	. . 3 ⊢ (𝑒 = 𝐺 → (℩𝑗 ∈ 𝑇 (𝑗‘𝑃) = ((𝑃 ∨ (𝑅‘𝑒)) ∧ ((𝑄‘𝑃) ∨ (𝑅‘(𝑒 ∘ ◡𝐷))))) = (℩𝑗 ∈ 𝑇 (𝑗‘𝑃) = ((𝑃 ∨ (𝑅‘𝐺)) ∧ ((𝑄‘𝑃) ∨ (𝑅‘(𝐺 ∘ ◡𝐷))))))
20		cdlemk3.u1	. . 3 ⊢ 𝑌 = (𝑑 ∈ 𝑇, 𝑒 ∈ 𝑇 ↦ (℩𝑗 ∈ 𝑇 (𝑗‘𝑃) = ((𝑃 ∨ (𝑅‘𝑒)) ∧ (((𝑆‘𝑑)‘𝑃) ∨ (𝑅‘(𝑒 ∘ ◡𝑑))))))
21		riotaex 7216	. . 3 ⊢ (℩𝑗 ∈ 𝑇 (𝑗‘𝑃) = ((𝑃 ∨ (𝑅‘𝐺)) ∧ ((𝑄‘𝑃) ∨ (𝑅‘(𝐺 ∘ ◡𝐷))))) ∈ V
22	11, 19, 20, 21	ovmpo 7411	. 2 ⊢ ((𝐷 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) → (𝐷𝑌𝐺) = (℩𝑗 ∈ 𝑇 (𝑗‘𝑃) = ((𝑃 ∨ (𝑅‘𝐺)) ∧ ((𝑄‘𝑃) ∨ (𝑅‘(𝐺 ∘ ◡𝐷))))))
23		cdlemk3.b	. . . 4 ⊢ 𝐵 = (Base‘𝐾)
24		cdlemk3.l	. . . 4 ⊢ ≤ = (le‘𝐾)
25		cdlemk3.j	. . . 4 ⊢ ∨ = (join‘𝐾)
26		cdlemk3.a	. . . 4 ⊢ 𝐴 = (Atoms‘𝐾)
27		cdlemk3.h	. . . 4 ⊢ 𝐻 = (LHyp‘𝐾)
28		cdlemk3.t	. . . 4 ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)
29		cdlemk3.r	. . . 4 ⊢ 𝑅 = ((trL‘𝐾)‘𝑊)
30		cdlemk3.m	. . . 4 ⊢ ∧ = (meet‘𝐾)
31		cdlemk3.u2	. . . 4 ⊢ 𝑍 = (𝑒 ∈ 𝑇 ↦ (℩𝑗 ∈ 𝑇 (𝑗‘𝑃) = ((𝑃 ∨ (𝑅‘𝑒)) ∧ ((𝑄‘𝑃) ∨ (𝑅‘(𝑒 ∘ ◡𝐷))))))
32	23, 24, 25, 26, 27, 28, 29, 30, 31	cdlemksv 38785	. . 3 ⊢ (𝐺 ∈ 𝑇 → (𝑍‘𝐺) = (℩𝑗 ∈ 𝑇 (𝑗‘𝑃) = ((𝑃 ∨ (𝑅‘𝐺)) ∧ ((𝑄‘𝑃) ∨ (𝑅‘(𝐺 ∘ ◡𝐷))))))
33	32	adantl 481	. 2 ⊢ ((𝐷 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) → (𝑍‘𝐺) = (℩𝑗 ∈ 𝑇 (𝑗‘𝑃) = ((𝑃 ∨ (𝑅‘𝐺)) ∧ ((𝑄‘𝑃) ∨ (𝑅‘(𝐺 ∘ ◡𝐷))))))
34	22, 33	eqtr4d 2781	1 ⊢ ((𝐷 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) → (𝐷𝑌𝐺) = (𝑍‘𝐺))

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1539   ∈ wcel 2108   ↦ cmpt 5153  ^◡ccnv 5579   ∘ ccom 5584  ‘cfv 6418  ℩crio 7211  (class class class)co 7255   ∈ cmpo 7257  Basecbs 16840  lecple 16895  joincjn 17944  meetcmee 17945  Atomscatm 37204  LHypclh 37925  LTrncltrn 38042  trLctrl 38099

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pr 5347

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ral 3068  df-rex 3069  df-rab 3072  df-v 3424  df-sbc 3712  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-br 5071  df-opab 5133  df-mpt 5154  df-id 5480  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-iota 6376  df-fun 6420  df-fv 6426  df-riota 7212  df-ov 7258  df-oprab 7259  df-mpo 7260

This theorem is referenced by:  cdlemk31  38837  cdlemkuel-3  38839  cdlemkuv2-3N  38840  cdlemk18-3N  38841  cdlemk22-3  38842  cdlemkyu  38868