cdlemkid2 - Mathbox for Norm Megill

	Mathbox for Norm Megill		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > cdlemkid2		Structured version Visualization version GIF version

Theorem cdlemkid2 41797

Description: Lemma for cdlemkid 41809. (Contributed by NM, 24-Jul-2013.)

**Hypotheses**
Ref	Expression
cdlemk5.b	⊢ 𝐵 = (Base‘𝐾)
cdlemk5.l	⊢ ≤ = (le‘𝐾)
cdlemk5.j	⊢ ∨ = (join‘𝐾)
cdlemk5.m	⊢ ∧ = (meet‘𝐾)
cdlemk5.a	⊢ 𝐴 = (Atoms‘𝐾)
cdlemk5.h	⊢ 𝐻 = (LHyp‘𝐾)
cdlemk5.t	⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)
cdlemk5.r	⊢ 𝑅 = ((trL‘𝐾)‘𝑊)
cdlemk5.z	⊢ 𝑍 = ((𝑃 ∨ (𝑅‘𝑏)) ∧ ((𝑁‘𝑃) ∨ (𝑅‘(𝑏 ∘ ^◡𝐹))))
cdlemk5.y	⊢ 𝑌 = ((𝑃 ∨ (𝑅‘𝑔)) ∧ (𝑍 ∨ (𝑅‘(𝑔 ∘ ^◡𝑏))))

**Assertion**
Ref	Expression
cdlemkid2	⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ 𝐺 = ( I ↾ 𝐵) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → ⦋𝐺 / 𝑔⦌𝑌 = 𝑃)

Distinct variable groups: ∧ ,𝑔 ∨ ,𝑔 𝐵,𝑔 𝑃,𝑔 𝑅,𝑔 𝑇,𝑔 𝑔,𝑍 𝑔,𝑏 Allowed substitution hints: 𝐴(𝑔, 𝑏) 𝐵(𝑏) 𝑃(𝑏) 𝑅(𝑏) 𝑇(𝑏) 𝐹(𝑔, 𝑏) 𝐺(𝑔, 𝑏) 𝐻(𝑔, 𝑏) ∨ (𝑏) 𝐾(𝑔, 𝑏) ≤ (𝑔, 𝑏) ∧ (𝑏) 𝑁(𝑔, 𝑏) 𝑊(𝑔, 𝑏) 𝑌(𝑔, 𝑏) 𝑍(𝑏)

