MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  iunocv Structured version   Visualization version   GIF version

Theorem iunocv 20817
Description: The orthocomplement of an indexed union. (Contributed by Mario Carneiro, 23-Oct-2015.)
Hypotheses
Ref Expression
inocv.o = (ocv‘𝑊)
iunocv.v 𝑉 = (Base‘𝑊)
Assertion
Ref Expression
iunocv ( 𝑥𝐴 𝐵) = (𝑉 𝑥𝐴 ( 𝐵))
Distinct variable groups:   𝑥,𝑉   𝑥,𝑊
Allowed substitution hints:   𝐴(𝑥)   𝐵(𝑥)   (𝑥)

Proof of Theorem iunocv
Dummy variables 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 iunss 4960 . . . . . . 7 ( 𝑥𝐴 𝐵𝑉 ↔ ∀𝑥𝐴 𝐵𝑉)
2 eliun 4914 . . . . . . . . . . 11 (𝑦 𝑥𝐴 𝐵 ↔ ∃𝑥𝐴 𝑦𝐵)
32imbi1i 352 . . . . . . . . . 10 ((𝑦 𝑥𝐴 𝐵 → (𝑧(·𝑖𝑊)𝑦) = (0g‘(Scalar‘𝑊))) ↔ (∃𝑥𝐴 𝑦𝐵 → (𝑧(·𝑖𝑊)𝑦) = (0g‘(Scalar‘𝑊))))
4 r19.23v 3277 . . . . . . . . . 10 (∀𝑥𝐴 (𝑦𝐵 → (𝑧(·𝑖𝑊)𝑦) = (0g‘(Scalar‘𝑊))) ↔ (∃𝑥𝐴 𝑦𝐵 → (𝑧(·𝑖𝑊)𝑦) = (0g‘(Scalar‘𝑊))))
53, 4bitr4i 280 . . . . . . . . 9 ((𝑦 𝑥𝐴 𝐵 → (𝑧(·𝑖𝑊)𝑦) = (0g‘(Scalar‘𝑊))) ↔ ∀𝑥𝐴 (𝑦𝐵 → (𝑧(·𝑖𝑊)𝑦) = (0g‘(Scalar‘𝑊))))
65albii 1813 . . . . . . . 8 (∀𝑦(𝑦 𝑥𝐴 𝐵 → (𝑧(·𝑖𝑊)𝑦) = (0g‘(Scalar‘𝑊))) ↔ ∀𝑦𝑥𝐴 (𝑦𝐵 → (𝑧(·𝑖𝑊)𝑦) = (0g‘(Scalar‘𝑊))))
7 df-ral 3141 . . . . . . . 8 (∀𝑦 𝑥𝐴 𝐵(𝑧(·𝑖𝑊)𝑦) = (0g‘(Scalar‘𝑊)) ↔ ∀𝑦(𝑦 𝑥𝐴 𝐵 → (𝑧(·𝑖𝑊)𝑦) = (0g‘(Scalar‘𝑊))))
8 df-ral 3141 . . . . . . . . . 10 (∀𝑦𝐵 (𝑧(·𝑖𝑊)𝑦) = (0g‘(Scalar‘𝑊)) ↔ ∀𝑦(𝑦𝐵 → (𝑧(·𝑖𝑊)𝑦) = (0g‘(Scalar‘𝑊))))
98ralbii 3163 . . . . . . . . 9 (∀𝑥𝐴𝑦𝐵 (𝑧(·𝑖𝑊)𝑦) = (0g‘(Scalar‘𝑊)) ↔ ∀𝑥𝐴𝑦(𝑦𝐵 → (𝑧(·𝑖𝑊)𝑦) = (0g‘(Scalar‘𝑊))))
10 ralcom4 3233 . . . . . . . . 9 (∀𝑥𝐴𝑦(𝑦𝐵 → (𝑧(·𝑖𝑊)𝑦) = (0g‘(Scalar‘𝑊))) ↔ ∀𝑦𝑥𝐴 (𝑦𝐵 → (𝑧(·𝑖𝑊)𝑦) = (0g‘(Scalar‘𝑊))))
119, 10bitri 277 . . . . . . . 8 (∀𝑥𝐴𝑦𝐵 (𝑧(·𝑖𝑊)𝑦) = (0g‘(Scalar‘𝑊)) ↔ ∀𝑦𝑥𝐴 (𝑦𝐵 → (𝑧(·𝑖𝑊)𝑦) = (0g‘(Scalar‘𝑊))))
126, 7, 113bitr4i 305 . . . . . . 7 (∀𝑦 𝑥𝐴 𝐵(𝑧(·𝑖𝑊)𝑦) = (0g‘(Scalar‘𝑊)) ↔ ∀𝑥𝐴𝑦𝐵 (𝑧(·𝑖𝑊)𝑦) = (0g‘(Scalar‘𝑊)))
131, 12anbi12i 628 . . . . . 6 (( 𝑥𝐴 𝐵𝑉 ∧ ∀𝑦 𝑥𝐴 𝐵(𝑧(·𝑖𝑊)𝑦) = (0g‘(Scalar‘𝑊))) ↔ (∀𝑥𝐴 𝐵𝑉 ∧ ∀𝑥𝐴𝑦𝐵 (𝑧(·𝑖𝑊)𝑦) = (0g‘(Scalar‘𝑊))))
14 r19.26 3168 . . . . . 6 (∀𝑥𝐴 (𝐵𝑉 ∧ ∀𝑦𝐵 (𝑧(·𝑖𝑊)𝑦) = (0g‘(Scalar‘𝑊))) ↔ (∀𝑥𝐴 𝐵𝑉 ∧ ∀𝑥𝐴𝑦𝐵 (𝑧(·𝑖𝑊)𝑦) = (0g‘(Scalar‘𝑊))))
1513, 14bitr4i 280 . . . . 5 (( 𝑥𝐴 𝐵𝑉 ∧ ∀𝑦 𝑥𝐴 𝐵(𝑧(·𝑖𝑊)𝑦) = (0g‘(Scalar‘𝑊))) ↔ ∀𝑥𝐴 (𝐵𝑉 ∧ ∀𝑦𝐵 (𝑧(·𝑖𝑊)𝑦) = (0g‘(Scalar‘𝑊))))
16 eliin 4915 . . . . . 6 (𝑧𝑉 → (𝑧 𝑥𝐴 ( 𝐵) ↔ ∀𝑥𝐴 𝑧 ∈ ( 𝐵)))
17 iunocv.v . . . . . . . . . 10 𝑉 = (Base‘𝑊)
18 eqid 2819 . . . . . . . . . 10 (·𝑖𝑊) = (·𝑖𝑊)
19 eqid 2819 . . . . . . . . . 10 (Scalar‘𝑊) = (Scalar‘𝑊)
20 eqid 2819 . . . . . . . . . 10 (0g‘(Scalar‘𝑊)) = (0g‘(Scalar‘𝑊))
21 inocv.o . . . . . . . . . 10 = (ocv‘𝑊)
2217, 18, 19, 20, 21elocv 20804 . . . . . . . . 9 (𝑧 ∈ ( 𝐵) ↔ (𝐵𝑉𝑧𝑉 ∧ ∀𝑦𝐵 (𝑧(·𝑖𝑊)𝑦) = (0g‘(Scalar‘𝑊))))
23 3anan12 1090 . . . . . . . . 9 ((𝐵𝑉𝑧𝑉 ∧ ∀𝑦𝐵 (𝑧(·𝑖𝑊)𝑦) = (0g‘(Scalar‘𝑊))) ↔ (𝑧𝑉 ∧ (𝐵𝑉 ∧ ∀𝑦𝐵 (𝑧(·𝑖𝑊)𝑦) = (0g‘(Scalar‘𝑊)))))
2422, 23bitri 277 . . . . . . . 8 (𝑧 ∈ ( 𝐵) ↔ (𝑧𝑉 ∧ (𝐵𝑉 ∧ ∀𝑦𝐵 (𝑧(·𝑖𝑊)𝑦) = (0g‘(Scalar‘𝑊)))))
2524baib 538 . . . . . . 7 (𝑧𝑉 → (𝑧 ∈ ( 𝐵) ↔ (𝐵𝑉 ∧ ∀𝑦𝐵 (𝑧(·𝑖𝑊)𝑦) = (0g‘(Scalar‘𝑊)))))
2625ralbidv 3195 . . . . . 6 (𝑧𝑉 → (∀𝑥𝐴 𝑧 ∈ ( 𝐵) ↔ ∀𝑥𝐴 (𝐵𝑉 ∧ ∀𝑦𝐵 (𝑧(·𝑖𝑊)𝑦) = (0g‘(Scalar‘𝑊)))))
2716, 26bitr2d 282 . . . . 5 (𝑧𝑉 → (∀𝑥𝐴 (𝐵𝑉 ∧ ∀𝑦𝐵 (𝑧(·𝑖𝑊)𝑦) = (0g‘(Scalar‘𝑊))) ↔ 𝑧 𝑥𝐴 ( 𝐵)))
2815, 27syl5bb 285 . . . 4 (𝑧𝑉 → (( 𝑥𝐴 𝐵𝑉 ∧ ∀𝑦 𝑥𝐴 𝐵(𝑧(·𝑖𝑊)𝑦) = (0g‘(Scalar‘𝑊))) ↔ 𝑧 𝑥𝐴 ( 𝐵)))
2928pm5.32i 577 . . 3 ((𝑧𝑉 ∧ ( 𝑥𝐴 𝐵𝑉 ∧ ∀𝑦 𝑥𝐴 𝐵(𝑧(·𝑖𝑊)𝑦) = (0g‘(Scalar‘𝑊)))) ↔ (𝑧𝑉𝑧 𝑥𝐴 ( 𝐵)))
3017, 18, 19, 20, 21elocv 20804 . . . 4 (𝑧 ∈ ( 𝑥𝐴 𝐵) ↔ ( 𝑥𝐴 𝐵𝑉𝑧𝑉 ∧ ∀𝑦 𝑥𝐴 𝐵(𝑧(·𝑖𝑊)𝑦) = (0g‘(Scalar‘𝑊))))
31 3anan12 1090 . . . 4 (( 𝑥𝐴 𝐵𝑉𝑧𝑉 ∧ ∀𝑦 𝑥𝐴 𝐵(𝑧(·𝑖𝑊)𝑦) = (0g‘(Scalar‘𝑊))) ↔ (𝑧𝑉 ∧ ( 𝑥𝐴 𝐵𝑉 ∧ ∀𝑦 𝑥𝐴 𝐵(𝑧(·𝑖𝑊)𝑦) = (0g‘(Scalar‘𝑊)))))
3230, 31bitri 277 . . 3 (𝑧 ∈ ( 𝑥𝐴 𝐵) ↔ (𝑧𝑉 ∧ ( 𝑥𝐴 𝐵𝑉 ∧ ∀𝑦 𝑥𝐴 𝐵(𝑧(·𝑖𝑊)𝑦) = (0g‘(Scalar‘𝑊)))))
33 elin 4167 . . 3 (𝑧 ∈ (𝑉 𝑥𝐴 ( 𝐵)) ↔ (𝑧𝑉𝑧 𝑥𝐴 ( 𝐵)))
3429, 32, 333bitr4i 305 . 2 (𝑧 ∈ ( 𝑥𝐴 𝐵) ↔ 𝑧 ∈ (𝑉 𝑥𝐴 ( 𝐵)))
3534eqriv 2816 1 ( 𝑥𝐴 𝐵) = (𝑉 𝑥𝐴 ( 𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 398  w3a 1081  wal 1528   = wceq 1530  wcel 2107  wral 3136  wrex 3137  cin 3933  wss 3934   ciun 4910   ciin 4911  cfv 6348  (class class class)co 7148  Basecbs 16475  Scalarcsca 16560  ·𝑖cip 16562  0gc0g 16705  ocvcocv 20796
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2791  ax-sep 5194  ax-nul 5201  ax-pow 5257  ax-pr 5320  ax-un 7453
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-mo 2616  df-eu 2648  df-clab 2798  df-cleq 2812  df-clel 2891  df-nfc 2961  df-ne 3015  df-ral 3141  df-rex 3142  df-rab 3145  df-v 3495  df-sbc 3771  df-dif 3937  df-un 3939  df-in 3941  df-ss 3950  df-nul 4290  df-if 4466  df-pw 4539  df-sn 4560  df-pr 4562  df-op 4566  df-uni 4831  df-iun 4912  df-iin 4913  df-br 5058  df-opab 5120  df-mpt 5138  df-id 5453  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-rn 5559  df-res 5560  df-ima 5561  df-iota 6307  df-fun 6350  df-fn 6351  df-f 6352  df-fv 6356  df-ov 7151  df-ocv 20799
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator