Theorem cdlemkuu 41650

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 6883	. . . . . . . . 9 ⊢ (𝑑 = 𝐷 → (𝑆‘𝑑) = (𝑆‘𝐷))
2		cdlemk3.o2	. . . . . . . . 9 ⊢ 𝑄 = (𝑆‘𝐷)
3	1, 2	eqtr4di 2816	. . . . . . . 8 ⊢ (𝑑 = 𝐷 → (𝑆‘𝑑) = 𝑄)
4	3	fveq1d 6885	. . . . . . 7 ⊢ (𝑑 = 𝐷 → ((𝑆‘𝑑)‘𝑃) = (𝑄‘𝑃))
5		cnveq 5861	. . . . . . . . 9 ⊢ (𝑑 = 𝐷 → ◡𝑑 = ◡𝐷)
6	5	coeq2d 5850	. . . . . . . 8 ⊢ (𝑑 = 𝐷 → (𝑒 ∘ ◡𝑑) = (𝑒 ∘ ◡𝐷))
7	6	fveq2d 6887	. . . . . . 7 ⊢ (𝑑 = 𝐷 → (𝑅‘(𝑒 ∘ ◡𝑑)) = (𝑅‘(𝑒 ∘ ◡𝐷)))
8	4, 7	oveq12d 7430	. . . . . 6 ⊢ (𝑑 = 𝐷 → (((𝑆‘𝑑)‘𝑃) ∨ (𝑅‘(𝑒 ∘ ◡𝑑))) = ((𝑄‘𝑃) ∨ (𝑅‘(𝑒 ∘ ◡𝐷))))
9	8	oveq2d 7428	. . . . 5 ⊢ (𝑑 = 𝐷 → ((𝑃 ∨ (𝑅‘𝑒)) ∧ (((𝑆‘𝑑)‘𝑃) ∨ (𝑅‘(𝑒 ∘ ◡𝑑)))) = ((𝑃 ∨ (𝑅‘𝑒)) ∧ ((𝑄‘𝑃) ∨ (𝑅‘(𝑒 ∘ ◡𝐷)))))
10	9	eqeq2d 2774	. . . 4 ⊢ (𝑑 = 𝐷 → ((𝑗‘𝑃) = ((𝑃 ∨ (𝑅‘𝑒)) ∧ (((𝑆‘𝑑)‘𝑃) ∨ (𝑅‘(𝑒 ∘ ◡𝑑)))) ↔ (𝑗‘𝑃) = ((𝑃 ∨ (𝑅‘𝑒)) ∧ ((𝑄‘𝑃) ∨ (𝑅‘(𝑒 ∘ ◡𝐷))))))
11	10	riotabidv 7371	. . 3 ⊢ (𝑑 = 𝐷 → (℩𝑗 ∈ 𝑇 (𝑗‘𝑃) = ((𝑃 ∨ (𝑅‘𝑒)) ∧ (((𝑆‘𝑑)‘𝑃) ∨ (𝑅‘(𝑒 ∘ ◡𝑑))))) = (℩𝑗 ∈ 𝑇 (𝑗‘𝑃) = ((𝑃 ∨ (𝑅‘𝑒)) ∧ ((𝑄‘𝑃) ∨ (𝑅‘(𝑒 ∘ ◡𝐷))))))
12		fveq2 6883	. . . . . . 7 ⊢ (𝑒 = 𝐺 → (𝑅‘𝑒) = (𝑅‘𝐺))
13	12	oveq2d 7428	. . . . . 6 ⊢ (𝑒 = 𝐺 → (𝑃 ∨ (𝑅‘𝑒)) = (𝑃 ∨ (𝑅‘𝐺)))
14		coeq1 5845	. . . . . . . 8 ⊢ (𝑒 = 𝐺 → (𝑒 ∘ ◡𝐷) = (𝐺 ∘ ◡𝐷))
15	14	fveq2d 6887	. . . . . . 7 ⊢ (𝑒 = 𝐺 → (𝑅‘(𝑒 ∘ ◡𝐷)) = (𝑅‘(𝐺 ∘ ◡𝐷)))
16	15	oveq2d 7428	. . . . . 6 ⊢ (𝑒 = 𝐺 → ((𝑄‘𝑃) ∨ (𝑅‘(𝑒 ∘ ◡𝐷))) = ((𝑄‘𝑃) ∨ (𝑅‘(𝐺 ∘ ◡𝐷))))
17	13, 16	oveq12d 7430	. . . . 5 ⊢ (𝑒 = 𝐺 → ((𝑃 ∨ (𝑅‘𝑒)) ∧ ((𝑄‘𝑃) ∨ (𝑅‘(𝑒 ∘ ◡𝐷)))) = ((𝑃 ∨ (𝑅‘𝐺)) ∧ ((𝑄‘𝑃) ∨ (𝑅‘(𝐺 ∘ ◡𝐷)))))
18	17	eqeq2d 2774	. . . 4 ⊢ (𝑒 = 𝐺 → ((𝑗‘𝑃) = ((𝑃 ∨ (𝑅‘𝑒)) ∧ ((𝑄‘𝑃) ∨ (𝑅‘(𝑒 ∘ ◡𝐷)))) ↔ (𝑗‘𝑃) = ((𝑃 ∨ (𝑅‘𝐺)) ∧ ((𝑄‘𝑃) ∨ (𝑅‘(𝐺 ∘ ◡𝐷))))))
19	18	riotabidv 7371	. . 3 ⊢ (𝑒 = 𝐺 → (℩𝑗 ∈ 𝑇 (𝑗‘𝑃) = ((𝑃 ∨ (𝑅‘𝑒)) ∧ ((𝑄‘𝑃) ∨ (𝑅‘(𝑒 ∘ ◡𝐷))))) = (℩𝑗 ∈ 𝑇 (𝑗‘𝑃) = ((𝑃 ∨ (𝑅‘𝐺)) ∧ ((𝑄‘𝑃) ∨ (𝑅‘(𝐺 ∘ ◡𝐷))))))
20		cdlemk3.u1	. . 3 ⊢ 𝑌 = (𝑑 ∈ 𝑇, 𝑒 ∈ 𝑇 ↦ (℩𝑗 ∈ 𝑇 (𝑗‘𝑃) = ((𝑃 ∨ (𝑅‘𝑒)) ∧ (((𝑆‘𝑑)‘𝑃) ∨ (𝑅‘(𝑒 ∘ ◡𝑑))))))
21		riotaex 7373	. . 3 ⊢ (℩𝑗 ∈ 𝑇 (𝑗‘𝑃) = ((𝑃 ∨ (𝑅‘𝐺)) ∧ ((𝑄‘𝑃) ∨ (𝑅‘(𝐺 ∘ ◡𝐷))))) ∈ V
22	11, 19, 20, 21	ovmpo 7572	. 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 41599	. . 3 ⊢ (𝐺 ∈ 𝑇 → (𝑍‘𝐺) = (℩𝑗 ∈ 𝑇 (𝑗‘𝑃) = ((𝑃 ∨ (𝑅‘𝐺)) ∧ ((𝑄‘𝑃) ∨ (𝑅‘(𝐺 ∘ ◡𝐷))))))
33	32	adantl 486	. 2 ⊢ ((𝐷 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) → (𝑍‘𝐺) = (℩𝑗 ∈ 𝑇 (𝑗‘𝑃) = ((𝑃 ∨ (𝑅‘𝐺)) ∧ ((𝑄‘𝑃) ∨ (𝑅‘(𝐺 ∘ ◡𝐷))))))
34	22, 33	eqtr4d 2801	1 ⊢ ((𝐷 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) → (𝐷𝑌𝐺) = (𝑍‘𝐺))

Syntax hints:   → wi 4   ∧ wa 400   = wceq 1570   ∈ wcel 2143   ↦ cmpt 5193  ^◡ccnv 5662   ∘ ccom 5667  ‘cfv 6538  ℩crio 7368  (class class class)co 7412   ∈ cmpo 7414  Basecbs 17270  lecple 17318  joincjn 18368  meetcmee 18369  Atomscatm 40018  LHypclh 40739  LTrncltrn 40856  trLctrl 40913

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5258  ax-nul 5270  ax-pr 5406

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-sbc 3746  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4288  df-if 4489  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4874  df-br 5111  df-opab 5175  df-mpt 5194  df-id 5558  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-iota 6494  df-fun 6540  df-fv 6546  df-riota 7369  df-ov 7415  df-oprab 7416  df-mpo 7417

This theorem is referenced by:  cdlemk31  41651  cdlemkuel-3  41653  cdlemkuv2-3N  41654  cdlemk18-3N  41655  cdlemk22-3  41656  cdlemkyu  41682