Users' Mathboxes Mathbox for Zhi Wang < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  isthincd2lem2 Structured version   Visualization version   GIF version

Theorem isthincd2lem2 47209
Description: Lemma for isthincd2 47211. (Contributed by Zhi Wang, 17-Sep-2024.)
Hypotheses
Ref Expression
isthincd2lem2.1 (๐œ‘ โ†’ ๐‘‹ โˆˆ ๐ต)
isthincd2lem2.2 (๐œ‘ โ†’ ๐‘Œ โˆˆ ๐ต)
isthincd2lem2.3 (๐œ‘ โ†’ ๐‘ โˆˆ ๐ต)
isthincd2lem2.4 (๐œ‘ โ†’ ๐น โˆˆ (๐‘‹๐ป๐‘Œ))
isthincd2lem2.5 (๐œ‘ โ†’ ๐บ โˆˆ (๐‘Œ๐ป๐‘))
isthincd2lem2.6 (๐œ‘ โ†’ โˆ€๐‘ฅ โˆˆ ๐ต โˆ€๐‘ฆ โˆˆ ๐ต โˆ€๐‘ง โˆˆ ๐ต โˆ€๐‘“ โˆˆ (๐‘ฅ๐ป๐‘ฆ)โˆ€๐‘” โˆˆ (๐‘ฆ๐ป๐‘ง)(๐‘”(โŸจ๐‘ฅ, ๐‘ฆโŸฉ ยท ๐‘ง)๐‘“) โˆˆ (๐‘ฅ๐ป๐‘ง))
Assertion
Ref Expression
isthincd2lem2 (๐œ‘ โ†’ (๐บ(โŸจ๐‘‹, ๐‘ŒโŸฉ ยท ๐‘)๐น) โˆˆ (๐‘‹๐ป๐‘))
Distinct variable groups:   ยท ,๐‘“,๐‘”,๐‘ง,๐‘ฅ,๐‘ฆ   ๐‘ง,๐ต,๐‘ฅ,๐‘ฆ   ๐‘“,๐ป,๐‘”,๐‘ง,๐‘ฅ,๐‘ฆ
Allowed substitution hints:   ๐œ‘(๐‘ฅ,๐‘ฆ,๐‘ง,๐‘“,๐‘”)   ๐ต(๐‘“,๐‘”)   ๐น(๐‘ฅ,๐‘ฆ,๐‘ง,๐‘“,๐‘”)   ๐บ(๐‘ฅ,๐‘ฆ,๐‘ง,๐‘“,๐‘”)   ๐‘‹(๐‘ฅ,๐‘ฆ,๐‘ง,๐‘“,๐‘”)   ๐‘Œ(๐‘ฅ,๐‘ฆ,๐‘ง,๐‘“,๐‘”)   ๐‘(๐‘ฅ,๐‘ฆ,๐‘ง,๐‘“,๐‘”)

