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

Theorem dih1dimatlem0 39563
Description: Lemma for dih1dimat 39565. (Contributed by NM, 11-Apr-2014.)
Hypotheses
Ref Expression
dih1dimat.h 𝐻 = (LHyp‘𝐾)
dih1dimat.u 𝑈 = ((DVecH‘𝐾)‘𝑊)
dih1dimat.i 𝐼 = ((DIsoH‘𝐾)‘𝑊)
dih1dimat.a 𝐴 = (LSAtoms‘𝑈)
dih1dimat.b 𝐵 = (Base‘𝐾)
dih1dimat.l = (le‘𝐾)
dih1dimat.c 𝐶 = (Atoms‘𝐾)
dih1dimat.p 𝑃 = ((oc‘𝐾)‘𝑊)
dih1dimat.t 𝑇 = ((LTrn‘𝐾)‘𝑊)
dih1dimat.r 𝑅 = ((trL‘𝐾)‘𝑊)
dih1dimat.e 𝐸 = ((TEndo‘𝐾)‘𝑊)
dih1dimat.o 𝑂 = (𝑇 ↦ ( I ↾ 𝐵))
dih1dimat.d 𝐹 = (Scalar‘𝑈)
dih1dimat.j 𝐽 = (invr𝐹)
dih1dimat.v 𝑉 = (Base‘𝑈)
dih1dimat.m · = ( ·𝑠𝑈)
dih1dimat.s 𝑆 = (LSubSp‘𝑈)
dih1dimat.n 𝑁 = (LSpan‘𝑈)
dih1dimat.z 0 = (0g𝑈)
dih1dimat.g 𝐺 = (𝑇 (𝑃) = (((𝐽𝑠)‘𝑓)‘𝑃))
Assertion
Ref Expression
dih1dimatlem0 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑓𝑇𝑠𝐸) ∧ 𝑠𝑂) → ((𝑖 = (𝑝𝐺) ∧ 𝑝𝐸) ↔ ((𝑖𝑇𝑝𝐸) ∧ ∃𝑡𝐸 (𝑖 = (𝑡𝑓) ∧ 𝑝 = (𝑡𝑠)))))
Distinct variable groups:   ,   𝐵,   𝑓,𝑖,𝑝,𝑠,𝑡,𝐸   𝑡,𝐹   𝐶,   𝑖,𝐺,𝑝,𝑡   𝑡,,𝐽   𝑓,𝑁,𝑠,𝑡   𝑓,,𝐾,𝑖,𝑝,𝑠,𝑡   𝑇,𝑓,,𝑖,𝑝,𝑠,𝑡   𝑈,𝑓,,𝑠,𝑡   𝑓,𝐻,,𝑖,𝑝,𝑠,𝑡   𝑓,𝑉,𝑖,𝑝,𝑠,𝑡   𝑓,𝑊,,𝑖,𝑝,𝑠,𝑡   𝑓,𝐼,𝑠   𝑖,𝑂,𝑝,𝑡   𝑃,   𝑡, ·
Allowed substitution hints:   𝐴(𝑡,𝑓,,𝑖,𝑠,𝑝)   𝐵(𝑡,𝑓,𝑖,𝑠,𝑝)   𝐶(𝑡,𝑓,𝑖,𝑠,𝑝)   𝑃(𝑡,𝑓,𝑖,𝑠,𝑝)   𝑅(𝑡,𝑓,,𝑖,𝑠,𝑝)   𝑆(𝑡,𝑓,,𝑖,𝑠,𝑝)   · (𝑓,,𝑖,𝑠,𝑝)   𝑈(𝑖,𝑝)   𝐸()   𝐹(𝑓,,𝑖,𝑠,𝑝)   𝐺(𝑓,,𝑠)   𝐼(𝑡,,𝑖,𝑝)   𝐽(𝑓,𝑖,𝑠,𝑝)   (𝑡,𝑓,𝑖,𝑠,𝑝)   𝑁(,𝑖,𝑝)   𝑂(𝑓,,𝑠)   𝑉()   0 (𝑡,𝑓,,𝑖,𝑠,𝑝)

