Theorem cdlemkuu 38033

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 6672	. . . . . . . . 9 ⊢ (𝑑 = 𝐷 → (𝑆‘𝑑) = (𝑆‘𝐷))
2		cdlemk3.o2	. . . . . . . . 9 ⊢ 𝑄 = (𝑆‘𝐷)
3	1, 2	syl6eqr 2876	. . . . . . . 8 ⊢ (𝑑 = 𝐷 → (𝑆‘𝑑) = 𝑄)
4	3	fveq1d 6674	. . . . . . 7 ⊢ (𝑑 = 𝐷 → ((𝑆‘𝑑)‘𝑃) = (𝑄‘𝑃))
5		cnveq 5746	. . . . . . . . 9 ⊢ (𝑑 = 𝐷 → ◡𝑑 = ◡𝐷)
6	5	coeq2d 5735	. . . . . . . 8 ⊢ (𝑑 = 𝐷 → (𝑒 ∘ ◡𝑑) = (𝑒 ∘ ◡𝐷))
7	6	fveq2d 6676	. . . . . . 7 ⊢ (𝑑 = 𝐷 → (𝑅‘(𝑒 ∘ ◡𝑑)) = (𝑅‘(𝑒 ∘ ◡𝐷)))
8	4, 7	oveq12d 7176	. . . . . 6 ⊢ (𝑑 = 𝐷 → (((𝑆‘𝑑)‘𝑃) ∨ (𝑅‘(𝑒 ∘ ◡𝑑))) = ((𝑄‘𝑃) ∨ (𝑅‘(𝑒 ∘ ◡𝐷))))
9	8	oveq2d 7174	. . . . 5 ⊢ (𝑑 = 𝐷 → ((𝑃 ∨ (𝑅‘𝑒)) ∧ (((𝑆‘𝑑)‘𝑃) ∨ (𝑅‘(𝑒 ∘ ◡𝑑)))) = ((𝑃 ∨ (𝑅‘𝑒)) ∧ ((𝑄‘𝑃) ∨ (𝑅‘(𝑒 ∘ ◡𝐷)))))
10	9	eqeq2d 2834	. . . 4 ⊢ (𝑑 = 𝐷 → ((𝑗‘𝑃) = ((𝑃 ∨ (𝑅‘𝑒)) ∧ (((𝑆‘𝑑)‘𝑃) ∨ (𝑅‘(𝑒 ∘ ◡𝑑)))) ↔ (𝑗‘𝑃) = ((𝑃 ∨ (𝑅‘𝑒)) ∧ ((𝑄‘𝑃) ∨ (𝑅‘(𝑒 ∘ ◡𝐷))))))
11	10	riotabidv 7118	. . 3 ⊢ (𝑑 = 𝐷 → (℩𝑗 ∈ 𝑇 (𝑗‘𝑃) = ((𝑃 ∨ (𝑅‘𝑒)) ∧ (((𝑆‘𝑑)‘𝑃) ∨ (𝑅‘(𝑒 ∘ ◡𝑑))))) = (℩𝑗 ∈ 𝑇 (𝑗‘𝑃) = ((𝑃 ∨ (𝑅‘𝑒)) ∧ ((𝑄‘𝑃) ∨ (𝑅‘(𝑒 ∘ ◡𝐷))))))
12		fveq2 6672	. . . . . . 7 ⊢ (𝑒 = 𝐺 → (𝑅‘𝑒) = (𝑅‘𝐺))
13	12	oveq2d 7174	. . . . . 6 ⊢ (𝑒 = 𝐺 → (𝑃 ∨ (𝑅‘𝑒)) = (𝑃 ∨ (𝑅‘𝐺)))
14		coeq1 5730	. . . . . . . 8 ⊢ (𝑒 = 𝐺 → (𝑒 ∘ ◡𝐷) = (𝐺 ∘ ◡𝐷))
15	14	fveq2d 6676	. . . . . . 7 ⊢ (𝑒 = 𝐺 → (𝑅‘(𝑒 ∘ ◡𝐷)) = (𝑅‘(𝐺 ∘ ◡𝐷)))
16	15	oveq2d 7174	. . . . . 6 ⊢ (𝑒 = 𝐺 → ((𝑄‘𝑃) ∨ (𝑅‘(𝑒 ∘ ◡𝐷))) = ((𝑄‘𝑃) ∨ (𝑅‘(𝐺 ∘ ◡𝐷))))
17	13, 16	oveq12d 7176	. . . . 5 ⊢ (𝑒 = 𝐺 → ((𝑃 ∨ (𝑅‘𝑒)) ∧ ((𝑄‘𝑃) ∨ (𝑅‘(𝑒 ∘ ◡𝐷)))) = ((𝑃 ∨ (𝑅‘𝐺)) ∧ ((𝑄‘𝑃) ∨ (𝑅‘(𝐺 ∘ ◡𝐷)))))
18	17	eqeq2d 2834	. . . 4 ⊢ (𝑒 = 𝐺 → ((𝑗‘𝑃) = ((𝑃 ∨ (𝑅‘𝑒)) ∧ ((𝑄‘𝑃) ∨ (𝑅‘(𝑒 ∘ ◡𝐷)))) ↔ (𝑗‘𝑃) = ((𝑃 ∨ (𝑅‘𝐺)) ∧ ((𝑄‘𝑃) ∨ (𝑅‘(𝐺 ∘ ◡𝐷))))))
19	18	riotabidv 7118	. . 3 ⊢ (𝑒 = 𝐺 → (℩𝑗 ∈ 𝑇 (𝑗‘𝑃) = ((𝑃 ∨ (𝑅‘𝑒)) ∧ ((𝑄‘𝑃) ∨ (𝑅‘(𝑒 ∘ ◡𝐷))))) = (℩𝑗 ∈ 𝑇 (𝑗‘𝑃) = ((𝑃 ∨ (𝑅‘𝐺)) ∧ ((𝑄‘𝑃) ∨ (𝑅‘(𝐺 ∘ ◡𝐷))))))
20		cdlemk3.u1	. . 3 ⊢ 𝑌 = (𝑑 ∈ 𝑇, 𝑒 ∈ 𝑇 ↦ (℩𝑗 ∈ 𝑇 (𝑗‘𝑃) = ((𝑃 ∨ (𝑅‘𝑒)) ∧ (((𝑆‘𝑑)‘𝑃) ∨ (𝑅‘(𝑒 ∘ ◡𝑑))))))
21		riotaex 7120	. . 3 ⊢ (℩𝑗 ∈ 𝑇 (𝑗‘𝑃) = ((𝑃 ∨ (𝑅‘𝐺)) ∧ ((𝑄‘𝑃) ∨ (𝑅‘(𝐺 ∘ ◡𝐷))))) ∈ V
22	11, 19, 20, 21	ovmpo 7312	. 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 37982	. . 3 ⊢ (𝐺 ∈ 𝑇 → (𝑍‘𝐺) = (℩𝑗 ∈ 𝑇 (𝑗‘𝑃) = ((𝑃 ∨ (𝑅‘𝐺)) ∧ ((𝑄‘𝑃) ∨ (𝑅‘(𝐺 ∘ ◡𝐷))))))
33	32	adantl 484	. 2 ⊢ ((𝐷 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) → (𝑍‘𝐺) = (℩𝑗 ∈ 𝑇 (𝑗‘𝑃) = ((𝑃 ∨ (𝑅‘𝐺)) ∧ ((𝑄‘𝑃) ∨ (𝑅‘(𝐺 ∘ ◡𝐷))))))
34	22, 33	eqtr4d 2861	1 ⊢ ((𝐷 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) → (𝐷𝑌𝐺) = (𝑍‘𝐺))

Syntax hints:   → wi 4   ∧ wa 398   = wceq 1537   ∈ wcel 2114   ↦ cmpt 5148  ^◡ccnv 5556   ∘ ccom 5561  ‘cfv 6357  ℩crio 7115  (class class class)co 7158   ∈ cmpo 7160  Basecbs 16485  lecple 16574  joincjn 17556  meetcmee 17557  Atomscatm 36401  LHypclh 37122  LTrncltrn 37239  trLctrl 37296

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795  ax-sep 5205  ax-nul 5212  ax-pr 5332

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-ral 3145  df-rex 3146  df-rab 3149  df-v 3498  df-sbc 3775  df-dif 3941  df-un 3943  df-in 3945  df-ss 3954  df-nul 4294  df-if 4470  df-sn 4570  df-pr 4572  df-op 4576  df-uni 4841  df-br 5069  df-opab 5131  df-mpt 5149  df-id 5462  df-xp 5563  df-rel 5564  df-cnv 5565  df-co 5566  df-dm 5567  df-iota 6316  df-fun 6359  df-fv 6365  df-riota 7116  df-ov 7161  df-oprab 7162  df-mpo 7163

This theorem is referenced by:  cdlemk31  38034  cdlemkuel-3  38036  cdlemkuv2-3N  38037  cdlemk18-3N  38038  cdlemk22-3  38039  cdlemkyu  38065