Proof of Theorem isthincd2lem2
Dummy variables ๐‘˜ ๐‘ข ๐‘ฃ ๐‘ค ๐‘™ are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 isthincd2lem2.6 . . . 4 (๐œ‘ โ†’ โˆ€๐‘ฅ โˆˆ ๐ต โˆ€๐‘ฆ โˆˆ ๐ต โˆ€๐‘ง โˆˆ ๐ต โˆ€๐‘“ โˆˆ (๐‘ฅ๐ป๐‘ฆ)โˆ€๐‘” โˆˆ (๐‘ฆ๐ป๐‘ง)(๐‘”(โŸจ๐‘ฅ, ๐‘ฆโŸฉ ยท ๐‘ง)๐‘“) โˆˆ (๐‘ฅ๐ป๐‘ง))
2 oveq1 7384 . . . . . 6 (๐‘ฅ = ๐‘ค โ†’ (๐‘ฅ๐ป๐‘ฆ) = (๐‘ค๐ป๐‘ฆ))
3 opeq1 4850 . . . . . . . . . 10 (๐‘ฅ = ๐‘ค โ†’ โŸจ๐‘ฅ, ๐‘ฆโŸฉ = โŸจ๐‘ค, ๐‘ฆโŸฉ)
43oveq1d 7392 . . . . . . . . 9 (๐‘ฅ = ๐‘ค โ†’ (โŸจ๐‘ฅ, ๐‘ฆโŸฉ ยท ๐‘ง) = (โŸจ๐‘ค, ๐‘ฆโŸฉ ยท ๐‘ง))
54oveqd 7394 . . . . . . . 8 (๐‘ฅ = ๐‘ค โ†’ (๐‘”(โŸจ๐‘ฅ, ๐‘ฆโŸฉ ยท ๐‘ง)๐‘“) = (๐‘”(โŸจ๐‘ค, ๐‘ฆโŸฉ ยท ๐‘ง)๐‘“))
6 oveq1 7384 . . . . . . . 8 (๐‘ฅ = ๐‘ค โ†’ (๐‘ฅ๐ป๐‘ง) = (๐‘ค๐ป๐‘ง))
75, 6eleq12d 2826 . . . . . . 7 (๐‘ฅ = ๐‘ค โ†’ ((๐‘”(โŸจ๐‘ฅ, ๐‘ฆโŸฉ ยท ๐‘ง)๐‘“) โˆˆ (๐‘ฅ๐ป๐‘ง) โ†” (๐‘”(โŸจ๐‘ค, ๐‘ฆโŸฉ ยท ๐‘ง)๐‘“) โˆˆ (๐‘ค๐ป๐‘ง)))
87ralbidv 3176 . . . . . 6 (๐‘ฅ = ๐‘ค โ†’ (โˆ€๐‘” โˆˆ (๐‘ฆ๐ป๐‘ง)(๐‘”(โŸจ๐‘ฅ, ๐‘ฆโŸฉ ยท ๐‘ง)๐‘“) โˆˆ (๐‘ฅ๐ป๐‘ง) โ†” โˆ€๐‘” โˆˆ (๐‘ฆ๐ป๐‘ง)(๐‘”(โŸจ๐‘ค, ๐‘ฆโŸฉ ยท ๐‘ง)๐‘“) โˆˆ (๐‘ค๐ป๐‘ง)))
92, 8raleqbidv 3330 . . . . 5 (๐‘ฅ = ๐‘ค โ†’ (โˆ€๐‘“ โˆˆ (๐‘ฅ๐ป๐‘ฆ)โˆ€๐‘” โˆˆ (๐‘ฆ๐ป๐‘ง)(๐‘”(โŸจ๐‘ฅ, ๐‘ฆโŸฉ ยท ๐‘ง)๐‘“) โˆˆ (๐‘ฅ๐ป๐‘ง) โ†” โˆ€๐‘“ โˆˆ (๐‘ค๐ป๐‘ฆ)โˆ€๐‘” โˆˆ (๐‘ฆ๐ป๐‘ง)(๐‘”(โŸจ๐‘ค, ๐‘ฆโŸฉ ยท ๐‘ง)๐‘“) โˆˆ (๐‘ค๐ป๐‘ง)))
10 oveq2 7385 . . . . . 6 (๐‘ฆ = ๐‘ฃ โ†’ (๐‘ค๐ป๐‘ฆ) = (๐‘ค๐ป๐‘ฃ))
11 oveq1 7384 . . . . . . 7 (๐‘ฆ = ๐‘ฃ โ†’ (๐‘ฆ๐ป๐‘ง) = (๐‘ฃ๐ป๐‘ง))
12 opeq2 4851 . . . . . . . . . 10 (๐‘ฆ = ๐‘ฃ โ†’ โŸจ๐‘ค, ๐‘ฆโŸฉ = โŸจ๐‘ค, ๐‘ฃโŸฉ)
1312oveq1d 7392 . . . . . . . . 9 (๐‘ฆ = ๐‘ฃ โ†’ (โŸจ๐‘ค, ๐‘ฆโŸฉ ยท ๐‘ง) = (โŸจ๐‘ค, ๐‘ฃโŸฉ ยท ๐‘ง))
1413oveqd 7394 . . . . . . . 8 (๐‘ฆ = ๐‘ฃ โ†’ (๐‘”(โŸจ๐‘ค, ๐‘ฆโŸฉ ยท ๐‘ง)๐‘“) = (๐‘”(โŸจ๐‘ค, ๐‘ฃโŸฉ ยท ๐‘ง)๐‘“))
1514eleq1d 2817 . . . . . . 7 (๐‘ฆ = ๐‘ฃ โ†’ ((๐‘”(โŸจ๐‘ค, ๐‘ฆโŸฉ ยท ๐‘ง)๐‘“) โˆˆ (๐‘ค๐ป๐‘ง) โ†” (๐‘”(โŸจ๐‘ค, ๐‘ฃโŸฉ ยท ๐‘ง)๐‘“) โˆˆ (๐‘ค๐ป๐‘ง)))
1611, 15raleqbidv 3330 . . . . . 6 (๐‘ฆ = ๐‘ฃ โ†’ (โˆ€๐‘” โˆˆ (๐‘ฆ๐ป๐‘ง)(๐‘”(โŸจ๐‘ค, ๐‘ฆโŸฉ ยท ๐‘ง)๐‘“) โˆˆ (๐‘ค๐ป๐‘ง) โ†” โˆ€๐‘” โˆˆ (๐‘ฃ๐ป๐‘ง)(๐‘”(โŸจ๐‘ค, ๐‘ฃโŸฉ ยท ๐‘ง)๐‘“) โˆˆ (๐‘ค๐ป๐‘ง)))
1710, 16raleqbidv 3330 . . . . 5 (๐‘ฆ = ๐‘ฃ โ†’ (โˆ€๐‘“ โˆˆ (๐‘ค๐ป๐‘ฆ)โˆ€๐‘” โˆˆ (๐‘ฆ๐ป๐‘ง)(๐‘”(โŸจ๐‘ค, ๐‘ฆโŸฉ ยท ๐‘ง)๐‘“) โˆˆ (๐‘ค๐ป๐‘ง) โ†” โˆ€๐‘“ โˆˆ (๐‘ค๐ป๐‘ฃ)โˆ€๐‘” โˆˆ (๐‘ฃ๐ป๐‘ง)(๐‘”(โŸจ๐‘ค, ๐‘ฃโŸฉ ยท ๐‘ง)๐‘“) โˆˆ (๐‘ค๐ป๐‘ง)))
18 oveq2 7385 . . . . . . . 8 (๐‘ง = ๐‘ข โ†’ (๐‘ฃ๐ป๐‘ง) = (๐‘ฃ๐ป๐‘ข))
19 oveq2 7385 . . . . . . . . . 10 (๐‘ง = ๐‘ข โ†’ (โŸจ๐‘ค, ๐‘ฃโŸฉ ยท ๐‘ง) = (โŸจ๐‘ค, ๐‘ฃโŸฉ ยท ๐‘ข))
2019oveqd 7394 . . . . . . . . 9 (๐‘ง = ๐‘ข โ†’ (๐‘”(โŸจ๐‘ค, ๐‘ฃโŸฉ ยท ๐‘ง)๐‘“) = (๐‘”(โŸจ๐‘ค, ๐‘ฃโŸฉ ยท ๐‘ข)๐‘“))
21 oveq2 7385 . . . . . . . . 9 (๐‘ง = ๐‘ข โ†’ (๐‘ค๐ป๐‘ง) = (๐‘ค๐ป๐‘ข))
2220, 21eleq12d 2826 . . . . . . . 8 (๐‘ง = ๐‘ข โ†’ ((๐‘”(โŸจ๐‘ค, ๐‘ฃโŸฉ ยท ๐‘ง)๐‘“) โˆˆ (๐‘ค๐ป๐‘ง) โ†” (๐‘”(โŸจ๐‘ค, ๐‘ฃโŸฉ ยท ๐‘ข)๐‘“) โˆˆ (๐‘ค๐ป๐‘ข)))
2318, 22raleqbidv 3330 . . . . . . 7 (๐‘ง = ๐‘ข โ†’ (โˆ€๐‘” โˆˆ (๐‘ฃ๐ป๐‘ง)(๐‘”(โŸจ๐‘ค, ๐‘ฃโŸฉ ยท ๐‘ง)๐‘“) โˆˆ (๐‘ค๐ป๐‘ง) โ†” โˆ€๐‘” โˆˆ (๐‘ฃ๐ป๐‘ข)(๐‘”(โŸจ๐‘ค, ๐‘ฃโŸฉ ยท ๐‘ข)๐‘“) โˆˆ (๐‘ค๐ป๐‘ข)))
2423ralbidv 3176 . . . . . 6 (๐‘ง = ๐‘ข โ†’ (โˆ€๐‘“ โˆˆ (๐‘ค๐ป๐‘ฃ)โˆ€๐‘” โˆˆ (๐‘ฃ๐ป๐‘ง)(๐‘”(โŸจ๐‘ค, ๐‘ฃโŸฉ ยท ๐‘ง)๐‘“) โˆˆ (๐‘ค๐ป๐‘ง) โ†” โˆ€๐‘“ โˆˆ (๐‘ค๐ป๐‘ฃ)โˆ€๐‘” โˆˆ (๐‘ฃ๐ป๐‘ข)(๐‘”(โŸจ๐‘ค, ๐‘ฃโŸฉ ยท ๐‘ข)๐‘“) โˆˆ (๐‘ค๐ป๐‘ข)))
25 oveq2 7385 . . . . . . . 8 (๐‘“ = ๐‘˜ โ†’ (๐‘”(โŸจ๐‘ค, ๐‘ฃโŸฉ ยท ๐‘ข)๐‘“) = (๐‘”(โŸจ๐‘ค, ๐‘ฃโŸฉ ยท ๐‘ข)๐‘˜))
2625eleq1d 2817 . . . . . . 7 (๐‘“ = ๐‘˜ โ†’ ((๐‘”(โŸจ๐‘ค, ๐‘ฃโŸฉ ยท ๐‘ข)๐‘“) โˆˆ (๐‘ค๐ป๐‘ข) โ†” (๐‘”(โŸจ๐‘ค, ๐‘ฃโŸฉ ยท ๐‘ข)๐‘˜) โˆˆ (๐‘ค๐ป๐‘ข)))
27 oveq1 7384 . . . . . . . 8 (๐‘” = ๐‘™ โ†’ (๐‘”(โŸจ๐‘ค, ๐‘ฃโŸฉ ยท ๐‘ข)๐‘˜) = (๐‘™(โŸจ๐‘ค, ๐‘ฃโŸฉ ยท ๐‘ข)๐‘˜))
2827eleq1d 2817 . . . . . . 7 (๐‘” = ๐‘™ โ†’ ((๐‘”(โŸจ๐‘ค, ๐‘ฃโŸฉ ยท ๐‘ข)๐‘˜) โˆˆ (๐‘ค๐ป๐‘ข) โ†” (๐‘™(โŸจ๐‘ค, ๐‘ฃโŸฉ ยท ๐‘ข)๐‘˜) โˆˆ (๐‘ค๐ป๐‘ข)))
2926, 28cbvral2vw 3235 . . . . . 6 (โˆ€๐‘“ โˆˆ (๐‘ค๐ป๐‘ฃ)โˆ€๐‘” โˆˆ (๐‘ฃ๐ป๐‘ข)(๐‘”(โŸจ๐‘ค, ๐‘ฃโŸฉ ยท ๐‘ข)๐‘“) โˆˆ (๐‘ค๐ป๐‘ข) โ†” โˆ€๐‘˜ โˆˆ (๐‘ค๐ป๐‘ฃ)โˆ€๐‘™ โˆˆ (๐‘ฃ๐ป๐‘ข)(๐‘™(โŸจ๐‘ค, ๐‘ฃโŸฉ ยท ๐‘ข)๐‘˜) โˆˆ (๐‘ค๐ป๐‘ข))
3024, 29bitrdi 286 . . . . 5 (๐‘ง = ๐‘ข โ†’ (โˆ€๐‘“ โˆˆ (๐‘ค๐ป๐‘ฃ)โˆ€๐‘” โˆˆ (๐‘ฃ๐ป๐‘ง)(๐‘”(โŸจ๐‘ค, ๐‘ฃโŸฉ ยท ๐‘ง)๐‘“) โˆˆ (๐‘ค๐ป๐‘ง) โ†” โˆ€๐‘˜ โˆˆ (๐‘ค๐ป๐‘ฃ)โˆ€๐‘™ โˆˆ (๐‘ฃ๐ป๐‘ข)(๐‘™(โŸจ๐‘ค, ๐‘ฃโŸฉ ยท ๐‘ข)๐‘˜) โˆˆ (๐‘ค๐ป๐‘ข)))
319, 17, 30cbvral3vw 3237 . . . 4 (โˆ€๐‘ฅ โˆˆ ๐ต โˆ€๐‘ฆ โˆˆ ๐ต โˆ€๐‘ง โˆˆ ๐ต โˆ€๐‘“ โˆˆ (๐‘ฅ๐ป๐‘ฆ)โˆ€๐‘” โˆˆ (๐‘ฆ๐ป๐‘ง)(๐‘”(โŸจ๐‘ฅ, ๐‘ฆโŸฉ ยท ๐‘ง)๐‘“) โˆˆ (๐‘ฅ๐ป๐‘ง) โ†” โˆ€๐‘ค โˆˆ ๐ต โˆ€๐‘ฃ โˆˆ ๐ต โˆ€๐‘ข โˆˆ ๐ต โˆ€๐‘˜ โˆˆ (๐‘ค๐ป๐‘ฃ)โˆ€๐‘™ โˆˆ (๐‘ฃ๐ป๐‘ข)(๐‘™(โŸจ๐‘ค, ๐‘ฃโŸฉ ยท ๐‘ข)๐‘˜) โˆˆ (๐‘ค๐ป๐‘ข))
321, 31sylib 217 . . 3 (๐œ‘ โ†’ โˆ€๐‘ค โˆˆ ๐ต โˆ€๐‘ฃ โˆˆ ๐ต โˆ€๐‘ข โˆˆ ๐ต โˆ€๐‘˜ โˆˆ (๐‘ค๐ป๐‘ฃ)โˆ€๐‘™ โˆˆ (๐‘ฃ๐ป๐‘ข)(๐‘™(โŸจ๐‘ค, ๐‘ฃโŸฉ ยท ๐‘ข)๐‘˜) โˆˆ (๐‘ค๐ป๐‘ข))
33 isthincd2lem2.1 . . . 4 (๐œ‘ โ†’ ๐‘‹ โˆˆ ๐ต)
34 isthincd2lem2.2 . . . 4 (๐œ‘ โ†’ ๐‘Œ โˆˆ ๐ต)
35 isthincd2lem2.3 . . . 4 (๐œ‘ โ†’ ๐‘ โˆˆ ๐ต)
36 oveq1 7384 . . . . . 6 (๐‘ค = ๐‘‹ โ†’ (๐‘ค๐ป๐‘ฃ) = (๐‘‹๐ป๐‘ฃ))
37 opeq1 4850 . . . . . . . . . 10 (๐‘ค = ๐‘‹ โ†’ โŸจ๐‘ค, ๐‘ฃโŸฉ = โŸจ๐‘‹, ๐‘ฃโŸฉ)
3837oveq1d 7392 . . . . . . . . 9 (๐‘ค = ๐‘‹ โ†’ (โŸจ๐‘ค, ๐‘ฃโŸฉ ยท ๐‘ข) = (โŸจ๐‘‹, ๐‘ฃโŸฉ ยท ๐‘ข))
3938oveqd 7394 . . . . . . . 8 (๐‘ค = ๐‘‹ โ†’ (๐‘™(โŸจ๐‘ค, ๐‘ฃโŸฉ ยท ๐‘ข)๐‘˜) = (๐‘™(โŸจ๐‘‹, ๐‘ฃโŸฉ ยท ๐‘ข)๐‘˜))
40 oveq1 7384 . . . . . . . 8 (๐‘ค = ๐‘‹ โ†’ (๐‘ค๐ป๐‘ข) = (๐‘‹๐ป๐‘ข))
4139, 40eleq12d 2826 . . . . . . 7 (๐‘ค = ๐‘‹ โ†’ ((๐‘™(โŸจ๐‘ค, ๐‘ฃโŸฉ ยท ๐‘ข)๐‘˜) โˆˆ (๐‘ค๐ป๐‘ข) โ†” (๐‘™(โŸจ๐‘‹, ๐‘ฃโŸฉ ยท ๐‘ข)๐‘˜) โˆˆ (๐‘‹๐ป๐‘ข)))
4241ralbidv 3176 . . . . . 6 (๐‘ค = ๐‘‹ โ†’ (โˆ€๐‘™ โˆˆ (๐‘ฃ๐ป๐‘ข)(๐‘™(โŸจ๐‘ค, ๐‘ฃโŸฉ ยท ๐‘ข)๐‘˜) โˆˆ (๐‘ค๐ป๐‘ข) โ†” โˆ€๐‘™ โˆˆ (๐‘ฃ๐ป๐‘ข)(๐‘™(โŸจ๐‘‹, ๐‘ฃโŸฉ ยท ๐‘ข)๐‘˜) โˆˆ (๐‘‹๐ป๐‘ข)))
4336, 42raleqbidv 3330 . . . . 5 (๐‘ค = ๐‘‹ โ†’ (โˆ€๐‘˜ โˆˆ (๐‘ค๐ป๐‘ฃ)โˆ€๐‘™ โˆˆ (๐‘ฃ๐ป๐‘ข)(๐‘™(โŸจ๐‘ค, ๐‘ฃโŸฉ ยท ๐‘ข)๐‘˜) โˆˆ (๐‘ค๐ป๐‘ข) โ†” โˆ€๐‘˜ โˆˆ (๐‘‹๐ป๐‘ฃ)โˆ€๐‘™ โˆˆ (๐‘ฃ๐ป๐‘ข)(๐‘™(โŸจ๐‘‹, ๐‘ฃโŸฉ ยท ๐‘ข)๐‘˜) โˆˆ (๐‘‹๐ป๐‘ข)))
44 oveq2 7385 . . . . . 6 (๐‘ฃ = ๐‘Œ โ†’ (๐‘‹๐ป๐‘ฃ) = (๐‘‹๐ป๐‘Œ))
45 oveq1 7384 . . . . . . 7 (๐‘ฃ = ๐‘Œ โ†’ (๐‘ฃ๐ป๐‘ข) = (๐‘Œ๐ป๐‘ข))
46 opeq2 4851 . . . . . . . . . 10 (๐‘ฃ = ๐‘Œ โ†’ โŸจ๐‘‹, ๐‘ฃโŸฉ = โŸจ๐‘‹, ๐‘ŒโŸฉ)
4746oveq1d 7392 . . . . . . . . 9 (๐‘ฃ = ๐‘Œ โ†’ (โŸจ๐‘‹, ๐‘ฃโŸฉ ยท ๐‘ข) = (โŸจ๐‘‹, ๐‘ŒโŸฉ ยท ๐‘ข))
4847oveqd 7394 . . . . . . . 8 (๐‘ฃ = ๐‘Œ โ†’ (๐‘™(โŸจ๐‘‹, ๐‘ฃโŸฉ ยท ๐‘ข)๐‘˜) = (๐‘™(โŸจ๐‘‹, ๐‘ŒโŸฉ ยท ๐‘ข)๐‘˜))
4948eleq1d 2817 . . . . . . 7 (๐‘ฃ = ๐‘Œ โ†’ ((๐‘™(โŸจ๐‘‹, ๐‘ฃโŸฉ ยท ๐‘ข)๐‘˜) โˆˆ (๐‘‹๐ป๐‘ข) โ†” (๐‘™(โŸจ๐‘‹, ๐‘ŒโŸฉ ยท ๐‘ข)๐‘˜) โˆˆ (๐‘‹๐ป๐‘ข)))
5045, 49raleqbidv 3330 . . . . . 6 (๐‘ฃ = ๐‘Œ โ†’ (โˆ€๐‘™ โˆˆ (๐‘ฃ๐ป๐‘ข)(๐‘™(โŸจ๐‘‹, ๐‘ฃโŸฉ ยท ๐‘ข)๐‘˜) โˆˆ (๐‘‹๐ป๐‘ข) โ†” โˆ€๐‘™ โˆˆ (๐‘Œ๐ป๐‘ข)(๐‘™(โŸจ๐‘‹, ๐‘ŒโŸฉ ยท ๐‘ข)๐‘˜) โˆˆ (๐‘‹๐ป๐‘ข)))
5144, 50raleqbidv 3330 . . . . 5 (๐‘ฃ = ๐‘Œ โ†’ (โˆ€๐‘˜ โˆˆ (๐‘‹๐ป๐‘ฃ)โˆ€๐‘™ โˆˆ (๐‘ฃ๐ป๐‘ข)(๐‘™(โŸจ๐‘‹, ๐‘ฃโŸฉ ยท ๐‘ข)๐‘˜) โˆˆ (๐‘‹๐ป๐‘ข) โ†” โˆ€๐‘˜ โˆˆ (๐‘‹๐ป๐‘Œ)โˆ€๐‘™ โˆˆ (๐‘Œ๐ป๐‘ข)(๐‘™(โŸจ๐‘‹, ๐‘ŒโŸฉ ยท ๐‘ข)๐‘˜) โˆˆ (๐‘‹๐ป๐‘ข)))
52 oveq2 7385 . . . . . . 7 (๐‘ข = ๐‘ โ†’ (๐‘Œ๐ป๐‘ข) = (๐‘Œ๐ป๐‘))
53 oveq2 7385 . . . . . . . . 9 (๐‘ข = ๐‘ โ†’ (โŸจ๐‘‹, ๐‘ŒโŸฉ ยท ๐‘ข) = (โŸจ๐‘‹, ๐‘ŒโŸฉ ยท ๐‘))
5453oveqd 7394 . . . . . . . 8 (๐‘ข = ๐‘ โ†’ (๐‘™(โŸจ๐‘‹, ๐‘ŒโŸฉ ยท ๐‘ข)๐‘˜) = (๐‘™(โŸจ๐‘‹, ๐‘ŒโŸฉ ยท ๐‘)๐‘˜))
55 oveq2 7385 . . . . . . . 8 (๐‘ข = ๐‘ โ†’ (๐‘‹๐ป๐‘ข) = (๐‘‹๐ป๐‘))
5654, 55eleq12d 2826 . . . . . . 7 (๐‘ข = ๐‘ โ†’ ((๐‘™(โŸจ๐‘‹, ๐‘ŒโŸฉ ยท ๐‘ข)๐‘˜) โˆˆ (๐‘‹๐ป๐‘ข) โ†” (๐‘™(โŸจ๐‘‹, ๐‘ŒโŸฉ ยท ๐‘)๐‘˜) โˆˆ (๐‘‹๐ป๐‘)))
5752, 56raleqbidv 3330 . . . . . 6 (๐‘ข = ๐‘ โ†’ (โˆ€๐‘™ โˆˆ (๐‘Œ๐ป๐‘ข)(๐‘™(โŸจ๐‘‹, ๐‘ŒโŸฉ ยท ๐‘ข)๐‘˜) โˆˆ (๐‘‹๐ป๐‘ข) โ†” โˆ€๐‘™ โˆˆ (๐‘Œ๐ป๐‘)(๐‘™(โŸจ๐‘‹, ๐‘ŒโŸฉ ยท ๐‘)๐‘˜) โˆˆ (๐‘‹๐ป๐‘)))
5857ralbidv 3176 . . . . 5 (๐‘ข = ๐‘ โ†’ (โˆ€๐‘˜ โˆˆ (๐‘‹๐ป๐‘Œ)โˆ€๐‘™ โˆˆ (๐‘Œ๐ป๐‘ข)(๐‘™(โŸจ๐‘‹, ๐‘ŒโŸฉ ยท ๐‘ข)๐‘˜) โˆˆ (๐‘‹๐ป๐‘ข) โ†” โˆ€๐‘˜ โˆˆ (๐‘‹๐ป๐‘Œ)โˆ€๐‘™ โˆˆ (๐‘Œ๐ป๐‘)(๐‘™(โŸจ๐‘‹, ๐‘ŒโŸฉ ยท ๐‘)๐‘˜) โˆˆ (๐‘‹๐ป๐‘)))
5943, 51, 58rspc3v 3608 . . . 4 ((๐‘‹ โˆˆ ๐ต โˆง ๐‘Œ โˆˆ ๐ต โˆง ๐‘ โˆˆ ๐ต) โ†’ (โˆ€๐‘ค โˆˆ ๐ต โˆ€๐‘ฃ โˆˆ ๐ต โˆ€๐‘ข โˆˆ ๐ต โˆ€๐‘˜ โˆˆ (๐‘ค๐ป๐‘ฃ)โˆ€๐‘™ โˆˆ (๐‘ฃ๐ป๐‘ข)(๐‘™(โŸจ๐‘ค, ๐‘ฃโŸฉ ยท ๐‘ข)๐‘˜) โˆˆ (๐‘ค๐ป๐‘ข) โ†’ โˆ€๐‘˜ โˆˆ (๐‘‹๐ป๐‘Œ)โˆ€๐‘™ โˆˆ (๐‘Œ๐ป๐‘)(๐‘™(โŸจ๐‘‹, ๐‘ŒโŸฉ ยท ๐‘)๐‘˜) โˆˆ (๐‘‹๐ป๐‘)))
6033, 34, 35, 59syl3anc 1371 . . 3 (๐œ‘ โ†’ (โˆ€๐‘ค โˆˆ ๐ต โˆ€๐‘ฃ โˆˆ ๐ต โˆ€๐‘ข โˆˆ ๐ต โˆ€๐‘˜ โˆˆ (๐‘ค๐ป๐‘ฃ)โˆ€๐‘™ โˆˆ (๐‘ฃ๐ป๐‘ข)(๐‘™(โŸจ๐‘ค, ๐‘ฃโŸฉ ยท ๐‘ข)๐‘˜) โˆˆ (๐‘ค๐ป๐‘ข) โ†’ โˆ€๐‘˜ โˆˆ (๐‘‹๐ป๐‘Œ)โˆ€๐‘™ โˆˆ (๐‘Œ๐ป๐‘)(๐‘™(โŸจ๐‘‹, ๐‘ŒโŸฉ ยท ๐‘)๐‘˜) โˆˆ (๐‘‹๐ป๐‘)))
6132, 60mpd 15 . 2 (๐œ‘ โ†’ โˆ€๐‘˜ โˆˆ (๐‘‹๐ป๐‘Œ)โˆ€๐‘™ โˆˆ (๐‘Œ๐ป๐‘)(๐‘™(โŸจ๐‘‹, ๐‘ŒโŸฉ ยท ๐‘)๐‘˜) โˆˆ (๐‘‹๐ป๐‘))
62 isthincd2lem2.4 . . 3 (๐œ‘ โ†’ ๐น โˆˆ (๐‘‹๐ป๐‘Œ))
63 isthincd2lem2.5 . . 3 (๐œ‘ โ†’ ๐บ โˆˆ (๐‘Œ๐ป๐‘))
64 oveq2 7385 . . . . 5 (๐‘˜ = ๐น โ†’ (๐‘™(โŸจ๐‘‹, ๐‘ŒโŸฉ ยท ๐‘)๐‘˜) = (๐‘™(โŸจ๐‘‹, ๐‘ŒโŸฉ ยท ๐‘)๐น))
6564eleq1d 2817 . . . 4 (๐‘˜ = ๐น โ†’ ((๐‘™(โŸจ๐‘‹, ๐‘ŒโŸฉ ยท ๐‘)๐‘˜) โˆˆ (๐‘‹๐ป๐‘) โ†” (๐‘™(โŸจ๐‘‹, ๐‘ŒโŸฉ ยท ๐‘)๐น) โˆˆ (๐‘‹๐ป๐‘)))
66 oveq1 7384 . . . . 5 (๐‘™ = ๐บ โ†’ (๐‘™(โŸจ๐‘‹, ๐‘ŒโŸฉ ยท ๐‘)๐น) = (๐บ(โŸจ๐‘‹, ๐‘ŒโŸฉ ยท ๐‘)๐น))
6766eleq1d 2817 . . . 4 (๐‘™ = ๐บ โ†’ ((๐‘™(โŸจ๐‘‹, ๐‘ŒโŸฉ ยท ๐‘)๐น) โˆˆ (๐‘‹๐ป๐‘) โ†” (๐บ(โŸจ๐‘‹, ๐‘ŒโŸฉ ยท ๐‘)๐น) โˆˆ (๐‘‹๐ป๐‘)))
6865, 67rspc2v 3604 . . 3 ((๐น โˆˆ (๐‘‹๐ป๐‘Œ) โˆง ๐บ โˆˆ (๐‘Œ๐ป๐‘)) โ†’ (โˆ€๐‘˜ โˆˆ (๐‘‹๐ป๐‘Œ)โˆ€๐‘™ โˆˆ (๐‘Œ๐ป๐‘)(๐‘™(โŸจ๐‘‹, ๐‘ŒโŸฉ ยท ๐‘)๐‘˜) โˆˆ (๐‘‹๐ป๐‘) โ†’ (๐บ(โŸจ๐‘‹, ๐‘ŒโŸฉ ยท ๐‘)๐น) โˆˆ (๐‘‹๐ป๐‘)))
6962, 63, 68syl2anc 584 . 2 (๐œ‘ โ†’ (โˆ€๐‘˜ โˆˆ (๐‘‹๐ป๐‘Œ)โˆ€๐‘™ โˆˆ (๐‘Œ๐ป๐‘)(๐‘™(โŸจ๐‘‹, ๐‘ŒโŸฉ ยท ๐‘)๐‘˜) โˆˆ (๐‘‹๐ป๐‘) โ†’ (๐บ(โŸจ๐‘‹, ๐‘ŒโŸฉ ยท ๐‘)๐น) โˆˆ (๐‘‹๐ป๐‘)))
7061, 69mpd 15 1 (๐œ‘ โ†’ (๐บ(โŸจ๐‘‹, ๐‘ŒโŸฉ ยท ๐‘)๐น) โˆˆ (๐‘‹๐ป๐‘))
Colors of variables: wff setvar class
Syntax hints:   โ†’ wi 4   = wceq 1541   โˆˆ wcel 2106  โˆ€wral 3060  โŸจcop 4612  (class class class)co 7377
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-ral 3061  df-rab 3419  df-v 3461  df-dif 3931  df-un 3933  df-in 3935  df-ss 3945  df-nul 4303  df-if 4507  df-sn 4607  df-pr 4609  df-op 4613  df-uni 4886  df-br 5126  df-iota 6468  df-fv 6524  df-ov 7380
This theorem is referenced by:  isthincd2  47211
  Copyright terms: Public domain W3C validator