Metamath Proof Explorer


Theorem dicn0

Description: The value of the partial isomorphism C is not empty. (Contributed by NM, 15-Feb-2014)

Ref Expression
Hypotheses dicn0.l ˙ = K
dicn0.a A = Atoms K
dicn0.h H = LHyp K
dicn0.i I = DIsoC K W
Assertion dicn0 K HL W H Q A ¬ Q ˙ W I Q

Proof

Step Hyp Ref Expression
1 dicn0.l ˙ = K
2 dicn0.a A = Atoms K
3 dicn0.h H = LHyp K
4 dicn0.i I = DIsoC K W
5 simpl K HL W H Q A ¬ Q ˙ W K HL W H
6 eqid oc K = oc K
7 1 6 2 3 lhpocnel K HL W H oc K W A ¬ oc K W ˙ W
8 7 adantr K HL W H Q A ¬ Q ˙ W oc K W A ¬ oc K W ˙ W
9 simpr K HL W H Q A ¬ Q ˙ W Q A ¬ Q ˙ W
10 eqid LTrn K W = LTrn K W
11 eqid ι g LTrn K W | g oc K W = Q = ι g LTrn K W | g oc K W = Q
12 1 2 3 10 11 ltrniotacl K HL W H oc K W A ¬ oc K W ˙ W Q A ¬ Q ˙ W ι g LTrn K W | g oc K W = Q LTrn K W
13 5 8 9 12 syl3anc K HL W H Q A ¬ Q ˙ W ι g LTrn K W | g oc K W = Q LTrn K W
14 eqid f LTrn K W I Base K = f LTrn K W I Base K
15 eqid Base K = Base K
16 14 15 tendo02 ι g LTrn K W | g oc K W = Q LTrn K W f LTrn K W I Base K ι g LTrn K W | g oc K W = Q = I Base K
17 13 16 syl K HL W H Q A ¬ Q ˙ W f LTrn K W I Base K ι g LTrn K W | g oc K W = Q = I Base K
18 17 eqcomd K HL W H Q A ¬ Q ˙ W I Base K = f LTrn K W I Base K ι g LTrn K W | g oc K W = Q
19 eqid TEndo K W = TEndo K W
20 15 3 10 19 14 tendo0cl K HL W H f LTrn K W I Base K TEndo K W
21 20 adantr K HL W H Q A ¬ Q ˙ W f LTrn K W I Base K TEndo K W
22 eqid oc K W = oc K W
23 fvex Base K V
24 resiexg Base K V I Base K V
25 23 24 ax-mp I Base K V
26 fvex LTrn K W V
27 26 mptex f LTrn K W I Base K V
28 1 2 3 22 10 19 4 25 27 dicopelval K HL W H Q A ¬ Q ˙ W I Base K f LTrn K W I Base K I Q I Base K = f LTrn K W I Base K ι g LTrn K W | g oc K W = Q f LTrn K W I Base K TEndo K W
29 18 21 28 mpbir2and K HL W H Q A ¬ Q ˙ W I Base K f LTrn K W I Base K I Q
30 29 ne0d K HL W H Q A ¬ Q ˙ W I Q