Theorem cdlemkuu 40897

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 6906	. . . . . . . . 9 ⊢ (𝑑 = 𝐷 → (𝑆‘𝑑) = (𝑆‘𝐷))
2		cdlemk3.o2	. . . . . . . . 9 ⊢ 𝑄 = (𝑆‘𝐷)
3	1, 2	eqtr4di 2795	. . . . . . . 8 ⊢ (𝑑 = 𝐷 → (𝑆‘𝑑) = 𝑄)
4	3	fveq1d 6908	. . . . . . 7 ⊢ (𝑑 = 𝐷 → ((𝑆‘𝑑)‘𝑃) = (𝑄‘𝑃))
5		cnveq 5884	. . . . . . . . 9 ⊢ (𝑑 = 𝐷 → ◡𝑑 = ◡𝐷)
6	5	coeq2d 5873	. . . . . . . 8 ⊢ (𝑑 = 𝐷 → (𝑒 ∘ ◡𝑑) = (𝑒 ∘ ◡𝐷))
7	6	fveq2d 6910	. . . . . . 7 ⊢ (𝑑 = 𝐷 → (𝑅‘(𝑒 ∘ ◡𝑑)) = (𝑅‘(𝑒 ∘ ◡𝐷)))
8	4, 7	oveq12d 7449	. . . . . 6 ⊢ (𝑑 = 𝐷 → (((𝑆‘𝑑)‘𝑃) ∨ (𝑅‘(𝑒 ∘ ◡𝑑))) = ((𝑄‘𝑃) ∨ (𝑅‘(𝑒 ∘ ◡𝐷))))
9	8	oveq2d 7447	. . . . 5 ⊢ (𝑑 = 𝐷 → ((𝑃 ∨ (𝑅‘𝑒)) ∧ (((𝑆‘𝑑)‘𝑃) ∨ (𝑅‘(𝑒 ∘ ◡𝑑)))) = ((𝑃 ∨ (𝑅‘𝑒)) ∧ ((𝑄‘𝑃) ∨ (𝑅‘(𝑒 ∘ ◡𝐷)))))
10	9	eqeq2d 2748	. . . 4 ⊢ (𝑑 = 𝐷 → ((𝑗‘𝑃) = ((𝑃 ∨ (𝑅‘𝑒)) ∧ (((𝑆‘𝑑)‘𝑃) ∨ (𝑅‘(𝑒 ∘ ◡𝑑)))) ↔ (𝑗‘𝑃) = ((𝑃 ∨ (𝑅‘𝑒)) ∧ ((𝑄‘𝑃) ∨ (𝑅‘(𝑒 ∘ ◡𝐷))))))
11	10	riotabidv 7390	. . 3 ⊢ (𝑑 = 𝐷 → (℩𝑗 ∈ 𝑇 (𝑗‘𝑃) = ((𝑃 ∨ (𝑅‘𝑒)) ∧ (((𝑆‘𝑑)‘𝑃) ∨ (𝑅‘(𝑒 ∘ ◡𝑑))))) = (℩𝑗 ∈ 𝑇 (𝑗‘𝑃) = ((𝑃 ∨ (𝑅‘𝑒)) ∧ ((𝑄‘𝑃) ∨ (𝑅‘(𝑒 ∘ ◡𝐷))))))
12		fveq2 6906	. . . . . . 7 ⊢ (𝑒 = 𝐺 → (𝑅‘𝑒) = (𝑅‘𝐺))
13	12	oveq2d 7447	. . . . . 6 ⊢ (𝑒 = 𝐺 → (𝑃 ∨ (𝑅‘𝑒)) = (𝑃 ∨ (𝑅‘𝐺)))
14		coeq1 5868	. . . . . . . 8 ⊢ (𝑒 = 𝐺 → (𝑒 ∘ ◡𝐷) = (𝐺 ∘ ◡𝐷))
15	14	fveq2d 6910	. . . . . . 7 ⊢ (𝑒 = 𝐺 → (𝑅‘(𝑒 ∘ ◡𝐷)) = (𝑅‘(𝐺 ∘ ◡𝐷)))
16	15	oveq2d 7447	. . . . . 6 ⊢ (𝑒 = 𝐺 → ((𝑄‘𝑃) ∨ (𝑅‘(𝑒 ∘ ◡𝐷))) = ((𝑄‘𝑃) ∨ (𝑅‘(𝐺 ∘ ◡𝐷))))
17	13, 16	oveq12d 7449	. . . . 5 ⊢ (𝑒 = 𝐺 → ((𝑃 ∨ (𝑅‘𝑒)) ∧ ((𝑄‘𝑃) ∨ (𝑅‘(𝑒 ∘ ◡𝐷)))) = ((𝑃 ∨ (𝑅‘𝐺)) ∧ ((𝑄‘𝑃) ∨ (𝑅‘(𝐺 ∘ ◡𝐷)))))
18	17	eqeq2d 2748	. . . 4 ⊢ (𝑒 = 𝐺 → ((𝑗‘𝑃) = ((𝑃 ∨ (𝑅‘𝑒)) ∧ ((𝑄‘𝑃) ∨ (𝑅‘(𝑒 ∘ ◡𝐷)))) ↔ (𝑗‘𝑃) = ((𝑃 ∨ (𝑅‘𝐺)) ∧ ((𝑄‘𝑃) ∨ (𝑅‘(𝐺 ∘ ◡𝐷))))))
19	18	riotabidv 7390	. . 3 ⊢ (𝑒 = 𝐺 → (℩𝑗 ∈ 𝑇 (𝑗‘𝑃) = ((𝑃 ∨ (𝑅‘𝑒)) ∧ ((𝑄‘𝑃) ∨ (𝑅‘(𝑒 ∘ ◡𝐷))))) = (℩𝑗 ∈ 𝑇 (𝑗‘𝑃) = ((𝑃 ∨ (𝑅‘𝐺)) ∧ ((𝑄‘𝑃) ∨ (𝑅‘(𝐺 ∘ ◡𝐷))))))
20		cdlemk3.u1	. . 3 ⊢ 𝑌 = (𝑑 ∈ 𝑇, 𝑒 ∈ 𝑇 ↦ (℩𝑗 ∈ 𝑇 (𝑗‘𝑃) = ((𝑃 ∨ (𝑅‘𝑒)) ∧ (((𝑆‘𝑑)‘𝑃) ∨ (𝑅‘(𝑒 ∘ ◡𝑑))))))
21		riotaex 7392	. . 3 ⊢ (℩𝑗 ∈ 𝑇 (𝑗‘𝑃) = ((𝑃 ∨ (𝑅‘𝐺)) ∧ ((𝑄‘𝑃) ∨ (𝑅‘(𝐺 ∘ ◡𝐷))))) ∈ V
22	11, 19, 20, 21	ovmpo 7593	. 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 40846	. . 3 ⊢ (𝐺 ∈ 𝑇 → (𝑍‘𝐺) = (℩𝑗 ∈ 𝑇 (𝑗‘𝑃) = ((𝑃 ∨ (𝑅‘𝐺)) ∧ ((𝑄‘𝑃) ∨ (𝑅‘(𝐺 ∘ ◡𝐷))))))
33	32	adantl 481	. 2 ⊢ ((𝐷 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) → (𝑍‘𝐺) = (℩𝑗 ∈ 𝑇 (𝑗‘𝑃) = ((𝑃 ∨ (𝑅‘𝐺)) ∧ ((𝑄‘𝑃) ∨ (𝑅‘(𝐺 ∘ ◡𝐷))))))
34	22, 33	eqtr4d 2780	1 ⊢ ((𝐷 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) → (𝐷𝑌𝐺) = (𝑍‘𝐺))

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2108   ↦ cmpt 5225  ^◡ccnv 5684   ∘ ccom 5689  ‘cfv 6561  ℩crio 7387  (class class class)co 7431   ∈ cmpo 7433  Basecbs 17247  lecple 17304  joincjn 18357  meetcmee 18358  Atomscatm 39264  LHypclh 39986  LTrncltrn 40103  trLctrl 40160

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-sbc 3789  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-opab 5206  df-mpt 5226  df-id 5578  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-iota 6514  df-fun 6563  df-fv 6569  df-riota 7388  df-ov 7434  df-oprab 7435  df-mpo 7436

This theorem is referenced by:  cdlemk31  40898  cdlemkuel-3  40900  cdlemkuv2-3N  40901  cdlemk18-3N  40902  cdlemk22-3  40903  cdlemkyu  40929