Proof of Theorem dih1dimatlem0
StepHypRef Expression
1 simprl 768 . . . 4 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑓𝑇𝑠𝐸) ∧ 𝑠𝑂) ∧ (𝑖 = (𝑝𝐺) ∧ 𝑝𝐸)) → 𝑖 = (𝑝𝐺))
2 simpl1 1190 . . . . 5 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑓𝑇𝑠𝐸) ∧ 𝑠𝑂) ∧ (𝑖 = (𝑝𝐺) ∧ 𝑝𝐸)) → (𝐾 ∈ HL ∧ 𝑊𝐻))
3 simprr 770 . . . . 5 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑓𝑇𝑠𝐸) ∧ 𝑠𝑂) ∧ (𝑖 = (𝑝𝐺) ∧ 𝑝𝐸)) → 𝑝𝐸)
4 dih1dimat.l . . . . . . . 8 = (le‘𝐾)
5 dih1dimat.c . . . . . . . 8 𝐶 = (Atoms‘𝐾)
6 dih1dimat.h . . . . . . . 8 𝐻 = (LHyp‘𝐾)
7 dih1dimat.p . . . . . . . 8 𝑃 = ((oc‘𝐾)‘𝑊)
84, 5, 6, 7lhpocnel2 38254 . . . . . . 7 ((𝐾 ∈ HL ∧ 𝑊𝐻) → (𝑃𝐶 ∧ ¬ 𝑃 𝑊))
92, 8syl 17 . . . . . 6 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑓𝑇𝑠𝐸) ∧ 𝑠𝑂) ∧ (𝑖 = (𝑝𝐺) ∧ 𝑝𝐸)) → (𝑃𝐶 ∧ ¬ 𝑃 𝑊))
10 simpl2r 1226 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑓𝑇𝑠𝐸) ∧ 𝑠𝑂) ∧ (𝑖 = (𝑝𝐺) ∧ 𝑝𝐸)) → 𝑠𝐸)
11 simpl3 1192 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑓𝑇𝑠𝐸) ∧ 𝑠𝑂) ∧ (𝑖 = (𝑝𝐺) ∧ 𝑝𝐸)) → 𝑠𝑂)
12 dih1dimat.b . . . . . . . . . . 11 𝐵 = (Base‘𝐾)
13 dih1dimat.t . . . . . . . . . . 11 𝑇 = ((LTrn‘𝐾)‘𝑊)
14 dih1dimat.e . . . . . . . . . . 11 𝐸 = ((TEndo‘𝐾)‘𝑊)
15 dih1dimat.o . . . . . . . . . . 11 𝑂 = (𝑇 ↦ ( I ↾ 𝐵))
16 dih1dimat.u . . . . . . . . . . 11 𝑈 = ((DVecH‘𝐾)‘𝑊)
17 dih1dimat.d . . . . . . . . . . 11 𝐹 = (Scalar‘𝑈)
18 dih1dimat.j . . . . . . . . . . 11 𝐽 = (invr𝐹)
1912, 6, 13, 14, 15, 16, 17, 18tendoinvcl 39339 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑠𝐸𝑠𝑂) → ((𝐽𝑠) ∈ 𝐸 ∧ (𝐽𝑠) ≠ 𝑂))
2019simpld 495 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑠𝐸𝑠𝑂) → (𝐽𝑠) ∈ 𝐸)
212, 10, 11, 20syl3anc 1370 . . . . . . . 8 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑓𝑇𝑠𝐸) ∧ 𝑠𝑂) ∧ (𝑖 = (𝑝𝐺) ∧ 𝑝𝐸)) → (𝐽𝑠) ∈ 𝐸)
22 simpl2l 1225 . . . . . . . 8 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑓𝑇𝑠𝐸) ∧ 𝑠𝑂) ∧ (𝑖 = (𝑝𝐺) ∧ 𝑝𝐸)) → 𝑓𝑇)
236, 13, 14tendocl 39002 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝐽𝑠) ∈ 𝐸𝑓𝑇) → ((𝐽𝑠)‘𝑓) ∈ 𝑇)
242, 21, 22, 23syl3anc 1370 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑓𝑇𝑠𝐸) ∧ 𝑠𝑂) ∧ (𝑖 = (𝑝𝐺) ∧ 𝑝𝐸)) → ((𝐽𝑠)‘𝑓) ∈ 𝑇)
254, 5, 6, 13ltrnel 38374 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝐽𝑠)‘𝑓) ∈ 𝑇 ∧ (𝑃𝐶 ∧ ¬ 𝑃 𝑊)) → ((((𝐽𝑠)‘𝑓)‘𝑃) ∈ 𝐶 ∧ ¬ (((𝐽𝑠)‘𝑓)‘𝑃) 𝑊))
262, 24, 9, 25syl3anc 1370 . . . . . 6 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑓𝑇𝑠𝐸) ∧ 𝑠𝑂) ∧ (𝑖 = (𝑝𝐺) ∧ 𝑝𝐸)) → ((((𝐽𝑠)‘𝑓)‘𝑃) ∈ 𝐶 ∧ ¬ (((𝐽𝑠)‘𝑓)‘𝑃) 𝑊))
27 dih1dimat.g . . . . . . 7 𝐺 = (𝑇 (𝑃) = (((𝐽𝑠)‘𝑓)‘𝑃))
284, 5, 6, 13, 27ltrniotacl 38814 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐶 ∧ ¬ 𝑃 𝑊) ∧ ((((𝐽𝑠)‘𝑓)‘𝑃) ∈ 𝐶 ∧ ¬ (((𝐽𝑠)‘𝑓)‘𝑃) 𝑊)) → 𝐺𝑇)
292, 9, 26, 28syl3anc 1370 . . . . 5 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑓𝑇𝑠𝐸) ∧ 𝑠𝑂) ∧ (𝑖 = (𝑝𝐺) ∧ 𝑝𝐸)) → 𝐺𝑇)
306, 13, 14tendocl 39002 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑝𝐸𝐺𝑇) → (𝑝𝐺) ∈ 𝑇)
312, 3, 29, 30syl3anc 1370 . . . 4 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑓𝑇𝑠𝐸) ∧ 𝑠𝑂) ∧ (𝑖 = (𝑝𝐺) ∧ 𝑝𝐸)) → (𝑝𝐺) ∈ 𝑇)
321, 31eqeltrd 2838 . . 3 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑓𝑇𝑠𝐸) ∧ 𝑠𝑂) ∧ (𝑖 = (𝑝𝐺) ∧ 𝑝𝐸)) → 𝑖𝑇)
336, 14tendococl 39007 . . . . 5 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑝𝐸 ∧ (𝐽𝑠) ∈ 𝐸) → (𝑝 ∘ (𝐽𝑠)) ∈ 𝐸)
342, 3, 21, 33syl3anc 1370 . . . 4 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑓𝑇𝑠𝐸) ∧ 𝑠𝑂) ∧ (𝑖 = (𝑝𝐺) ∧ 𝑝𝐸)) → (𝑝 ∘ (𝐽𝑠)) ∈ 𝐸)
35 simp1 1135 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑓𝑇𝑠𝐸) ∧ 𝑠𝑂) → (𝐾 ∈ HL ∧ 𝑊𝐻))
3683ad2ant1 1132 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑓𝑇𝑠𝐸) ∧ 𝑠𝑂) → (𝑃𝐶 ∧ ¬ 𝑃 𝑊))
37203adant2l 1177 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑓𝑇𝑠𝐸) ∧ 𝑠𝑂) → (𝐽𝑠) ∈ 𝐸)
38 simp2l 1198 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑓𝑇𝑠𝐸) ∧ 𝑠𝑂) → 𝑓𝑇)
3935, 37, 38, 23syl3anc 1370 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑓𝑇𝑠𝐸) ∧ 𝑠𝑂) → ((𝐽𝑠)‘𝑓) ∈ 𝑇)
4035, 39, 36, 25syl3anc 1370 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑓𝑇𝑠𝐸) ∧ 𝑠𝑂) → ((((𝐽𝑠)‘𝑓)‘𝑃) ∈ 𝐶 ∧ ¬ (((𝐽𝑠)‘𝑓)‘𝑃) 𝑊))
4135, 36, 40, 28syl3anc 1370 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑓𝑇𝑠𝐸) ∧ 𝑠𝑂) → 𝐺𝑇)
424, 5, 6, 13, 27ltrniotaval 38816 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑃𝐶 ∧ ¬ 𝑃 𝑊) ∧ ((((𝐽𝑠)‘𝑓)‘𝑃) ∈ 𝐶 ∧ ¬ (((𝐽𝑠)‘𝑓)‘𝑃) 𝑊)) → (𝐺𝑃) = (((𝐽𝑠)‘𝑓)‘𝑃))
4335, 36, 40, 42syl3anc 1370 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑓𝑇𝑠𝐸) ∧ 𝑠𝑂) → (𝐺𝑃) = (((𝐽𝑠)‘𝑓)‘𝑃))
444, 5, 6, 13cdlemd 38442 . . . . . . . 8 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝐺𝑇 ∧ ((𝐽𝑠)‘𝑓) ∈ 𝑇) ∧ (𝑃𝐶 ∧ ¬ 𝑃 𝑊) ∧ (𝐺𝑃) = (((𝐽𝑠)‘𝑓)‘𝑃)) → 𝐺 = ((𝐽𝑠)‘𝑓))
4535, 41, 39, 36, 43, 44syl311anc 1383 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑓𝑇𝑠𝐸) ∧ 𝑠𝑂) → 𝐺 = ((𝐽𝑠)‘𝑓))
4645adantr 481 . . . . . 6 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑓𝑇𝑠𝐸) ∧ 𝑠𝑂) ∧ (𝑖 = (𝑝𝐺) ∧ 𝑝𝐸)) → 𝐺 = ((𝐽𝑠)‘𝑓))
4746fveq2d 6816 . . . . 5 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑓𝑇𝑠𝐸) ∧ 𝑠𝑂) ∧ (𝑖 = (𝑝𝐺) ∧ 𝑝𝐸)) → (𝑝𝐺) = (𝑝‘((𝐽𝑠)‘𝑓)))
486, 13, 14tendocoval 39001 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑝𝐸 ∧ (𝐽𝑠) ∈ 𝐸) ∧ 𝑓𝑇) → ((𝑝 ∘ (𝐽𝑠))‘𝑓) = (𝑝‘((𝐽𝑠)‘𝑓)))
492, 3, 21, 22, 48syl121anc 1374 . . . . 5 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑓𝑇𝑠𝐸) ∧ 𝑠𝑂) ∧ (𝑖 = (𝑝𝐺) ∧ 𝑝𝐸)) → ((𝑝 ∘ (𝐽𝑠))‘𝑓) = (𝑝‘((𝐽𝑠)‘𝑓)))
5047, 1, 493eqtr4d 2787 . . . 4 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑓𝑇𝑠𝐸) ∧ 𝑠𝑂) ∧ (𝑖 = (𝑝𝐺) ∧ 𝑝𝐸)) → 𝑖 = ((𝑝 ∘ (𝐽𝑠))‘𝑓))
51 coass 6191 . . . . 5 ((𝑝 ∘ (𝐽𝑠)) ∘ 𝑠) = (𝑝 ∘ ((𝐽𝑠) ∘ 𝑠))
5212, 6, 13, 14, 15, 16, 17, 18tendolinv 39340 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑠𝐸𝑠𝑂) → ((𝐽𝑠) ∘ 𝑠) = ( I ↾ 𝑇))
532, 10, 11, 52syl3anc 1370 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑓𝑇𝑠𝐸) ∧ 𝑠𝑂) ∧ (𝑖 = (𝑝𝐺) ∧ 𝑝𝐸)) → ((𝐽𝑠) ∘ 𝑠) = ( I ↾ 𝑇))
5453coeq2d 5792 . . . . . 6 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑓𝑇𝑠𝐸) ∧ 𝑠𝑂) ∧ (𝑖 = (𝑝𝐺) ∧ 𝑝𝐸)) → (𝑝 ∘ ((𝐽𝑠) ∘ 𝑠)) = (𝑝 ∘ ( I ↾ 𝑇)))
556, 13, 14tendo1mulr 39006 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑝𝐸) → (𝑝 ∘ ( I ↾ 𝑇)) = 𝑝)
562, 3, 55syl2anc 584 . . . . . 6 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑓𝑇𝑠𝐸) ∧ 𝑠𝑂) ∧ (𝑖 = (𝑝𝐺) ∧ 𝑝𝐸)) → (𝑝 ∘ ( I ↾ 𝑇)) = 𝑝)
5754, 56eqtrd 2777 . . . . 5 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑓𝑇𝑠𝐸) ∧ 𝑠𝑂) ∧ (𝑖 = (𝑝𝐺) ∧ 𝑝𝐸)) → (𝑝 ∘ ((𝐽𝑠) ∘ 𝑠)) = 𝑝)
5851, 57eqtr2id 2790 . . . 4 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑓𝑇𝑠𝐸) ∧ 𝑠𝑂) ∧ (𝑖 = (𝑝𝐺) ∧ 𝑝𝐸)) → 𝑝 = ((𝑝 ∘ (𝐽𝑠)) ∘ 𝑠))
59 fveq1 6811 . . . . . . 7 (𝑡 = (𝑝 ∘ (𝐽𝑠)) → (𝑡𝑓) = ((𝑝 ∘ (𝐽𝑠))‘𝑓))
6059eqeq2d 2748 . . . . . 6 (𝑡 = (𝑝 ∘ (𝐽𝑠)) → (𝑖 = (𝑡𝑓) ↔ 𝑖 = ((𝑝 ∘ (𝐽𝑠))‘𝑓)))
61 coeq1 5787 . . . . . . 7 (𝑡 = (𝑝 ∘ (𝐽𝑠)) → (𝑡𝑠) = ((𝑝 ∘ (𝐽𝑠)) ∘ 𝑠))
6261eqeq2d 2748 . . . . . 6 (𝑡 = (𝑝 ∘ (𝐽𝑠)) → (𝑝 = (𝑡𝑠) ↔ 𝑝 = ((𝑝 ∘ (𝐽𝑠)) ∘ 𝑠)))
6360, 62anbi12d 631 . . . . 5 (𝑡 = (𝑝 ∘ (𝐽𝑠)) → ((𝑖 = (𝑡𝑓) ∧ 𝑝 = (𝑡𝑠)) ↔ (𝑖 = ((𝑝 ∘ (𝐽𝑠))‘𝑓) ∧ 𝑝 = ((𝑝 ∘ (𝐽𝑠)) ∘ 𝑠))))
6463rspcev 3570 . . . 4 (((𝑝 ∘ (𝐽𝑠)) ∈ 𝐸 ∧ (𝑖 = ((𝑝 ∘ (𝐽𝑠))‘𝑓) ∧ 𝑝 = ((𝑝 ∘ (𝐽𝑠)) ∘ 𝑠))) → ∃𝑡𝐸 (𝑖 = (𝑡𝑓) ∧ 𝑝 = (𝑡𝑠)))
6534, 50, 58, 64syl12anc 834 . . 3 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑓𝑇𝑠𝐸) ∧ 𝑠𝑂) ∧ (𝑖 = (𝑝𝐺) ∧ 𝑝𝐸)) → ∃𝑡𝐸 (𝑖 = (𝑡𝑓) ∧ 𝑝 = (𝑡𝑠)))
6632, 3, 65jca31 515 . 2 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑓𝑇𝑠𝐸) ∧ 𝑠𝑂) ∧ (𝑖 = (𝑝𝐺) ∧ 𝑝𝐸)) → ((𝑖𝑇𝑝𝐸) ∧ ∃𝑡𝐸 (𝑖 = (𝑡𝑓) ∧ 𝑝 = (𝑡𝑠))))
67 simp3r 1201 . . . . . . . 8 (((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑓𝑇𝑠𝐸) ∧ 𝑠𝑂) ∧ (𝑖𝑇𝑝𝐸)) ∧ 𝑡𝐸 ∧ (𝑖 = (𝑡𝑓) ∧ 𝑝 = (𝑡𝑠))) → 𝑝 = (𝑡𝑠))
6867fveq1d 6814 . . . . . . 7 (((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑓𝑇𝑠𝐸) ∧ 𝑠𝑂) ∧ (𝑖𝑇𝑝𝐸)) ∧ 𝑡𝐸 ∧ (𝑖 = (𝑡𝑓) ∧ 𝑝 = (𝑡𝑠))) → (𝑝‘((𝐽𝑠)‘𝑓)) = ((𝑡𝑠)‘((𝐽𝑠)‘𝑓)))
69 simp1l1 1265 . . . . . . . 8 (((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑓𝑇𝑠𝐸) ∧ 𝑠𝑂) ∧ (𝑖𝑇𝑝𝐸)) ∧ 𝑡𝐸 ∧ (𝑖 = (𝑡𝑓) ∧ 𝑝 = (𝑡𝑠))) → (𝐾 ∈ HL ∧ 𝑊𝐻))
70 simp2 1136 . . . . . . . . 9 (((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑓𝑇𝑠𝐸) ∧ 𝑠𝑂) ∧ (𝑖𝑇𝑝𝐸)) ∧ 𝑡𝐸 ∧ (𝑖 = (𝑡𝑓) ∧ 𝑝 = (𝑡𝑠))) → 𝑡𝐸)
71 simpl2r 1226 . . . . . . . . . 10 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑓𝑇𝑠𝐸) ∧ 𝑠𝑂) ∧ (𝑖𝑇𝑝𝐸)) → 𝑠𝐸)
72713ad2ant1 1132 . . . . . . . . 9 (((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑓𝑇𝑠𝐸) ∧ 𝑠𝑂) ∧ (𝑖𝑇𝑝𝐸)) ∧ 𝑡𝐸 ∧ (𝑖 = (𝑡𝑓) ∧ 𝑝 = (𝑡𝑠))) → 𝑠𝐸)
736, 14tendococl 39007 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑡𝐸𝑠𝐸) → (𝑡𝑠) ∈ 𝐸)
7469, 70, 72, 73syl3anc 1370 . . . . . . . 8 (((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑓𝑇𝑠𝐸) ∧ 𝑠𝑂) ∧ (𝑖𝑇𝑝𝐸)) ∧ 𝑡𝐸 ∧ (𝑖 = (𝑡𝑓) ∧ 𝑝 = (𝑡𝑠))) → (𝑡𝑠) ∈ 𝐸)
75 simp1l3 1267 . . . . . . . . 9 (((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑓𝑇𝑠𝐸) ∧ 𝑠𝑂) ∧ (𝑖𝑇𝑝𝐸)) ∧ 𝑡𝐸 ∧ (𝑖 = (𝑡𝑓) ∧ 𝑝 = (𝑡𝑠))) → 𝑠𝑂)
7669, 72, 75, 20syl3anc 1370 . . . . . . . 8 (((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑓𝑇𝑠𝐸) ∧ 𝑠𝑂) ∧ (𝑖𝑇𝑝𝐸)) ∧ 𝑡𝐸 ∧ (𝑖 = (𝑡𝑓) ∧ 𝑝 = (𝑡𝑠))) → (𝐽𝑠) ∈ 𝐸)
77 simpl2l 1225 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑓𝑇𝑠𝐸) ∧ 𝑠𝑂) ∧ (𝑖𝑇𝑝𝐸)) → 𝑓𝑇)
78773ad2ant1 1132 . . . . . . . 8 (((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑓𝑇𝑠𝐸) ∧ 𝑠𝑂) ∧ (𝑖𝑇𝑝𝐸)) ∧ 𝑡𝐸 ∧ (𝑖 = (𝑡𝑓) ∧ 𝑝 = (𝑡𝑠))) → 𝑓𝑇)
796, 13, 14tendocoval 39001 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ ((𝑡𝑠) ∈ 𝐸 ∧ (𝐽𝑠) ∈ 𝐸) ∧ 𝑓𝑇) → (((𝑡𝑠) ∘ (𝐽𝑠))‘𝑓) = ((𝑡𝑠)‘((𝐽𝑠)‘𝑓)))
8069, 74, 76, 78, 79syl121anc 1374 . . . . . . 7 (((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑓𝑇𝑠𝐸) ∧ 𝑠𝑂) ∧ (𝑖𝑇𝑝𝐸)) ∧ 𝑡𝐸 ∧ (𝑖 = (𝑡𝑓) ∧ 𝑝 = (𝑡𝑠))) → (((𝑡𝑠) ∘ (𝐽𝑠))‘𝑓) = ((𝑡𝑠)‘((𝐽𝑠)‘𝑓)))
81 coass 6191 . . . . . . . . 9 ((𝑡𝑠) ∘ (𝐽𝑠)) = (𝑡 ∘ (𝑠 ∘ (𝐽𝑠)))
8212, 6, 13, 14, 15, 16, 17, 18tendorinv 39341 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑠𝐸𝑠𝑂) → (𝑠 ∘ (𝐽𝑠)) = ( I ↾ 𝑇))
8369, 72, 75, 82syl3anc 1370 . . . . . . . . . . 11 (((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑓𝑇𝑠𝐸) ∧ 𝑠𝑂) ∧ (𝑖𝑇𝑝𝐸)) ∧ 𝑡𝐸 ∧ (𝑖 = (𝑡𝑓) ∧ 𝑝 = (𝑡𝑠))) → (𝑠 ∘ (𝐽𝑠)) = ( I ↾ 𝑇))
8483coeq2d 5792 . . . . . . . . . 10 (((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑓𝑇𝑠𝐸) ∧ 𝑠𝑂) ∧ (𝑖𝑇𝑝𝐸)) ∧ 𝑡𝐸 ∧ (𝑖 = (𝑡𝑓) ∧ 𝑝 = (𝑡𝑠))) → (𝑡 ∘ (𝑠 ∘ (𝐽𝑠))) = (𝑡 ∘ ( I ↾ 𝑇)))
856, 13, 14tendo1mulr 39006 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ 𝑡𝐸) → (𝑡 ∘ ( I ↾ 𝑇)) = 𝑡)
8669, 70, 85syl2anc 584 . . . . . . . . . 10 (((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑓𝑇𝑠𝐸) ∧ 𝑠𝑂) ∧ (𝑖𝑇𝑝𝐸)) ∧ 𝑡𝐸 ∧ (𝑖 = (𝑡𝑓) ∧ 𝑝 = (𝑡𝑠))) → (𝑡 ∘ ( I ↾ 𝑇)) = 𝑡)
8784, 86eqtrd 2777 . . . . . . . . 9 (((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑓𝑇𝑠𝐸) ∧ 𝑠𝑂) ∧ (𝑖𝑇𝑝𝐸)) ∧ 𝑡𝐸 ∧ (𝑖 = (𝑡𝑓) ∧ 𝑝 = (𝑡𝑠))) → (𝑡 ∘ (𝑠 ∘ (𝐽𝑠))) = 𝑡)
8881, 87eqtrid 2789 . . . . . . . 8 (((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑓𝑇𝑠𝐸) ∧ 𝑠𝑂) ∧ (𝑖𝑇𝑝𝐸)) ∧ 𝑡𝐸 ∧ (𝑖 = (𝑡𝑓) ∧ 𝑝 = (𝑡𝑠))) → ((𝑡𝑠) ∘ (𝐽𝑠)) = 𝑡)
8988fveq1d 6814 . . . . . . 7 (((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑓𝑇𝑠𝐸) ∧ 𝑠𝑂) ∧ (𝑖𝑇𝑝𝐸)) ∧ 𝑡𝐸 ∧ (𝑖 = (𝑡𝑓) ∧ 𝑝 = (𝑡𝑠))) → (((𝑡𝑠) ∘ (𝐽𝑠))‘𝑓) = (𝑡𝑓))
9068, 80, 893eqtr2rd 2784 . . . . . 6 (((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑓𝑇𝑠𝐸) ∧ 𝑠𝑂) ∧ (𝑖𝑇𝑝𝐸)) ∧ 𝑡𝐸 ∧ (𝑖 = (𝑡𝑓) ∧ 𝑝 = (𝑡𝑠))) → (𝑡𝑓) = (𝑝‘((𝐽𝑠)‘𝑓)))
91 simp3l 1200 . . . . . 6 (((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑓𝑇𝑠𝐸) ∧ 𝑠𝑂) ∧ (𝑖𝑇𝑝𝐸)) ∧ 𝑡𝐸 ∧ (𝑖 = (𝑡𝑓) ∧ 𝑝 = (𝑡𝑠))) → 𝑖 = (𝑡𝑓))
9245adantr 481 . . . . . . . 8 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑓𝑇𝑠𝐸) ∧ 𝑠𝑂) ∧ (𝑖𝑇𝑝𝐸)) → 𝐺 = ((𝐽𝑠)‘𝑓))
93923ad2ant1 1132 . . . . . . 7 (((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑓𝑇𝑠𝐸) ∧ 𝑠𝑂) ∧ (𝑖𝑇𝑝𝐸)) ∧ 𝑡𝐸 ∧ (𝑖 = (𝑡𝑓) ∧ 𝑝 = (𝑡𝑠))) → 𝐺 = ((𝐽𝑠)‘𝑓))
9493fveq2d 6816 . . . . . 6 (((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑓𝑇𝑠𝐸) ∧ 𝑠𝑂) ∧ (𝑖𝑇𝑝𝐸)) ∧ 𝑡𝐸 ∧ (𝑖 = (𝑡𝑓) ∧ 𝑝 = (𝑡𝑠))) → (𝑝𝐺) = (𝑝‘((𝐽𝑠)‘𝑓)))
9590, 91, 943eqtr4d 2787 . . . . 5 (((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑓𝑇𝑠𝐸) ∧ 𝑠𝑂) ∧ (𝑖𝑇𝑝𝐸)) ∧ 𝑡𝐸 ∧ (𝑖 = (𝑡𝑓) ∧ 𝑝 = (𝑡𝑠))) → 𝑖 = (𝑝𝐺))
9695rexlimdv3a 3153 . . . 4 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑓𝑇𝑠𝐸) ∧ 𝑠𝑂) ∧ (𝑖𝑇𝑝𝐸)) → (∃𝑡𝐸 (𝑖 = (𝑡𝑓) ∧ 𝑝 = (𝑡𝑠)) → 𝑖 = (𝑝𝐺)))
9796impr 455 . . 3 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑓𝑇𝑠𝐸) ∧ 𝑠𝑂) ∧ ((𝑖𝑇𝑝𝐸) ∧ ∃𝑡𝐸 (𝑖 = (𝑡𝑓) ∧ 𝑝 = (𝑡𝑠)))) → 𝑖 = (𝑝𝐺))
98 simprlr 777 . . 3 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑓𝑇𝑠𝐸) ∧ 𝑠𝑂) ∧ ((𝑖𝑇𝑝𝐸) ∧ ∃𝑡𝐸 (𝑖 = (𝑡𝑓) ∧ 𝑝 = (𝑡𝑠)))) → 𝑝𝐸)
9997, 98jca 512 . 2 ((((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑓𝑇𝑠𝐸) ∧ 𝑠𝑂) ∧ ((𝑖𝑇𝑝𝐸) ∧ ∃𝑡𝐸 (𝑖 = (𝑡𝑓) ∧ 𝑝 = (𝑡𝑠)))) → (𝑖 = (𝑝𝐺) ∧ 𝑝𝐸))
10066, 99impbida 798 1 (((𝐾 ∈ HL ∧ 𝑊𝐻) ∧ (𝑓𝑇𝑠𝐸) ∧ 𝑠𝑂) → ((𝑖 = (𝑝𝐺) ∧ 𝑝𝐸) ↔ ((𝑖𝑇𝑝𝐸) ∧ ∃𝑡𝐸 (𝑖 = (𝑡𝑓) ∧ 𝑝 = (𝑡𝑠)))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 396  w3a 1086   = wceq 1540  wcel 2105  wne 2941  wrex 3071   class class class wbr 5087  cmpt 5170   I cid 5506  cres 5610  ccom 5612  cfv 6466  crio 7273  Basecbs 16989  Scalarcsca 17042   ·𝑠 cvsca 17043  lecple 17046  occoc 17047  0gc0g 17227  invrcinvr 19988  LSubSpclss 20276  LSpanclspn 20316  LSAtomsclsa 37208  Atomscatm 37497  HLchlt 37584  LHypclh 38219  LTrncltrn 38336  trLctrl 38393  TEndoctendo 38987  DVecHcdvh 39313  DIsoHcdih 39463
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 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2708  ax-rep 5224  ax-sep 5238  ax-nul 5245  ax-pow 5303  ax-pr 5367  ax-un 7630  ax-cnex 11007  ax-resscn 11008  ax-1cn 11009  ax-icn 11010  ax-addcl 11011  ax-addrcl 11012  ax-mulcl 11013  ax-mulrcl 11014  ax-mulcom 11015  ax-addass 11016  ax-mulass 11017  ax-distr 11018  ax-i2m1 11019  ax-1ne0 11020  ax-1rid 11021  ax-rnegex 11022  ax-rrecex 11023  ax-cnre 11024  ax-pre-lttri 11025  ax-pre-lttrn 11026  ax-pre-ltadd 11027  ax-pre-mulgt0 11028  ax-riotaBAD 37187
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2887  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rmo 3350  df-reu 3351  df-rab 3405  df-v 3443  df-sbc 3727  df-csb 3843  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-pss 3916  df-nul 4268  df-if 4472  df-pw 4547  df-sn 4572  df-pr 4574  df-tp 4576  df-op 4578  df-uni 4851  df-iun 4939  df-iin 4940  df-br 5088  df-opab 5150  df-mpt 5171  df-tr 5205  df-id 5507  df-eprel 5513  df-po 5521  df-so 5522  df-fr 5563  df-we 5565  df-xp 5614  df-rel 5615  df-cnv 5616  df-co 5617  df-dm 5618  df-rn 5619  df-res 5620  df-ima 5621  df-pred 6225  df-ord 6292  df-on 6293  df-lim 6294  df-suc 6295  df-iota 6418  df-fun 6468  df-fn 6469  df-f 6470  df-f1 6471  df-fo 6472  df-f1o 6473  df-fv 6474  df-riota 7274  df-ov 7320  df-oprab 7321  df-mpo 7322  df-om 7760  df-1st 7878  df-2nd 7879  df-tpos 8091  df-undef 8138  df-frecs 8146  df-wrecs 8177  df-recs 8251  df-rdg 8290  df-1o 8346  df-er 8548  df-map 8667  df-en 8784  df-dom 8785  df-sdom 8786  df-fin 8787  df-pnf 11091  df-mnf 11092  df-xr 11093  df-ltxr 11094  df-le 11095  df-sub 11287  df-neg 11288  df-nn 12054  df-2 12116  df-3 12117  df-4 12118  df-5 12119  df-6 12120  df-n0 12314  df-z 12400  df-uz 12663  df-fz 13320  df-struct 16925  df-sets 16942  df-slot 16960  df-ndx 16972  df-base 16990  df-ress 17019  df-plusg 17052  df-mulr 17053  df-sca 17055  df-vsca 17056  df-0g 17229  df-proset 18090  df-poset 18108  df-plt 18125  df-lub 18141  df-glb 18142  df-join 18143  df-meet 18144  df-p0 18220  df-p1 18221  df-lat 18227  df-clat 18294  df-mgm 18403  df-sgrp 18452  df-mnd 18463  df-grp 18656  df-minusg 18657  df-mgp 19796  df-ur 19813  df-ring 19860  df-oppr 19937  df-dvdsr 19958  df-unit 19959  df-invr 19989  df-dvr 20000  df-drng 20072  df-oposet 37410  df-ol 37412  df-oml 37413  df-covers 37500  df-ats 37501  df-atl 37532  df-cvlat 37556  df-hlat 37585  df-llines 37733  df-lplanes 37734  df-lvols 37735  df-lines 37736  df-psubsp 37738  df-pmap 37739  df-padd 38031  df-lhyp 38223  df-laut 38224  df-ldil 38339  df-ltrn 38340  df-trl 38394  df-tendo 38990  df-edring 38992  df-dvech 39314
This theorem is referenced by:  dih1dimatlem  39564
  Copyright terms: Public domain W3C validator