**Proof of Theorem cdlemkid2**
Step	Hyp	Ref	Expression
1		simp32 1229	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ 𝐺 = ( I ↾ 𝐵) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → 𝐺 = ( I ↾ 𝐵))
2	1	csbeq1d 3851	. 2 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ 𝐺 = ( I ↾ 𝐵) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → ⦋𝐺 / 𝑔⦌𝑌 = ⦋( I ↾ 𝐵) / 𝑔⦌𝑌)
3		cdlemk5.b	. . . . . 6 ⊢ 𝐵 = (Base‘𝐾)
4		cdlemk5.h	. . . . . 6 ⊢ 𝐻 = (LHyp‘𝐾)
5		cdlemk5.t	. . . . . 6 ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)
6	3, 4, 5	idltrn 41023	. . . . 5 ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → ( I ↾ 𝐵) ∈ 𝑇)
7	6	3ad2ant1 1151	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ 𝐺 = ( I ↾ 𝐵) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → ( I ↾ 𝐵) ∈ 𝑇)
8		cdlemk5.y	. . . . 5 ⊢ 𝑌 = ((𝑃 ∨ (𝑅‘𝑔)) ∧ (𝑍 ∨ (𝑅‘(𝑔 ∘ ^◡𝑏))))
9	8	cdlemk41 41793	. . . 4 ⊢ (( I ↾ 𝐵) ∈ 𝑇 → ⦋( I ↾ 𝐵) / 𝑔⦌𝑌 = ((𝑃 ∨ (𝑅‘( I ↾ 𝐵))) ∧ (𝑍 ∨ (𝑅‘(( I ↾ 𝐵) ∘ ^◡𝑏)))))
10	7, 9	syl 18	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ 𝐺 = ( I ↾ 𝐵) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → ⦋( I ↾ 𝐵) / 𝑔⦌𝑌 = ((𝑃 ∨ (𝑅‘( I ↾ 𝐵))) ∧ (𝑍 ∨ (𝑅‘(( I ↾ 𝐵) ∘ ^◡𝑏)))))
11		eqid 2760	. . . . . . . . 9 ⊢ (0.‘𝐾) = (0.‘𝐾)
12		cdlemk5.r	. . . . . . . . 9 ⊢ 𝑅 = ((trL‘𝐾)‘𝑊)
13	3, 11, 4, 12	trlid0 41049	. . . . . . . 8 ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → (𝑅‘( I ↾ 𝐵)) = (0.‘𝐾))
14	13	3ad2ant1 1151	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ 𝐺 = ( I ↾ 𝐵) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → (𝑅‘( I ↾ 𝐵)) = (0.‘𝐾))
15	14	oveq2d 7429	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ 𝐺 = ( I ↾ 𝐵) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → (𝑃 ∨ (𝑅‘( I ↾ 𝐵))) = (𝑃 ∨ (0.‘𝐾)))
16		simp1l 1216	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ 𝐺 = ( I ↾ 𝐵) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → 𝐾 ∈ HL)
17		hlol 40234	. . . . . . . 8 ⊢ (𝐾 ∈ HL → 𝐾 ∈ OL)
18	16, 17	syl 18	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ 𝐺 = ( I ↾ 𝐵) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → 𝐾 ∈ OL)
19		simp31l 1315	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ 𝐺 = ( I ↾ 𝐵) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → 𝑃 ∈ 𝐴)
20		cdlemk5.a	. . . . . . . . 9 ⊢ 𝐴 = (Atoms‘𝐾)
21	3, 20	atbase 40162	. . . . . . . 8 ⊢ (𝑃 ∈ 𝐴 → 𝑃 ∈ 𝐵)
22	19, 21	syl 18	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ 𝐺 = ( I ↾ 𝐵) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → 𝑃 ∈ 𝐵)
23		cdlemk5.j	. . . . . . . 8 ⊢ ∨ = (join‘𝐾)
24	3, 23, 11	olj01 40098	. . . . . . 7 ⊢ ((𝐾 ∈ OL ∧ 𝑃 ∈ 𝐵) → (𝑃 ∨ (0.‘𝐾)) = 𝑃)
25	18, 22, 24	syl2anc 596	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ 𝐺 = ( I ↾ 𝐵) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → (𝑃 ∨ (0.‘𝐾)) = 𝑃)
26	15, 25	eqtrd 2795	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ 𝐺 = ( I ↾ 𝐵) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → (𝑃 ∨ (𝑅‘( I ↾ 𝐵))) = 𝑃)
27		simp1 1154	. . . . . . . . . . 11 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ 𝐺 = ( I ↾ 𝐵) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
28		simp33l 1319	. . . . . . . . . . . 12 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ 𝐺 = ( I ↾ 𝐵) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → 𝑏 ∈ 𝑇)
29	4, 5	ltrncnv 41019	. . . . . . . . . . . 12 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑏 ∈ 𝑇) → ^◡𝑏 ∈ 𝑇)
30	27, 28, 29	syl2anc 596	. . . . . . . . . . 11 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ 𝐺 = ( I ↾ 𝐵) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → ^◡𝑏 ∈ 𝑇)
31	3, 4, 5	ltrn1o 40997	. . . . . . . . . . 11 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ^◡𝑏 ∈ 𝑇) → ^◡𝑏:𝐵–1-1-onto→𝐵)
32	27, 30, 31	syl2anc 596	. . . . . . . . . 10 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ 𝐺 = ( I ↾ 𝐵) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → ^◡𝑏:𝐵–1-1-onto→𝐵)
33		f1of 6817	. . . . . . . . . 10 ⊢ (^◡𝑏:𝐵–1-1-onto→𝐵 → ^◡𝑏:𝐵⟶𝐵)
34		fcoi2 6750	. . . . . . . . . 10 ⊢ (^◡𝑏:𝐵⟶𝐵 → (( I ↾ 𝐵) ∘ ^◡𝑏) = ^◡𝑏)
35	32, 33, 34	3syl 19	. . . . . . . . 9 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ 𝐺 = ( I ↾ 𝐵) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → (( I ↾ 𝐵) ∘ ^◡𝑏) = ^◡𝑏)
36	35	fveq2d 6882	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ 𝐺 = ( I ↾ 𝐵) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → (𝑅‘(( I ↾ 𝐵) ∘ ^◡𝑏)) = (𝑅‘^◡𝑏))
37	4, 5, 12	trlcnv 41038	. . . . . . . . 9 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑏 ∈ 𝑇) → (𝑅‘^◡𝑏) = (𝑅‘𝑏))
38	27, 28, 37	syl2anc 596	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ 𝐺 = ( I ↾ 𝐵) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → (𝑅‘^◡𝑏) = (𝑅‘𝑏))
39	36, 38	eqtrd 2795	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ 𝐺 = ( I ↾ 𝐵) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → (𝑅‘(( I ↾ 𝐵) ∘ ^◡𝑏)) = (𝑅‘𝑏))
40	39	oveq2d 7429	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ 𝐺 = ( I ↾ 𝐵) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → (𝑍 ∨ (𝑅‘(( I ↾ 𝐵) ∘ ^◡𝑏))) = (𝑍 ∨ (𝑅‘𝑏)))
41		simp31 1228	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ 𝐺 = ( I ↾ 𝐵) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊))
42		simp33 1230	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ 𝐺 = ( I ↾ 𝐵) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))
43	41, 42	jca 521	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ 𝐺 = ( I ↾ 𝐵) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵))))
44		cdlemk5.l	. . . . . . . 8 ⊢ ≤ = (le‘𝐾)
45		cdlemk5.m	. . . . . . . 8 ⊢ ∧ = (meet‘𝐾)
46		cdlemk5.z	. . . . . . . 8 ⊢ 𝑍 = ((𝑃 ∨ (𝑅‘𝑏)) ∧ ((𝑁‘𝑃) ∨ (𝑅‘(𝑏 ∘ ^◡𝐹))))
47	3, 44, 23, 45, 20, 4, 5, 12, 46	cdlemkid1 41795	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → (𝑍 ∨ (𝑅‘𝑏)) = (𝑃 ∨ (𝑅‘𝑏)))
48	43, 47	syld3an3 1436	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ 𝐺 = ( I ↾ 𝐵) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → (𝑍 ∨ (𝑅‘𝑏)) = (𝑃 ∨ (𝑅‘𝑏)))
49	40, 48	eqtrd 2795	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ 𝐺 = ( I ↾ 𝐵) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → (𝑍 ∨ (𝑅‘(( I ↾ 𝐵) ∘ ^◡𝑏))) = (𝑃 ∨ (𝑅‘𝑏)))
50	26, 49	oveq12d 7431	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ 𝐺 = ( I ↾ 𝐵) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → ((𝑃 ∨ (𝑅‘( I ↾ 𝐵))) ∧ (𝑍 ∨ (𝑅‘(( I ↾ 𝐵) ∘ ^◡𝑏)))) = (𝑃 ∧ (𝑃 ∨ (𝑅‘𝑏))))
51	16	hllatd 40237	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ 𝐺 = ( I ↾ 𝐵) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → 𝐾 ∈ Lat)
52	3, 4, 5, 12	trlcl 41037	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑏 ∈ 𝑇) → (𝑅‘𝑏) ∈ 𝐵)
53	27, 28, 52	syl2anc 596	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ 𝐺 = ( I ↾ 𝐵) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → (𝑅‘𝑏) ∈ 𝐵)
54	3, 23, 45	latabs2 18564	. . . . 5 ⊢ ((𝐾 ∈ Lat ∧ 𝑃 ∈ 𝐵 ∧ (𝑅‘𝑏) ∈ 𝐵) → (𝑃 ∧ (𝑃 ∨ (𝑅‘𝑏))) = 𝑃)
55	51, 22, 53, 54	syl3anc 1398	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ 𝐺 = ( I ↾ 𝐵) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → (𝑃 ∧ (𝑃 ∨ (𝑅‘𝑏))) = 𝑃)
56	50, 55	eqtrd 2795	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ 𝐺 = ( I ↾ 𝐵) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → ((𝑃 ∨ (𝑅‘( I ↾ 𝐵))) ∧ (𝑍 ∨ (𝑅‘(( I ↾ 𝐵) ∘ ^◡𝑏)))) = 𝑃)
57	10, 56	eqtrd 2795	. 2 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ 𝐺 = ( I ↾ 𝐵) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → ⦋( I ↾ 𝐵) / 𝑔⦌𝑌 = 𝑃)
58	2, 57	eqtrd 2795	1 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ 𝑁 ∈ 𝑇 ∧ (𝑅‘𝐹) = (𝑅‘𝑁)) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ 𝐺 = ( I ↾ 𝐵) ∧ (𝑏 ∈ 𝑇 ∧ 𝑏 ≠ ( I ↾ 𝐵)))) → ⦋𝐺 / 𝑔⦌𝑌 = 𝑃)

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ∧ wa 401 ∧ w3a 1103 = wceq 1570 ∈ wcel 2145 ≠ wne 2955 ⦋csb 3847 class class class wbr 5103 I cid 5549 ^◡ccnv 5654 ↾ cres 5657 ∘ ccom 5659 ⟶wf 6529 –1-1-onto→wf1o 6532 ‘cfv 6533 (class class class)co 7413 Basecbs 17301 lecple 17349 joincjn 18399 meetcmee 18400 0.cp0 18509 Latclat 18519 OLcol 40047 Atomscatm 40136 HLchlt 40223 LHypclh 40857 LTrncltrn 40974 trLctrl 41031

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2213 ax-ext 2732 ax-rep 5232 ax-sep 5251 ax-nul 5263 ax-pow 5330 ax-pr 5398 ax-un 7736 ax-riotaBAD 39826

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 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-rmo 3365 df-reu 3366 df-rab 3413 df-v 3452 df-sbc 3740 df-csb 3848 df-dif 3902 df-un 3904 df-in 3906 df-ss 3916 df-nul 4280 df-if 4483 df-pw 4559 df-sn 4585 df-pr 4587 df-op 4591 df-uni 4868 df-iun 4953 df-iin 4954 df-br 5104 df-opab 5168 df-mpt 5187 df-id 5550 df-xp 5661 df-rel 5662 df-cnv 5663 df-co 5664 df-dm 5665 df-rn 5666 df-res 5667 df-ima 5668 df-iota 6489 df-fun 6535 df-fn 6536 df-f 6537 df-f1 6538 df-fo 6539 df-f1o 6540 df-fv 6541 df-riota 7370 df-ov 7416 df-oprab 7417 df-mpo 7418 df-1st 7986 df-2nd 7987 df-undef 8271 df-map 8828 df-proset 18382 df-poset 18401 df-plt 18416 df-lub 18432 df-glb 18433 df-join 18434 df-meet 18435 df-p0 18511 df-p1 18512 df-lat 18520 df-clat 18587 df-oposet 40049 df-ol 40051 df-oml 40052 df-covers 40139 df-ats 40140 df-atl 40171 df-cvlat 40195 df-hlat 40224 df-llines 40371 df-lplanes 40372 df-lvols 40373 df-lines 40374 df-psubsp 40376 df-pmap 40377 df-padd 40669 df-lhyp 40861 df-laut 40862 df-ldil 40977 df-ltrn 40978 df-trl 41032

This theorem is used by: cdlemkid3N 41806 cdlemkid4 41807

W3C validator