Theorem cdlemkuu 42046

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 6886	. . . . . . . . 9 ⊢ (𝑑 = 𝐷 → (𝑆‘𝑑) = (𝑆‘𝐷))
2		cdlemk3.o2	. . . . . . . . 9 ⊢ 𝑄 = (𝑆‘𝐷)
3	1, 2	eqtr4di 2813	. . . . . . . 8 ⊢ (𝑑 = 𝐷 → (𝑆‘𝑑) = 𝑄)
4	3	fveq1d 6888	. . . . . . 7 ⊢ (𝑑 = 𝐷 → ((𝑆‘𝑑)‘𝑃) = (𝑄‘𝑃))
5		cnveq 5850	. . . . . . . . 9 ⊢ (𝑑 = 𝐷 → ◡𝑑 = ◡𝐷)
6	5	coeq2d 5839	. . . . . . . 8 ⊢ (𝑑 = 𝐷 → (𝑒 ∘ ◡𝑑) = (𝑒 ∘ ◡𝐷))
7	6	fveq2d 6890	. . . . . . 7 ⊢ (𝑑 = 𝐷 → (𝑅‘(𝑒 ∘ ◡𝑑)) = (𝑅‘(𝑒 ∘ ◡𝐷)))
8	4, 7	oveq12d 7439	. . . . . 6 ⊢ (𝑑 = 𝐷 → (((𝑆‘𝑑)‘𝑃) ∨ (𝑅‘(𝑒 ∘ ◡𝑑))) = ((𝑄‘𝑃) ∨ (𝑅‘(𝑒 ∘ ◡𝐷))))
9	8	oveq2d 7437	. . . . 5 ⊢ (𝑑 = 𝐷 → ((𝑃 ∨ (𝑅‘𝑒)) ∧ (((𝑆‘𝑑)‘𝑃) ∨ (𝑅‘(𝑒 ∘ ◡𝑑)))) = ((𝑃 ∨ (𝑅‘𝑒)) ∧ ((𝑄‘𝑃) ∨ (𝑅‘(𝑒 ∘ ◡𝐷)))))
10	9	eqeq2d 2771	. . . 4 ⊢ (𝑑 = 𝐷 → ((𝑗‘𝑃) = ((𝑃 ∨ (𝑅‘𝑒)) ∧ (((𝑆‘𝑑)‘𝑃) ∨ (𝑅‘(𝑒 ∘ ◡𝑑)))) ↔ (𝑗‘𝑃) = ((𝑃 ∨ (𝑅‘𝑒)) ∧ ((𝑄‘𝑃) ∨ (𝑅‘(𝑒 ∘ ◡𝐷))))))
11	10	riotabidv 7380	. . 3 ⊢ (𝑑 = 𝐷 → (℩𝑗 ∈ 𝑇 (𝑗‘𝑃) = ((𝑃 ∨ (𝑅‘𝑒)) ∧ (((𝑆‘𝑑)‘𝑃) ∨ (𝑅‘(𝑒 ∘ ◡𝑑))))) = (℩𝑗 ∈ 𝑇 (𝑗‘𝑃) = ((𝑃 ∨ (𝑅‘𝑒)) ∧ ((𝑄‘𝑃) ∨ (𝑅‘(𝑒 ∘ ◡𝐷))))))
12		fveq2 6886	. . . . . . 7 ⊢ (𝑒 = 𝐺 → (𝑅‘𝑒) = (𝑅‘𝐺))
13	12	oveq2d 7437	. . . . . 6 ⊢ (𝑒 = 𝐺 → (𝑃 ∨ (𝑅‘𝑒)) = (𝑃 ∨ (𝑅‘𝐺)))
14		coeq1 5834	. . . . . . . 8 ⊢ (𝑒 = 𝐺 → (𝑒 ∘ ◡𝐷) = (𝐺 ∘ ◡𝐷))
15	14	fveq2d 6890	. . . . . . 7 ⊢ (𝑒 = 𝐺 → (𝑅‘(𝑒 ∘ ◡𝐷)) = (𝑅‘(𝐺 ∘ ◡𝐷)))
16	15	oveq2d 7437	. . . . . 6 ⊢ (𝑒 = 𝐺 → ((𝑄‘𝑃) ∨ (𝑅‘(𝑒 ∘ ◡𝐷))) = ((𝑄‘𝑃) ∨ (𝑅‘(𝐺 ∘ ◡𝐷))))
17	13, 16	oveq12d 7439	. . . . 5 ⊢ (𝑒 = 𝐺 → ((𝑃 ∨ (𝑅‘𝑒)) ∧ ((𝑄‘𝑃) ∨ (𝑅‘(𝑒 ∘ ◡𝐷)))) = ((𝑃 ∨ (𝑅‘𝐺)) ∧ ((𝑄‘𝑃) ∨ (𝑅‘(𝐺 ∘ ◡𝐷)))))
18	17	eqeq2d 2771	. . . 4 ⊢ (𝑒 = 𝐺 → ((𝑗‘𝑃) = ((𝑃 ∨ (𝑅‘𝑒)) ∧ ((𝑄‘𝑃) ∨ (𝑅‘(𝑒 ∘ ◡𝐷)))) ↔ (𝑗‘𝑃) = ((𝑃 ∨ (𝑅‘𝐺)) ∧ ((𝑄‘𝑃) ∨ (𝑅‘(𝐺 ∘ ◡𝐷))))))
19	18	riotabidv 7380	. . 3 ⊢ (𝑒 = 𝐺 → (℩𝑗 ∈ 𝑇 (𝑗‘𝑃) = ((𝑃 ∨ (𝑅‘𝑒)) ∧ ((𝑄‘𝑃) ∨ (𝑅‘(𝑒 ∘ ◡𝐷))))) = (℩𝑗 ∈ 𝑇 (𝑗‘𝑃) = ((𝑃 ∨ (𝑅‘𝐺)) ∧ ((𝑄‘𝑃) ∨ (𝑅‘(𝐺 ∘ ◡𝐷))))))
20		cdlemk3.u1	. . 3 ⊢ 𝑌 = (𝑑 ∈ 𝑇, 𝑒 ∈ 𝑇 ↦ (℩𝑗 ∈ 𝑇 (𝑗‘𝑃) = ((𝑃 ∨ (𝑅‘𝑒)) ∧ (((𝑆‘𝑑)‘𝑃) ∨ (𝑅‘(𝑒 ∘ ◡𝑑))))))
21		riotaex 7382	. . 3 ⊢ (℩𝑗 ∈ 𝑇 (𝑗‘𝑃) = ((𝑃 ∨ (𝑅‘𝐺)) ∧ ((𝑄‘𝑃) ∨ (𝑅‘(𝐺 ∘ ◡𝐷))))) ∈ V
22	11, 19, 20, 21	ovmpo 7581	. 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 41995	. . 3 ⊢ (𝐺 ∈ 𝑇 → (𝑍‘𝐺) = (℩𝑗 ∈ 𝑇 (𝑗‘𝑃) = ((𝑃 ∨ (𝑅‘𝐺)) ∧ ((𝑄‘𝑃) ∨ (𝑅‘(𝐺 ∘ ◡𝐷))))))
33	32	adantl 487	. 2 ⊢ ((𝐷 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) → (𝑍‘𝐺) = (℩𝑗 ∈ 𝑇 (𝑗‘𝑃) = ((𝑃 ∨ (𝑅‘𝐺)) ∧ ((𝑄‘𝑃) ∨ (𝑅‘(𝐺 ∘ ◡𝐷))))))
34	22, 33	eqtr4d 2798	1 ⊢ ((𝐷 ∈ 𝑇 ∧ 𝐺 ∈ 𝑇) → (𝐷𝑌𝐺) = (𝑍‘𝐺))

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1569   ∈ wcel 2144   ↦ cmpt 5185  ^◡ccnv 5649   ∘ ccom 5654  ‘cfv 6539  ℩crio 7377  (class class class)co 7421   ∈ cmpo 7423  Basecbs 17393  lecple 17441  joincjn 18491  meetcmee 18492  Atomscatm 40414  LHypclh 41135  LTrncltrn 41252  trLctrl 41309

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pr 5390

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-sbc 3739  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-br 5103  df-opab 5167  df-mpt 5186  df-id 5545  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-iota 6494  df-fun 6541  df-fv 6547  df-riota 7378  df-ov 7424  df-oprab 7425  df-mpo 7426

This theorem is used by:  cdlemk31  42047  cdlemkuel-3  42049  cdlemkuv2-3N  42050  cdlemk18-3N  42051  cdlemk22-3  42052  cdlemkyu  42078