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

Theorem islshpat 37235
Description: Hyperplane properties expressed with subspace sum and an atom. TODO: can proof be shortened? Seems long for a simple variation of islshpsm 37198. (Contributed by NM, 11-Jan-2015.)
Hypotheses
Ref Expression
islshpat.v 𝑉 = (Base‘𝑊)
islshpat.s 𝑆 = (LSubSp‘𝑊)
islshpat.p = (LSSum‘𝑊)
islshpat.h 𝐻 = (LSHyp‘𝑊)
islshpat.a 𝐴 = (LSAtoms‘𝑊)
islshpat.w (𝜑𝑊 ∈ LMod)
Assertion
Ref Expression
islshpat (𝜑 → (𝑈𝐻 ↔ (𝑈𝑆𝑈𝑉 ∧ ∃𝑞𝐴 (𝑈 𝑞) = 𝑉)))
Distinct variable groups:   ,𝑞   𝑆,𝑞   𝑈,𝑞   𝑉,𝑞   𝑊,𝑞   𝜑,𝑞
Allowed substitution hints:   𝐴(𝑞)   𝐻(𝑞)

Proof of Theorem islshpat
Dummy variable 𝑣 is distinct from all other variables.
StepHypRef Expression
1 islshpat.v . . 3 𝑉 = (Base‘𝑊)
2 eqid 2737 . . 3 (LSpan‘𝑊) = (LSpan‘𝑊)
3 islshpat.s . . 3 𝑆 = (LSubSp‘𝑊)
4 islshpat.p . . 3 = (LSSum‘𝑊)
5 islshpat.h . . 3 𝐻 = (LSHyp‘𝑊)
6 islshpat.w . . 3 (𝜑𝑊 ∈ LMod)
71, 2, 3, 4, 5, 6islshpsm 37198 . 2 (𝜑 → (𝑈𝐻 ↔ (𝑈𝑆𝑈𝑉 ∧ ∃𝑣𝑉 (𝑈 ((LSpan‘𝑊)‘{𝑣})) = 𝑉)))
8 df-3an 1088 . . . . 5 ((𝑈𝑆𝑈𝑉 ∧ ∃𝑣𝑉 (𝑈 ((LSpan‘𝑊)‘{𝑣})) = 𝑉) ↔ ((𝑈𝑆𝑈𝑉) ∧ ∃𝑣𝑉 (𝑈 ((LSpan‘𝑊)‘{𝑣})) = 𝑉))
9 r19.42v 3184 . . . . 5 (∃𝑣𝑉 ((𝑈𝑆𝑈𝑉) ∧ (𝑈 ((LSpan‘𝑊)‘{𝑣})) = 𝑉) ↔ ((𝑈𝑆𝑈𝑉) ∧ ∃𝑣𝑉 (𝑈 ((LSpan‘𝑊)‘{𝑣})) = 𝑉))
108, 9bitr4i 277 . . . 4 ((𝑈𝑆𝑈𝑉 ∧ ∃𝑣𝑉 (𝑈 ((LSpan‘𝑊)‘{𝑣})) = 𝑉) ↔ ∃𝑣𝑉 ((𝑈𝑆𝑈𝑉) ∧ (𝑈 ((LSpan‘𝑊)‘{𝑣})) = 𝑉))
11 df-rex 3072 . . . . . . . 8 (∃𝑣𝑉 ((𝑈𝑆𝑈𝑉) ∧ (𝑈 ((LSpan‘𝑊)‘{𝑣})) = 𝑉) ↔ ∃𝑣(𝑣𝑉 ∧ ((𝑈𝑆𝑈𝑉) ∧ (𝑈 ((LSpan‘𝑊)‘{𝑣})) = 𝑉)))
12 simpr 485 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑣𝑉) ∧ (𝑈𝑆𝑈𝑉)) ∧ 𝑣 = (0g𝑊)) → 𝑣 = (0g𝑊))
1312sneqd 4583 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑣𝑉) ∧ (𝑈𝑆𝑈𝑉)) ∧ 𝑣 = (0g𝑊)) → {𝑣} = {(0g𝑊)})
1413fveq2d 6815 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑣𝑉) ∧ (𝑈𝑆𝑈𝑉)) ∧ 𝑣 = (0g𝑊)) → ((LSpan‘𝑊)‘{𝑣}) = ((LSpan‘𝑊)‘{(0g𝑊)}))
156ad3antrrr 727 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑣𝑉) ∧ (𝑈𝑆𝑈𝑉)) ∧ 𝑣 = (0g𝑊)) → 𝑊 ∈ LMod)
16 eqid 2737 . . . . . . . . . . . . . . . . . . . . 21 (0g𝑊) = (0g𝑊)
1716, 2lspsn0 20342 . . . . . . . . . . . . . . . . . . . 20 (𝑊 ∈ LMod → ((LSpan‘𝑊)‘{(0g𝑊)}) = {(0g𝑊)})
1815, 17syl 17 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑣𝑉) ∧ (𝑈𝑆𝑈𝑉)) ∧ 𝑣 = (0g𝑊)) → ((LSpan‘𝑊)‘{(0g𝑊)}) = {(0g𝑊)})
1914, 18eqtrd 2777 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑣𝑉) ∧ (𝑈𝑆𝑈𝑉)) ∧ 𝑣 = (0g𝑊)) → ((LSpan‘𝑊)‘{𝑣}) = {(0g𝑊)})
2019oveq2d 7331 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑣𝑉) ∧ (𝑈𝑆𝑈𝑉)) ∧ 𝑣 = (0g𝑊)) → (𝑈 ((LSpan‘𝑊)‘{𝑣})) = (𝑈 {(0g𝑊)}))
21 simplrl 774 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑣𝑉) ∧ (𝑈𝑆𝑈𝑉)) ∧ 𝑣 = (0g𝑊)) → 𝑈𝑆)
223lsssubg 20291 . . . . . . . . . . . . . . . . . . 19 ((𝑊 ∈ LMod ∧ 𝑈𝑆) → 𝑈 ∈ (SubGrp‘𝑊))
2315, 21, 22syl2anc 584 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑣𝑉) ∧ (𝑈𝑆𝑈𝑉)) ∧ 𝑣 = (0g𝑊)) → 𝑈 ∈ (SubGrp‘𝑊))
2416, 4lsm01 19345 . . . . . . . . . . . . . . . . . 18 (𝑈 ∈ (SubGrp‘𝑊) → (𝑈 {(0g𝑊)}) = 𝑈)
2523, 24syl 17 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑣𝑉) ∧ (𝑈𝑆𝑈𝑉)) ∧ 𝑣 = (0g𝑊)) → (𝑈 {(0g𝑊)}) = 𝑈)
2620, 25eqtrd 2777 . . . . . . . . . . . . . . . 16 ((((𝜑𝑣𝑉) ∧ (𝑈𝑆𝑈𝑉)) ∧ 𝑣 = (0g𝑊)) → (𝑈 ((LSpan‘𝑊)‘{𝑣})) = 𝑈)
27 simplrr 775 . . . . . . . . . . . . . . . 16 ((((𝜑𝑣𝑉) ∧ (𝑈𝑆𝑈𝑉)) ∧ 𝑣 = (0g𝑊)) → 𝑈𝑉)
2826, 27eqnetrd 3009 . . . . . . . . . . . . . . 15 ((((𝜑𝑣𝑉) ∧ (𝑈𝑆𝑈𝑉)) ∧ 𝑣 = (0g𝑊)) → (𝑈 ((LSpan‘𝑊)‘{𝑣})) ≠ 𝑉)
2928ex 413 . . . . . . . . . . . . . 14 (((𝜑𝑣𝑉) ∧ (𝑈𝑆𝑈𝑉)) → (𝑣 = (0g𝑊) → (𝑈 ((LSpan‘𝑊)‘{𝑣})) ≠ 𝑉))
3029necon2d 2964 . . . . . . . . . . . . 13 (((𝜑𝑣𝑉) ∧ (𝑈𝑆𝑈𝑉)) → ((𝑈 ((LSpan‘𝑊)‘{𝑣})) = 𝑉𝑣 ≠ (0g𝑊)))
3130pm4.71rd 563 . . . . . . . . . . . 12 (((𝜑𝑣𝑉) ∧ (𝑈𝑆𝑈𝑉)) → ((𝑈 ((LSpan‘𝑊)‘{𝑣})) = 𝑉 ↔ (𝑣 ≠ (0g𝑊) ∧ (𝑈 ((LSpan‘𝑊)‘{𝑣})) = 𝑉)))
3231pm5.32da 579 . . . . . . . . . . 11 ((𝜑𝑣𝑉) → (((𝑈𝑆𝑈𝑉) ∧ (𝑈 ((LSpan‘𝑊)‘{𝑣})) = 𝑉) ↔ ((𝑈𝑆𝑈𝑉) ∧ (𝑣 ≠ (0g𝑊) ∧ (𝑈 ((LSpan‘𝑊)‘{𝑣})) = 𝑉))))
3332pm5.32da 579 . . . . . . . . . 10 (𝜑 → ((𝑣𝑉 ∧ ((𝑈𝑆𝑈𝑉) ∧ (𝑈 ((LSpan‘𝑊)‘{𝑣})) = 𝑉)) ↔ (𝑣𝑉 ∧ ((𝑈𝑆𝑈𝑉) ∧ (𝑣 ≠ (0g𝑊) ∧ (𝑈 ((LSpan‘𝑊)‘{𝑣})) = 𝑉)))))
34 eldifsn 4732 . . . . . . . . . . . 12 (𝑣 ∈ (𝑉 ∖ {(0g𝑊)}) ↔ (𝑣𝑉𝑣 ≠ (0g𝑊)))
3534anbi1i 624 . . . . . . . . . . 11 ((𝑣 ∈ (𝑉 ∖ {(0g𝑊)}) ∧ ((𝑈𝑆𝑈𝑉) ∧ (𝑈 ((LSpan‘𝑊)‘{𝑣})) = 𝑉)) ↔ ((𝑣𝑉𝑣 ≠ (0g𝑊)) ∧ ((𝑈𝑆𝑈𝑉) ∧ (𝑈 ((LSpan‘𝑊)‘{𝑣})) = 𝑉)))
36 anass 469 . . . . . . . . . . . 12 (((𝑣𝑉𝑣 ≠ (0g𝑊)) ∧ ((𝑈𝑆𝑈𝑉) ∧ (𝑈 ((LSpan‘𝑊)‘{𝑣})) = 𝑉)) ↔ (𝑣𝑉 ∧ (𝑣 ≠ (0g𝑊) ∧ ((𝑈𝑆𝑈𝑉) ∧ (𝑈 ((LSpan‘𝑊)‘{𝑣})) = 𝑉))))
37 an12 642 . . . . . . . . . . . . 13 ((𝑣 ≠ (0g𝑊) ∧ ((𝑈𝑆𝑈𝑉) ∧ (𝑈 ((LSpan‘𝑊)‘{𝑣})) = 𝑉)) ↔ ((𝑈𝑆𝑈𝑉) ∧ (𝑣 ≠ (0g𝑊) ∧ (𝑈 ((LSpan‘𝑊)‘{𝑣})) = 𝑉)))
3837anbi2i 623 . . . . . . . . . . . 12 ((𝑣𝑉 ∧ (𝑣 ≠ (0g𝑊) ∧ ((𝑈𝑆𝑈𝑉) ∧ (𝑈 ((LSpan‘𝑊)‘{𝑣})) = 𝑉))) ↔ (𝑣𝑉 ∧ ((𝑈𝑆𝑈𝑉) ∧ (𝑣 ≠ (0g𝑊) ∧ (𝑈 ((LSpan‘𝑊)‘{𝑣})) = 𝑉))))
3936, 38bitri 274 . . . . . . . . . . 11 (((𝑣𝑉𝑣 ≠ (0g𝑊)) ∧ ((𝑈𝑆𝑈𝑉) ∧ (𝑈 ((LSpan‘𝑊)‘{𝑣})) = 𝑉)) ↔ (𝑣𝑉 ∧ ((𝑈𝑆𝑈𝑉) ∧ (𝑣 ≠ (0g𝑊) ∧ (𝑈 ((LSpan‘𝑊)‘{𝑣})) = 𝑉))))
4035, 39bitr2i 275 . . . . . . . . . 10 ((𝑣𝑉 ∧ ((𝑈𝑆𝑈𝑉) ∧ (𝑣 ≠ (0g𝑊) ∧ (𝑈 ((LSpan‘𝑊)‘{𝑣})) = 𝑉))) ↔ (𝑣 ∈ (𝑉 ∖ {(0g𝑊)}) ∧ ((𝑈𝑆𝑈𝑉) ∧ (𝑈 ((LSpan‘𝑊)‘{𝑣})) = 𝑉)))
4133, 40bitrdi 286 . . . . . . . . 9 (𝜑 → ((𝑣𝑉 ∧ ((𝑈𝑆𝑈𝑉) ∧ (𝑈 ((LSpan‘𝑊)‘{𝑣})) = 𝑉)) ↔ (𝑣 ∈ (𝑉 ∖ {(0g𝑊)}) ∧ ((𝑈𝑆𝑈𝑉) ∧ (𝑈 ((LSpan‘𝑊)‘{𝑣})) = 𝑉))))
4241exbidv 1923 . . . . . . . 8 (𝜑 → (∃𝑣(𝑣𝑉 ∧ ((𝑈𝑆𝑈𝑉) ∧ (𝑈 ((LSpan‘𝑊)‘{𝑣})) = 𝑉)) ↔ ∃𝑣(𝑣 ∈ (𝑉 ∖ {(0g𝑊)}) ∧ ((𝑈𝑆𝑈𝑉) ∧ (𝑈 ((LSpan‘𝑊)‘{𝑣})) = 𝑉))))
4311, 42bitrid 282 . . . . . . 7 (𝜑 → (∃𝑣𝑉 ((𝑈𝑆𝑈𝑉) ∧ (𝑈 ((LSpan‘𝑊)‘{𝑣})) = 𝑉) ↔ ∃𝑣(𝑣 ∈ (𝑉 ∖ {(0g𝑊)}) ∧ ((𝑈𝑆𝑈𝑉) ∧ (𝑈 ((LSpan‘𝑊)‘{𝑣})) = 𝑉))))
44 fvex 6824 . . . . . . . . . 10 ((LSpan‘𝑊)‘{𝑣}) ∈ V
4544rexcom4b 3470 . . . . . . . . 9 (∃𝑞𝑣 ∈ (𝑉 ∖ {(0g𝑊)})(((𝑈𝑆𝑈𝑉) ∧ (𝑈 ((LSpan‘𝑊)‘{𝑣})) = 𝑉) ∧ 𝑞 = ((LSpan‘𝑊)‘{𝑣})) ↔ ∃𝑣 ∈ (𝑉 ∖ {(0g𝑊)})((𝑈𝑆𝑈𝑉) ∧ (𝑈 ((LSpan‘𝑊)‘{𝑣})) = 𝑉))
46 df-rex 3072 . . . . . . . . 9 (∃𝑣 ∈ (𝑉 ∖ {(0g𝑊)})((𝑈𝑆𝑈𝑉) ∧ (𝑈 ((LSpan‘𝑊)‘{𝑣})) = 𝑉) ↔ ∃𝑣(𝑣 ∈ (𝑉 ∖ {(0g𝑊)}) ∧ ((𝑈𝑆𝑈𝑉) ∧ (𝑈 ((LSpan‘𝑊)‘{𝑣})) = 𝑉)))
4745, 46bitr2i 275 . . . . . . . 8 (∃𝑣(𝑣 ∈ (𝑉 ∖ {(0g𝑊)}) ∧ ((𝑈𝑆𝑈𝑉) ∧ (𝑈 ((LSpan‘𝑊)‘{𝑣})) = 𝑉)) ↔ ∃𝑞𝑣 ∈ (𝑉 ∖ {(0g𝑊)})(((𝑈𝑆𝑈𝑉) ∧ (𝑈 ((LSpan‘𝑊)‘{𝑣})) = 𝑉) ∧ 𝑞 = ((LSpan‘𝑊)‘{𝑣})))
48 ancom 461 . . . . . . . . . 10 ((((𝑈𝑆𝑈𝑉) ∧ (𝑈 ((LSpan‘𝑊)‘{𝑣})) = 𝑉) ∧ 𝑞 = ((LSpan‘𝑊)‘{𝑣})) ↔ (𝑞 = ((LSpan‘𝑊)‘{𝑣}) ∧ ((𝑈𝑆𝑈𝑉) ∧ (𝑈 ((LSpan‘𝑊)‘{𝑣})) = 𝑉)))
4948rexbii 3094 . . . . . . . . 9 (∃𝑣 ∈ (𝑉 ∖ {(0g𝑊)})(((𝑈𝑆𝑈𝑉) ∧ (𝑈 ((LSpan‘𝑊)‘{𝑣})) = 𝑉) ∧ 𝑞 = ((LSpan‘𝑊)‘{𝑣})) ↔ ∃𝑣 ∈ (𝑉 ∖ {(0g𝑊)})(𝑞 = ((LSpan‘𝑊)‘{𝑣}) ∧ ((𝑈𝑆𝑈𝑉) ∧ (𝑈 ((LSpan‘𝑊)‘{𝑣})) = 𝑉)))
5049exbii 1849 . . . . . . . 8 (∃𝑞𝑣 ∈ (𝑉 ∖ {(0g𝑊)})(((𝑈𝑆𝑈𝑉) ∧ (𝑈 ((LSpan‘𝑊)‘{𝑣})) = 𝑉) ∧ 𝑞 = ((LSpan‘𝑊)‘{𝑣})) ↔ ∃𝑞𝑣 ∈ (𝑉 ∖ {(0g𝑊)})(𝑞 = ((LSpan‘𝑊)‘{𝑣}) ∧ ((𝑈𝑆𝑈𝑉) ∧ (𝑈 ((LSpan‘𝑊)‘{𝑣})) = 𝑉)))
5147, 50bitri 274 . . . . . . 7 (∃𝑣(𝑣 ∈ (𝑉 ∖ {(0g𝑊)}) ∧ ((𝑈𝑆𝑈𝑉) ∧ (𝑈 ((LSpan‘𝑊)‘{𝑣})) = 𝑉)) ↔ ∃𝑞𝑣 ∈ (𝑉 ∖ {(0g𝑊)})(𝑞 = ((LSpan‘𝑊)‘{𝑣}) ∧ ((𝑈𝑆𝑈𝑉) ∧ (𝑈 ((LSpan‘𝑊)‘{𝑣})) = 𝑉)))
5243, 51bitrdi 286 . . . . . 6 (𝜑 → (∃𝑣𝑉 ((𝑈𝑆𝑈𝑉) ∧ (𝑈 ((LSpan‘𝑊)‘{𝑣})) = 𝑉) ↔ ∃𝑞𝑣 ∈ (𝑉 ∖ {(0g𝑊)})(𝑞 = ((LSpan‘𝑊)‘{𝑣}) ∧ ((𝑈𝑆𝑈𝑉) ∧ (𝑈 ((LSpan‘𝑊)‘{𝑣})) = 𝑉))))
53 r19.41v 3182 . . . . . . . 8 (∃𝑣 ∈ (𝑉 ∖ {(0g𝑊)})(𝑞 = ((LSpan‘𝑊)‘{𝑣}) ∧ ((𝑈𝑆𝑈𝑉) ∧ (𝑈 𝑞) = 𝑉)) ↔ (∃𝑣 ∈ (𝑉 ∖ {(0g𝑊)})𝑞 = ((LSpan‘𝑊)‘{𝑣}) ∧ ((𝑈𝑆𝑈𝑉) ∧ (𝑈 𝑞) = 𝑉)))
54 oveq2 7323 . . . . . . . . . . . 12 (𝑞 = ((LSpan‘𝑊)‘{𝑣}) → (𝑈 𝑞) = (𝑈 ((LSpan‘𝑊)‘{𝑣})))
5554eqeq1d 2739 . . . . . . . . . . 11 (𝑞 = ((LSpan‘𝑊)‘{𝑣}) → ((𝑈 𝑞) = 𝑉 ↔ (𝑈 ((LSpan‘𝑊)‘{𝑣})) = 𝑉))
5655anbi2d 629 . . . . . . . . . 10 (𝑞 = ((LSpan‘𝑊)‘{𝑣}) → (((𝑈𝑆𝑈𝑉) ∧ (𝑈 𝑞) = 𝑉) ↔ ((𝑈𝑆𝑈𝑉) ∧ (𝑈 ((LSpan‘𝑊)‘{𝑣})) = 𝑉)))
5756pm5.32i 575 . . . . . . . . 9 ((𝑞 = ((LSpan‘𝑊)‘{𝑣}) ∧ ((𝑈𝑆𝑈𝑉) ∧ (𝑈 𝑞) = 𝑉)) ↔ (𝑞 = ((LSpan‘𝑊)‘{𝑣}) ∧ ((𝑈𝑆𝑈𝑉) ∧ (𝑈 ((LSpan‘𝑊)‘{𝑣})) = 𝑉)))
5857rexbii 3094 . . . . . . . 8 (∃𝑣 ∈ (𝑉 ∖ {(0g𝑊)})(𝑞 = ((LSpan‘𝑊)‘{𝑣}) ∧ ((𝑈𝑆𝑈𝑉) ∧ (𝑈 𝑞) = 𝑉)) ↔ ∃𝑣 ∈ (𝑉 ∖ {(0g𝑊)})(𝑞 = ((LSpan‘𝑊)‘{𝑣}) ∧ ((𝑈𝑆𝑈𝑉) ∧ (𝑈 ((LSpan‘𝑊)‘{𝑣})) = 𝑉)))
5953, 58bitr3i 276 . . . . . . 7 ((∃𝑣 ∈ (𝑉 ∖ {(0g𝑊)})𝑞 = ((LSpan‘𝑊)‘{𝑣}) ∧ ((𝑈𝑆𝑈𝑉) ∧ (𝑈 𝑞) = 𝑉)) ↔ ∃𝑣 ∈ (𝑉 ∖ {(0g𝑊)})(𝑞 = ((LSpan‘𝑊)‘{𝑣}) ∧ ((𝑈𝑆𝑈𝑉) ∧ (𝑈 ((LSpan‘𝑊)‘{𝑣})) = 𝑉)))
6059exbii 1849 . . . . . 6 (∃𝑞(∃𝑣 ∈ (𝑉 ∖ {(0g𝑊)})𝑞 = ((LSpan‘𝑊)‘{𝑣}) ∧ ((𝑈𝑆𝑈𝑉) ∧ (𝑈 𝑞) = 𝑉)) ↔ ∃𝑞𝑣 ∈ (𝑉 ∖ {(0g𝑊)})(𝑞 = ((LSpan‘𝑊)‘{𝑣}) ∧ ((𝑈𝑆𝑈𝑉) ∧ (𝑈 ((LSpan‘𝑊)‘{𝑣})) = 𝑉)))
6152, 60bitr4di 288 . . . . 5 (𝜑 → (∃𝑣𝑉 ((𝑈𝑆𝑈𝑉) ∧ (𝑈 ((LSpan‘𝑊)‘{𝑣})) = 𝑉) ↔ ∃𝑞(∃𝑣 ∈ (𝑉 ∖ {(0g𝑊)})𝑞 = ((LSpan‘𝑊)‘{𝑣}) ∧ ((𝑈𝑆𝑈𝑉) ∧ (𝑈 𝑞) = 𝑉))))
62 islshpat.a . . . . . . . . 9 𝐴 = (LSAtoms‘𝑊)
631, 2, 16, 62islsat 37209 . . . . . . . 8 (𝑊 ∈ LMod → (𝑞𝐴 ↔ ∃𝑣 ∈ (𝑉 ∖ {(0g𝑊)})𝑞 = ((LSpan‘𝑊)‘{𝑣})))
646, 63syl 17 . . . . . . 7 (𝜑 → (𝑞𝐴 ↔ ∃𝑣 ∈ (𝑉 ∖ {(0g𝑊)})𝑞 = ((LSpan‘𝑊)‘{𝑣})))
6564anbi1d 630 . . . . . 6 (𝜑 → ((𝑞𝐴 ∧ ((𝑈𝑆𝑈𝑉) ∧ (𝑈 𝑞) = 𝑉)) ↔ (∃𝑣 ∈ (𝑉 ∖ {(0g𝑊)})𝑞 = ((LSpan‘𝑊)‘{𝑣}) ∧ ((𝑈𝑆𝑈𝑉) ∧ (𝑈 𝑞) = 𝑉))))
6665exbidv 1923 . . . . 5 (𝜑 → (∃𝑞(𝑞𝐴 ∧ ((𝑈𝑆𝑈𝑉) ∧ (𝑈 𝑞) = 𝑉)) ↔ ∃𝑞(∃𝑣 ∈ (𝑉 ∖ {(0g𝑊)})𝑞 = ((LSpan‘𝑊)‘{𝑣}) ∧ ((𝑈𝑆𝑈𝑉) ∧ (𝑈 𝑞) = 𝑉))))
6761, 66bitr4d 281 . . . 4 (𝜑 → (∃𝑣𝑉 ((𝑈𝑆𝑈𝑉) ∧ (𝑈 ((LSpan‘𝑊)‘{𝑣})) = 𝑉) ↔ ∃𝑞(𝑞𝐴 ∧ ((𝑈𝑆𝑈𝑉) ∧ (𝑈 𝑞) = 𝑉))))
6810, 67bitrid 282 . . 3 (𝜑 → ((𝑈𝑆𝑈𝑉 ∧ ∃𝑣𝑉 (𝑈 ((LSpan‘𝑊)‘{𝑣})) = 𝑉) ↔ ∃𝑞(𝑞𝐴 ∧ ((𝑈𝑆𝑈𝑉) ∧ (𝑈 𝑞) = 𝑉))))
69 df-3an 1088 . . . 4 ((𝑈𝑆𝑈𝑉 ∧ ∃𝑞𝐴 (𝑈 𝑞) = 𝑉) ↔ ((𝑈𝑆𝑈𝑉) ∧ ∃𝑞𝐴 (𝑈 𝑞) = 𝑉))
70 r19.42v 3184 . . . . 5 (∃𝑞𝐴 ((𝑈𝑆𝑈𝑉) ∧ (𝑈 𝑞) = 𝑉) ↔ ((𝑈𝑆𝑈𝑉) ∧ ∃𝑞𝐴 (𝑈 𝑞) = 𝑉))
71 df-rex 3072 . . . . 5 (∃𝑞𝐴 ((𝑈𝑆𝑈𝑉) ∧ (𝑈 𝑞) = 𝑉) ↔ ∃𝑞(𝑞𝐴 ∧ ((𝑈𝑆𝑈𝑉) ∧ (𝑈 𝑞) = 𝑉)))
7270, 71bitr3i 276 . . . 4 (((𝑈𝑆𝑈𝑉) ∧ ∃𝑞𝐴 (𝑈 𝑞) = 𝑉) ↔ ∃𝑞(𝑞𝐴 ∧ ((𝑈𝑆𝑈𝑉) ∧ (𝑈 𝑞) = 𝑉)))
7369, 72bitr2i 275 . . 3 (∃𝑞(𝑞𝐴 ∧ ((𝑈𝑆𝑈𝑉) ∧ (𝑈 𝑞) = 𝑉)) ↔ (𝑈𝑆𝑈𝑉 ∧ ∃𝑞𝐴 (𝑈 𝑞) = 𝑉))
7468, 73bitrdi 286 . 2 (𝜑 → ((𝑈𝑆𝑈𝑉 ∧ ∃𝑣𝑉 (𝑈 ((LSpan‘𝑊)‘{𝑣})) = 𝑉) ↔ (𝑈𝑆𝑈𝑉 ∧ ∃𝑞𝐴 (𝑈 𝑞) = 𝑉)))
757, 74bitrd 278 1 (𝜑 → (𝑈𝐻 ↔ (𝑈𝑆𝑈𝑉 ∧ ∃𝑞𝐴 (𝑈 𝑞) = 𝑉)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396  w3a 1086   = wceq 1540  wex 1780  wcel 2105  wne 2941  wrex 3071  cdif 3894  {csn 4571  cfv 6465  (class class class)co 7315  Basecbs 16982  0gc0g 17220  SubGrpcsubg 18818  LSSumclsm 19308  LModclmod 20195  LSubSpclss 20265  LSpanclspn 20305  LSAtomsclsa 37192  LSHypclsh 37193
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 7628  ax-cnex 11000  ax-resscn 11001  ax-1cn 11002  ax-icn 11003  ax-addcl 11004  ax-addrcl 11005  ax-mulcl 11006  ax-mulrcl 11007  ax-mulcom 11008  ax-addass 11009  ax-mulass 11010  ax-distr 11011  ax-i2m1 11012  ax-1ne0 11013  ax-1rid 11014  ax-rnegex 11015  ax-rrecex 11016  ax-cnre 11017  ax-pre-lttri 11018  ax-pre-lttrn 11019  ax-pre-ltadd 11020  ax-pre-mulgt0 11021
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-op 4578  df-uni 4851  df-int 4893  df-iun 4939  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 5562  df-we 5564  df-xp 5613  df-rel 5614  df-cnv 5615  df-co 5616  df-dm 5617  df-rn 5618  df-res 5619  df-ima 5620  df-pred 6224  df-ord 6291  df-on 6292  df-lim 6293  df-suc 6294  df-iota 6417  df-fun 6467  df-fn 6468  df-f 6469  df-f1 6470  df-fo 6471  df-f1o 6472  df-fv 6473  df-riota 7272  df-ov 7318  df-oprab 7319  df-mpo 7320  df-om 7758  df-1st 7876  df-2nd 7877  df-frecs 8144  df-wrecs 8175  df-recs 8249  df-rdg 8288  df-er 8546  df-en 8782  df-dom 8783  df-sdom 8784  df-pnf 11084  df-mnf 11085  df-xr 11086  df-ltxr 11087  df-le 11088  df-sub 11280  df-neg 11281  df-nn 12047  df-2 12109  df-sets 16935  df-slot 16953  df-ndx 16965  df-base 16983  df-ress 17012  df-plusg 17045  df-0g 17222  df-mgm 18396  df-sgrp 18445  df-mnd 18456  df-submnd 18501  df-grp 18649  df-minusg 18650  df-sbg 18651  df-subg 18821  df-cntz 18992  df-lsm 19310  df-cmn 19456  df-abl 19457  df-mgp 19789  df-ur 19806  df-ring 19853  df-lmod 20197  df-lss 20266  df-lsp 20306  df-lsatoms 37194  df-lshyp 37195
This theorem is referenced by:  islshpcv  37271
  Copyright terms: Public domain W3C validator