Metamath Proof Explorer

Theorem dvh4dimat

Description: There is an atom that is outside the subspace sum of 3 others. (Contributed by NM, 25-Apr-2015)

Ref Expression
Hypotheses dvh4dimat.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
dvh4dimat.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
dvh4dimat.s ⊢ ⊕ = ( LSSum ‘ 𝑈 )
dvh4dimat.a ⊢ 𝐴 = ( LSAtoms ‘ 𝑈 )
dvh4dimat.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
dvh4dimat.p ⊢ ( 𝜑 → 𝑃 ∈ 𝐴 )
dvh4dimat.q ⊢ ( 𝜑 → 𝑄 ∈ 𝐴 )
dvh4dimat.r ⊢ ( 𝜑 → 𝑅 ∈ 𝐴 )
Assertion dvh4dimat ( 𝜑 → ∃ 𝑠 ∈ 𝐴 ¬ 𝑠 ⊆ ( ( 𝑃 ⊕ 𝑄 ) ⊕ 𝑅 ) )

Proof

Step Hyp Ref Expression
1 dvh4dimat.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2 dvh4dimat.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
3 dvh4dimat.s ⊢ ⊕ = ( LSSum ‘ 𝑈 )
4 dvh4dimat.a ⊢ 𝐴 = ( LSAtoms ‘ 𝑈 )
5 dvh4dimat.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
6 dvh4dimat.p ⊢ ( 𝜑 → 𝑃 ∈ 𝐴 )
7 dvh4dimat.q ⊢ ( 𝜑 → 𝑄 ∈ 𝐴 )
8 dvh4dimat.r ⊢ ( 𝜑 → 𝑅 ∈ 𝐴 )
9 5 simpld ⊢ ( 𝜑 → 𝐾 ∈ HL )
10 eqid ⊢ ( Atoms ‘ 𝐾 ) = ( Atoms ‘ 𝐾 )
11 eqid ⊢ ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
12 10 1 2 11 4 dihlatat ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑃 ∈ 𝐴 ) → ( ◡ ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑃 ) ∈ ( Atoms ‘ 𝐾 ) )
13 5 6 12 syl2anc ⊢ ( 𝜑 → ( ◡ ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑃 ) ∈ ( Atoms ‘ 𝐾 ) )
14 10 1 2 11 4 dihlatat ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑄 ∈ 𝐴 ) → ( ◡ ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑄 ) ∈ ( Atoms ‘ 𝐾 ) )
15 5 7 14 syl2anc ⊢ ( 𝜑 → ( ◡ ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑄 ) ∈ ( Atoms ‘ 𝐾 ) )
16 10 1 2 11 4 dihlatat ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑅 ∈ 𝐴 ) → ( ◡ ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑅 ) ∈ ( Atoms ‘ 𝐾 ) )
17 5 8 16 syl2anc ⊢ ( 𝜑 → ( ◡ ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑅 ) ∈ ( Atoms ‘ 𝐾 ) )
18 eqid ⊢ ( join ‘ 𝐾 ) = ( join ‘ 𝐾 )
19 eqid ⊢ ( le ‘ 𝐾 ) = ( le ‘ 𝐾 )
20 18 19 10 3dim3 ⊢ ( ( 𝐾 ∈ HL ∧ ( ( ◡ ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑃 ) ∈ ( Atoms ‘ 𝐾 ) ∧ ( ◡ ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑄 ) ∈ ( Atoms ‘ 𝐾 ) ∧ ( ◡ ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑅 ) ∈ ( Atoms ‘ 𝐾 ) ) ) → ∃ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ¬ 𝑟 ( le ‘ 𝐾 ) ( ( ( ◡ ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑃 ) ( join ‘ 𝐾 ) ( ◡ ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑄 ) ) ( join ‘ 𝐾 ) ( ◡ ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑅 ) ) )
21 9 13 15 17 20 syl13anc ⊢ ( 𝜑 → ∃ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ¬ 𝑟 ( le ‘ 𝐾 ) ( ( ( ◡ ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑃 ) ( join ‘ 𝐾 ) ( ◡ ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑄 ) ) ( join ‘ 𝐾 ) ( ◡ ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑅 ) ) )
22 5 adantr ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
23 1 2 11 4 dih1dimat ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑃 ∈ 𝐴 ) → 𝑃 ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) )
24 5 6 23 syl2anc ⊢ ( 𝜑 → 𝑃 ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) )
25 1 11 2 3 4 5 24 7 dihsmatrn ⊢ ( 𝜑 → ( 𝑃 ⊕ 𝑄 ) ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) )
26 25 adantr ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) → ( 𝑃 ⊕ 𝑄 ) ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) )
27 8 adantr ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) → 𝑅 ∈ 𝐴 )
28 18 1 11 2 3 4 22 26 27 dihjat4 ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) → ( ( 𝑃 ⊕ 𝑄 ) ⊕ 𝑅 ) = ( ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ◡ ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑃 ⊕ 𝑄 ) ) ( join ‘ 𝐾 ) ( ◡ ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑅 ) ) ) )
29 24 adantr ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) → 𝑃 ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) )
30 7 adantr ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) → 𝑄 ∈ 𝐴 )
31 18 1 11 2 3 4 22 29 30 dihjat6 ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) → ( ◡ ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑃 ⊕ 𝑄 ) ) = ( ( ◡ ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑃 ) ( join ‘ 𝐾 ) ( ◡ ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑄 ) ) )
32 31 fvoveq1d ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) → ( ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ◡ ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑃 ⊕ 𝑄 ) ) ( join ‘ 𝐾 ) ( ◡ ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑅 ) ) ) = ( ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( ◡ ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑃 ) ( join ‘ 𝐾 ) ( ◡ ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑄 ) ) ( join ‘ 𝐾 ) ( ◡ ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑅 ) ) ) )
33 28 32 eqtrd ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) → ( ( 𝑃 ⊕ 𝑄 ) ⊕ 𝑅 ) = ( ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( ◡ ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑃 ) ( join ‘ 𝐾 ) ( ◡ ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑄 ) ) ( join ‘ 𝐾 ) ( ◡ ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑅 ) ) ) )
34 33 sseq2d ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) → ( ( ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑟 ) ⊆ ( ( 𝑃 ⊕ 𝑄 ) ⊕ 𝑅 ) ↔ ( ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑟 ) ⊆ ( ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( ◡ ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑃 ) ( join ‘ 𝐾 ) ( ◡ ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑄 ) ) ( join ‘ 𝐾 ) ( ◡ ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑅 ) ) ) ) )
35 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
36 35 10 atbase ⊢ ( 𝑟 ∈ ( Atoms ‘ 𝐾 ) → 𝑟 ∈ ( Base ‘ 𝐾 ) )
37 36 adantl ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) → 𝑟 ∈ ( Base ‘ 𝐾 ) )
38 9 hllatd ⊢ ( 𝜑 → 𝐾 ∈ Lat )
39 35 18 10 hlatjcl ⊢ ( ( 𝐾 ∈ HL ∧ ( ◡ ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑃 ) ∈ ( Atoms ‘ 𝐾 ) ∧ ( ◡ ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑄 ) ∈ ( Atoms ‘ 𝐾 ) ) → ( ( ◡ ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑃 ) ( join ‘ 𝐾 ) ( ◡ ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑄 ) ) ∈ ( Base ‘ 𝐾 ) )
40 9 13 15 39 syl3anc ⊢ ( 𝜑 → ( ( ◡ ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑃 ) ( join ‘ 𝐾 ) ( ◡ ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑄 ) ) ∈ ( Base ‘ 𝐾 ) )
41 35 10 atbase ⊢ ( ( ◡ ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑅 ) ∈ ( Atoms ‘ 𝐾 ) → ( ◡ ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑅 ) ∈ ( Base ‘ 𝐾 ) )
42 17 41 syl ⊢ ( 𝜑 → ( ◡ ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑅 ) ∈ ( Base ‘ 𝐾 ) )
43 35 18 latjcl ⊢ ( ( 𝐾 ∈ Lat ∧ ( ( ◡ ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑃 ) ( join ‘ 𝐾 ) ( ◡ ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑄 ) ) ∈ ( Base ‘ 𝐾 ) ∧ ( ◡ ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑅 ) ∈ ( Base ‘ 𝐾 ) ) → ( ( ( ◡ ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑃 ) ( join ‘ 𝐾 ) ( ◡ ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑄 ) ) ( join ‘ 𝐾 ) ( ◡ ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑅 ) ) ∈ ( Base ‘ 𝐾 ) )
44 38 40 42 43 syl3anc ⊢ ( 𝜑 → ( ( ( ◡ ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑃 ) ( join ‘ 𝐾 ) ( ◡ ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑄 ) ) ( join ‘ 𝐾 ) ( ◡ ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑅 ) ) ∈ ( Base ‘ 𝐾 ) )
45 44 adantr ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) → ( ( ( ◡ ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑃 ) ( join ‘ 𝐾 ) ( ◡ ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑄 ) ) ( join ‘ 𝐾 ) ( ◡ ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑅 ) ) ∈ ( Base ‘ 𝐾 ) )
46 35 19 1 11 dihord ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑟 ∈ ( Base ‘ 𝐾 ) ∧ ( ( ( ◡ ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑃 ) ( join ‘ 𝐾 ) ( ◡ ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑄 ) ) ( join ‘ 𝐾 ) ( ◡ ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑅 ) ) ∈ ( Base ‘ 𝐾 ) ) → ( ( ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑟 ) ⊆ ( ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( ◡ ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑃 ) ( join ‘ 𝐾 ) ( ◡ ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑄 ) ) ( join ‘ 𝐾 ) ( ◡ ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑅 ) ) ) ↔ 𝑟 ( le ‘ 𝐾 ) ( ( ( ◡ ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑃 ) ( join ‘ 𝐾 ) ( ◡ ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑄 ) ) ( join ‘ 𝐾 ) ( ◡ ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑅 ) ) ) )
47 22 37 45 46 syl3anc ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) → ( ( ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑟 ) ⊆ ( ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( ( ◡ ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑃 ) ( join ‘ 𝐾 ) ( ◡ ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑄 ) ) ( join ‘ 𝐾 ) ( ◡ ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑅 ) ) ) ↔ 𝑟 ( le ‘ 𝐾 ) ( ( ( ◡ ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑃 ) ( join ‘ 𝐾 ) ( ◡ ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑄 ) ) ( join ‘ 𝐾 ) ( ◡ ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑅 ) ) ) )
48 34 47 bitr2d ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) → ( 𝑟 ( le ‘ 𝐾 ) ( ( ( ◡ ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑃 ) ( join ‘ 𝐾 ) ( ◡ ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑄 ) ) ( join ‘ 𝐾 ) ( ◡ ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑅 ) ) ↔ ( ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑟 ) ⊆ ( ( 𝑃 ⊕ 𝑄 ) ⊕ 𝑅 ) ) )
49 48 notbid ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) → ( ¬ 𝑟 ( le ‘ 𝐾 ) ( ( ( ◡ ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑃 ) ( join ‘ 𝐾 ) ( ◡ ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑄 ) ) ( join ‘ 𝐾 ) ( ◡ ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑅 ) ) ↔ ¬ ( ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑟 ) ⊆ ( ( 𝑃 ⊕ 𝑄 ) ⊕ 𝑅 ) ) )
50 49 rexbidva ⊢ ( 𝜑 → ( ∃ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ¬ 𝑟 ( le ‘ 𝐾 ) ( ( ( ◡ ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑃 ) ( join ‘ 𝐾 ) ( ◡ ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑄 ) ) ( join ‘ 𝐾 ) ( ◡ ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑅 ) ) ↔ ∃ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ¬ ( ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑟 ) ⊆ ( ( 𝑃 ⊕ 𝑄 ) ⊕ 𝑅 ) ) )
51 21 50 mpbid ⊢ ( 𝜑 → ∃ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ¬ ( ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑟 ) ⊆ ( ( 𝑃 ⊕ 𝑄 ) ⊕ 𝑅 ) )
52 10 1 2 11 4 dihatlat ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) → ( ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑟 ) ∈ 𝐴 )
53 5 52 sylan ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ) → ( ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑟 ) ∈ 𝐴 )
54 10 1 2 11 4 dihlatat ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑠 ∈ 𝐴 ) → ( ◡ ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑠 ) ∈ ( Atoms ‘ 𝐾 ) )
55 5 54 sylan ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐴 ) → ( ◡ ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑠 ) ∈ ( Atoms ‘ 𝐾 ) )
56 5 adantr ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐴 ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
57 1 2 11 4 dih1dimat ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑠 ∈ 𝐴 ) → 𝑠 ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) )
58 5 57 sylan ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐴 ) → 𝑠 ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) )
59 1 11 dihcnvid2 ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑠 ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ) → ( ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ◡ ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑠 ) ) = 𝑠 )
60 56 58 59 syl2anc ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐴 ) → ( ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ◡ ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑠 ) ) = 𝑠 )
61 60 eqcomd ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐴 ) → 𝑠 = ( ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ◡ ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑠 ) ) )
62 fveq2 ⊢ ( 𝑟 = ( ◡ ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑠 ) → ( ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑟 ) = ( ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ◡ ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑠 ) ) )
63 62 rspceeqv ⊢ ( ( ( ◡ ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑠 ) ∈ ( Atoms ‘ 𝐾 ) ∧ 𝑠 = ( ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ◡ ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑠 ) ) ) → ∃ 𝑟 ∈ ( Atoms ‘ 𝐾 ) 𝑠 = ( ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑟 ) )
64 55 61 63 syl2anc ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐴 ) → ∃ 𝑟 ∈ ( Atoms ‘ 𝐾 ) 𝑠 = ( ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑟 ) )
65 sseq1 ⊢ ( 𝑠 = ( ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑟 ) → ( 𝑠 ⊆ ( ( 𝑃 ⊕ 𝑄 ) ⊕ 𝑅 ) ↔ ( ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑟 ) ⊆ ( ( 𝑃 ⊕ 𝑄 ) ⊕ 𝑅 ) ) )
66 65 notbid ⊢ ( 𝑠 = ( ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑟 ) → ( ¬ 𝑠 ⊆ ( ( 𝑃 ⊕ 𝑄 ) ⊕ 𝑅 ) ↔ ¬ ( ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑟 ) ⊆ ( ( 𝑃 ⊕ 𝑄 ) ⊕ 𝑅 ) ) )
67 66 adantl ⊢ ( ( 𝜑 ∧ 𝑠 = ( ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑟 ) ) → ( ¬ 𝑠 ⊆ ( ( 𝑃 ⊕ 𝑄 ) ⊕ 𝑅 ) ↔ ¬ ( ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑟 ) ⊆ ( ( 𝑃 ⊕ 𝑄 ) ⊕ 𝑅 ) ) )
68 53 64 67 rexxfrd ⊢ ( 𝜑 → ( ∃ 𝑠 ∈ 𝐴 ¬ 𝑠 ⊆ ( ( 𝑃 ⊕ 𝑄 ) ⊕ 𝑅 ) ↔ ∃ 𝑟 ∈ ( Atoms ‘ 𝐾 ) ¬ ( ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑟 ) ⊆ ( ( 𝑃 ⊕ 𝑄 ) ⊕ 𝑅 ) ) )
69 51 68 mpbird ⊢ ( 𝜑 → ∃ 𝑠 ∈ 𝐴 ¬ 𝑠 ⊆ ( ( 𝑃 ⊕ 𝑄 ) ⊕ 𝑅 ) )